%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM936_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 : n013.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:39 PM UTC 2026 % Result : Timeout 300.60s 43.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM936_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.38 % Computer : n013.cluster.edu % 0.10/0.38 % Model : x86_64 x86_64 % 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.38 % Memory : 8046.5625MB % 0.10/0.38 % OS : Linux 6.8.0-71-generic % 0.10/0.38 % CPULimit : 300 % 0.10/0.38 % WCLimit : 300 % 0.10/0.38 % DateTime : Sun Sep 27 21:46:51 UTC 2026 % 0.10/0.38 % CPUTime : % 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.10/0.42 Running first-order theorem proving % 0.10/0.42 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 % 5.16/1.81 % (581098)Detected formulas, will run a generic FOF schedule. % 5.16/1.81 % (581103)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=3850158547:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 5.16/1.81 % (581108)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2114812205:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 5.16/1.81 % (581106)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3895171224:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 5.16/1.81 % (581107)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2696435392:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 5.16/1.81 % (581105)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=2027765900:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 5.16/1.81 % (581104)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=2509651061:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 5.16/1.81 % (581109)dis-21_1_sil=8000:lcm=predicate:random_seed=1788817395: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) % 5.16/1.81 % (581106)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.16/1.81 % (581105)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 5.16/1.81 % (581106)Refutation not found, incomplete strategy % 5.16/1.81 % (581106)------------------------------ % 5.16/1.81 % (581106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.16/1.81 % (581106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.16/1.81 % (581106)CaDiCaL version: 2.1.3 % 5.16/1.81 % (581106)Termination reason: Refutation not found, incomplete strategy % 5.16/1.81 % (581106)Time elapsed: 0.005 s % 5.16/1.81 % (581106)Peak memory usage: 88 MB % 5.16/1.81 % (581106)Instructions burned: 6 (million) % 5.16/1.81 % (581109)Refutation not found, incomplete strategy % 5.16/1.81 % (581109)------------------------------ % 5.16/1.81 % (581109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.16/1.81 % (581109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.16/1.81 % (581109)CaDiCaL version: 2.1.3 % 5.16/1.81 % (581109)Termination reason: Refutation not found, incomplete strategy % 5.16/1.81 % (581109)Time elapsed: 0.009 s % 5.16/1.81 % (581109)Peak memory usage: 88 MB % 5.16/1.81 % (581109)Instructions burned: 16 (million) % 5.16/1.81 % (581107)Instruction limit reached! % 5.16/1.81 % (581107)------------------------------ % 5.16/1.81 % (581107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.16/1.81 % (581107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.16/1.81 % (581107)CaDiCaL version: 2.1.3 % 5.16/1.81 % (581107)Termination reason: Instruction limit % 5.16/1.81 % (581107)Termination phase: Saturation % 5.16/1.81 % (581107)Time elapsed: 0.065 s % 5.16/1.81 % (581107)Peak memory usage: 88 MB % 5.16/1.81 % (581107)Instructions burned: 119 (million) % 5.16/1.81 % (581108)Instruction limit reached! % 5.16/1.81 % (581108)------------------------------ % 5.16/1.81 % (581108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.16/1.81 % (581108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.16/1.81 % (581108)CaDiCaL version: 2.1.3 % 5.16/1.81 % (581108)Termination reason: Instruction limit % 5.16/1.81 % (581108)Termination phase: Saturation % 5.16/1.81 % (581108)Time elapsed: 0.078 s % 5.16/1.81 % (581108)Peak memory usage: 90 MB % 5.16/1.81 % (581108)Instructions burned: 139 (million) % 5.16/1.81 % (581103)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.16/1.81 % (581103)------------------------------ % 5.16/1.81 % (581103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.16/1.81 % (581103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.16/1.81 % (581103)CaDiCaL version: 2.1.3 % 5.16/1.81 % (581103)Termination reason: Unknown % 5.16/1.81 % (581103)Termination phase: Saturation % 5.16/1.81 % (581103)Time elapsed: 0.199 s % 5.16/1.81 % (581103)Peak memory usage: 113 MB % 8.62/2.05 % (581103)Instructions burned: 542 (million) % 8.62/2.05 % (581117)lrs+10_1_sil=8000:sp=occurrence:random_seed=3228993854:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 8.62/2.05 % (581118)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2480275701:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 8.62/2.05 % (581106)------------------------------ % 8.62/2.05 % (581106)------------------------------ % 8.62/2.05 % (581109)------------------------------ % 8.62/2.05 % (581109)------------------------------ % 8.62/2.05 % (581119)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1230535670:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 8.62/2.05 % (581118)Instruction limit reached! % 8.62/2.05 % (581118)------------------------------ % 8.62/2.05 % (581118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.62/2.05 % (581118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/2.05 % (581118)CaDiCaL version: 2.1.3 % 8.62/2.05 % (581118)Termination reason: Instruction limit % 8.62/2.05 % (581118)Termination phase: Saturation % 8.62/2.05 % (581118)Time elapsed: 0.083 s % 8.62/2.05 % (581118)Peak memory usage: 89 MB % 8.62/2.05 % (581118)Instructions burned: 158 (million) % 8.62/2.05 % (581119)Instruction limit reached! % 8.62/2.05 % (581119)------------------------------ % 8.62/2.05 % (581119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.62/2.05 % (581119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/2.05 % (581119)CaDiCaL version: 2.1.3 % 8.62/2.05 % (581119)Termination reason: Instruction limit % 8.62/2.05 % (581119)Termination phase: Saturation % 8.62/2.05 % (581119)Time elapsed: 0.096 s % 8.62/2.05 % (581119)Peak memory usage: 91 MB % 8.62/2.05 % (581119)Instructions burned: 327 (million) % 8.62/2.05 % (581105)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.62/2.05 % (581104)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.62/2.05 % (581104)------------------------------ % 8.62/2.05 % (581104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.62/2.05 % (581105)------------------------------ % 8.62/2.05 % (581105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.62/2.05 % (581105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/2.05 % (581104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/2.05 % (581104)CaDiCaL version: 2.1.3 % 8.62/2.05 % (581105)CaDiCaL version: 2.1.3 % 8.62/2.05 % (581105)Termination reason: Unknown % 8.62/2.05 % (581105)Termination phase: Saturation % 8.62/2.05 % (581104)Termination reason: Unknown % 8.62/2.05 % (581104)Termination phase: Saturation % 8.62/2.05 % (581105)Time elapsed: 0.366 s % 8.62/2.05 % (581104)Time elapsed: 0.366 s % 8.62/2.05 % (581104)Peak memory usage: 112 MB % 8.62/2.05 % (581105)Peak memory usage: 112 MB % 8.62/2.05 % (581104)Instructions burned: 547 (million) % 8.62/2.05 % (581105)Instructions burned: 542 (million) % 8.62/2.05 % (581117)Instruction limit reached! % 8.62/2.05 % (581117)------------------------------ % 8.62/2.05 % (581117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.62/2.05 % (581117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/2.05 % (581117)CaDiCaL version: 2.1.3 % 8.62/2.05 % (581117)Termination reason: Instruction limit % 8.62/2.05 % (581117)Termination phase: Saturation % 8.62/2.05 % (581117)Time elapsed: 0.146 s % 8.62/2.05 % (581117)Peak memory usage: 90 MB % 8.62/2.05 % (581117)Instructions burned: 286 (million) % 8.62/2.05 % (581124)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=558562396:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 8.62/2.05 % (581123)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=619017617:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 8.62/2.05 % (581124)Refutation not found, incomplete strategy % 8.62/2.05 % (581124)------------------------------ % 8.62/2.05 % (581124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.62/2.05 % (581124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.62/2.05 % (581124)CaDiCaL version: 2.1.3 % 8.62/2.05 % (581124)Termination reason: Refutation not found, incomplete strategy % 8.62/2.05 % (581124)Time elapsed: 0.007 s % 8.62/2.05 % (581124)Peak memory usage: 88 MB % 8.62/2.05 % (581124)Instructions burned: 11 (million) % 9.76/2.33 % (581126)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2671535156:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 9.76/2.33 % (581125)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2238452049:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 9.76/2.33 % (581126)Instruction limit reached! % 9.76/2.33 % (581126)------------------------------ % 9.76/2.33 % (581126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.33 % (581126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.33 % (581126)CaDiCaL version: 2.1.3 % 9.76/2.33 % (581126)Termination reason: Instruction limit % 9.76/2.33 % (581126)Termination phase: Saturation % 9.76/2.33 % (581126)Time elapsed: 0.035 s % 9.76/2.33 % (581126)Peak memory usage: 90 MB % 9.76/2.33 % (581126)Instructions burned: 114 (million) % 9.76/2.33 % (581129)lrs+10_1_sil=8000:sp=occurrence:random_seed=2499605236:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi) % 9.76/2.33 % (581127)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3233264121:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 9.76/2.33 % (581128)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3197674918:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 9.76/2.33 % (581127)Refutation not found, incomplete strategy % 9.76/2.33 % (581127)------------------------------ % 9.76/2.33 % (581127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.33 % (581127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.33 % (581127)CaDiCaL version: 2.1.3 % 9.76/2.33 % (581127)Termination reason: Refutation not found, incomplete strategy % 9.76/2.33 % (581127)Time elapsed: 0.006 s % 9.76/2.33 % (581127)Peak memory usage: 88 MB % 9.76/2.33 % (581127)Instructions burned: 10 (million) % 9.76/2.33 % (581123)Instruction limit reached! % 9.76/2.33 % (581123)------------------------------ % 9.76/2.33 % (581123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.33 % (581123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.33 % (581123)CaDiCaL version: 2.1.3 % 9.76/2.33 % (581123)Termination reason: Instruction limit % 9.76/2.33 % (581123)Termination phase: Saturation % 9.76/2.33 % (581123)Time elapsed: 0.144 s % 9.76/2.33 % (581123)Peak memory usage: 91 MB % 9.76/2.33 % (581123)Instructions burned: 249 (million) % 9.76/2.33 % (581128)Instruction limit reached! % 9.76/2.33 % (581128)------------------------------ % 9.76/2.33 % (581128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.33 % (581128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.33 % (581128)CaDiCaL version: 2.1.3 % 9.76/2.33 % (581128)Termination reason: Instruction limit % 9.76/2.33 % (581128)Termination phase: Saturation % 9.76/2.33 % (581128)Time elapsed: 0.057 s % 9.76/2.33 % (581128)Peak memory usage: 89 MB % 9.76/2.33 % (581128)Instructions burned: 115 (million) % 9.76/2.33 % (581134)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2006443314:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 9.76/2.33 % (581134)Refutation not found, incomplete strategy % 9.76/2.33 % (581134)------------------------------ % 9.76/2.33 % (581134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.33 % (581134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.33 % (581134)CaDiCaL version: 2.1.3 % 9.76/2.33 % (581134)Termination reason: Refutation not found, incomplete strategy % 9.76/2.33 % (581134)Time elapsed: 0.003 s % 9.76/2.33 % (581134)Peak memory usage: 88 MB % 9.76/2.33 % (581134)Instructions burned: 9 (million) % 9.76/2.33 % (581124)------------------------------ % 9.76/2.33 % (581124)------------------------------ % 9.76/2.33 % (581138)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1753264167:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 9.76/2.33 % (581139)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3896374100:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2992 on theBenchmark for (2992ds/134Mi) % 9.76/2.33 % (581127)------------------------------ % 9.76/2.33 % (581127)------------------------------ % 9.76/2.33 % (581134)------------------------------ % 9.76/2.33 % (581134)------------------------------ % 11.49/2.65 % (581139)Instruction limit reached! % 11.49/2.65 % (581139)------------------------------ % 11.49/2.65 % (581139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.65 % (581139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.65 % (581139)CaDiCaL version: 2.1.3 % 11.49/2.65 % (581139)Termination reason: Instruction limit % 11.49/2.65 % (581139)Termination phase: Saturation % 11.49/2.65 % (581139)Time elapsed: 0.073 s % 11.49/2.65 % (581139)Peak memory usage: 90 MB % 11.49/2.65 % (581139)Instructions burned: 136 (million) % 11.49/2.65 % (581141)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2055493360:st=8:i=592:sd=3:ep=RST:ss=axioms_2991 on theBenchmark for (2991ds/592Mi) % 11.49/2.65 % (581125)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.49/2.65 % (581125)------------------------------ % 11.49/2.65 % (581125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.65 % (581125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.65 % (581125)CaDiCaL version: 2.1.3 % 11.49/2.65 % (581125)Termination reason: Unknown % 11.49/2.65 % (581125)Termination phase: Saturation % 11.49/2.65 % (581125)Time elapsed: 0.372 s % 11.49/2.65 % (581125)Peak memory usage: 114 MB % 11.49/2.65 % (581125)Instructions burned: 542 (million) % 11.49/2.65 % (581141)Refutation not found, incomplete strategy % 11.49/2.65 % (581141)------------------------------ % 11.49/2.65 % (581141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.65 % (581141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.65 % (581141)CaDiCaL version: 2.1.3 % 11.49/2.65 % (581141)Termination reason: Refutation not found, incomplete strategy % 11.49/2.65 % (581141)Time elapsed: 0.007 s % 11.49/2.65 % (581141)Peak memory usage: 88 MB % 11.49/2.65 % (581141)Instructions burned: 12 (million) % 11.49/2.65 % (581145)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=1624501822:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/125Mi) % 11.49/2.65 % (581145)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.49/2.65 % (581144)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2793070503:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 11.49/2.65 % (581145)Instruction limit reached! % 11.49/2.65 % (581145)------------------------------ % 11.49/2.65 % (581145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.65 % (581145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.65 % (581145)CaDiCaL version: 2.1.3 % 11.49/2.65 % (581145)Termination reason: Instruction limit % 11.49/2.65 % (581145)Termination phase: Saturation % 11.49/2.65 % (581145)Time elapsed: 0.040 s % 11.49/2.65 % (581145)Peak memory usage: 90 MB % 11.49/2.65 % (581145)Instructions burned: 127 (million) % 11.49/2.65 % (581146)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1121100836:i=134:gtgl=5:slsql=off:gtg=exists_sym_2990 on theBenchmark for (2990ds/134Mi) % 11.49/2.65 % (581148)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1719742573:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/141Mi) % 11.49/2.65 % (581129)Instruction limit reached! % 11.49/2.65 % (581129)------------------------------ % 11.49/2.65 % (581129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.65 % (581129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.65 % (581129)CaDiCaL version: 2.1.3 % 11.49/2.65 % (581129)Termination reason: Instruction limit % 11.49/2.65 % (581129)Termination phase: Saturation % 11.49/2.65 % (581129)Time elapsed: 0.491 s % 11.49/2.65 % (581129)Peak memory usage: 95 MB % 11.49/2.65 % (581129)Instructions burned: 907 (million) % 11.49/2.65 % (581148)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 11.49/2.65 % (581148)Refutation not found, incomplete strategy % 11.49/2.65 % (581148)------------------------------ % 11.49/2.65 % (581148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.49/2.65 % (581148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.49/2.65 % (581148)CaDiCaL version: 2.1.3 % 11.49/2.65 % (581148)Termination reason: Refutation not found, incomplete strategy % 13.17/2.96 % (581148)Time elapsed: 0.003 s % 13.17/2.96 % (581148)Peak memory usage: 88 MB % 13.17/2.96 % (581148)Instructions burned: 5 (million) % 13.17/2.96 % (581146)Instruction limit reached! % 13.17/2.96 % (581146)------------------------------ % 13.17/2.96 % (581146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.17/2.96 % (581146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.17/2.96 % (581146)CaDiCaL version: 2.1.3 % 13.17/2.96 % (581146)Termination reason: Instruction limit % 13.17/2.96 % (581146)Termination phase: Saturation % 13.17/2.96 % (581146)Time elapsed: 0.067 s % 13.17/2.96 % (581146)Peak memory usage: 89 MB % 13.17/2.96 % (581146)Instructions burned: 136 (million) % 13.17/2.96 % (581151)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3994674854:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/431Mi) % 13.17/2.96 % (581151)Refutation not found, incomplete strategy % 13.17/2.96 % (581151)------------------------------ % 13.17/2.96 % (581151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.17/2.96 % (581151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.17/2.96 % (581151)CaDiCaL version: 2.1.3 % 13.17/2.96 % (581151)Termination reason: Refutation not found, incomplete strategy % 13.17/2.96 % (581151)Time elapsed: 0.004 s % 13.17/2.96 % (581151)Peak memory usage: 88 MB % 13.17/2.96 % (581151)Instructions burned: 13 (million) % 13.17/2.96 % (581138)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.17/2.96 % (581138)------------------------------ % 13.17/2.96 % (581138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.17/2.96 % (581138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.17/2.96 % (581138)CaDiCaL version: 2.1.3 % 13.17/2.96 % (581138)Termination reason: Unknown % 13.17/2.96 % (581138)Termination phase: Saturation % 13.17/2.96 % (581138)Time elapsed: 0.368 s % 13.17/2.96 % (581138)Peak memory usage: 113 MB % 13.17/2.96 % (581138)Instructions burned: 544 (million) % 13.17/2.96 % (581141)------------------------------ % 13.17/2.96 % (581141)------------------------------ % 13.17/2.96 % (581154)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=3874273535:i=6060:aac=none:ins=25_2988 on theBenchmark for (2988ds/6060Mi) % 13.17/2.96 % (581155)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=3744377150:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2987 on theBenchmark for (2987ds/150Mi) % 13.17/2.96 % (581155)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 13.17/2.96 % (581151)------------------------------ % 13.17/2.96 % (581151)------------------------------ % 13.17/2.96 % (581157)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=770410999:i=14155:bd=all_2987 on theBenchmark for (2987ds/14155Mi) % 13.17/2.96 % (581148)------------------------------ % 13.17/2.96 % (581148)------------------------------ % 13.17/2.96 % (581158)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1985331638:i=667:av=off:fsr=off_2987 on theBenchmark for (2987ds/667Mi) % 13.17/2.96 % (581158)Refutation not found, incomplete strategy % 13.17/2.96 % (581158)------------------------------ % 13.17/2.96 % (581158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.17/2.96 % (581158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.17/2.96 % (581158)CaDiCaL version: 2.1.3 % 13.17/2.96 % (581158)Termination reason: Refutation not found, incomplete strategy % 13.17/2.96 % (581158)Time elapsed: 0.007 s % 13.17/2.96 % (581158)Peak memory usage: 88 MB % 13.17/2.96 % (581158)Instructions burned: 11 (million) % 13.17/2.96 % (581155)Instruction limit reached! % 13.17/2.96 % (581155)------------------------------ % 13.17/2.96 % (581155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.17/2.96 % (581155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.17/2.96 % (581155)CaDiCaL version: 2.1.3 % 13.17/2.96 % (581155)Termination reason: Instruction limit % 13.17/2.96 % (581155)Termination phase: Saturation % 13.17/2.96 % (581155)Time elapsed: 0.096 s % 13.17/2.96 % (581155)Peak memory usage: 90 MB % 13.17/2.96 % (581155)Instructions burned: 150 (million) % 13.17/2.96 % (581144)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.65/3.43 % (581144)------------------------------ % 17.65/3.43 % (581144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.43 % (581144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.43 % (581144)CaDiCaL version: 2.1.3 % 17.65/3.43 % (581144)Termination reason: Unknown % 17.65/3.43 % (581144)Termination phase: Saturation % 17.65/3.43 % (581144)Time elapsed: 0.367 s % 17.65/3.43 % (581144)Peak memory usage: 113 MB % 17.65/3.43 % (581144)Instructions burned: 542 (million) % 17.65/3.43 % (581161)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=3701310620:s2a=on:i=185:s2at=1.8:fdi=4_2986 on theBenchmark for (2986ds/185Mi) % 17.65/3.43 % (581161)Instruction limit reached! % 17.65/3.43 % (581161)------------------------------ % 17.65/3.43 % (581161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.43 % (581161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.43 % (581161)CaDiCaL version: 2.1.3 % 17.65/3.43 % (581161)Termination reason: Instruction limit % 17.65/3.43 % (581161)Termination phase: Saturation % 17.65/3.43 % (581161)Time elapsed: 0.058 s % 17.65/3.43 % (581161)Peak memory usage: 91 MB % 17.65/3.43 % (581161)Instructions burned: 187 (million) % 17.65/3.43 % (581164)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3400923883:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2985 on theBenchmark for (2985ds/193Mi) % 17.65/3.43 % (581165)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4165053275:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2985 on theBenchmark for (2985ds/4850Mi) % 17.65/3.43 % (581165)Refutation not found, incomplete strategy % 17.65/3.43 % (581165)------------------------------ % 17.65/3.43 % (581165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.43 % (581165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.43 % (581165)CaDiCaL version: 2.1.3 % 17.65/3.43 % (581165)Termination reason: Refutation not found, incomplete strategy % 17.65/3.43 % (581165)Time elapsed: 0.005 s % 17.65/3.43 % (581165)Peak memory usage: 87 MB % 17.65/3.43 % (581165)Instructions burned: 8 (million) % 17.65/3.43 % (581166)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2771546059:i=12111:sd=1:ss=included_2985 on theBenchmark for (2985ds/12111Mi) % 17.65/3.43 % (581168)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2640556068:i=319:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/319Mi) % 17.65/3.43 % (581164)Instruction limit reached! % 17.65/3.43 % (581164)------------------------------ % 17.65/3.43 % (581164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.43 % (581164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.43 % (581164)CaDiCaL version: 2.1.3 % 17.65/3.43 % (581164)Termination reason: Instruction limit % 17.65/3.43 % (581164)Termination phase: Saturation % 17.65/3.43 % (581164)Time elapsed: 0.105 s % 17.65/3.43 % (581164)Peak memory usage: 90 MB % 17.65/3.43 % (581164)Instructions burned: 195 (million) % 17.65/3.43 % (581158)------------------------------ % 17.65/3.43 % (581158)------------------------------ % 17.65/3.43 % (581154)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 17.65/3.43 % (581154)------------------------------ % 17.65/3.43 % (581154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.43 % (581154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.43 % (581154)CaDiCaL version: 2.1.3 % 17.65/3.43 % (581154)Termination reason: Unknown % 17.65/3.43 % (581154)Termination phase: Saturation % 17.65/3.43 % (581154)Time elapsed: 0.368 s % 17.65/3.43 % (581154)Peak memory usage: 114 MB % 17.65/3.43 % (581154)Instructions burned: 542 (million) % 17.65/3.43 % (581168)Instruction limit reached! % 17.65/3.43 % (581168)------------------------------ % 17.65/3.43 % (581168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.65/3.43 % (581168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.65/3.43 % (581168)CaDiCaL version: 2.1.3 % 17.65/3.43 % (581168)Termination reason: Instruction limit % 17.65/3.43 % (581168)Termination phase: Saturation % 17.65/3.43 % (581168)Time elapsed: 0.105 s % 17.65/3.43 % (581168)Peak memory usage: 93 MB % 19.82/3.94 % (581168)Instructions burned: 323 (million) % 19.82/3.94 % (581157)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.82/3.94 % (581157)------------------------------ % 19.82/3.94 % (581157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.82/3.94 % (581157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.82/3.94 % (581157)CaDiCaL version: 2.1.3 % 19.82/3.94 % (581157)Termination reason: Unknown % 19.82/3.94 % (581157)Termination phase: Saturation % 19.82/3.94 % (581157)Time elapsed: 0.367 s % 19.82/3.94 % (581157)Peak memory usage: 114 MB % 19.82/3.94 % (581157)Instructions burned: 542 (million) % 19.82/3.94 % (581173)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=494159974:i=2064:ep=RST_2983 on theBenchmark for (2983ds/2064Mi) % 19.82/3.94 % (581173)Refutation not found, incomplete strategy % 19.82/3.94 % (581173)------------------------------ % 19.82/3.94 % (581173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.82/3.94 % (581173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.82/3.94 % (581173)CaDiCaL version: 2.1.3 % 19.82/3.94 % (581173)Termination reason: Refutation not found, incomplete strategy % 19.82/3.94 % (581173)Time elapsed: 0.006 s % 19.82/3.94 % (581173)Peak memory usage: 88 MB % 19.82/3.94 % (581173)Instructions burned: 12 (million) % 19.82/3.94 % (581165)------------------------------ % 19.82/3.94 % (581165)------------------------------ % 19.82/3.94 % (581174)dis-1011_128_sil=32000:random_seed=3409182674:i=3706:ep=RST:av=off_2982 on theBenchmark for (2982ds/3706Mi) % 19.82/3.94 % (581175)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=741397144:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2982 on theBenchmark for (2982ds/757Mi) % 19.82/3.94 % (581175)Refutation not found, incomplete strategy % 19.82/3.94 % (581175)------------------------------ % 19.82/3.94 % (581175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.82/3.94 % (581175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.82/3.94 % (581175)CaDiCaL version: 2.1.3 % 19.82/3.94 % (581175)Termination reason: Refutation not found, incomplete strategy % 19.82/3.94 % (581175)Time elapsed: 0.007 s % 19.82/3.94 % (581175)Peak memory usage: 89 MB % 19.82/3.94 % (581175)Instructions burned: 11 (million) % 19.82/3.94 % (581176)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2468637429:i=13913:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/13913Mi) % 19.82/3.94 % (581177)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3486499623:i=9925:aac=none_2982 on theBenchmark for (2982ds/9925Mi) % 19.82/3.94 % (581166)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.82/3.94 % (581166)------------------------------ % 19.82/3.94 % (581166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.82/3.94 % (581166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.82/3.94 % (581166)CaDiCaL version: 2.1.3 % 19.82/3.94 % (581166)Termination reason: Unknown % 19.82/3.94 % (581166)Termination phase: Saturation % 19.82/3.94 % (581166)Time elapsed: 0.367 s % 19.82/3.94 % (581166)Peak memory usage: 114 MB % 19.82/3.94 % (581166)Instructions burned: 544 (million) % 19.82/3.94 % (581180)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1582378728:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2981 on theBenchmark for (2981ds/2479Mi) % 19.82/3.94 % (581180)Refutation not found, incomplete strategy % 19.82/3.94 % (581180)------------------------------ % 19.82/3.94 % (581180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.82/3.94 % (581180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.82/3.94 % (581180)CaDiCaL version: 2.1.3 % 19.82/3.94 % (581180)Termination reason: Refutation not found, incomplete strategy % 19.82/3.94 % (581180)Time elapsed: 0.007 s % 19.82/3.94 % (581180)Peak memory usage: 88 MB % 19.82/3.94 % (581180)Instructions burned: 10 (million) % 19.82/3.94 % (581173)------------------------------ % 19.82/3.94 % (581173)------------------------------ % 19.82/3.94 % (581176)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.82/3.94 % (581176)------------------------------ % 19.82/3.94 % (581176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.82/3.94 % (581176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.43/4.74 % (581176)CaDiCaL version: 2.1.3 % 26.43/4.74 % (581176)Termination reason: Unknown % 26.43/4.74 % (581176)Termination phase: Saturation % 26.43/4.74 % (581176)Time elapsed: 0.199 s % 26.43/4.74 % (581176)Peak memory usage: 113 MB % 26.43/4.74 % (581176)Instructions burned: 542 (million) % 26.43/4.74 % (581175)------------------------------ % 26.43/4.74 % (581175)------------------------------ % 26.43/4.74 % (581184)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3947297325:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/440Mi) % 26.43/4.74 % (581184)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 26.43/4.74 % (581187)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=1328374722:cts=off:i=3034:av=off:er=known:fsd=on_2978 on theBenchmark for (2978ds/3034Mi) % 26.43/4.74 % (581186)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2095607744:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2979 on theBenchmark for (2979ds/11145Mi) % 26.43/4.74 % (581180)------------------------------ % 26.43/4.74 % (581180)------------------------------ % 26.43/4.74 % (581188)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3245273259:st=2:s2a=on:i=524:s2at=2:ss=axioms_2978 on theBenchmark for (2978ds/524Mi) % 26.43/4.74 % (581177)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.43/4.74 % (581177)------------------------------ % 26.43/4.74 % (581177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.43/4.74 % (581177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.43/4.74 % (581177)CaDiCaL version: 2.1.3 % 26.43/4.74 % (581177)Termination reason: Unknown % 26.43/4.74 % (581177)Termination phase: Saturation % 26.43/4.74 % (581177)Time elapsed: 0.368 s % 26.43/4.74 % (581177)Peak memory usage: 113 MB % 26.43/4.74 % (581177)Instructions burned: 542 (million) % 26.43/4.74 % (581184)Instruction limit reached! % 26.43/4.74 % (581184)------------------------------ % 26.43/4.74 % (581184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.43/4.74 % (581184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.43/4.74 % (581184)CaDiCaL version: 2.1.3 % 26.43/4.74 % (581184)Termination reason: Instruction limit % 26.43/4.74 % (581184)Termination phase: Saturation % 26.43/4.74 % (581184)Time elapsed: 0.218 s % 26.43/4.74 % (581184)Peak memory usage: 90 MB % 26.43/4.74 % (581184)Instructions burned: 440 (million) % 26.43/4.74 % (581187)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.43/4.74 % (581187)------------------------------ % 26.43/4.74 % (581187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.43/4.74 % (581187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.43/4.74 % (581187)CaDiCaL version: 2.1.3 % 26.43/4.74 % (581187)Termination reason: Unknown % 26.43/4.74 % (581187)Termination phase: Saturation % 26.43/4.74 % (581187)Time elapsed: 0.198 s % 26.43/4.74 % (581187)Peak memory usage: 113 MB % 26.43/4.74 % (581187)Instructions burned: 543 (million) % 26.43/4.74 % (581193)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2250894253:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2977 on theBenchmark for (2977ds/1016Mi) % 26.43/4.74 % (581194)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=814649849:i=14123:bd=preordered:ins=4_2976 on theBenchmark for (2976ds/14123Mi) % 26.43/4.74 % (581195)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3429365747:i=5781:kws=precedence:bd=all:rawr=on_2976 on theBenchmark for (2976ds/5781Mi) % 26.43/4.74 % (581197)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=2981152637:i=2448:gtgl=5:bd=preordered:gtg=all_2975 on theBenchmark for (2975ds/2448Mi) % 26.43/4.74 % (581188)Instruction limit reached! % 26.43/4.74 % (581188)------------------------------ % 26.43/4.74 % (581188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.43/4.74 % (581188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.43/4.74 % (581188)CaDiCaL version: 2.1.3 % 26.43/4.74 % (581188)Termination reason: Instruction limit % 32.35/5.61 % (581188)Termination phase: Saturation % 32.35/5.61 % (581188)Time elapsed: 0.276 s % 32.35/5.61 % (581188)Peak memory usage: 92 MB % 32.35/5.61 % (581188)Instructions burned: 524 (million) % 32.35/5.61 % (581186)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.35/5.61 % (581186)------------------------------ % 32.35/5.61 % (581186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.35/5.61 % (581186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.61 % (581186)CaDiCaL version: 2.1.3 % 32.35/5.61 % (581186)Termination reason: Unknown % 32.35/5.61 % (581186)Termination phase: Saturation % 32.35/5.61 % (581186)Time elapsed: 0.361 s % 32.35/5.61 % (581186)Peak memory usage: 113 MB % 32.35/5.61 % (581186)Instructions burned: 541 (million) % 32.35/5.61 % (581202)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1336250862:i=3223:kws=precedence:fgj=on:av=off_2974 on theBenchmark for (2974ds/3223Mi) % 32.35/5.61 % (581197)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.35/5.61 % (581197)------------------------------ % 32.35/5.61 % (581197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.35/5.61 % (581197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.61 % (581197)CaDiCaL version: 2.1.3 % 32.35/5.61 % (581197)Termination reason: Unknown % 32.35/5.61 % (581197)Termination phase: Saturation % 32.35/5.61 % (581197)Time elapsed: 0.198 s % 32.35/5.61 % (581197)Peak memory usage: 113 MB % 32.35/5.61 % (581197)Instructions burned: 546 (million) % 32.35/5.61 % (581203)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2877090257:st=5.6:i=2033:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/2033Mi) % 32.35/5.61 % (581205)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3591010103:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2972 on theBenchmark for (2972ds/2055Mi) % 32.35/5.61 % (581194)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.35/5.61 % (581194)------------------------------ % 32.35/5.61 % (581194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.35/5.61 % (581194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.61 % (581194)CaDiCaL version: 2.1.3 % 32.35/5.61 % (581194)Termination reason: Unknown % 32.35/5.61 % (581194)Termination phase: Saturation % 32.35/5.61 % (581194)Time elapsed: 0.364 s % 32.35/5.61 % (581194)Peak memory usage: 113 MB % 32.35/5.61 % (581194)Instructions burned: 541 (million) % 32.35/5.61 % (581193)Instruction limit reached! % 32.35/5.61 % (581193)------------------------------ % 32.35/5.61 % (581193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.35/5.61 % (581193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.61 % (581193)CaDiCaL version: 2.1.3 % 32.35/5.61 % (581193)Termination reason: Instruction limit % 32.35/5.61 % (581193)Termination phase: Saturation % 32.35/5.61 % (581193)Time elapsed: 0.529 s % 32.35/5.61 % (581193)Peak memory usage: 99 MB % 32.35/5.61 % (581193)Instructions burned: 1018 (million) % 32.35/5.61 % (581208)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=2353869763:i=21611:sd=3:ss=axioms_2971 on theBenchmark for (2971ds/21611Mi) % 32.35/5.61 % (581205)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.35/5.61 % (581205)------------------------------ % 32.35/5.61 % (581205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.35/5.61 % (581205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.61 % (581205)CaDiCaL version: 2.1.3 % 32.35/5.61 % (581205)Termination reason: Unknown % 32.35/5.61 % (581205)Termination phase: Saturation % 32.35/5.61 % (581205)Time elapsed: 0.197 s % 32.35/5.61 % (581205)Peak memory usage: 113 MB % 32.35/5.61 % (581205)Instructions burned: 543 (million) % 32.35/5.61 % (581202)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 32.35/5.61 % (581202)------------------------------ % 32.35/5.61 % (581202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.35/5.61 % (581202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.35/5.61 % (581202)CaDiCaL version: 2.1.3 % 32.35/5.61 % (581202)Termination reason: Unknown % 32.35/5.61 % (581202)Termination phase: Saturation % 32.35/5.61 % (581202)Time elapsed: 0.362 s % 38.21/6.32 % (581202)Peak memory usage: 113 MB % 38.21/6.32 % (581202)Instructions burned: 543 (million) % 38.21/6.32 % (581203)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.21/6.32 % (581203)------------------------------ % 38.21/6.32 % (581203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.21/6.32 % (581203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.21/6.32 % (581203)CaDiCaL version: 2.1.3 % 38.21/6.32 % (581203)Termination reason: Unknown % 38.21/6.32 % (581203)Termination phase: Saturation % 38.21/6.32 % (581203)Time elapsed: 0.365 s % 38.21/6.32 % (581203)Peak memory usage: 113 MB % 38.21/6.32 % (581203)Instructions burned: 543 (million) % 38.21/6.32 % (581209)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1468839933:i=4835:sd=13:ss=axioms:sgt=23_2970 on theBenchmark for (2970ds/4835Mi) % 38.21/6.32 % (581211)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=3531776176:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2969 on theBenchmark for (2969ds/797Mi) % 38.21/6.32 % (581211)Refutation not found, incomplete strategy % 38.21/6.32 % (581211)------------------------------ % 38.21/6.32 % (581211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.21/6.32 % (581211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.21/6.32 % (581211)CaDiCaL version: 2.1.3 % 38.21/6.32 % (581211)Termination reason: Refutation not found, incomplete strategy % 38.21/6.32 % (581211)Time elapsed: 0.006 s % 38.21/6.32 % (581211)Peak memory usage: 88 MB % 38.21/6.32 % (581211)Instructions burned: 18 (million) % 38.21/6.32 % (581212)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=452242807:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2969 on theBenchmark for (2969ds/2326Mi) % 38.21/6.32 % (581213)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=852197682:i=6038:nm=6_2968 on theBenchmark for (2968ds/6038Mi) % 38.21/6.32 % (581211)------------------------------ % 38.21/6.32 % (581211)------------------------------ % 38.21/6.32 % (581208)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.21/6.32 % (581208)------------------------------ % 38.21/6.32 % (581208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.21/6.32 % (581208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.21/6.32 % (581208)CaDiCaL version: 2.1.3 % 38.21/6.32 % (581208)Termination reason: Unknown % 38.21/6.32 % (581208)Termination phase: Saturation % 38.21/6.32 % (581208)Time elapsed: 0.366 s % 38.21/6.32 % (581208)Peak memory usage: 113 MB % 38.21/6.32 % (581208)Instructions burned: 540 (million) % 38.21/6.32 % (581218)lrs+10_1_sil=32000:sp=occurrence:random_seed=1997261054:st=2:i=33334:sd=3:ss=included:sgt=32_2966 on theBenchmark for (2966ds/33334Mi) % 38.21/6.32 % (581219)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=854510172:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2965 on theBenchmark for (2965ds/1008Mi) % 38.21/6.32 % (581213)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.21/6.32 % (581213)------------------------------ % 38.21/6.32 % (581213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.21/6.32 % (581213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.21/6.32 % (581213)CaDiCaL version: 2.1.3 % 38.21/6.32 % (581213)Termination reason: Unknown % 38.21/6.32 % (581213)Termination phase: Saturation % 38.21/6.32 % (581213)Time elapsed: 0.440 s % 38.21/6.32 % (581213)Peak memory usage: 113 MB % 38.21/6.32 % (581213)Instructions burned: 542 (million) % 38.21/6.32 % (581174)Instruction limit reached! % 38.21/6.32 % (581174)------------------------------ % 38.21/6.32 % (581174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.21/6.32 % (581174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.21/6.32 % (581174)CaDiCaL version: 2.1.3 % 38.21/6.32 % (581174)Termination reason: Instruction limit % 38.21/6.32 % (581174)Termination phase: Saturation % 38.21/6.32 % (581174)Time elapsed: 1.998 s % 38.21/6.32 % (581174)Peak memory usage: 119 MB % 38.21/6.32 % (581174)Instructions burned: 3707 (million) % 38.21/6.32 % (581222)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=1057130068:i=8327:s2at=5:bd=preordered_2962 on theBenchmark for (2962ds/8327Mi) % 40.13/6.85 % (581223)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=3494020707:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2961 on theBenchmark for (2961ds/1083Mi) % 40.13/6.85 % (581219)Instruction limit reached! % 40.13/6.85 % (581219)------------------------------ % 40.13/6.85 % (581219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.13/6.85 % (581219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.13/6.85 % (581219)CaDiCaL version: 2.1.3 % 40.13/6.85 % (581219)Termination reason: Instruction limit % 40.13/6.85 % (581219)Termination phase: Saturation % 40.13/6.85 % (581219)Time elapsed: 0.596 s % 40.13/6.85 % (581219)Peak memory usage: 93 MB % 40.13/6.85 % (581219)Instructions burned: 1009 (million) % 40.13/6.85 % (581222)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.13/6.85 % (581222)------------------------------ % 40.13/6.85 % (581222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.13/6.85 % (581222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.13/6.85 % (581222)CaDiCaL version: 2.1.3 % 40.13/6.85 % (581222)Termination reason: Unknown % 40.13/6.85 % (581222)Termination phase: Saturation % 40.13/6.85 % (581222)Time elapsed: 0.358 s % 40.13/6.85 % (581222)Peak memory usage: 113 MB % 40.13/6.85 % (581222)Instructions burned: 541 (million) % 40.13/6.85 % (581226)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3333121896:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2958 on theBenchmark for (2958ds/1084Mi) % 40.13/6.85 % (581227)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4294782529:i=6995:s2at=5:gtg=all_2957 on theBenchmark for (2957ds/6995Mi) % 40.13/6.85 % (581223)Instruction limit reached! % 40.13/6.85 % (581223)------------------------------ % 40.13/6.85 % (581223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.13/6.85 % (581223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.13/6.85 % (581223)CaDiCaL version: 2.1.3 % 40.13/6.85 % (581223)Termination reason: Instruction limit % 40.13/6.85 % (581223)Termination phase: Saturation % 40.13/6.85 % (581223)Time elapsed: 0.486 s % 40.13/6.85 % (581223)Peak memory usage: 98 MB % 40.13/6.85 % (581223)Instructions burned: 1083 (million) % 40.13/6.85 % (581212)Instruction limit reached! % 40.13/6.85 % (581212)------------------------------ % 40.13/6.85 % (581212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.13/6.85 % (581212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.13/6.85 % (581212)CaDiCaL version: 2.1.3 % 40.13/6.85 % (581212)Termination reason: Instruction limit % 40.13/6.85 % (581212)Termination phase: Saturation % 40.13/6.85 % (581212)Time elapsed: 1.388 s % 40.13/6.85 % (581212)Peak memory usage: 107 MB % 40.13/6.85 % (581212)Instructions burned: 2327 (million) % 40.13/6.85 % (581230)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=436489052:st=2:i=6225:sd=15:ss=axioms_2954 on theBenchmark for (2954ds/6225Mi) % 40.13/6.85 % (581230)Refutation not found, incomplete strategy % 40.13/6.85 % (581230)------------------------------ % 40.13/6.85 % (581230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.13/6.85 % (581230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.13/6.85 % (581230)CaDiCaL version: 2.1.3 % 40.13/6.85 % (581230)Termination reason: Refutation not found, incomplete strategy % 40.13/6.85 % (581230)Time elapsed: 0.007 s % 40.13/6.85 % (581230)Peak memory usage: 88 MB % 40.13/6.85 % (581230)Instructions burned: 11 (million) % 40.13/6.85 % (581227)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 40.13/6.85 % (581227)------------------------------ % 40.13/6.85 % (581227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 40.13/6.85 % (581227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 40.13/6.85 % (581227)CaDiCaL version: 2.1.3 % 40.13/6.85 % (581227)Termination reason: Unknown % 40.13/6.85 % (581227)Termination phase: Saturation % 40.13/6.85 % (581227)Time elapsed: 0.362 s % 40.13/6.85 % (581227)Peak memory usage: 114 MB % 40.13/6.85 % (581227)Instructions burned: 545 (million) % 45.49/7.39 % (581231)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2497118050:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2953 on theBenchmark for (2953ds/3372Mi) % 45.49/7.39 % (581226)Instruction limit reached! % 45.49/7.39 % (581226)------------------------------ % 45.49/7.39 % (581226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.39 % (581226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.39 % (581226)CaDiCaL version: 2.1.3 % 45.49/7.39 % (581226)Termination reason: Instruction limit % 45.49/7.39 % (581226)Termination phase: Saturation % 45.49/7.39 % (581226)Time elapsed: 0.505 s % 45.49/7.39 % (581226)Peak memory usage: 94 MB % 45.49/7.39 % (581226)Instructions burned: 1084 (million) % 45.49/7.39 % (581233)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1702344010:st=2.3:i=26457:sd=10:ss=included:sgt=8_2952 on theBenchmark for (2952ds/26457Mi) % 45.49/7.39 % (581230)------------------------------ % 45.49/7.39 % (581230)------------------------------ % 45.49/7.39 % (581235)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=2411543873:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2951 on theBenchmark for (2951ds/13494Mi) % 45.49/7.39 % (581237)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=2572704097:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2950 on theBenchmark for (2950ds/2503Mi) % 45.49/7.39 % (581237)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 45.49/7.39 % (581231)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.49/7.39 % (581231)------------------------------ % 45.49/7.39 % (581231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.39 % (581231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.39 % (581231)CaDiCaL version: 2.1.3 % 45.49/7.39 % (581231)Termination reason: Unknown % 45.49/7.39 % (581231)Termination phase: Saturation % 45.49/7.39 % (581231)Time elapsed: 0.363 s % 45.49/7.39 % (581231)Peak memory usage: 113 MB % 45.49/7.39 % (581231)Instructions burned: 541 (million) % 45.49/7.39 % (581233)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.49/7.39 % (581233)------------------------------ % 45.49/7.39 % (581233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.39 % (581233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.39 % (581233)CaDiCaL version: 2.1.3 % 45.49/7.39 % (581233)Termination reason: Unknown % 45.49/7.39 % (581233)Termination phase: Saturation % 45.49/7.39 % (581233)Time elapsed: 0.363 s % 45.49/7.39 % (581233)Peak memory usage: 113 MB % 45.49/7.39 % (581233)Instructions burned: 543 (million) % 45.49/7.39 % (581240)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3426308298:i=2559:sd=1:ep=RSTC:ss=axioms_2948 on theBenchmark for (2948ds/2559Mi) % 45.49/7.39 % (581235)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.49/7.39 % (581235)------------------------------ % 45.49/7.39 % (581235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.39 % (581235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.39 % (581235)CaDiCaL version: 2.1.3 % 45.49/7.39 % (581235)Termination reason: Unknown % 45.49/7.39 % (581235)Termination phase: Saturation % 45.49/7.39 % (581235)Time elapsed: 0.361 s % 45.49/7.39 % (581235)Peak memory usage: 114 MB % 45.49/7.39 % (581235)Instructions burned: 544 (million) % 45.49/7.39 % (581241)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2910097067:i=30753:av=off:ss=included_2947 on theBenchmark for (2947ds/30753Mi) % 45.49/7.39 % (581237)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.49/7.39 % (581237)------------------------------ % 45.49/7.39 % (581237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.49/7.39 % (581237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.49/7.39 % (581237)CaDiCaL version: 2.1.3 % 45.49/7.39 % (581237)Termination reason: Unknown % 45.49/7.39 % (581237)Termination phase: Saturation % 45.49/7.39 % (581237)Time elapsed: 0.361 s % 45.49/7.39 % (581237)Peak memory usage: 113 MB % 50.97/8.04 % (581237)Instructions burned: 541 (million) % 50.97/8.04 % (581243)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2498356198:i=26473:ep=RSTC_2946 on theBenchmark for (2946ds/26473Mi) % 50.97/8.04 % (581209)Instruction limit reached! % 50.97/8.04 % (581209)------------------------------ % 50.97/8.04 % (581209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.97/8.04 % (581209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.97/8.04 % (581209)CaDiCaL version: 2.1.3 % 50.97/8.04 % (581209)Termination reason: Instruction limit % 50.97/8.04 % (581209)Termination phase: Saturation % 50.97/8.04 % (581209)Time elapsed: 2.381 s % 50.97/8.04 % (581209)Peak memory usage: 107 MB % 50.97/8.04 % (581209)Instructions burned: 4835 (million) % 50.97/8.04 % (581195)Instruction limit reached! % 50.97/8.04 % (581195)------------------------------ % 50.97/8.04 % (581195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.97/8.04 % (581195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.97/8.04 % (581195)CaDiCaL version: 2.1.3 % 50.97/8.04 % (581195)Termination reason: Instruction limit % 50.97/8.04 % (581195)Termination phase: Saturation % 50.97/8.04 % (581195)Time elapsed: 3.077 s % 50.97/8.04 % (581195)Peak memory usage: 120 MB % 50.97/8.04 % (581195)Instructions burned: 5782 (million) % 50.97/8.04 % (581245)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=2109278533:cts=off:i=2759:kws=inv_arity:fgj=on_2945 on theBenchmark for (2945ds/2759Mi) % 50.97/8.04 % (581247)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=3200098846:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2944 on theBenchmark for (2944ds/5665Mi) % 50.97/8.04 % (581247)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 50.97/8.04 % (581240)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.97/8.04 % (581240)------------------------------ % 50.97/8.04 % (581240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.97/8.04 % (581240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.97/8.04 % (581240)CaDiCaL version: 2.1.3 % 50.97/8.04 % (581240)Termination reason: Unknown % 50.97/8.04 % (581240)Termination phase: Saturation % 50.97/8.04 % (581240)Time elapsed: 0.364 s % 50.97/8.04 % (581240)Peak memory usage: 113 MB % 50.97/8.04 % (581240)Instructions burned: 542 (million) % 50.97/8.04 % (581248)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=1691900296:i=1532:ep=RS:ss=axioms_2943 on theBenchmark for (2943ds/1532Mi) % 50.97/8.04 % (581241)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.97/8.04 % (581241)------------------------------ % 50.97/8.04 % (581241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.97/8.04 % (581241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.97/8.04 % (581241)CaDiCaL version: 2.1.3 % 50.97/8.04 % (581241)Termination reason: Unknown % 50.97/8.04 % (581241)Termination phase: Saturation % 50.97/8.04 % (581241)Time elapsed: 0.364 s % 50.97/8.04 % (581241)Peak memory usage: 113 MB % 50.97/8.04 % (581241)Instructions burned: 543 (million) % 50.97/8.04 % (581251)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1766843194:i=1565:sd=2:ss=axioms:sgt=32_2943 on theBenchmark for (2943ds/1565Mi) % 50.97/8.04 % (581245)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.97/8.04 % (581245)------------------------------ % 50.97/8.04 % (581245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.97/8.04 % (581245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.97/8.04 % (581245)CaDiCaL version: 2.1.3 % 50.97/8.04 % (581245)Termination reason: Unknown % 50.97/8.04 % (581245)Termination phase: Saturation % 50.97/8.04 % (581245)Time elapsed: 0.363 s % 50.97/8.04 % (581245)Peak memory usage: 114 MB % 50.97/8.04 % (581245)Instructions burned: 544 (million) % 50.97/8.04 % (581253)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=3092426594:i=1572:fgj=on:gsp=on_2941 on theBenchmark for (2941ds/1572Mi) % 54.14/8.67 % (581253)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 54.14/8.67 % (581247)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.14/8.67 % (581247)------------------------------ % 54.14/8.67 % (581247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.14/8.67 % (581247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.14/8.67 % (581247)CaDiCaL version: 2.1.3 % 54.14/8.67 % (581247)Termination reason: Unknown % 54.14/8.67 % (581247)Termination phase: Saturation % 54.14/8.67 % (581247)Time elapsed: 0.361 s % 54.14/8.67 % (581247)Peak memory usage: 113 MB % 54.14/8.67 % (581247)Instructions burned: 542 (million) % 54.14/8.67 % (581248)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.14/8.67 % (581248)------------------------------ % 54.14/8.67 % (581248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.14/8.67 % (581248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.14/8.67 % (581248)CaDiCaL version: 2.1.3 % 54.14/8.67 % (581248)Termination reason: Unknown % 54.14/8.67 % (581248)Termination phase: Saturation % 54.14/8.67 % (581248)Time elapsed: 0.361 s % 54.14/8.67 % (581248)Peak memory usage: 113 MB % 54.14/8.67 % (581248)Instructions burned: 543 (million) % 54.14/8.67 % (581256)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2073784659:i=6052:sd=4:ss=axioms:sgt=24_2940 on theBenchmark for (2940ds/6052Mi) % 54.14/8.67 % (581257)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=3544325306:i=3500:sd=1:bd=preordered:sup=off:ss=included_2939 on theBenchmark for (2939ds/3500Mi) % 54.14/8.67 % (581251)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.14/8.67 % (581251)------------------------------ % 54.14/8.67 % (581251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.14/8.67 % (581251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.14/8.67 % (581251)CaDiCaL version: 2.1.3 % 54.14/8.67 % (581251)Termination reason: Unknown % 54.14/8.67 % (581251)Termination phase: Saturation % 54.14/8.67 % (581251)Time elapsed: 0.364 s % 54.14/8.67 % (581251)Peak memory usage: 113 MB % 54.14/8.67 % (581251)Instructions burned: 542 (million) % 54.14/8.67 % (581258)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=2120217958:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2938 on theBenchmark for (2938ds/1842Mi) % 54.14/8.67 % (581258)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 54.14/8.67 % (581253)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.14/8.67 % (581253)------------------------------ % 54.14/8.67 % (581253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.14/8.67 % (581253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.14/8.67 % (581253)CaDiCaL version: 2.1.3 % 54.14/8.67 % (581253)Termination reason: Unknown % 54.14/8.67 % (581253)Termination phase: Saturation % 54.14/8.67 % (581253)Time elapsed: 0.364 s % 54.14/8.67 % (581253)Peak memory usage: 113 MB % 54.14/8.67 % (581253)Instructions burned: 542 (million) % 54.14/8.67 % (581261)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=409021372:i=66096:add=on_2937 on theBenchmark for (2937ds/66096Mi) % 54.14/8.67 % (581256)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.14/8.67 % (581256)------------------------------ % 54.14/8.67 % (581256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.14/8.67 % (581256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.14/8.67 % (581256)CaDiCaL version: 2.1.3 % 54.14/8.67 % (581256)Termination reason: Unknown % 54.14/8.67 % (581256)Termination phase: Saturation % 54.14/8.67 % (581256)Time elapsed: 0.362 s % 54.14/8.67 % (581256)Peak memory usage: 113 MB % 54.14/8.67 % (581256)Instructions burned: 541 (million) % 54.14/8.67 % (581263)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1424614313:i=1884:sd=1:nm=60:ss=axioms_2936 on theBenchmark for (2936ds/1884Mi) % 59.35/9.34 % (581257)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.35/9.34 % (581257)------------------------------ % 59.35/9.34 % (581257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.35/9.34 % (581257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.35/9.34 % (581257)CaDiCaL version: 2.1.3 % 59.35/9.34 % (581257)Termination reason: Unknown % 59.35/9.34 % (581257)Termination phase: Saturation % 59.35/9.34 % (581257)Time elapsed: 0.364 s % 59.35/9.34 % (581257)Peak memory usage: 113 MB % 59.35/9.34 % (581257)Instructions burned: 543 (million) % 59.35/9.34 % (581258)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.35/9.34 % (581258)------------------------------ % 59.35/9.34 % (581258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.35/9.34 % (581258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.35/9.34 % (581258)CaDiCaL version: 2.1.3 % 59.35/9.34 % (581258)Termination reason: Unknown % 59.35/9.34 % (581258)Termination phase: Saturation % 59.35/9.34 % (581258)Time elapsed: 0.361 s % 59.35/9.34 % (581258)Peak memory usage: 113 MB % 59.35/9.34 % (581258)Instructions burned: 542 (million) % 59.35/9.34 % (581265)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1602588031:cts=off:i=5469:bs=on:fsr=off_2934 on theBenchmark for (2934ds/5469Mi) % 59.35/9.34 % (581267)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=189972325:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2934 on theBenchmark for (2934ds/2037Mi) % 59.35/9.34 % (581261)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.35/9.34 % (581261)------------------------------ % 59.35/9.34 % (581261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.35/9.34 % (581261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.35/9.34 % (581261)CaDiCaL version: 2.1.3 % 59.35/9.34 % (581261)Termination reason: Unknown % 59.35/9.34 % (581261)Termination phase: Saturation % 59.35/9.34 % (581261)Time elapsed: 0.363 s % 59.35/9.34 % (581261)Peak memory usage: 113 MB % 59.35/9.34 % (581261)Instructions burned: 543 (million) % 59.35/9.34 % (581268)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2301386942:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2933 on theBenchmark for (2933ds/2110Mi) % 59.35/9.34 % (581263)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.35/9.34 % (581263)------------------------------ % 59.35/9.34 % (581263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.35/9.34 % (581263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.35/9.34 % (581263)CaDiCaL version: 2.1.3 % 59.35/9.34 % (581263)Termination reason: Unknown % 59.35/9.34 % (581263)Termination phase: Saturation % 59.35/9.34 % (581263)Time elapsed: 0.364 s % 59.35/9.34 % (581263)Peak memory usage: 113 MB % 59.35/9.34 % (581263)Instructions burned: 539 (million) % 59.35/9.34 % (581271)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=4012815542:i=2430:add=off:aac=none:nm=16_2932 on theBenchmark for (2932ds/2430Mi) % 59.35/9.34 % (581273)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=3928140251:cond=fast:i=4891_2931 on theBenchmark for (2931ds/4891Mi) % 59.35/9.34 % (581267)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.35/9.34 % (581267)------------------------------ % 59.35/9.34 % (581267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.35/9.34 % (581267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.35/9.34 % (581267)CaDiCaL version: 2.1.3 % 59.35/9.34 % (581267)Termination reason: Unknown % 59.35/9.34 % (581267)Termination phase: Saturation % 59.35/9.34 % (581267)Time elapsed: 0.367 s % 59.35/9.34 % (581267)Peak memory usage: 114 MB % 59.35/9.34 % (581267)Instructions burned: 549 (million) % 59.35/9.34 % (581268)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 59.35/9.34 % (581268)------------------------------ % 59.35/9.34 % (581268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.35/9.34 % (581268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.13/10.10 % (581268)CaDiCaL version: 2.1.3 % 65.13/10.10 % (581268)Termination reason: Unknown % 65.13/10.10 % (581268)Termination phase: Saturation % 65.13/10.10 % (581268)Time elapsed: 0.361 s % 65.13/10.10 % (581268)Peak memory usage: 114 MB % 65.13/10.10 % (581268)Instructions burned: 547 (million) % 65.13/10.10 % (581271)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.13/10.10 % (581271)------------------------------ % 65.13/10.10 % (581271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.13/10.10 % (581271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.13/10.10 % (581271)CaDiCaL version: 2.1.3 % 65.13/10.10 % (581271)Termination reason: Unknown % 65.13/10.10 % (581271)Termination phase: Saturation % 65.13/10.10 % (581271)Time elapsed: 0.361 s % 65.13/10.10 % (581271)Peak memory usage: 113 MB % 65.13/10.10 % (581271)Instructions burned: 543 (million) % 65.13/10.10 % (581276)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=4046292957:st=2:i=14845:sd=2:ss=included:fsd=on_2928 on theBenchmark for (2928ds/14845Mi) % 65.13/10.10 % (581277)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=4216648913:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2928 on theBenchmark for (2928ds/7534Mi) % 65.13/10.10 % (581273)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.13/10.10 % (581273)------------------------------ % 65.13/10.10 % (581273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.13/10.10 % (581273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.13/10.10 % (581273)CaDiCaL version: 2.1.3 % 65.13/10.10 % (581273)Termination reason: Unknown % 65.13/10.10 % (581273)Termination phase: Saturation % 65.13/10.10 % (581273)Time elapsed: 0.363 s % 65.13/10.10 % (581273)Peak memory usage: 113 MB % 65.13/10.10 % (581273)Instructions burned: 543 (million) % 65.13/10.10 % (581279)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=376827764:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2927 on theBenchmark for (2927ds/10353Mi) % 65.13/10.10 % (581281)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4121501527:i=7860_2925 on theBenchmark for (2925ds/7860Mi) % 65.13/10.10 % (581281)Refutation not found, incomplete strategy % 65.13/10.10 % (581281)------------------------------ % 65.13/10.10 % (581281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.13/10.10 % (581281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.13/10.10 % (581281)CaDiCaL version: 2.1.3 % 65.13/10.10 % (581281)Termination reason: Refutation not found, incomplete strategy % 65.13/10.10 % (581281)Time elapsed: 0.007 s % 65.13/10.10 % (581281)Peak memory usage: 88 MB % 65.13/10.10 % (581281)Instructions burned: 11 (million) % 65.13/10.10 % (581276)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.13/10.10 % (581276)------------------------------ % 65.13/10.10 % (581276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.13/10.10 % (581276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.13/10.10 % (581276)CaDiCaL version: 2.1.3 % 65.13/10.10 % (581276)Termination reason: Unknown % 65.13/10.10 % (581276)Termination phase: Saturation % 65.13/10.10 % (581276)Time elapsed: 0.362 s % 65.13/10.10 % (581276)Peak memory usage: 114 MB % 65.13/10.10 % (581276)Instructions burned: 542 (million) % 65.13/10.10 % (581277)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.13/10.10 % (581277)------------------------------ % 65.13/10.10 % (581277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.13/10.10 % (581277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.13/10.10 % (581277)CaDiCaL version: 2.1.3 % 65.13/10.10 % (581277)Termination reason: Unknown % 65.13/10.10 % (581277)Termination phase: Saturation % 65.13/10.10 % (581277)Time elapsed: 0.361 s % 65.13/10.10 % (581277)Peak memory usage: 114 MB % 65.13/10.10 % (581277)Instructions burned: 545 (million) % 65.13/10.10 % (581279)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 65.13/10.10 % (581279)------------------------------ % 65.13/10.10 % (581279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.87/10.78 % (581279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.87/10.78 % (581279)CaDiCaL version: 2.1.3 % 67.87/10.78 % (581279)Termination reason: Unknown % 67.87/10.78 % (581279)Termination phase: Saturation % 67.87/10.78 % (581279)Time elapsed: 0.363 s % 67.87/10.78 % (581279)Peak memory usage: 113 MB % 67.87/10.78 % (581279)Instructions burned: 541 (million) % 67.87/10.78 % (581284)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=662176632:i=7896:sd=2:bs=on:ss=included:sgt=20_2923 on theBenchmark for (2923ds/7896Mi) % 67.87/10.78 % (581281)------------------------------ % 67.87/10.78 % (581281)------------------------------ % 67.87/10.78 % (581285)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2436837175:i=5812:gtgl=2:gtg=all_2922 on theBenchmark for (2922ds/5812Mi) % 67.87/10.78 % (581287)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=2079478432:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2921 on theBenchmark for (2921ds/2965Mi) % 67.87/10.78 % (581289)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=4239861494:i=2967:kws=precedence:bd=preordered:av=off_2921 on theBenchmark for (2921ds/2967Mi) % 67.87/10.78 % (581284)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.87/10.78 % (581284)------------------------------ % 67.87/10.78 % (581284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.87/10.78 % (581284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.87/10.78 % (581284)CaDiCaL version: 2.1.3 % 67.87/10.78 % (581284)Termination reason: Unknown % 67.87/10.78 % (581284)Termination phase: Saturation % 67.87/10.78 % (581284)Time elapsed: 0.361 s % 67.87/10.78 % (581284)Peak memory usage: 113 MB % 67.87/10.78 % (581284)Instructions burned: 541 (million) % 67.87/10.78 % (581285)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.87/10.78 % (581285)------------------------------ % 67.87/10.78 % (581285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.87/10.78 % (581285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.87/10.78 % (581285)CaDiCaL version: 2.1.3 % 67.87/10.78 % (581285)Termination reason: Unknown % 67.87/10.78 % (581285)Termination phase: Saturation % 67.87/10.78 % (581285)Time elapsed: 0.360 s % 67.87/10.78 % (581285)Peak memory usage: 114 MB % 67.87/10.78 % (581285)Instructions burned: 546 (million) % 67.87/10.78 % (581287)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.87/10.78 % (581287)------------------------------ % 67.87/10.78 % (581287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.87/10.78 % (581287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.87/10.78 % (581287)CaDiCaL version: 2.1.3 % 67.87/10.78 % (581287)Termination reason: Unknown % 67.87/10.78 % (581287)Termination phase: Saturation % 67.87/10.78 % (581287)Time elapsed: 0.359 s % 67.87/10.78 % (581287)Peak memory usage: 113 MB % 67.87/10.78 % (581287)Instructions burned: 543 (million) % 67.87/10.78 % (581292)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=517456951:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2918 on theBenchmark for (2918ds/3022Mi) % 67.87/10.78 % (581289)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.87/10.78 % (581289)------------------------------ % 67.87/10.78 % (581289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.87/10.78 % (581289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.87/10.78 % (581289)CaDiCaL version: 2.1.3 % 67.87/10.78 % (581289)Termination reason: Unknown % 67.87/10.78 % (581289)Termination phase: Saturation % 67.87/10.78 % (581289)Time elapsed: 0.359 s % 67.87/10.78 % (581289)Peak memory usage: 113 MB % 67.87/10.78 % (581289)Instructions burned: 543 (million) % 67.87/10.78 % (581293)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=574601779:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2917 on theBenchmark for (2917ds/3207Mi) % 74.58/11.50 % (581294)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2533083612:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2916 on theBenchmark for (2916ds/3289Mi) % 74.58/11.50 % (581297)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1918782852:i=38569:sd=3:ss=axioms:sgt=32_2916 on theBenchmark for (2916ds/38569Mi) % 74.58/11.50 % (581292)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.58/11.50 % (581292)------------------------------ % 74.58/11.50 % (581292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.58/11.50 % (581292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.58/11.50 % (581292)CaDiCaL version: 2.1.3 % 74.58/11.50 % (581292)Termination reason: Unknown % 74.58/11.50 % (581292)Termination phase: Saturation % 74.58/11.50 % (581292)Time elapsed: 0.362 s % 74.58/11.50 % (581292)Peak memory usage: 113 MB % 74.58/11.50 % (581292)Instructions burned: 542 (million) % 74.58/11.50 % (581293)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.58/11.50 % (581293)------------------------------ % 74.58/11.50 % (581293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.58/11.50 % (581293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.58/11.50 % (581293)CaDiCaL version: 2.1.3 % 74.58/11.50 % (581293)Termination reason: Unknown % 74.58/11.50 % (581293)Termination phase: Saturation % 74.58/11.50 % (581293)Time elapsed: 0.359 s % 74.58/11.50 % (581293)Peak memory usage: 114 MB % 74.58/11.50 % (581293)Instructions burned: 542 (million) % 74.58/11.50 % (581294)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.58/11.50 % (581294)------------------------------ % 74.58/11.50 % (581294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.58/11.50 % (581294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.58/11.50 % (581294)CaDiCaL version: 2.1.3 % 74.58/11.50 % (581294)Termination reason: Unknown % 74.58/11.50 % (581294)Termination phase: Saturation % 74.58/11.50 % (581294)Time elapsed: 0.361 s % 74.58/11.50 % (581294)Peak memory usage: 113 MB % 74.58/11.50 % (581294)Instructions burned: 545 (million) % 74.58/11.50 % (581300)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=202795787:cts=off:i=3394_2912 on theBenchmark for (2912ds/3394Mi) % 74.58/11.50 % (581301)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=1969891440:i=33824:bd=preordered_2912 on theBenchmark for (2912ds/33824Mi) % 74.58/11.50 % (581297)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.58/11.50 % (581297)------------------------------ % 74.58/11.50 % (581297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.58/11.50 % (581297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.58/11.50 % (581297)CaDiCaL version: 2.1.3 % 74.58/11.50 % (581297)Termination reason: Unknown % 74.58/11.50 % (581297)Termination phase: Saturation % 74.58/11.50 % (581297)Time elapsed: 0.363 s % 74.58/11.50 % (581297)Peak memory usage: 113 MB % 74.58/11.50 % (581297)Instructions burned: 543 (million) % 74.58/11.50 % (581302)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=541223447:i=20684:bd=all:gtg=exists_sym_2911 on theBenchmark for (2911ds/20684Mi) % 74.58/11.50 % (581305)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=2786462706: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_2910 on theBenchmark for (2910ds/7222Mi) % 74.58/11.50 % (581305)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 74.58/11.50 % (581300)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.58/11.50 % (581300)------------------------------ % 74.58/11.50 % (581300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.58/11.50 % (581300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.58/11.50 % (581300)CaDiCaL version: 2.1.3 % 74.58/11.50 % (581300)Termination reason: Unknown % 74.58/11.50 % (581300)Termination phase: Saturation % 74.58/11.50 % (581300)Time elapsed: 0.362 s % 80.50/12.33 % (581300)Peak memory usage: 113 MB % 80.50/12.33 % (581300)Instructions burned: 543 (million) % 80.50/12.33 % (581301)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.50/12.33 % (581301)------------------------------ % 80.50/12.33 % (581301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.50/12.33 % (581301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.50/12.33 % (581301)CaDiCaL version: 2.1.3 % 80.50/12.33 % (581301)Termination reason: Unknown % 80.50/12.33 % (581301)Termination phase: Saturation % 80.50/12.33 % (581301)Time elapsed: 0.361 s % 80.50/12.33 % (581301)Peak memory usage: 114 MB % 80.50/12.33 % (581301)Instructions burned: 543 (million) % 80.50/12.33 % (581302)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.50/12.33 % (581302)------------------------------ % 80.50/12.33 % (581302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.50/12.33 % (581302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.50/12.33 % (581302)CaDiCaL version: 2.1.3 % 80.50/12.33 % (581302)Termination reason: Unknown % 80.50/12.33 % (581302)Termination phase: Saturation % 80.50/12.33 % (581302)Time elapsed: 0.361 s % 80.50/12.33 % (581302)Peak memory usage: 114 MB % 80.50/12.33 % (581302)Instructions burned: 545 (million) % 80.50/12.33 % (581308)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1092628106:st=4:i=7295:sd=4:ep=R:ss=axioms_2907 on theBenchmark for (2907ds/7295Mi) % 80.50/12.33 % (581309)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=1894185294:i=4036:ins=10_2907 on theBenchmark for (2907ds/4036Mi) % 80.50/12.33 % (581305)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.50/12.33 % (581305)------------------------------ % 80.50/12.33 % (581305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.50/12.33 % (581305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.50/12.33 % (581305)CaDiCaL version: 2.1.3 % 80.50/12.33 % (581305)Termination reason: Unknown % 80.50/12.33 % (581305)Termination phase: Saturation % 80.50/12.33 % (581305)Time elapsed: 0.377 s % 80.50/12.33 % (581305)Peak memory usage: 114 MB % 80.50/12.33 % (581305)Instructions burned: 549 (million) % 80.50/12.33 % (581310)lrs+10_1_sil=128000:lcm=predicate:random_seed=789966332:st=3:i=43697:sd=5:ss=axioms_2906 on theBenchmark for (2906ds/43697Mi) % 80.50/12.33 % (581313)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=497403293:i=17599:gtg=all:ss=axioms:fsd=on_2905 on theBenchmark for (2905ds/17599Mi) % 80.50/12.33 % (581308)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.50/12.33 % (581308)------------------------------ % 80.50/12.33 % (581308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.50/12.33 % (581308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.50/12.33 % (581308)CaDiCaL version: 2.1.3 % 80.50/12.33 % (581308)Termination reason: Unknown % 80.50/12.33 % (581308)Termination phase: Saturation % 80.50/12.33 % (581308)Time elapsed: 0.440 s % 80.50/12.33 % (581308)Peak memory usage: 112 MB % 80.50/12.33 % (581309)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 80.50/12.33 % (581308)Instructions burned: 546 (million) % 80.50/12.33 % (581309)------------------------------ % 80.50/12.33 % (581309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.50/12.33 % (581309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.50/12.33 % (581309)CaDiCaL version: 2.1.3 % 80.50/12.33 % (581309)Termination reason: Unknown % 80.50/12.33 % (581309)Termination phase: Saturation % 80.50/12.33 % (581309)Time elapsed: 0.420 s % 80.50/12.33 % (581309)Peak memory usage: 112 MB % 80.50/12.33 % (581309)Instructions burned: 540 (million) % 80.50/12.33 % (581265)Instruction limit reached! % 80.50/12.33 % (581265)------------------------------ % 80.50/12.33 % (581265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 80.50/12.33 % (581265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.50/12.33 % (581265)CaDiCaL version: 2.1.3 % 80.50/12.33 % (581265)Termination reason: Instruction limit % 80.50/12.33 % (581265)Termination phase: Saturation % 80.50/12.33 % (581265)Time elapsed: 3.241 s % 80.50/12.33 % (581265)Peak memory usage: 121 MB % 80.50/12.33 % (581265)Instructions burned: 5469 (million) % 83.99/13.01 % (581316)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=343531166:i=4547:bd=preordered_2901 on theBenchmark for (2901ds/4547Mi) % 83.99/13.01 % (581317)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=4189075229:i=9294:av=off_2901 on theBenchmark for (2901ds/9294Mi) % 83.99/13.01 % (581318)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2149521696:i=32849:add=on_2900 on theBenchmark for (2900ds/32849Mi) % 83.99/13.01 % (581313)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.99/13.01 % (581313)------------------------------ % 83.99/13.01 % (581313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.99/13.01 % (581313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.99/13.01 % (581313)CaDiCaL version: 2.1.3 % 83.99/13.01 % (581313)Termination reason: Unknown % 83.99/13.01 % (581313)Termination phase: Saturation % 83.99/13.01 % (581313)Time elapsed: 0.454 s % 83.99/13.01 % (581313)Peak memory usage: 113 MB % 83.99/13.01 % (581313)Instructions burned: 545 (million) % 83.99/13.01 % (581322)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=56703808:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2899 on theBenchmark for (2899ds/4793Mi) % 83.99/13.01 % (581316)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.99/13.01 % (581316)------------------------------ % 83.99/13.01 % (581316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.99/13.01 % (581316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.99/13.01 % (581316)CaDiCaL version: 2.1.3 % 83.99/13.01 % (581316)Termination reason: Unknown % 83.99/13.01 % (581316)Termination phase: Saturation % 83.99/13.01 % (581316)Time elapsed: 0.359 s % 83.99/13.01 % (581316)Peak memory usage: 113 MB % 83.99/13.01 % (581316)Instructions burned: 542 (million) % 83.99/13.01 % (581317)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.99/13.01 % (581317)------------------------------ % 83.99/13.01 % (581317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.99/13.01 % (581317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.99/13.01 % (581317)CaDiCaL version: 2.1.3 % 83.99/13.01 % (581317)Termination reason: Unknown % 83.99/13.01 % (581317)Termination phase: Saturation % 83.99/13.01 % (581317)Time elapsed: 0.360 s % 83.99/13.01 % (581317)Peak memory usage: 113 MB % 83.99/13.01 % (581317)Instructions burned: 542 (million) % 83.99/13.01 % (581318)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.99/13.01 % (581318)------------------------------ % 83.99/13.01 % (581318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.99/13.01 % (581318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.99/13.01 % (581318)CaDiCaL version: 2.1.3 % 83.99/13.01 % (581318)Termination reason: Unknown % 83.99/13.01 % (581318)Termination phase: Saturation % 83.99/13.01 % (581318)Time elapsed: 0.362 s % 83.99/13.01 % (581318)Peak memory usage: 113 MB % 83.99/13.01 % (581318)Instructions burned: 543 (million) % 83.99/13.01 % (581324)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=390382419:i=4840:nm=4:av=off_2896 on theBenchmark for (2896ds/4840Mi) % 83.99/13.01 % (581325)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=729259619:cts=off:i=5002_2896 on theBenchmark for (2896ds/5002Mi) % 83.99/13.01 % (581326)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=695023679:i=30479:sd=3:ss=axioms_2895 on theBenchmark for (2895ds/30479Mi) % 83.99/13.01 % (581322)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 83.99/13.01 % (581322)------------------------------ % 83.99/13.01 % (581322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.99/13.01 % (581322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.99/13.01 % (581322)CaDiCaL version: 2.1.3 % 83.99/13.01 % (581322)Termination reason: Unknown % 83.99/13.01 % (581322)Termination phase: Saturation % 102.10/15.34 % (581322)Time elapsed: 0.391 s % 102.10/15.34 % (581322)Peak memory usage: 113 MB % 102.10/15.34 % (581322)Instructions burned: 542 (million) % 102.10/15.34 % (581330)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=1226720809:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2893 on theBenchmark for (2893ds/11035Mi) % 102.10/15.34 % (581330)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 102.10/15.34 % (581324)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.10/15.34 % (581324)------------------------------ % 102.10/15.34 % (581324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.34 % (581324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.34 % (581324)CaDiCaL version: 2.1.3 % 102.10/15.34 % (581324)Termination reason: Unknown % 102.10/15.34 % (581324)Termination phase: Saturation % 102.10/15.34 % (581324)Time elapsed: 0.422 s % 102.10/15.34 % (581324)Peak memory usage: 112 MB % 102.10/15.34 % (581324)Instructions burned: 542 (million) % 102.10/15.34 % (581325)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.10/15.34 % (581325)------------------------------ % 102.10/15.34 % (581325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.34 % (581325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.34 % (581325)CaDiCaL version: 2.1.3 % 102.10/15.34 % (581325)Termination reason: Unknown % 102.10/15.34 % (581325)Termination phase: Saturation % 102.10/15.34 % (581325)Time elapsed: 0.422 s % 102.10/15.34 % (581325)Peak memory usage: 112 MB % 102.10/15.34 % (581325)Instructions burned: 542 (million) % 102.10/15.34 % (581326)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.10/15.34 % (581326)------------------------------ % 102.10/15.34 % (581326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.34 % (581326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.34 % (581326)CaDiCaL version: 2.1.3 % 102.10/15.34 % (581326)Termination reason: Unknown % 102.10/15.34 % (581326)Termination phase: Saturation % 102.10/15.35 % (581326)Time elapsed: 0.359 s % 102.10/15.35 % (581326)Peak memory usage: 113 MB % 102.10/15.35 % (581326)Instructions burned: 539 (million) % 102.10/15.35 % (581332)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1424879860:i=5835_2890 on theBenchmark for (2890ds/5835Mi) % 102.10/15.35 % (581333)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=538568825:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2890 on theBenchmark for (2890ds/5890Mi) % 102.10/15.35 % (581334)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=1335905046:cts=off:i=19910:ep=RS_2890 on theBenchmark for (2890ds/19910Mi) % 102.10/15.35 % (581334)Refutation not found, incomplete strategy % 102.10/15.35 % (581334)------------------------------ % 102.10/15.35 % (581334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.35 % (581334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.35 % (581334)CaDiCaL version: 2.1.3 % 102.10/15.35 % (581334)Termination reason: Refutation not found, incomplete strategy % 102.10/15.35 % (581334)Time elapsed: 0.006 s % 102.10/15.35 % (581334)Peak memory usage: 88 MB % 102.10/15.35 % (581334)Instructions burned: 11 (million) % 102.10/15.35 % (581330)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 102.10/15.35 % (581330)------------------------------ % 102.10/15.35 % (581330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.10/15.35 % (581330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.10/15.35 % (581330)CaDiCaL version: 2.1.3 % 102.10/15.35 % (581330)Termination reason: Unknown % 102.10/15.35 % (581330)Termination phase: Saturation % 102.10/15.35 % (581330)Time elapsed: 0.361 s % 102.10/15.35 % (581330)Peak memory usage: 114 MB % 102.10/15.35 % (581330)Instructions burned: 543 (million) % 102.10/15.35 % (581338)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=3493750741:i=20312:bd=preordered:fsr=off:er=filter_2888 on theBenchmark for (2888ds/20312Mi) % 102.10/15.35 % (581334)------------------------------ % 102.10/15.35 % (581334)------------------------------ % 102.10/15.35 % (581332)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.13/17.31 % (581333)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.13/17.31 % (581332)------------------------------ % 116.13/17.31 % (581332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.13/17.31 % (581333)------------------------------ % 116.13/17.31 % (581333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.13/17.31 % (581332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.13/17.31 % (581333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.13/17.31 % (581332)CaDiCaL version: 2.1.3 % 116.13/17.31 % (581333)CaDiCaL version: 2.1.3 % 116.13/17.31 % (581332)Termination reason: Unknown % 116.13/17.31 % (581332)Termination phase: Saturation % 116.13/17.31 % (581333)Termination reason: Unknown % 116.13/17.31 % (581333)Termination phase: Saturation % 116.13/17.31 % (581332)Time elapsed: 0.361 s % 116.13/17.31 % (581333)Time elapsed: 0.361 s % 116.13/17.31 % (581332)Peak memory usage: 112 MB % 116.13/17.31 % (581333)Peak memory usage: 112 MB % 116.13/17.31 % (581333)Instructions burned: 543 (million) % 116.13/17.31 % (581332)Instructions burned: 543 (million) % 116.13/17.31 % (581340)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=1890873974:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2886 on theBenchmark for (2886ds/13822Mi) % 116.13/17.31 % (581342)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=772790293:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2885 on theBenchmark for (2885ds/15184Mi) % 116.13/17.31 % (581341)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=826021887:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2885 on theBenchmark for (2885ds/7144Mi) % 116.13/17.31 % (581338)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.13/17.31 % (581338)------------------------------ % 116.13/17.31 % (581338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.13/17.31 % (581338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.13/17.31 % (581338)CaDiCaL version: 2.1.3 % 116.13/17.31 % (581338)Termination reason: Unknown % 116.13/17.31 % (581338)Termination phase: Saturation % 116.13/17.31 % (581338)Time elapsed: 0.362 s % 116.13/17.31 % (581338)Peak memory usage: 114 MB % 116.13/17.31 % (581338)Instructions burned: 542 (million) % 116.13/17.31 % (581346)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=332820382:i=107375_2883 on theBenchmark for (2883ds/107375Mi) % 116.13/17.31 % (581340)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.13/17.31 % (581340)------------------------------ % 116.13/17.31 % (581340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.13/17.31 % (581340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.13/17.31 % (581340)CaDiCaL version: 2.1.3 % 116.13/17.31 % (581340)Termination reason: Unknown % 116.13/17.31 % (581340)Termination phase: Saturation % 116.13/17.31 % (581340)Time elapsed: 0.364 s % 116.13/17.31 % (581340)Peak memory usage: 114 MB % 116.13/17.31 % (581340)Instructions burned: 543 (million) % 116.13/17.31 % (581342)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 116.13/17.31 % (581342)------------------------------ % 116.13/17.31 % (581342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.13/17.31 % (581342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.13/17.31 % (581342)CaDiCaL version: 2.1.3 % 116.13/17.31 % (581342)Termination reason: Unknown % 116.13/17.31 % (581342)Termination phase: Saturation % 116.13/17.31 % (581342)Time elapsed: 0.360 s % 116.13/17.31 % (581342)Peak memory usage: 114 MB % 116.13/17.31 % (581342)Instructions burned: 543 (million) % 116.13/17.31 % (581348)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=4009650462:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2880 on theBenchmark for (2880ds/7958Mi) % 116.13/17.31 % (581349)dis+10_128_sil=16000:nwc=0.7:random_seed=2802297805:i=15999:nm=2:gsp=on_2880 on theBenchmark for (2880ds/15999Mi) % 116.13/17.31 % (581349)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 124.83/18.67 % (581346)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.83/18.67 % (581346)------------------------------ % 124.83/18.67 % (581346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.83/18.67 % (581346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.83/18.67 % (581346)CaDiCaL version: 2.1.3 % 124.83/18.67 % (581346)Termination reason: Unknown % 124.83/18.67 % (581346)Termination phase: Saturation % 124.83/18.67 % (581346)Time elapsed: 0.361 s % 124.83/18.67 % (581346)Peak memory usage: 113 MB % 124.83/18.67 % (581346)Instructions burned: 542 (million) % 124.83/18.67 % (581352)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=507685106:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2877 on theBenchmark for (2877ds/8139Mi) % 124.83/18.67 % (581348)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.83/18.67 % (581348)------------------------------ % 124.83/18.67 % (581348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.83/18.67 % (581348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.83/18.67 % (581348)CaDiCaL version: 2.1.3 % 124.83/18.67 % (581348)Termination reason: Unknown % 124.83/18.67 % (581348)Termination phase: Saturation % 124.83/18.67 % (581348)Time elapsed: 0.360 s % 124.83/18.67 % (581348)Peak memory usage: 114 MB % 124.83/18.67 % (581348)Instructions burned: 543 (million) % 124.83/18.67 % (581354)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=990697505:st=4:i=8950:sd=5:ss=axioms_2875 on theBenchmark for (2875ds/8950Mi) % 124.83/18.67 % (581354)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.83/18.67 % (581354)------------------------------ % 124.83/18.67 % (581354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.83/18.67 % (581354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.83/18.67 % (581354)CaDiCaL version: 2.1.3 % 124.83/18.67 % (581354)Termination reason: Unknown % 124.83/18.67 % (581354)Termination phase: Saturation % 124.83/18.67 % (581354)Time elapsed: 0.359 s % 124.83/18.67 % (581354)Peak memory usage: 113 MB % 124.83/18.67 % (581354)Instructions burned: 543 (million) % 124.83/18.67 % (581356)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3205282398:i=9809:ins=10:av=off_2870 on theBenchmark for (2870ds/9809Mi) % 124.83/18.67 % (581356)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.83/18.67 % (581356)------------------------------ % 124.83/18.67 % (581356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.83/18.67 % (581356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.83/18.67 % (581356)CaDiCaL version: 2.1.3 % 124.83/18.67 % (581356)Termination reason: Unknown % 124.83/18.67 % (581356)Termination phase: Saturation % 124.83/18.67 % (581356)Time elapsed: 0.358 s % 124.83/18.67 % (581356)Peak memory usage: 114 MB % 124.83/18.67 % (581356)Instructions burned: 543 (million) % 124.83/18.67 % (581417)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2692260396:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2865 on theBenchmark for (2865ds/9885Mi) % 124.83/18.67 % (581417)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.83/18.67 % (581417)------------------------------ % 124.83/18.67 % (581417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.83/18.67 % (581417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.83/18.67 % (581417)CaDiCaL version: 2.1.3 % 124.83/18.67 % (581417)Termination reason: Unknown % 124.83/18.67 % (581417)Termination phase: Saturation % 124.83/18.67 % (581417)Time elapsed: 0.357 s % 124.83/18.67 % (581417)Peak memory usage: 114 MB % 124.83/18.67 % (581417)Instructions burned: 543 (million) % 124.83/18.67 % (581476)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=4047798696:cond=fast:i=32078:fgj=on:av=off_2860 on theBenchmark for (2860ds/32078Mi) % 124.83/18.67 % (581476)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.83/18.67 % (581476)------------------------------ % 124.83/18.67 % (581476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.83/18.67 % (581476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.37/24.07 % (581476)CaDiCaL version: 2.1.3 % 164.37/24.07 % (581476)Termination reason: Unknown % 164.37/24.07 % (581476)Termination phase: Saturation % 164.37/24.07 % (581476)Time elapsed: 0.359 s % 164.37/24.07 % (581476)Peak memory usage: 113 MB % 164.37/24.07 % (581476)Instructions burned: 542 (million) % 164.37/24.07 % (581218)Instruction limit reached! % 164.37/24.07 % (581218)------------------------------ % 164.37/24.07 % (581218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.37/24.07 % (581218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.37/24.07 % (581218)CaDiCaL version: 2.1.3 % 164.37/24.07 % (581218)Termination reason: Instruction limit % 164.37/24.07 % (581218)Termination phase: Saturation % 164.37/24.07 % (581218)Time elapsed: 11.160 s % 164.37/24.07 % (581218)Peak memory usage: 256 MB % 164.37/24.07 % (581218)Instructions burned: 33335 (million) % 164.37/24.07 % (581580)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=4882494:i=11101:bd=all:ss=axioms:sgt=8_2855 on theBenchmark for (2855ds/11101Mi) % 164.37/24.07 % (581594)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:fd=preordered:flr=on:random_seed=2888097945:cond=on:i=13220:s2at=3:aac=none:fsd=on_2853 on theBenchmark for (2853ds/13220Mi) % 164.37/24.07 % (581594)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 164.37/24.07 % (581594)------------------------------ % 164.37/24.07 % (581594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.37/24.07 % (581594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.37/24.07 % (581594)CaDiCaL version: 2.1.3 % 164.37/24.07 % (581594)Termination reason: Unknown % 164.37/24.07 % (581594)Termination phase: Saturation % 164.37/24.07 % (581594)Time elapsed: 0.193 s % 164.37/24.07 % (581594)Peak memory usage: 113 MB % 164.37/24.07 % (581594)Instructions burned: 543 (million) % 164.37/24.07 % (581597)lrs-1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:spb=goal:urr=on:newcnf=on:random_seed=193209943:st=5:i=13528:sd=2:kws=inv_frequency:gtg=exists_top:ss=axioms_2850 on theBenchmark for (2850ds/13528Mi) % 164.37/24.07 % (581597)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 164.37/24.07 % (581597)------------------------------ % 164.37/24.07 % (581597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.37/24.07 % (581597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.37/24.07 % (581597)CaDiCaL version: 2.1.3 % 164.37/24.07 % (581597)Termination reason: Unknown % 164.37/24.07 % (581597)Termination phase: Saturation % 164.37/24.07 % (581597)Time elapsed: 0.207 s % 164.37/24.07 % (581597)Peak memory usage: 114 MB % 164.37/24.07 % (581597)Instructions burned: 544 (million) % 164.37/24.07 % (581607)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=2467671102:st=6:i=14854:ep=RS:nm=2:av=off:gtg=exists_all:ss=included_2846 on theBenchmark for (2846ds/14854Mi) % 164.37/24.07 % (581607)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 164.37/24.07 % (581607)------------------------------ % 164.37/24.07 % (581607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.37/24.07 % (581607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.37/24.07 % (581607)CaDiCaL version: 2.1.3 % 164.37/24.07 % (581607)Termination reason: Unknown % 164.37/24.07 % (581607)Termination phase: Saturation % 164.37/24.07 % (581607)Time elapsed: 0.270 s % 164.37/24.07 % (581607)Peak memory usage: 114 MB % 164.37/24.07 % (581607)Instructions burned: 551 (million) % 164.37/24.07 % (581620)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:spb=goal_then_units:random_seed=185376489:i=14974:ss=axioms:sgt=16_2841 on theBenchmark for (2841ds/14974Mi) % 164.37/24.07 % (581620)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 164.37/24.07 % (581620)------------------------------ % 164.37/24.07 % (581620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 164.37/24.07 % (581620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 164.37/24.07 % (581620)CaDiCaL version: 2.1.3 % 164.37/24.07 % (581620)Termination reason: Unknown % 164.37/24.07 % (581620)Termination phase: Saturation % 164.37/24.07 % (581620)Time elapsed: 0.298 s % 164.37/24.07 % (581620)Peak memory usage: 113 MB % 164.37/24.07 % (581620)Instructions burned: 543 (million) % 164.37/24.07 % (581634)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=4007413078:i=33081:aac=none:fgj=on:bd=all:fsr=off_2837 on theBenchmark for (2837ds/33081Mi) % 182.80/26.71 % (581341)Instruction limit reached! % 182.80/26.71 % (581341)------------------------------ % 182.80/26.71 % (581341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.80/26.71 % (581341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.80/26.71 % (581341)CaDiCaL version: 2.1.3 % 182.80/26.71 % (581341)Termination reason: Instruction limit % 182.80/26.71 % (581341)Termination phase: Saturation % 182.80/26.71 % (581341)Time elapsed: 4.992 s % 182.80/26.71 % (581341)Peak memory usage: 151 MB % 182.80/26.71 % (581341)Instructions burned: 7144 (million) % 182.80/26.71 % (581634)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 182.80/26.71 % (581634)------------------------------ % 182.80/26.71 % (581634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.80/26.71 % (581634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.80/26.71 % (581634)CaDiCaL version: 2.1.3 % 182.80/26.71 % (581634)Termination reason: Unknown % 182.80/26.71 % (581634)Termination phase: Saturation % 182.80/26.71 % (581634)Time elapsed: 0.288 s % 182.80/26.71 % (581634)Peak memory usage: 113 MB % 182.80/26.71 % (581634)Instructions burned: 543 (million) % 182.80/26.71 % (581646)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=165927338:i=50856:s2at=6:kws=arity:bd=preordered:nm=0:er=filter_2833 on theBenchmark for (2833ds/50856Mi) % 182.80/26.71 % (581650)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=3987276765:i=69865_2832 on theBenchmark for (2832ds/69865Mi) % 182.80/26.71 % (581650)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 182.80/26.71 % (581650)------------------------------ % 182.80/26.71 % (581650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.80/26.71 % (581650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.80/26.71 % (581650)CaDiCaL version: 2.1.3 % 182.80/26.71 % (581650)Termination reason: Unknown % 182.80/26.71 % (581650)Termination phase: Saturation % 182.80/26.71 % (581650)Time elapsed: 0.303 s % 182.80/26.71 % (581650)Peak memory usage: 113 MB % 182.80/26.71 % (581650)Instructions burned: 542 (million) % 182.80/26.71 % (581646)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 182.80/26.71 % (581646)------------------------------ % 182.80/26.71 % (581646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.80/26.71 % (581646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.80/26.71 % (581646)CaDiCaL version: 2.1.3 % 182.80/26.71 % (581646)Termination reason: Unknown % 182.80/26.71 % (581646)Termination phase: Saturation % 182.80/26.71 % (581646)Time elapsed: 0.558 s % 182.80/26.71 % (581646)Peak memory usage: 114 MB % 182.80/26.71 % (581646)Instructions burned: 542 (million) % 182.80/26.71 % (581664)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=1079235248:cond=fast:i=17802:gtgl=3:gtg=all_2827 on theBenchmark for (2827ds/17802Mi) % 182.80/26.71 % (581669)lrs+10_1_sil=128000:sas=cadical:urr=on:br=off:random_seed=807509748:i=96644_2825 on theBenchmark for (2825ds/96644Mi) % 182.80/26.71 % (581664)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 182.80/26.71 % (581664)------------------------------ % 182.80/26.71 % (581664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.80/26.71 % (581664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.80/26.71 % (581664)CaDiCaL version: 2.1.3 % 182.80/26.71 % (581664)Termination reason: Unknown % 182.80/26.71 % (581664)Termination phase: Saturation % 182.80/26.71 % (581664)Time elapsed: 0.269 s % 182.80/26.71 % (581664)Peak memory usage: 113 MB % 182.80/26.71 % (581664)Instructions burned: 545 (million) % 182.80/26.71 % (581352)Instruction limit reached! % 182.80/26.71 % (581352)------------------------------ % 182.80/26.71 % (581352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 182.80/26.71 % (581352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 182.80/26.71 % (581352)CaDiCaL version: 2.1.3 % 182.80/26.71 % (581352)Termination reason: Instruction limit % 182.80/26.71 % (581352)Termination phase: Saturation % 194.96/28.59 % (581352)Time elapsed: 5.426 s % 194.96/28.59 % (581352)Peak memory usage: 122 MB % 194.96/28.59 % (581352)Instructions burned: 8140 (million) % 194.96/28.59 % (581680)WARNING Broken Constraint: if extensionality_resolution(known) has been set then inequality_splitting(9) is equal to 0 % 194.96/28.59 % (581680)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=2925458000:cond=fast:i=21161:kws=arity_squared:bd=preordered:nm=16:ins=9:er=known_2822 on theBenchmark for (2822ds/21161Mi) % 194.96/28.59 % (581681)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=2754882463:i=22761:gtg=all:ss=axioms:fsd=on_2821 on theBenchmark for (2821ds/22761Mi) % 194.96/28.59 % (581681)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 194.96/28.59 % (581681)------------------------------ % 194.96/28.59 % (581681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.96/28.59 % (581681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.96/28.59 % (581681)CaDiCaL version: 2.1.3 % 194.96/28.59 % (581681)Termination reason: Unknown % 194.96/28.59 % (581681)Termination phase: Saturation % 194.96/28.59 % (581681)Time elapsed: 0.557 s % 194.96/28.59 % (581681)Peak memory usage: 113 MB % 194.96/28.59 % (581681)Instructions burned: 545 (million) % 194.96/28.59 % (581702)dis-1011_7_sil=128000:fde=none:erd=off:fd=off:nwc=1:random_seed=3862412532:st=2:s2a=on:i=23713:s2at=2:sd=4:sup=off:ss=axioms_2813 on theBenchmark for (2813ds/23713Mi) % 194.96/28.59 % (581702)Refutation not found, incomplete strategy % 194.96/28.59 % (581702)------------------------------ % 194.96/28.59 % (581702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.96/28.59 % (581702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.96/28.59 % (581702)CaDiCaL version: 2.1.3 % 194.96/28.59 % (581702)Termination reason: Refutation not found, incomplete strategy % 194.96/28.59 % (581702)Time elapsed: 0.008 s % 194.96/28.59 % (581702)Peak memory usage: 88 MB % 194.96/28.59 % (581702)Instructions burned: 6 (million) % 194.96/28.59 % (581702)------------------------------ % 194.96/28.59 % (581702)------------------------------ % 194.96/28.59 % (581713)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=unary_first:kmz=on:random_seed=3709883465:i=26509:kws=inv_arity:fgj=on:bd=preordered:av=off_2806 on theBenchmark for (2806ds/26509Mi) % 194.96/28.59 % (581713)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 194.96/28.59 % (581713)------------------------------ % 194.96/28.59 % (581713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.96/28.59 % (581713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.96/28.59 % (581713)CaDiCaL version: 2.1.3 % 194.96/28.59 % (581713)Termination reason: Unknown % 194.96/28.59 % (581713)Termination phase: Saturation % 194.96/28.59 % (581713)Time elapsed: 0.527 s % 194.96/28.59 % (581713)Peak memory usage: 113 MB % 194.96/28.59 % (581713)Instructions burned: 542 (million) % 194.96/28.59 % (581725)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=911122951:i=28957:kws=inv_frequency:add=on:fgj=on:bs=on:bd=all:er=known_2798 on theBenchmark for (2798ds/28957Mi) % 194.96/28.59 % (581243)Instruction limit reached! % 194.96/28.59 % (581243)------------------------------ % 194.96/28.59 % (581243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 194.96/28.59 % (581243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 194.96/28.59 % (581243)CaDiCaL version: 2.1.3 % 194.96/28.59 % (581243)Termination reason: Instruction limit % 194.96/28.59 % (581243)Termination phase: Saturation % 194.96/28.59 % (581243)Time elapsed: 16.722 s % 194.96/28.59 % (581243)Peak memory usage: 329 MB % 194.96/28.59 % (581243)Instructions burned: 26473 (million) % 194.96/28.59 % (581748)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=1320357710:i=29246:s2at=-1:kws=inv_arity:ins=10_2776 on theBenchmark for (2776ds/29246Mi) % 194.96/28.59 % (581748)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 194.96/28.59 % (581748)------------------------------ % 194.96/28.59 % (581748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.04/30.06 % (581748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.04/30.06 % (581748)CaDiCaL version: 2.1.3 % 207.04/30.06 % (581748)Termination reason: Unknown % 207.04/30.06 % (581748)Termination phase: Saturation % 207.04/30.06 % (581748)Time elapsed: 0.593 s % 207.04/30.06 % (581748)Peak memory usage: 114 MB % 207.04/30.06 % (581748)Instructions burned: 543 (million) % 207.04/30.06 % (581758)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=2146721735:cond=on:i=30082:s2at=6:kws=inv_precedence:aac=none:ins=10:gsp=on_2767 on theBenchmark for (2767ds/30082Mi) % 207.04/30.06 % (581758)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 207.04/30.06 % (581758)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.04/30.06 % (581758)------------------------------ % 207.04/30.06 % (581758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.04/30.06 % (581758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.04/30.06 % (581758)CaDiCaL version: 2.1.3 % 207.04/30.06 % (581758)Termination reason: Unknown % 207.04/30.06 % (581758)Termination phase: Saturation % 207.04/30.06 % (581758)Time elapsed: 0.605 s % 207.04/30.06 % (581758)Peak memory usage: 114 MB % 207.04/30.06 % (581758)Instructions burned: 548 (million) % 207.04/30.06 % (581769)lrs+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:fd=preordered:random_seed=93753432:i=32262:bd=preordered_2759 on theBenchmark for (2759ds/32262Mi) % 207.04/30.06 % (581349)Instruction limit reached! % 207.04/30.06 % (581349)------------------------------ % 207.04/30.06 % (581349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.04/30.06 % (581349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.04/30.06 % (581349)CaDiCaL version: 2.1.3 % 207.04/30.06 % (581349)Termination reason: Instruction limit % 207.04/30.06 % (581349)Termination phase: Saturation % 207.04/30.06 % (581349)Time elapsed: 12.498 s % 207.04/30.06 % (581349)Peak memory usage: 213 MB % 207.04/30.06 % (581349)Instructions burned: 15999 (million) % 207.04/30.06 % (581769)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.04/30.06 % (581769)------------------------------ % 207.04/30.06 % (581769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.04/30.06 % (581769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.04/30.06 % (581769)CaDiCaL version: 2.1.3 % 207.04/30.06 % (581769)Termination reason: Unknown % 207.04/30.06 % (581769)Termination phase: Saturation % 207.04/30.06 % (581769)Time elapsed: 0.599 s % 207.04/30.06 % (581769)Peak memory usage: 113 MB % 207.04/30.06 % (581769)Instructions burned: 543 (million) % 207.04/30.06 % (581776)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:random_seed=141972566:i=32870:sd=4:fgj=on:ss=axioms:sgt=128_2753 on theBenchmark for (2753ds/32870Mi) % 207.04/30.06 % (581780)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=1187840615:i=33295:kws=precedence:fgj=on:bd=preordered:ins=1_2750 on theBenchmark for (2750ds/33295Mi) % 207.04/30.06 % (581776)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 207.04/30.06 % (581776)------------------------------ % 207.04/30.06 % (581776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.04/30.06 % (581776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.04/30.06 % (581776)CaDiCaL version: 2.1.3 % 207.04/30.06 % (581776)Termination reason: Unknown % 207.04/30.06 % (581776)Termination phase: Saturation % 207.04/30.06 % (581776)Time elapsed: 0.586 s % 207.04/30.06 % (581776)Peak memory usage: 113 MB % 207.04/30.06 % (581776)Instructions burned: 543 (million) % 207.04/30.06 % (581580)Instruction limit reached! % 207.04/30.06 % (581580)------------------------------ % 207.04/30.06 % (581580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 207.04/30.06 % (581580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 207.04/30.06 % (581580)CaDiCaL version: 2.1.3 % 207.04/30.06 % (581580)Termination reason: Instruction limit % 207.04/30.06 % (581580)Termination phase: Saturation % 207.04/30.06 % (581580)Time elapsed: 10.993 s % 207.04/30.06 % (581580)Peak memory usage: 153 MB % 207.04/30.06 % (581580)Instructions burned: 11103 (million) % 207.04/30.06 % (581787)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=3660815532:s2a=on:i=36826:kws=arity_squared:fgj=on:bd=preordered:nm=32:gtg=position_2744 on theBenchmark for (2744ds/36826Mi) % 211.73/30.88 % (581780)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.73/30.88 % (581780)------------------------------ % 211.73/30.88 % (581780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.88 % (581780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.88 % (581780)CaDiCaL version: 2.1.3 % 211.73/30.88 % (581780)Termination reason: Unknown % 211.73/30.88 % (581780)Termination phase: Saturation % 211.73/30.88 % (581780)Time elapsed: 0.599 s % 211.73/30.88 % (581780)Peak memory usage: 114 MB % 211.73/30.88 % (581780)Instructions burned: 544 (million) % 211.73/30.88 % (581789)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=1647673335:st=2:i=92981:kws=inv_arity:fgj=on:ins=2:ss=axioms_2743 on theBenchmark for (2743ds/92981Mi) % 211.73/30.88 % (581793)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=64000:npcc=on:bsr=unit_only:random_seed=3811604090:s2pl=on:i=49423_2741 on theBenchmark for (2741ds/49423Mi) % 211.73/30.88 % (581789)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.73/30.88 % (581789)------------------------------ % 211.73/30.88 % (581789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.88 % (581789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.88 % (581789)CaDiCaL version: 2.1.3 % 211.73/30.88 % (581789)Termination reason: Unknown % 211.73/30.88 % (581789)Termination phase: Saturation % 211.73/30.88 % (581789)Time elapsed: 0.598 s % 211.73/30.88 % (581789)Peak memory usage: 114 MB % 211.73/30.88 % (581789)Instructions burned: 542 (million) % 211.73/30.88 % (581793)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.73/30.88 % (581793)------------------------------ % 211.73/30.88 % (581793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.88 % (581793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.88 % (581793)CaDiCaL version: 2.1.3 % 211.73/30.88 % (581793)Termination reason: Unknown % 211.73/30.88 % (581793)Termination phase: Saturation % 211.73/30.88 % (581793)Time elapsed: 0.592 s % 211.73/30.88 % (581793)Peak memory usage: 113 MB % 211.73/30.88 % (581793)Instructions burned: 544 (million) % 211.73/30.88 % (581802)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=2236460999:st=3:prac=on:i=57299:s2at=6:sd=10:add=on:ss=axioms_2734 on theBenchmark for (2734ds/57299Mi) % 211.73/30.88 % (581805)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=82753130:i=127679:s2at=3:bs=on:bd=preordered:fsd=on_2732 on theBenchmark for (2732ds/127679Mi) % 211.73/30.88 % (581802)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.73/30.88 % (581802)------------------------------ % 211.73/30.88 % (581802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.88 % (581802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.88 % (581802)CaDiCaL version: 2.1.3 % 211.73/30.88 % (581802)Termination reason: Unknown % 211.73/30.88 % (581802)Termination phase: Saturation % 211.73/30.88 % (581802)Time elapsed: 0.603 s % 211.73/30.88 % (581802)Peak memory usage: 113 MB % 211.73/30.88 % (581802)Instructions burned: 543 (million) % 211.73/30.88 % (581805)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 211.73/30.88 % (581805)------------------------------ % 211.73/30.88 % (581805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.73/30.88 % (581805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.73/30.88 % (581805)CaDiCaL version: 2.1.3 % 211.73/30.88 % (581805)Termination reason: Unknown % 211.73/30.88 % (581805)Termination phase: Saturation % 211.73/30.88 % (581805)Time elapsed: 0.549 s % 211.73/30.88 % (581805)Peak memory usage: 114 MB % 211.73/30.88 % (581805)Instructions burned: 543 (million) % 211.73/30.88 % (581814)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=3229857276:i=69402:add=on:aac=none:fsr=off_2725 on theBenchmark for (2725ds/69402Mi) % 221.19/32.08 % (581817)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=1939837402:i=100512:doe=on:fgj=on:bd=all:fsd=on_2723 on theBenchmark for (2723ds/100512Mi) % 221.19/32.08 % (581680)Instruction limit reached! % 221.19/32.08 % (581680)------------------------------ % 221.19/32.08 % (581680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.19/32.08 % (581680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.19/32.08 % (581680)CaDiCaL version: 2.1.3 % 221.19/32.08 % (581680)Termination reason: Instruction limit % 221.19/32.08 % (581680)Termination phase: Saturation % 221.19/32.08 % (581680)Time elapsed: 10.179 s % 221.19/32.08 % (581680)Peak memory usage: 241 MB % 221.19/32.08 % (581680)Instructions burned: 21162 (million) % 221.19/32.08 % (581814)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.19/32.08 % (581814)------------------------------ % 221.19/32.08 % (581814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.19/32.08 % (581814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.19/32.08 % (581814)CaDiCaL version: 2.1.3 % 221.19/32.08 % (581814)Termination reason: Unknown % 221.19/32.08 % (581814)Termination phase: Saturation % 221.19/32.08 % (581814)Time elapsed: 0.605 s % 221.19/32.08 % (581814)Peak memory usage: 113 MB % 221.19/32.08 % (581814)Instructions burned: 542 (million) % 221.19/32.08 % (581825)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=1482003462:i=138761:kws=inv_arity_squared:fgj=on:bd=preordered_2718 on theBenchmark for (2718ds/138761Mi) % 221.19/32.08 % (581817)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.19/32.08 % (581817)------------------------------ % 221.19/32.08 % (581817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.19/32.08 % (581817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.19/32.08 % (581817)CaDiCaL version: 2.1.3 % 221.19/32.08 % (581817)Termination reason: Unknown % 221.19/32.08 % (581817)Termination phase: Saturation % 221.19/32.08 % (581817)Time elapsed: 0.550 s % 221.19/32.08 % (581817)Peak memory usage: 113 MB % 221.19/32.08 % (581817)Instructions burned: 542 (million) % 221.19/32.08 % (581827)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=2549688944:i=282386:rtra=on_2716 on theBenchmark for (2716ds/282386Mi) % 221.19/32.08 % (581825)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.19/32.08 % (581825)------------------------------ % 221.19/32.08 % (581825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.19/32.08 % (581825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.19/32.08 % (581825)CaDiCaL version: 2.1.3 % 221.19/32.08 % (581825)Termination reason: Unknown % 221.19/32.08 % (581825)Termination phase: Saturation % 221.19/32.08 % (581825)Time elapsed: 0.318 s % 221.19/32.08 % (581825)Peak memory usage: 113 MB % 221.19/32.08 % (581825)Instructions burned: 543 (million) % 221.19/32.08 % (581830)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=1132256123:i=269354:sd=20:aac=none:nm=16:rtra=on:ss=included:sgt=10_2715 on theBenchmark for (2715ds/269354Mi) % 221.19/32.08 % (581835)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=993210003:i=283390:sd=1:nm=32:rtra=on:gsp=on:ss=included_2713 on theBenchmark for (2713ds/283390Mi) % 221.19/32.08 % (581835)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 221.19/32.08 % (581827)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 221.19/32.08 % (581827)------------------------------ % 221.19/32.08 % (581827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 221.19/32.08 % (581827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 221.19/32.08 % (581827)CaDiCaL version: 2.1.3 % 221.19/32.08 % (581827)Termination reason: Unknown % 221.19/32.08 % (581827)Termination phase: Saturation % 221.19/32.08 % (581827)Time elapsed: 0.603 s % 230.08/33.56 % (581827)Peak memory usage: 113 MB % 230.08/33.56 % (581827)Instructions burned: 543 (million) % 230.08/33.56 % (581835)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 230.08/33.56 % (581835)------------------------------ % 230.08/33.56 % (581835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.08/33.56 % (581835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.56 % (581835)CaDiCaL version: 2.1.3 % 230.08/33.56 % (581835)Termination reason: Unknown % 230.08/33.56 % (581835)Termination phase: Saturation % 230.08/33.56 % (581835)Time elapsed: 0.313 s % 230.08/33.56 % (581835)Peak memory usage: 113 MB % 230.08/33.56 % (581835)Instructions burned: 543 (million) % 230.08/33.56 % (581830)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 230.08/33.56 % (581830)------------------------------ % 230.08/33.56 % (581830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.08/33.56 % (581830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.56 % (581830)CaDiCaL version: 2.1.3 % 230.08/33.56 % (581830)Termination reason: Unknown % 230.08/33.56 % (581830)Termination phase: Saturation % 230.08/33.56 % (581830)Time elapsed: 0.544 s % 230.08/33.56 % (581830)Peak memory usage: 114 MB % 230.08/33.56 % (581830)Instructions burned: 546 (million) % 230.08/33.56 % (581845)dis-1010_2:3_sil=16000:si=on:sp=reverse_frequency:random_seed=1362439935:i=238:av=off:rtra=on:ss=axioms_2707 on theBenchmark for (2707ds/238Mi) % 230.08/33.56 % (581843)lrs+1010_1_to=lpo:sil=32000:si=on:sos=on:spb=goal_then_units:bce=on:random_seed=2749829416:i=218:sd=1:ins=1:rtra=on:gsp=on:ss=axioms_2707 on theBenchmark for (2707ds/218Mi) % 230.08/33.56 % (581843)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 230.08/33.56 % (581843)Refutation not found, incomplete strategy % 230.08/33.56 % (581843)------------------------------ % 230.08/33.56 % (581843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.08/33.56 % (581843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.56 % (581843)CaDiCaL version: 2.1.3 % 230.08/33.56 % (581843)Termination reason: Refutation not found, incomplete strategy % 230.08/33.56 % (581843)Time elapsed: 0.008 s % 230.08/33.56 % (581843)Peak memory usage: 88 MB % 230.08/33.56 % (581843)Instructions burned: 6 (million) % 230.08/33.56 % (581846)dis-1011_1_sil=16000:fde=unused:si=on:s2agt=70:random_seed=771951198:s2a=on:i=278:rtra=on:gtg=position_2707 on theBenchmark for (2707ds/278Mi) % 230.08/33.56 % (581845)Instruction limit reached! % 230.08/33.56 % (581845)------------------------------ % 230.08/33.56 % (581845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.08/33.56 % (581845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.56 % (581845)CaDiCaL version: 2.1.3 % 230.08/33.56 % (581845)Termination reason: Instruction limit % 230.08/33.56 % (581845)Termination phase: Saturation % 230.08/33.56 % (581845)Time elapsed: 0.113 s % 230.08/33.56 % (581845)Peak memory usage: 90 MB % 230.08/33.56 % (581845)Instructions burned: 239 (million) % 230.08/33.56 % (581846)Instruction limit reached! % 230.08/33.56 % (581846)------------------------------ % 230.08/33.56 % (581846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.08/33.56 % (581846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.56 % (581846)CaDiCaL version: 2.1.3 % 230.08/33.56 % (581846)Termination reason: Instruction limit % 230.08/33.56 % (581846)Termination phase: Saturation % 230.08/33.56 % (581846)Time elapsed: 0.209 s % 230.08/33.56 % (581846)Peak memory usage: 91 MB % 230.08/33.56 % (581846)Instructions burned: 279 (million) % 230.08/33.56 % (581852)dis-21_1_sil=8000:si=on:lcm=predicate:random_seed=835100523:st=5:avsq=on:i=258:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:rtra=on:ss=included_2704 on theBenchmark for (2704ds/258Mi) % 230.08/33.56 % (581852)Refutation not found, incomplete strategy % 230.08/33.56 % (581852)------------------------------ % 230.08/33.56 % (581852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.08/33.56 % (581852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.08/33.56 % (581852)CaDiCaL version: 2.1.3 % 230.08/33.56 % (581852)Termination reason: Refutation not found, incomplete strategy % 230.08/33.56 % (581852)Time elapsed: 0.009 s % 230.08/33.56 % (581852)Peak memory usage: 88 MB % 230.08/33.56 % (581852)Instructions burned: 16 (million) % 230.08/33.56 % (581843)------------------------------ % 230.08/33.56 % (581843)------------------------------ % 230.08/33.56 % (581855)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=2771401816:i=570:sd=3:rtra=on:ss=axioms:sgt=8_2702 on theBenchmark for (2702ds/570Mi) % 237.77/34.48 % (581852)------------------------------ % 237.77/34.48 % (581852)------------------------------ % 237.77/34.48 % (581859)lrs+10_1_sil=32000:si=on:urr=on:br=off:random_seed=5183663:i=314:sd=1:rtra=on:gtg=position:ss=axioms:sgt=8_2701 on theBenchmark for (2701ds/314Mi) % 237.77/34.48 % (581862)lrs+1011_1_sil=32000:si=on:sp=occurrence:random_seed=3882547812:i=650:sd=1:rtra=on:ss=axioms:sgt=32_2699 on theBenchmark for (2699ds/650Mi) % 237.77/34.48 % (581859)Instruction limit reached! % 237.77/34.48 % (581859)------------------------------ % 237.77/34.48 % (581859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.77/34.48 % (581859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.77/34.48 % (581859)CaDiCaL version: 2.1.3 % 237.77/34.48 % (581859)Termination reason: Instruction limit % 237.77/34.48 % (581859)Termination phase: Saturation % 237.77/34.48 % (581859)Time elapsed: 0.303 s % 237.77/34.48 % (581859)Peak memory usage: 91 MB % 237.77/34.48 % (581859)Instructions burned: 315 (million) % 237.77/34.48 % (581855)Instruction limit reached! % 237.77/34.48 % (581855)------------------------------ % 237.77/34.48 % (581855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.77/34.48 % (581855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.77/34.48 % (581855)CaDiCaL version: 2.1.3 % 237.77/34.48 % (581855)Termination reason: Instruction limit % 237.77/34.48 % (581855)Termination phase: Saturation % 237.77/34.48 % (581855)Time elapsed: 0.519 s % 237.77/34.48 % (581855)Peak memory usage: 93 MB % 237.77/34.48 % (581855)Instructions burned: 571 (million) % 237.77/34.48 % (581862)Instruction limit reached! % 237.77/34.48 % (581862)------------------------------ % 237.77/34.48 % (581862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.77/34.48 % (581862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.77/34.48 % (581862)CaDiCaL version: 2.1.3 % 237.77/34.48 % (581862)Termination reason: Instruction limit % 237.77/34.48 % (581862)Termination phase: Saturation % 237.77/34.48 % (581862)Time elapsed: 0.331 s % 237.77/34.48 % (581862)Peak memory usage: 94 MB % 237.77/34.48 % (581862)Instructions burned: 651 (million) % 237.77/34.48 % (581868)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=1294693388:s2a=on:i=496:s2at=1.23:rtra=on:gtg=position_2695 on theBenchmark for (2695ds/496Mi) % 237.77/34.48 % (581871)lrs+1002_1_to=lpo:sil=8000:si=on:sos=on:random_seed=1641400326:st=4:cts=off:i=588:sd=2:ins=7:rtra=on:amm=off:ss=axioms_2694 on theBenchmark for (2694ds/588Mi) % 237.77/34.48 % (581872)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:si=on:random_seed=3671852886:i=4700:rtra=on_2694 on theBenchmark for (2694ds/4700Mi) % 237.77/34.48 % (581871)Refutation not found, incomplete strategy % 237.77/34.48 % (581871)------------------------------ % 237.77/34.48 % (581871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.77/34.48 % (581871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.77/34.48 % (581871)CaDiCaL version: 2.1.3 % 237.77/34.48 % (581871)Termination reason: Refutation not found, incomplete strategy % 237.77/34.48 % (581871)Time elapsed: 0.012 s % 237.77/34.48 % (581871)Peak memory usage: 88 MB % 237.77/34.48 % (581871)Instructions burned: 12 (million) % 237.77/34.48 % (581872)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 237.77/34.48 % (581872)------------------------------ % 237.77/34.48 % (581872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.77/34.48 % (581872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.77/34.48 % (581872)CaDiCaL version: 2.1.3 % 237.77/34.48 % (581872)Termination reason: Unknown % 237.77/34.48 % (581872)Termination phase: Saturation % 237.77/34.48 % (581872)Time elapsed: 0.316 s % 237.77/34.48 % (581872)Peak memory usage: 113 MB % 237.77/34.48 % (581872)Instructions burned: 543 (million) % 237.77/34.48 % (581871)------------------------------ % 237.77/34.48 % (581871)------------------------------ % 237.77/34.48 % (581868)Instruction limit reached! % 237.77/34.48 % (581868)------------------------------ % 237.77/34.48 % (581868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.77/34.48 % (581868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.77/34.48 % (581868)CaDiCaL version: 2.1.3 % 237.77/34.48 % (581868)Termination reason: Instruction limit % 237.77/34.48 % (581868)Termination phase: Saturation % 243.76/35.35 % (581868)Time elapsed: 0.468 s % 243.76/35.35 % (581868)Peak memory usage: 94 MB % 243.76/35.35 % (581868)Instructions burned: 497 (million) % 243.76/35.35 % (581880)dis-1011_32:1_sfv=off:sil=16000:si=on:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3041279279:cts=off:i=226:fsr=off:rtra=on:ss=included:sgt=4_2688 on theBenchmark for (2688ds/226Mi) % 243.76/35.35 % (581880)Instruction limit reached! % 243.76/35.35 % (581880)------------------------------ % 243.76/35.35 % (581880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.76/35.35 % (581880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.76/35.35 % (581880)CaDiCaL version: 2.1.3 % 243.76/35.35 % (581880)Termination reason: Instruction limit % 243.76/35.35 % (581880)Termination phase: Saturation % 243.76/35.35 % (581880)Time elapsed: 0.118 s % 243.76/35.35 % (581880)Peak memory usage: 92 MB % 243.76/35.35 % (581880)Instructions burned: 227 (million) % 243.76/35.35 % (581883)dis-1003_1024_sil=8000:si=on:sos=all:sac=on:random_seed=4151898382:cond=fast:i=228:sd=1:nm=0:fsr=off:rtra=on:gtg=exists_sym:ss=axioms_2687 on theBenchmark for (2687ds/228Mi) % 243.76/35.35 % (581882)lrs-1004_1_sil=8000:si=on:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1962435579:i=254:av=off:fsr=off:rtra=on:sup=off_2687 on theBenchmark for (2687ds/254Mi) % 243.76/35.35 % (581882)Refutation not found, incomplete strategy % 243.76/35.35 % (581882)------------------------------ % 243.76/35.35 % (581882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.76/35.35 % (581882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.76/35.35 % (581882)CaDiCaL version: 2.1.3 % 243.76/35.35 % (581882)Termination reason: Refutation not found, incomplete strategy % 243.76/35.35 % (581882)Time elapsed: 0.009 s % 243.76/35.35 % (581882)Peak memory usage: 88 MB % 243.76/35.35 % (581882)Instructions burned: 11 (million) % 243.76/35.35 % (581883)Instruction limit reached! % 243.76/35.35 % (581883)------------------------------ % 243.76/35.35 % (581883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.76/35.35 % (581883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.76/35.35 % (581883)CaDiCaL version: 2.1.3 % 243.76/35.35 % (581883)Termination reason: Instruction limit % 243.76/35.35 % (581883)Termination phase: Saturation % 243.76/35.35 % (581883)Time elapsed: 0.204 s % 243.76/35.35 % (581883)Peak memory usage: 89 MB % 243.76/35.35 % (581883)Instructions burned: 228 (million) % 243.76/35.35 % (581889)lrs+10_1_sil=8000:si=on:sp=occurrence:random_seed=775593013:st=1.2:i=1814:sd=14:rtra=on:ss=axioms:sgt=12_2685 on theBenchmark for (2685ds/1814Mi) % 243.76/35.35 % (581882)------------------------------ % 243.76/35.35 % (581882)------------------------------ % 243.76/35.35 % (581894)dis-1010_1_sil=16000:fde=unused:si=on:sp=occurrence:sos=on:random_seed=4226331953:i=874:sd=1:aac=none:rtra=on:ss=included_2683 on theBenchmark for (2683ds/874Mi) % 243.76/35.35 % (581894)Refutation not found, incomplete strategy % 243.76/35.35 % (581894)------------------------------ % 243.76/35.35 % (581894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.76/35.35 % (581894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.76/35.35 % (581894)CaDiCaL version: 2.1.3 % 243.76/35.35 % (581894)Termination reason: Refutation not found, incomplete strategy % 243.76/35.35 % (581894)Time elapsed: 0.011 s % 243.76/35.35 % (581894)Peak memory usage: 88 MB % 243.76/35.35 % (581894)Instructions burned: 9 (million) % 243.76/35.35 % (581897)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:si=on:random_seed=3708118161:i=10404:rtra=on:ss=axioms:sgt=16_2680 on theBenchmark for (2680ds/10404Mi) % 243.76/35.35 % (581894)------------------------------ % 243.76/35.35 % (581894)------------------------------ % 243.76/35.35 % (581889)Instruction limit reached! % 243.76/35.35 % (581889)------------------------------ % 243.76/35.35 % (581889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.76/35.35 % (581889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.76/35.35 % (581889)CaDiCaL version: 2.1.3 % 243.76/35.35 % (581889)Termination reason: Instruction limit % 243.76/35.35 % (581889)Termination phase: Saturation % 243.76/35.35 % (581889)Time elapsed: 0.932 s % 243.76/35.35 % (581889)Peak memory usage: 103 MB % 243.76/35.35 % (581889)Instructions burned: 1814 (million) % 243.76/35.35 % (581904)dis+10_3:1_sil=8000:si=on:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2364044284:i=268:sd=2:doe=on:nm=16:rtra=on:sup=off:ss=included_2676 on theBenchmark for (2676ds/268Mi) % 252.54/36.57 % (581897)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.54/36.57 % (581897)------------------------------ % 252.54/36.57 % (581897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.54/36.57 % (581897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.54/36.57 % (581897)CaDiCaL version: 2.1.3 % 252.54/36.57 % (581897)Termination reason: Unknown % 252.54/36.57 % (581897)Termination phase: Saturation % 252.54/36.57 % (581897)Time elapsed: 0.562 s % 252.54/36.57 % (581897)Peak memory usage: 114 MB % 252.54/36.57 % (581897)Instructions burned: 545 (million) % 252.54/36.57 % (581907)lrs+1002_8_sil=8000:si=on:sp=occurrence:sos=on:sac=on:random_seed=4216776860:st=8:i=1184:sd=3:ep=RST:rtra=on:ss=axioms_2673 on theBenchmark for (2673ds/1184Mi) % 252.54/36.57 % (581907)Refutation not found, incomplete strategy % 252.54/36.57 % (581907)------------------------------ % 252.54/36.57 % (581907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.54/36.57 % (581907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.54/36.57 % (581907)CaDiCaL version: 2.1.3 % 252.54/36.57 % (581907)Termination reason: Refutation not found, incomplete strategy % 252.54/36.57 % (581907)Time elapsed: 0.006 s % 252.54/36.57 % (581907)Peak memory usage: 88 MB % 252.54/36.57 % (581907)Instructions burned: 12 (million) % 252.54/36.57 % (581904)Instruction limit reached! % 252.54/36.57 % (581904)------------------------------ % 252.54/36.57 % (581904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.54/36.57 % (581904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.54/36.57 % (581904)CaDiCaL version: 2.1.3 % 252.54/36.57 % (581904)Termination reason: Instruction limit % 252.54/36.57 % (581904)Termination phase: Saturation % 252.54/36.57 % (581904)Time elapsed: 0.240 s % 252.54/36.57 % (581904)Peak memory usage: 90 MB % 252.54/36.57 % (581904)Instructions burned: 268 (million) % 252.54/36.57 % (581910)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:si=on:random_seed=3167488310:st=3:i=26386:sd=3:rtra=on:ss=axioms_2672 on theBenchmark for (2672ds/26386Mi) % 252.54/36.57 % (581907)------------------------------ % 252.54/36.57 % (581907)------------------------------ % 252.54/36.57 % (581914)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=793238224:i=250:slsql=off:bs=unit_only:rtra=on:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2670 on theBenchmark for (2670ds/250Mi) % 252.54/36.57 % (581914)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 252.54/36.57 % (581917)lrs+10_1024_to=lpo:sil=8000:tgt=full:si=on:sp=arity:slsq=on:random_seed=364659863:i=268:gtgl=5:slsql=off:rtra=on:gtg=exists_sym_2669 on theBenchmark for (2669ds/268Mi) % 252.54/36.57 % (581917)Instruction limit reached! % 252.54/36.57 % (581917)------------------------------ % 252.54/36.57 % (581917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.54/36.57 % (581917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.54/36.57 % (581917)CaDiCaL version: 2.1.3 % 252.54/36.57 % (581917)Termination reason: Instruction limit % 252.54/36.57 % (581917)Termination phase: Saturation % 252.54/36.57 % (581917)Time elapsed: 0.134 s % 252.54/36.57 % (581917)Peak memory usage: 91 MB % 252.54/36.57 % (581917)Instructions burned: 269 (million) % 252.54/36.57 % (581914)Instruction limit reached! % 252.54/36.57 % (581914)------------------------------ % 252.54/36.57 % (581914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.54/36.57 % (581914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.54/36.57 % (581914)CaDiCaL version: 2.1.3 % 252.54/36.57 % (581914)Termination reason: Instruction limit % 252.54/36.57 % (581914)Termination phase: Saturation % 252.54/36.57 % (581914)Time elapsed: 0.247 s % 252.54/36.57 % (581914)Peak memory usage: 92 MB % 252.54/36.57 % (581914)Instructions burned: 250 (million) % 252.54/36.57 % (581910)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 252.54/36.57 % (581910)------------------------------ % 252.54/36.57 % (581910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 252.54/36.57 % (581910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 252.54/36.57 % (581910)CaDiCaL version: 2.1.3 % 252.54/36.57 % (581910)Termination reason: Unknown % 252.54/36.57 % (581910)Termination phase: Saturation % 252.54/36.57 % (581910)Time elapsed: 0.557 s % 252.54/36.57 % (581910)Peak memory usage: 114 MB % 252.54/36.57 % (581910)Instructions burned: 542 (million) % 261.02/37.81 % (581924)lrs+10_1_sil=16000:plsq=on:plsqc=1:si=on:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1545984422:i=282:sd=1:rtra=on:gsp=on:sup=off:ss=axioms:sgt=8_2665 on theBenchmark for (2665ds/282Mi) % 261.02/37.81 % (581924)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 261.02/37.81 % (581924)Refutation not found, incomplete strategy % 261.02/37.81 % (581924)------------------------------ % 261.02/37.81 % (581924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.02/37.81 % (581924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.02/37.81 % (581924)CaDiCaL version: 2.1.3 % 261.02/37.81 % (581924)Termination reason: Refutation not found, incomplete strategy % 261.02/37.81 % (581924)Time elapsed: 0.004 s % 261.02/37.81 % (581924)Peak memory usage: 88 MB % 261.02/37.81 % (581924)Instructions burned: 5 (million) % 261.02/37.81 % (581925)lrs+1011_1_sil=8000:plsq=on:si=on:sp=occurrence:fs=off:random_seed=2781464291:i=862:sd=1:fsr=off:rtra=on:sup=off:ss=axioms:sgt=64_2665 on theBenchmark for (2665ds/862Mi) % 261.02/37.81 % (581925)Refutation not found, incomplete strategy % 261.02/37.81 % (581925)------------------------------ % 261.02/37.81 % (581925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.02/37.81 % (581925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.02/37.81 % (581925)CaDiCaL version: 2.1.3 % 261.02/37.81 % (581925)Termination reason: Refutation not found, incomplete strategy % 261.02/37.81 % (581925)Time elapsed: 0.007 s % 261.02/37.81 % (581925)Peak memory usage: 88 MB % 261.02/37.81 % (581925)Instructions burned: 12 (million) % 261.02/37.81 % (581927)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:si=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=898897389:i=12120:aac=none:ins=25:rtra=on_2663 on theBenchmark for (2663ds/12120Mi) % 261.02/37.81 % (581924)------------------------------ % 261.02/37.81 % (581924)------------------------------ % 261.02/37.81 % (581925)------------------------------ % 261.02/37.81 % (581925)------------------------------ % 261.02/37.81 % (581935)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:si=on:sp=arity:urr=on:random_seed=2290352237:i=28310:bd=all:rtra=on_2660 on theBenchmark for (2660ds/28310Mi) % 261.02/37.81 % (581934)lrs+10_16_anc=all:slsqr=32,1:sil=8000:si=on:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2731816799:avsq=on:s2a=on:i=300:kws=precedence:nicw=on:rtra=on:gsp=on:rawr=on_2660 on theBenchmark for (2660ds/300Mi) % 261.02/37.81 % (581934)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 261.02/37.81 % (581934)Instruction limit reached! % 261.02/37.81 % (581934)------------------------------ % 261.02/37.81 % (581934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.02/37.81 % (581934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.02/37.81 % (581934)CaDiCaL version: 2.1.3 % 261.02/37.81 % (581934)Termination reason: Instruction limit % 261.02/37.81 % (581934)Termination phase: Saturation % 261.02/37.81 % (581934)Time elapsed: 0.286 s % 261.02/37.81 % (581934)Peak memory usage: 92 MB % 261.02/37.81 % (581934)Instructions burned: 300 (million) % 261.02/37.81 % (581935)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.02/37.81 % (581935)------------------------------ % 261.02/37.81 % (581935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.02/37.81 % (581935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.02/37.81 % (581935)CaDiCaL version: 2.1.3 % 261.02/37.81 % (581935)Termination reason: Unknown % 261.02/37.81 % (581935)Termination phase: Saturation % 261.02/37.81 % (581935)Time elapsed: 0.312 s % 261.02/37.81 % (581935)Peak memory usage: 114 MB % 261.02/37.81 % (581935)Instructions burned: 543 (million) % 261.02/37.81 % (581927)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 261.02/37.81 % (581927)------------------------------ % 261.02/37.81 % (581927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 261.02/37.81 % (581927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 261.02/37.81 % (581927)CaDiCaL version: 2.1.3 % 261.02/37.81 % (581927)Termination reason: Unknown % 261.02/37.81 % (581927)Termination phase: Saturation % 261.02/37.81 % (581927)Time elapsed: 0.578 s % 261.02/37.81 % (581927)Peak memory usage: 114 MB % 261.02/37.81 % (581927)Instructions burned: 543 (million) % 277.71/40.13 % (581942)lrs+10_1024_sil=16000:plsq=on:si=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=969561098:i=1334:av=off:fsr=off:rtra=on_2655 on theBenchmark for (2655ds/1334Mi) % 277.71/40.13 % (581942)Refutation not found, incomplete strategy % 277.71/40.13 % (581942)------------------------------ % 277.71/40.13 % (581942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.71/40.13 % (581942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.71/40.13 % (581942)CaDiCaL version: 2.1.3 % 277.71/40.13 % (581942)Termination reason: Refutation not found, incomplete strategy % 277.71/40.13 % (581942)Time elapsed: 0.010 s % 277.71/40.13 % (581942)Peak memory usage: 88 MB % 277.71/40.13 % (581942)Instructions burned: 11 (million) % 277.71/40.13 % (581943)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:si=on:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1775321318:s2a=on:i=370:s2at=1.8:rtra=on:fdi=4_2655 on theBenchmark for (2655ds/370Mi) % 277.71/40.13 % (581946)dis+1010_14_anc=all:to=lpo:sil=8000:si=on:sp=arity:slsq=on:random_seed=2485328382:i=386:ins=10:fsr=off:rtra=on:ss=axioms:fsd=on_2654 on theBenchmark for (2654ds/386Mi) % 277.71/40.13 % (581946)Instruction limit reached! % 277.71/40.13 % (581946)------------------------------ % 277.71/40.13 % (581946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.71/40.13 % (581946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.71/40.13 % (581946)CaDiCaL version: 2.1.3 % 277.71/40.13 % (581946)Termination reason: Instruction limit % 277.71/40.13 % (581946)Termination phase: Saturation % 277.71/40.13 % (581946)Time elapsed: 0.198 s % 277.71/40.13 % (581946)Peak memory usage: 92 MB % 277.71/40.13 % (581946)Instructions burned: 387 (million) % 277.71/40.13 % (581943)Instruction limit reached! % 277.71/40.13 % (581943)------------------------------ % 277.71/40.13 % (581943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.71/40.13 % (581943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.71/40.13 % (581943)CaDiCaL version: 2.1.3 % 277.71/40.13 % (581943)Termination reason: Instruction limit % 277.71/40.13 % (581943)Termination phase: Saturation % 277.71/40.13 % (581943)Time elapsed: 0.287 s % 277.71/40.13 % (581943)Peak memory usage: 92 MB % 277.71/40.13 % (581943)Instructions burned: 370 (million) % 277.71/40.13 % (581942)------------------------------ % 277.71/40.13 % (581942)------------------------------ % 277.71/40.13 % (581955)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:si=on:sp=const_frequency:acc=on:urr=on:random_seed=442240970:i=24222:sd=1:rtra=on:ss=included_2650 on theBenchmark for (2650ds/24222Mi) % 277.71/40.13 % (581954)dis+1011_7_sil=8000:si=on:sp=occurrence:sos=all:fd=off:random_seed=545171857:st=5.3:i=9700:sd=4:av=off:rtra=on:sup=off:ss=included:sgt=16_2650 on theBenchmark for (2650ds/9700Mi) % 277.71/40.13 % (581954)Refutation not found, incomplete strategy % 277.71/40.13 % (581954)------------------------------ % 277.71/40.13 % (581954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.71/40.13 % (581954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.71/40.13 % (581954)CaDiCaL version: 2.1.3 % 277.71/40.13 % (581954)Termination reason: Refutation not found, incomplete strategy % 277.71/40.13 % (581954)Time elapsed: 0.008 s % 277.71/40.13 % (581954)Peak memory usage: 87 MB % 277.71/40.13 % (581954)Instructions burned: 8 (million) % 277.71/40.13 % (581956)lrs-11_32_anc=all:sil=8000:si=on:spb=goal_then_units:sac=on:random_seed=2647453215:i=638:kws=precedence:fsr=off:rtra=on_2649 on theBenchmark for (2649ds/638Mi) % 277.71/40.13 % (581955)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 277.71/40.13 % (581955)------------------------------ % 277.71/40.13 % (581955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.71/40.13 % (581955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.71/40.13 % (581955)CaDiCaL version: 2.1.3 % 277.71/40.13 % (581955)Termination reason: Unknown % 277.71/40.13 % (581955)Termination phase: Saturation % 277.71/40.13 % (581955)Time elapsed: 0.315 s % 277.71/40.13 % (581955)Peak memory usage: 114 MB % 277.71/40.13 % (581955)Instructions burned: 544 (million) % 277.71/40.13 % (581954)------------------------------ % 277.71/40.13 % (581954)------------------------------ % 277.71/40.13 % (581963)dis+2_1024_sil=8000:si=on:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2359466443:i=4128:ep=RST:rtra=on_2645 on theBenchmark for (2645ds/4128Mi) % 300.60/43.33 % (581963)Refutation not found, incomplete strategy % 300.60/43.33 % (581963)------------------------------ % 300.60/43.33 % (581963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581963)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581963)Termination reason: Refutation not found, incomplete strategy % 300.60/43.33 % (581963)Time elapsed: 0.006 s % 300.60/43.33 % (581963)Peak memory usage: 88 MB % 300.60/43.33 % (581963)Instructions burned: 12 (million) % 300.60/43.33 % (581964)dis-1011_128_sil=32000:si=on:random_seed=653925991:i=7412:ep=RST:av=off:rtra=on_2644 on theBenchmark for (2644ds/7412Mi) % 300.60/43.33 % (581956)Instruction limit reached! % 300.60/43.33 % (581956)------------------------------ % 300.60/43.33 % (581956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581956)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581956)Termination reason: Instruction limit % 300.60/43.33 % (581956)Termination phase: Saturation % 300.60/43.33 % (581956)Time elapsed: 0.584 s % 300.60/43.33 % (581956)Peak memory usage: 97 MB % 300.60/43.33 % (581956)Instructions burned: 638 (million) % 300.60/43.33 % (581963)------------------------------ % 300.60/43.33 % (581963)------------------------------ % 300.60/43.33 % (581969)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:si=on:sp=occurrence:random_seed=1800548995:i=27826:rtra=on:ss=axioms:sgt=8_2640 on theBenchmark for (2640ds/27826Mi) % 300.60/43.33 % (581968)lrs-1002_1_sil=8000:plsq=on:si=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=706989823:i=1514:sd=2:fsr=off:rtra=on:ss=axioms:sgt=40_2641 on theBenchmark for (2641ds/1514Mi) % 300.60/43.33 % (581968)Refutation not found, incomplete strategy % 300.60/43.33 % (581968)------------------------------ % 300.60/43.33 % (581968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581968)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581968)Termination reason: Refutation not found, incomplete strategy % 300.60/43.33 % (581968)Time elapsed: 0.012 s % 300.60/43.33 % (581968)Peak memory usage: 89 MB % 300.60/43.33 % (581968)Instructions burned: 11 (million) % 300.60/43.33 % (581969)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.60/43.33 % (581969)------------------------------ % 300.60/43.33 % (581969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581969)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581969)Termination reason: Unknown % 300.60/43.33 % (581969)Termination phase: Saturation % 300.60/43.33 % (581969)Time elapsed: 0.326 s % 300.60/43.33 % (581969)Peak memory usage: 113 MB % 300.60/43.33 % (581969)Instructions burned: 542 (million) % 300.60/43.33 % (581968)------------------------------ % 300.60/43.33 % (581968)------------------------------ % 300.60/43.33 % (581976)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=const_frequency:sos=all:lma=off:random_seed=2410570576:i=19850:aac=none:rtra=on_2635 on theBenchmark for (2635ds/19850Mi) % 300.60/43.33 % (581977)dis-1010_50_to=lpo:sil=32000:si=on:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3063757320:i=4958:sd=2:nm=16:fsr=off:rtra=on:ss=axioms_2634 on theBenchmark for (2634ds/4958Mi) % 300.60/43.33 % (581977)Refutation not found, incomplete strategy % 300.60/43.33 % (581977)------------------------------ % 300.60/43.33 % (581977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581977)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581977)Termination reason: Refutation not found, incomplete strategy % 300.60/43.33 % (581977)Time elapsed: 0.012 s % 300.60/43.33 % (581977)Peak memory usage: 88 MB % 300.60/43.33 % (581977)Instructions burned: 11 (million) % 300.60/43.33 % (581976)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.60/43.33 % (581976)------------------------------ % 300.60/43.33 % (581976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581976)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581976)Termination reason: Unknown % 300.60/43.33 % (581976)Termination phase: Saturation % 300.60/43.33 % (581976)Time elapsed: 0.295 s % 300.60/43.33 % (581976)Peak memory usage: 113 MB % 300.60/43.33 % (581976)Instructions burned: 543 (million) % 300.60/43.33 % (581977)------------------------------ % 300.60/43.33 % (581977)------------------------------ % 300.60/43.33 % (581982)ott+1002_64_sil=16000:si=on:sp=const_min:nwc=0.5:random_seed=3603888270:i=880:nm=2:av=off:rtra=on:gtg=exists_all:fdi=8:gsp=on_2630 on theBenchmark for (2630ds/880Mi) % 300.60/43.33 % (581982)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs. % 300.60/43.33 % (581985)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:si=on:erd=off:lsd=100:bsr=unit_only:random_seed=4067003129:st=1.5:i=22290:s2at=3:sd=3:fsr=off:rtra=on:ss=axioms_2627 on theBenchmark for (2627ds/22290Mi) % 300.60/43.33 % (581982)Instruction limit reached! % 300.60/43.33 % (581982)------------------------------ % 300.60/43.33 % (581982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581982)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581982)Termination reason: Instruction limit % 300.60/43.33 % (581982)Termination phase: Saturation % 300.60/43.33 % (581982)Time elapsed: 0.452 s % 300.60/43.33 % (581982)Peak memory usage: 92 MB % 300.60/43.33 % (581982)Instructions burned: 881 (million) % 300.60/43.33 % (581985)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.60/43.33 % (581985)------------------------------ % 300.60/43.33 % (581985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581985)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581985)Termination reason: Unknown % 300.60/43.33 % (581985)Termination phase: Saturation % 300.60/43.33 % (581985)Time elapsed: 0.454 s % 300.60/43.33 % (581985)Peak memory usage: 114 MB % 300.60/43.33 % (581985)Instructions burned: 542 (million) % 300.60/43.33 % (581988)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:si=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4032296793:cts=off:i=6068:av=off:rtra=on:er=known:fsd=on_2623 on theBenchmark for (2623ds/6068Mi) % 300.60/43.33 % (581989)lrs-1011_64:1_sil=8000:si=on:erd=off:urr=on:nwc=0.7:br=off:random_seed=2432947047:st=2:s2a=on:i=1048:s2at=2:rtra=on:ss=axioms_2621 on theBenchmark for (2621ds/1048Mi) % 300.60/43.33 % (581988)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.60/43.33 % (581988)------------------------------ % 300.60/43.33 % (581988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581988)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581988)Termination reason: Unknown % 300.60/43.33 % (581988)Termination phase: Saturation % 300.60/43.33 % (581988)Time elapsed: 0.321 s % 300.60/43.33 % (581988)Peak memory usage: 113 MB % 300.60/43.33 % (581988)Instructions burned: 543 (million) % 300.60/43.33 % (581994)lrs+1011_16:1_sil=8000:si=on:acc=on:urr=on:fd=preordered:flr=on:random_seed=2929591109:avsq=on:i=2032:avsqr=676809,524288:sd=1:rtra=on:ss=axioms_2617 on theBenchmark for (2617ds/2032Mi) % 300.60/43.33 % (581989)Instruction limit reached! % 300.60/43.33 % (581989)------------------------------ % 300.60/43.33 % (581989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581989)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581989)Termination reason: Instruction limit % 300.60/43.33 % (581989)Termination phase: Saturation % 300.60/43.33 % (581989)Time elapsed: 0.624 s % 300.60/43.33 % (581989)Peak memory usage: 96 MB % 300.60/43.33 % (581989)Instructions burned: 1049 (million) % 300.60/43.33 % (581996)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:si=on:s2agt=16:random_seed=1375195096:i=28246:bd=preordered:ins=4:rtra=on_2612 on theBenchmark for (2612ds/28246Mi) % 300.60/43.33 % (581996)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p % 300.60/43.33 % (581996)------------------------------ % 300.60/43.33 % (581996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.60/43.33 % (581996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.60/43.33 % (581996)CaDiCaL version: 2.1.3 % 300.60/43.33 % (581996)Termination reason: Unknown % 300.60/43.33 % (581996)Termi % 300.60/43.34 Terminated %------------------------------------------------------------------------------