%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW274+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:00 PM UTC 2026 % Result : Timeout 287.66s 41.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW274+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.17 % Computer : n015.cluster.edu % 0.08/0.17 % Model : x86_64 x86_64 % 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.17 % Memory : 8046.5625MB % 0.08/0.17 % OS : Linux 6.8.0-71-generic % 0.08/0.17 % CPULimit : 300 % 0.08/0.17 % WCLimit : 300 % 0.08/0.17 % DateTime : Mon Sep 28 13:31:16 UTC 2026 % 0.08/0.17 % CPUTime : % 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 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 % 12.22/2.41 % (2627138)Detected formulas, will run a generic FOF schedule. % 12.22/2.41 % (2627147)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2834548753:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 12.22/2.41 % (2627147)Instruction limit reached! % 12.22/2.41 % (2627147)------------------------------ % 12.22/2.41 % (2627147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.22/2.41 % (2627147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.22/2.41 % (2627147)CaDiCaL version: 2.1.3 % 12.22/2.41 % (2627147)Termination reason: Instruction limit % 12.22/2.41 % (2627147)Termination phase: Saturation % 12.22/2.41 % (2627147)Time elapsed: 0.040 s % 12.22/2.41 % (2627147)Peak memory usage: 90 MB % 12.22/2.41 % (2627147)Instructions burned: 121 (million) % 12.22/2.41 % (2627143)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=205233593:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 12.22/2.41 % (2627146)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1322333092:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 12.22/2.41 % (2627145)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=2872771495:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 12.22/2.41 % (2627144)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=1793560627:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 12.22/2.41 % (2627148)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2218630012:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 12.22/2.41 % (2627149)dis-21_1_sil=8000:lcm=predicate:random_seed=1751586141: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) % 12.22/2.41 % (2627146)Refutation not found, incomplete strategy % 12.22/2.41 % (2627146)------------------------------ % 12.22/2.41 % (2627146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.22/2.41 % (2627146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.22/2.41 % (2627146)CaDiCaL version: 2.1.3 % 12.22/2.41 % (2627146)Termination reason: Refutation not found, incomplete strategy % 12.22/2.41 % (2627146)Time elapsed: 0.014 s % 12.22/2.41 % (2627146)Peak memory usage: 90 MB % 12.22/2.41 % (2627146)Instructions burned: 23 (million) % 12.22/2.41 % (2627149)Instruction limit reached! % 12.22/2.41 % (2627149)------------------------------ % 12.22/2.41 % (2627149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.22/2.41 % (2627149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.22/2.41 % (2627149)CaDiCaL version: 2.1.3 % 12.22/2.41 % (2627149)Termination reason: Instruction limit % 12.22/2.41 % (2627149)Termination phase: Saturation % 12.22/2.41 % (2627149)Time elapsed: 0.070 s % 12.22/2.41 % (2627149)Peak memory usage: 90 MB % 12.22/2.41 % (2627149)Instructions burned: 130 (million) % 12.22/2.41 % (2627148)Instruction limit reached! % 12.22/2.41 % (2627148)------------------------------ % 12.22/2.41 % (2627148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.22/2.41 % (2627148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.22/2.41 % (2627148)CaDiCaL version: 2.1.3 % 12.22/2.41 % (2627148)Termination reason: Instruction limit % 12.22/2.41 % (2627148)Termination phase: Saturation % 12.22/2.41 % (2627148)Time elapsed: 0.080 s % 12.22/2.41 % (2627148)Peak memory usage: 91 MB % 12.22/2.41 % (2627148)Instructions burned: 140 (million) % 12.22/2.41 % (2627151)lrs+10_1_sil=8000:sp=occurrence:random_seed=289969498:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 12.22/2.41 % (2627151)Instruction limit reached! % 12.22/2.41 % (2627151)------------------------------ % 12.22/2.41 % (2627151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.22/2.41 % (2627151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.22/2.41 % (2627151)CaDiCaL version: 2.1.3 % 12.22/2.41 % (2627151)Termination reason: Instruction limit % 12.22/2.41 % (2627151)Termination phase: Saturation % 12.22/2.41 % (2627151)Time elapsed: 0.099 s % 12.22/2.41 % (2627151)Peak memory usage: 92 MB % 12.22/2.41 % (2627151)Instructions burned: 286 (million) % 19.43/3.48 % (2627158)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3898594408:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 19.43/3.48 % (2627146)------------------------------ % 19.43/3.48 % (2627146)------------------------------ % 19.43/3.48 % (2627159)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2039806520:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 19.43/3.48 % (2627158)Instruction limit reached! % 19.43/3.48 % (2627158)------------------------------ % 19.43/3.48 % (2627158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.48 % (2627158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.48 % (2627158)CaDiCaL version: 2.1.3 % 19.43/3.48 % (2627158)Termination reason: Instruction limit % 19.43/3.48 % (2627158)Termination phase: Saturation % 19.43/3.48 % (2627158)Time elapsed: 0.094 s % 19.43/3.48 % (2627158)Peak memory usage: 91 MB % 19.43/3.48 % (2627158)Instructions burned: 158 (million) % 19.43/3.48 % (2627161)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=3365063201:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 19.43/3.48 % (2627161)Instruction limit reached! % 19.43/3.48 % (2627161)------------------------------ % 19.43/3.48 % (2627161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.48 % (2627161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.48 % (2627161)CaDiCaL version: 2.1.3 % 19.43/3.48 % (2627161)Termination reason: Instruction limit % 19.43/3.48 % (2627161)Termination phase: Saturation % 19.43/3.48 % (2627161)Time elapsed: 0.072 s % 19.43/3.48 % (2627161)Peak memory usage: 94 MB % 19.43/3.48 % (2627161)Instructions burned: 248 (million) % 19.43/3.48 % (2627164)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2332574575:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 19.43/3.48 % (2627159)Instruction limit reached! % 19.43/3.48 % (2627159)------------------------------ % 19.43/3.48 % (2627159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.48 % (2627159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.48 % (2627159)CaDiCaL version: 2.1.3 % 19.43/3.48 % (2627159)Termination reason: Instruction limit % 19.43/3.48 % (2627159)Termination phase: Saturation % 19.43/3.48 % (2627159)Time elapsed: 0.209 s % 19.43/3.48 % (2627159)Peak memory usage: 93 MB % 19.43/3.48 % (2627159)Instructions burned: 325 (million) % 19.43/3.48 % (2627165)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3588529872:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 19.43/3.48 % (2627167)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2238060894:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 19.43/3.48 % (2627167)Instruction limit reached! % 19.43/3.48 % (2627167)------------------------------ % 19.43/3.48 % (2627167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.48 % (2627167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.48 % (2627167)CaDiCaL version: 2.1.3 % 19.43/3.48 % (2627167)Termination reason: Instruction limit % 19.43/3.48 % (2627167)Termination phase: Saturation % 19.43/3.48 % (2627167)Time elapsed: 0.032 s % 19.43/3.48 % (2627167)Peak memory usage: 90 MB % 19.43/3.48 % (2627167)Instructions burned: 114 (million) % 19.43/3.48 % (2627164)Instruction limit reached! % 19.43/3.48 % (2627164)------------------------------ % 19.43/3.48 % (2627164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.43/3.48 % (2627164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.43/3.48 % (2627164)CaDiCaL version: 2.1.3 % 19.43/3.48 % (2627164)Termination reason: Instruction limit % 19.43/3.48 % (2627164)Termination phase: Saturation % 19.43/3.48 % (2627164)Time elapsed: 0.170 s % 19.43/3.48 % (2627164)Peak memory usage: 91 MB % 19.43/3.48 % (2627164)Instructions burned: 294 (million) % 19.43/3.48 % (2627169)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3201421654:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 19.43/3.48 % (2627172)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3532516200:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 19.43/3.48 % (2627169)Refutation not found, incomplete strategy % 19.43/3.48 % (2627169)------------------------------ % 19.43/3.48 % (2627169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.40/5.58 % (2627169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.40/5.58 % (2627169)CaDiCaL version: 2.1.3 % 34.40/5.58 % (2627169)Termination reason: Refutation not found, incomplete strategy % 34.40/5.58 % (2627169)Time elapsed: 0.056 s % 34.40/5.58 % (2627169)Peak memory usage: 90 MB % 34.40/5.58 % (2627169)Instructions burned: 111 (million) % 34.40/5.58 % (2627172)Instruction limit reached! % 34.40/5.58 % (2627172)------------------------------ % 34.40/5.58 % (2627172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.40/5.58 % (2627172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.40/5.58 % (2627172)CaDiCaL version: 2.1.3 % 34.40/5.58 % (2627172)Termination reason: Instruction limit % 34.40/5.58 % (2627172)Termination phase: Saturation % 34.40/5.58 % (2627172)Time elapsed: 0.032 s % 34.40/5.58 % (2627172)Peak memory usage: 90 MB % 34.40/5.58 % (2627172)Instructions burned: 115 (million) % 34.40/5.58 % (2627173)lrs+10_1_sil=8000:sp=occurrence:random_seed=215308707:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 34.40/5.58 % (2627176)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=619263853:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 34.40/5.58 % (2627169)------------------------------ % 34.40/5.58 % (2627169)------------------------------ % 34.40/5.58 % (2627176)Instruction limit reached! % 34.40/5.58 % (2627176)------------------------------ % 34.40/5.58 % (2627176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.40/5.58 % (2627176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.40/5.58 % (2627176)CaDiCaL version: 2.1.3 % 34.40/5.58 % (2627176)Termination reason: Instruction limit % 34.40/5.58 % (2627176)Termination phase: Saturation % 34.40/5.58 % (2627176)Time elapsed: 0.124 s % 34.40/5.58 % (2627176)Peak memory usage: 93 MB % 34.40/5.58 % (2627176)Instructions burned: 439 (million) % 34.40/5.58 % (2627180)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=373054780:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 34.40/5.58 % (2627179)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=921002461:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 34.40/5.58 % (2627180)Instruction limit reached! % 34.40/5.58 % (2627180)------------------------------ % 34.40/5.58 % (2627180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.40/5.58 % (2627180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.40/5.58 % (2627180)CaDiCaL version: 2.1.3 % 34.40/5.58 % (2627180)Termination reason: Instruction limit % 34.40/5.58 % (2627180)Termination phase: Saturation % 34.40/5.58 % (2627180)Time elapsed: 0.041 s % 34.40/5.58 % (2627180)Peak memory usage: 92 MB % 34.40/5.58 % (2627180)Instructions burned: 137 (million) % 34.40/5.58 % (2627183)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3899458837:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi) % 34.40/5.58 % (2627173)Instruction limit reached! % 34.40/5.58 % (2627173)------------------------------ % 34.40/5.58 % (2627173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.40/5.58 % (2627173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.40/5.58 % (2627173)CaDiCaL version: 2.1.3 % 34.40/5.58 % (2627173)Termination reason: Instruction limit % 34.40/5.58 % (2627173)Termination phase: Saturation % 34.40/5.58 % (2627173)Time elapsed: 0.587 s % 34.40/5.58 % (2627173)Peak memory usage: 97 MB % 34.40/5.58 % (2627173)Instructions burned: 908 (million) % 34.40/5.58 % (2627183)Instruction limit reached! % 34.40/5.58 % (2627183)------------------------------ % 34.40/5.58 % (2627183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.40/5.58 % (2627183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.40/5.58 % (2627183)CaDiCaL version: 2.1.3 % 34.40/5.58 % (2627183)Termination reason: Instruction limit % 34.40/5.58 % (2627183)Termination phase: Saturation % 34.40/5.58 % (2627183)Time elapsed: 0.161 s % 34.40/5.58 % (2627183)Peak memory usage: 98 MB % 34.40/5.58 % (2627183)Instructions burned: 595 (million) % 34.40/5.58 % (2627185)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2039321106:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 34.40/5.58 % (2627186)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=2304081982:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi) % 67.31/10.19 % (2627186)Instruction limit reached! % 67.31/10.19 % (2627186)------------------------------ % 67.31/10.19 % (2627186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (2627186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (2627186)CaDiCaL version: 2.1.3 % 67.31/10.19 % (2627186)Termination reason: Instruction limit % 67.31/10.19 % (2627186)Termination phase: Saturation % 67.31/10.19 % (2627186)Time elapsed: 0.033 s % 67.31/10.19 % (2627186)Peak memory usage: 90 MB % 67.31/10.19 % (2627186)Instructions burned: 127 (million) % 67.31/10.19 % (2627189)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2550251123:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi) % 67.31/10.19 % (2627189)Instruction limit reached! % 67.31/10.19 % (2627189)------------------------------ % 67.31/10.19 % (2627189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (2627189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (2627189)CaDiCaL version: 2.1.3 % 67.31/10.19 % (2627189)Termination reason: Instruction limit % 67.31/10.19 % (2627189)Termination phase: Saturation % 67.31/10.19 % (2627189)Time elapsed: 0.035 s % 67.31/10.19 % (2627189)Peak memory usage: 90 MB % 67.31/10.19 % (2627189)Instructions burned: 135 (million) % 67.31/10.19 % (2627191)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1633688858:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 67.31/10.19 % (2627191)Refutation not found, incomplete strategy % 67.31/10.19 % (2627191)------------------------------ % 67.31/10.19 % (2627191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (2627191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (2627191)CaDiCaL version: 2.1.3 % 67.31/10.19 % (2627191)Termination reason: Refutation not found, incomplete strategy % 67.31/10.19 % (2627191)Time elapsed: 0.005 s % 67.31/10.19 % (2627191)Peak memory usage: 89 MB % 67.31/10.19 % (2627191)Instructions burned: 13 (million) % 67.31/10.19 % (2627165)Instruction limit reached! % 67.31/10.19 % (2627165)------------------------------ % 67.31/10.19 % (2627165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (2627165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (2627165)CaDiCaL version: 2.1.3 % 67.31/10.19 % (2627165)Termination reason: Instruction limit % 67.31/10.19 % (2627165)Termination phase: Saturation % 67.31/10.19 % (2627165)Time elapsed: 1.445 s % 67.31/10.19 % (2627165)Peak memory usage: 144 MB % 67.31/10.19 % (2627165)Instructions burned: 2352 (million) % 67.31/10.19 % (2627191)------------------------------ % 67.31/10.19 % (2627191)------------------------------ % 67.31/10.19 % (2627193)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2039721735:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 67.31/10.19 % (2627194)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=951407620:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi) % 67.31/10.19 % (2627193)Instruction limit reached! % 67.31/10.19 % (2627193)------------------------------ % 67.31/10.19 % (2627193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (2627193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (2627193)CaDiCaL version: 2.1.3 % 67.31/10.19 % (2627193)Termination reason: Instruction limit % 67.31/10.19 % (2627193)Termination phase: Saturation % 67.31/10.19 % (2627193)Time elapsed: 0.267 s % 67.31/10.19 % (2627193)Peak memory usage: 92 MB % 67.31/10.19 % (2627193)Instructions burned: 431 (million) % 67.31/10.19 % (2627197)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=140742697:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi) % 67.31/10.19 % (2627197)Instruction limit reached! % 67.31/10.19 % (2627197)------------------------------ % 67.31/10.19 % (2627197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (2627197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.64/13.17 % (2627197)CaDiCaL version: 2.1.3 % 88.64/13.17 % (2627197)Termination reason: Instruction limit % 88.64/13.17 % (2627197)Termination phase: Saturation % 88.64/13.17 % (2627197)Time elapsed: 0.082 s % 88.64/13.17 % (2627197)Peak memory usage: 91 MB % 88.64/13.17 % (2627197)Instructions burned: 150 (million) % 88.64/13.17 % (2627199)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1061898032:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi) % 88.64/13.17 % (2627179)Instruction limit reached! % 88.64/13.17 % (2627179)------------------------------ % 88.64/13.17 % (2627179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.64/13.17 % (2627179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.64/13.17 % (2627179)CaDiCaL version: 2.1.3 % 88.64/13.17 % (2627179)Termination reason: Instruction limit % 88.64/13.17 % (2627179)Termination phase: Saturation % 88.64/13.17 % (2627179)Time elapsed: 2.997 s % 88.64/13.17 % (2627179)Peak memory usage: 163 MB % 88.64/13.17 % (2627179)Instructions burned: 5203 (million) % 88.64/13.17 % (2627194)Instruction limit reached! % 88.64/13.17 % (2627194)------------------------------ % 88.64/13.17 % (2627194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.64/13.17 % (2627194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.64/13.17 % (2627194)CaDiCaL version: 2.1.3 % 88.64/13.17 % (2627194)Termination reason: Instruction limit % 88.64/13.17 % (2627194)Termination phase: Saturation % 88.64/13.17 % (2627194)Time elapsed: 2.048 s % 88.64/13.17 % (2627194)Peak memory usage: 181 MB % 88.64/13.17 % (2627194)Instructions burned: 6062 (million) % 88.64/13.17 % (2627202)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2454471636:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi) % 88.64/13.17 % (2627202)Refutation not found, incomplete strategy % 88.64/13.17 % (2627202)------------------------------ % 88.64/13.17 % (2627202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.64/13.17 % (2627202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.64/13.17 % (2627202)CaDiCaL version: 2.1.3 % 88.64/13.17 % (2627202)Termination reason: Refutation not found, incomplete strategy % 88.64/13.17 % (2627202)Time elapsed: 0.061 s % 88.64/13.17 % (2627202)Peak memory usage: 91 MB % 88.64/13.17 % (2627202)Instructions burned: 119 (million) % 88.64/13.17 % (2627203)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=3853790174:s2a=on:i=185:s2at=1.8:fdi=4_2955 on theBenchmark for (2955ds/185Mi) % 88.64/13.17 % (2627203)Instruction limit reached! % 88.64/13.17 % (2627203)------------------------------ % 88.64/13.17 % (2627203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.64/13.17 % (2627203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.64/13.17 % (2627203)CaDiCaL version: 2.1.3 % 88.64/13.17 % (2627203)Termination reason: Instruction limit % 88.64/13.17 % (2627203)Termination phase: Saturation % 88.64/13.17 % (2627203)Time elapsed: 0.055 s % 88.64/13.17 % (2627203)Peak memory usage: 92 MB % 88.64/13.17 % (2627203)Instructions burned: 188 (million) % 88.64/13.17 % (2627206)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1881087560:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2954 on theBenchmark for (2954ds/193Mi) % 88.64/13.17 % (2627202)------------------------------ % 88.64/13.17 % (2627202)------------------------------ % 88.64/13.17 % (2627206)Instruction limit reached! % 88.64/13.17 % (2627206)------------------------------ % 88.64/13.17 % (2627206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.64/13.17 % (2627206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.64/13.17 % (2627206)CaDiCaL version: 2.1.3 % 88.64/13.17 % (2627206)Termination reason: Instruction limit % 88.64/13.17 % (2627206)Termination phase: Saturation % 88.64/13.17 % (2627206)Time elapsed: 0.067 s % 88.64/13.17 % (2627206)Peak memory usage: 93 MB % 88.64/13.17 % (2627206)Instructions burned: 195 (million) % 88.64/13.17 % (2627209)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2952890956:i=12111:sd=1:ss=included_2951 on theBenchmark for (2951ds/12111Mi) % 88.64/13.17 % (2627208)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2092263919:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2952 on theBenchmark for (2952ds/4850Mi) % 123.42/18.12 % (2627208)Refutation not found, incomplete strategy % 123.42/18.12 % (2627208)------------------------------ % 123.42/18.12 % (2627208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.42/18.12 % (2627208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.42/18.12 % (2627208)CaDiCaL version: 2.1.3 % 123.42/18.12 % (2627208)Termination reason: Refutation not found, incomplete strategy % 123.42/18.12 % (2627208)Time elapsed: 0.045 s % 123.42/18.12 % (2627208)Peak memory usage: 90 MB % 123.42/18.12 % (2627208)Instructions burned: 91 (million) % 123.42/18.12 % (2627208)------------------------------ % 123.42/18.12 % (2627208)------------------------------ % 123.42/18.12 % (2627212)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3396149644:i=319:kws=precedence:fsr=off_2947 on theBenchmark for (2947ds/319Mi) % 123.42/18.12 % (2627212)Instruction limit reached! % 123.42/18.12 % (2627212)------------------------------ % 123.42/18.12 % (2627212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.42/18.12 % (2627212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.42/18.12 % (2627212)CaDiCaL version: 2.1.3 % 123.42/18.12 % (2627212)Termination reason: Instruction limit % 123.42/18.12 % (2627212)Termination phase: Saturation % 123.42/18.12 % (2627212)Time elapsed: 0.183 s % 123.42/18.12 % (2627212)Peak memory usage: 94 MB % 123.42/18.12 % (2627212)Instructions burned: 319 (million) % 123.42/18.12 % (2627214)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2159123530:i=2064:ep=RST_2944 on theBenchmark for (2944ds/2064Mi) % 123.42/18.12 % (2627214)Instruction limit reached! % 123.42/18.12 % (2627214)------------------------------ % 123.42/18.12 % (2627214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.42/18.12 % (2627214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.42/18.12 % (2627214)CaDiCaL version: 2.1.3 % 123.42/18.12 % (2627214)Termination reason: Instruction limit % 123.42/18.12 % (2627214)Termination phase: Saturation % 123.42/18.12 % (2627214)Time elapsed: 1.045 s % 123.42/18.12 % (2627214)Peak memory usage: 104 MB % 123.42/18.12 % (2627214)Instructions burned: 2066 (million) % 123.42/18.12 % (2627216)dis-1011_128_sil=32000:random_seed=44421525:i=3706:ep=RST:av=off_2932 on theBenchmark for (2932ds/3706Mi) % 123.42/18.12 % (2627209)Instruction limit reached! % 123.42/18.12 % (2627209)------------------------------ % 123.42/18.12 % (2627209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.42/18.12 % (2627209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.42/18.12 % (2627209)CaDiCaL version: 2.1.3 % 123.42/18.12 % (2627209)Termination reason: Instruction limit % 123.42/18.12 % (2627209)Termination phase: Saturation % 123.42/18.12 % (2627209)Time elapsed: 4.092 s % 123.42/18.12 % (2627209)Peak memory usage: 235 MB % 123.42/18.12 % (2627209)Instructions burned: 12112 (million) % 123.42/18.12 % (2627216)Instruction limit reached! % 123.42/18.12 % (2627216)------------------------------ % 123.42/18.12 % (2627216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.42/18.12 % (2627216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.42/18.12 % (2627216)CaDiCaL version: 2.1.3 % 123.42/18.12 % (2627216)Termination reason: Instruction limit % 123.42/18.12 % (2627216)Termination phase: Saturation % 123.42/18.12 % (2627216)Time elapsed: 2.154 s % 123.42/18.12 % (2627216)Peak memory usage: 127 MB % 123.42/18.12 % (2627216)Instructions burned: 3707 (million) % 123.42/18.12 % (2627218)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2741983059:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2909 on theBenchmark for (2909ds/757Mi) % 123.42/18.12 % (2627219)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3297279692:i=13913:ss=axioms:sgt=8_2908 on theBenchmark for (2908ds/13913Mi) % 123.42/18.12 % (2627218)Instruction limit reached! % 123.42/18.12 % (2627218)------------------------------ % 123.42/18.12 % (2627218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.42/18.12 % (2627218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.42/18.12 % (2627218)CaDiCaL version: 2.1.3 % 123.42/18.12 % (2627218)Termination reason: Instruction limit % 123.42/18.12 % (2627218)Termination phase: Saturation % 123.42/18.12 % (2627218)Time elapsed: 0.248 s % 123.42/18.12 % (2627218)Peak memory usage: 97 MB % 123.42/18.12 % (2627218)Instructions burned: 760 (million) % 123.42/18.12 % (2627222)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4232820586:i=9925:aac=none_2905 on theBenchmark for (2905ds/9925Mi) % 138.66/20.28 % (2627185)Instruction limit reached! % 138.66/20.28 % (2627185)------------------------------ % 138.66/20.28 % (2627185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.66/20.28 % (2627185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.66/20.28 % (2627185)CaDiCaL version: 2.1.3 % 138.66/20.28 % (2627185)Termination reason: Instruction limit % 138.66/20.28 % (2627185)Termination phase: Saturation % 138.66/20.28 % (2627185)Time elapsed: 7.847 s % 138.66/20.28 % (2627185)Peak memory usage: 223 MB % 138.66/20.28 % (2627185)Instructions burned: 13195 (million) % 138.66/20.28 % (2627224)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1620331637:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2903 on theBenchmark for (2903ds/2479Mi) % 138.66/20.28 % (2627224)Refutation not found, incomplete strategy % 138.66/20.28 % (2627224)------------------------------ % 138.66/20.28 % (2627224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.66/20.28 % (2627224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.66/20.28 % (2627224)CaDiCaL version: 2.1.3 % 138.66/20.28 % (2627224)Termination reason: Refutation not found, incomplete strategy % 138.66/20.28 % (2627224)Time elapsed: 0.184 s % 138.66/20.28 % (2627224)Peak memory usage: 91 MB % 138.66/20.28 % (2627224)Instructions burned: 352 (million) % 138.66/20.28 % (2627224)------------------------------ % 138.66/20.28 % (2627224)------------------------------ % 138.66/20.28 % (2627226)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2944871102:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2897 on theBenchmark for (2897ds/440Mi) % 138.66/20.28 % (2627226)Instruction limit reached! % 138.66/20.28 % (2627226)------------------------------ % 138.66/20.28 % (2627226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.66/20.28 % (2627226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.66/20.28 % (2627226)CaDiCaL version: 2.1.3 % 138.66/20.28 % (2627226)Termination reason: Instruction limit % 138.66/20.28 % (2627226)Termination phase: Saturation % 138.66/20.28 % (2627226)Time elapsed: 0.239 s % 138.66/20.28 % (2627226)Peak memory usage: 94 MB % 138.66/20.28 % (2627226)Instructions burned: 441 (million) % 138.66/20.28 % (2627228)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=473069038:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2893 on theBenchmark for (2893ds/11145Mi) % 138.66/20.28 % (2627199)Instruction limit reached! % 138.66/20.28 % (2627199)------------------------------ % 138.66/20.28 % (2627199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.66/20.28 % (2627199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.66/20.28 % (2627199)CaDiCaL version: 2.1.3 % 138.66/20.28 % (2627199)Termination reason: Instruction limit % 138.66/20.28 % (2627199)Termination phase: Saturation % 138.66/20.28 % (2627199)Time elapsed: 8.546 s % 138.66/20.28 % (2627199)Peak memory usage: 230 MB % 138.66/20.28 % (2627199)Instructions burned: 14155 (million) % 138.66/20.28 % (2627230)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=1140744556:cts=off:i=3034:av=off:er=known:fsd=on_2884 on theBenchmark for (2884ds/3034Mi) % 138.66/20.28 % (2627222)Instruction limit reached! % 138.66/20.28 % (2627222)------------------------------ % 138.66/20.28 % (2627222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.66/20.28 % (2627222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.66/20.28 % (2627222)CaDiCaL version: 2.1.3 % 138.66/20.28 % (2627222)Termination reason: Instruction limit % 138.66/20.28 % (2627222)Termination phase: Saturation % 138.66/20.28 % (2627222)Time elapsed: 2.704 s % 138.66/20.28 % (2627222)Peak memory usage: 170 MB % 138.66/20.28 % (2627222)Instructions burned: 9926 (million) % 138.66/20.28 % (2627232)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=906736066:st=2:s2a=on:i=524:s2at=2:ss=axioms_2877 on theBenchmark for (2877ds/524Mi) % 138.66/20.28 % (2627232)Instruction limit reached! % 138.66/20.28 % (2627232)------------------------------ % 138.66/20.28 % (2627232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.66/20.28 % (2627232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.66/20.28 % (2627232)CaDiCaL version: 2.1.3 % 138.66/20.28 % (2627232)Termination reason: Instruction limit % 170.02/24.61 % (2627232)Termination phase: Saturation % 170.02/24.61 % (2627232)Time elapsed: 0.140 s % 170.02/24.61 % (2627232)Peak memory usage: 97 MB % 170.02/24.61 % (2627232)Instructions burned: 526 (million) % 170.02/24.61 % (2627234)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1370498837:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2874 on theBenchmark for (2874ds/1016Mi) % 170.02/24.61 % (2627234)Instruction limit reached! % 170.02/24.61 % (2627234)------------------------------ % 170.02/24.61 % (2627234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.02/24.61 % (2627234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.02/24.61 % (2627234)CaDiCaL version: 2.1.3 % 170.02/24.61 % (2627234)Termination reason: Instruction limit % 170.02/24.61 % (2627234)Termination phase: Saturation % 170.02/24.61 % (2627234)Time elapsed: 0.254 s % 170.02/24.61 % (2627234)Peak memory usage: 100 MB % 170.02/24.61 % (2627234)Instructions burned: 1017 (million) % 170.02/24.61 % (2627236)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2911145263:i=14123:bd=preordered:ins=4_2870 on theBenchmark for (2870ds/14123Mi) % 170.02/24.61 % (2627230)Instruction limit reached! % 170.02/24.61 % (2627230)------------------------------ % 170.02/24.61 % (2627230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.02/24.61 % (2627230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.02/24.61 % (2627230)CaDiCaL version: 2.1.3 % 170.02/24.61 % (2627230)Termination reason: Instruction limit % 170.02/24.61 % (2627230)Termination phase: Saturation % 170.02/24.61 % (2627230)Time elapsed: 1.689 s % 170.02/24.61 % (2627230)Peak memory usage: 141 MB % 170.02/24.61 % (2627230)Instructions burned: 3036 (million) % 170.02/24.61 % (2627238)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=854046309:i=5781:kws=precedence:bd=all:rawr=on_2865 on theBenchmark for (2865ds/5781Mi) % 170.02/24.61 % (2627238)Instruction limit reached! % 170.02/24.61 % (2627238)------------------------------ % 170.02/24.61 % (2627238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.02/24.61 % (2627238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.02/24.61 % (2627238)CaDiCaL version: 2.1.3 % 170.02/24.61 % (2627238)Termination reason: Instruction limit % 170.02/24.61 % (2627238)Termination phase: Saturation % 170.02/24.61 % (2627238)Time elapsed: 3.393 s % 170.02/24.61 % (2627238)Peak memory usage: 125 MB % 170.02/24.61 % (2627238)Instructions burned: 5781 (million) % 170.02/24.61 % (2627240)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=1602304727:i=2448:gtgl=5:bd=preordered:gtg=all_2830 on theBenchmark for (2830ds/2448Mi) % 170.02/24.61 % (2627228)Instruction limit reached! % 170.02/24.61 % (2627228)------------------------------ % 170.02/24.61 % (2627228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.02/24.61 % (2627228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.02/24.61 % (2627228)CaDiCaL version: 2.1.3 % 170.02/24.61 % (2627228)Termination reason: Instruction limit % 170.02/24.61 % (2627228)Termination phase: Saturation % 170.02/24.61 % (2627228)Time elapsed: 6.517 s % 170.02/24.61 % (2627228)Peak memory usage: 222 MB % 170.02/24.61 % (2627228)Instructions burned: 11145 (million) % 170.02/24.61 % (2627236)Instruction limit reached! % 170.02/24.61 % (2627236)------------------------------ % 170.02/24.61 % (2627236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.02/24.61 % (2627236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.02/24.61 % (2627236)CaDiCaL version: 2.1.3 % 170.02/24.61 % (2627236)Termination reason: Instruction limit % 170.02/24.61 % (2627236)Termination phase: Saturation % 170.02/24.61 % (2627236)Time elapsed: 4.383 s % 170.02/24.61 % (2627236)Peak memory usage: 219 MB % 170.02/24.61 % (2627236)Instructions burned: 14125 (million) % 170.02/24.61 % (2627219)Instruction limit reached! % 170.02/24.61 % (2627219)------------------------------ % 170.02/24.61 % (2627219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 170.02/24.61 % (2627219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 170.02/24.61 % (2627219)CaDiCaL version: 2.1.3 % 170.02/24.61 % (2627219)Termination reason: Instruction limit % 170.02/24.61 % (2627219)Termination phase: Saturation % 170.02/24.61 % (2627219)Time elapsed: 8.174 s % 170.02/24.61 % (2627219)Peak memory usage: 232 MB % 170.02/24.61 % (2627219)Instructions burned: 13914 (million) % 170.02/24.61 % (2627242)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2368086493:i=3223:kws=precedence:fgj=on:av=off_2826 on theBenchmark for (2826ds/3223Mi) % 202.54/29.20 % (2627243)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3616261153:st=5.6:i=2033:sd=3:ss=axioms_2825 on theBenchmark for (2825ds/2033Mi) % 202.54/29.20 % (2627245)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=226104226:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2825 on theBenchmark for (2825ds/2055Mi) % 202.54/29.20 % (2627243)Instruction limit reached! % 202.54/29.20 % (2627243)------------------------------ % 202.54/29.20 % (2627243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.54/29.20 % (2627243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/29.20 % (2627243)CaDiCaL version: 2.1.3 % 202.54/29.20 % (2627243)Termination reason: Instruction limit % 202.54/29.20 % (2627243)Termination phase: Saturation % 202.54/29.20 % (2627243)Time elapsed: 0.680 s % 202.54/29.20 % (2627243)Peak memory usage: 139 MB % 202.54/29.20 % (2627243)Instructions burned: 2036 (million) % 202.54/29.20 % (2627249)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=952193031:i=21611:sd=3:ss=axioms_2817 on theBenchmark for (2817ds/21611Mi) % 202.54/29.20 % (2627240)Instruction limit reached! % 202.54/29.20 % (2627240)------------------------------ % 202.54/29.20 % (2627240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.54/29.20 % (2627240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/29.20 % (2627240)CaDiCaL version: 2.1.3 % 202.54/29.20 % (2627240)Termination reason: Instruction limit % 202.54/29.20 % (2627240)Termination phase: Saturation % 202.54/29.20 % (2627240)Time elapsed: 1.410 s % 202.54/29.20 % (2627240)Peak memory usage: 148 MB % 202.54/29.20 % (2627240)Instructions burned: 2450 (million) % 202.54/29.20 % (2627251)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1387963183:i=4835:sd=13:ss=axioms:sgt=23_2814 on theBenchmark for (2814ds/4835Mi) % 202.54/29.20 % (2627245)Instruction limit reached! % 202.54/29.20 % (2627245)------------------------------ % 202.54/29.20 % (2627245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.54/29.20 % (2627245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/29.20 % (2627245)CaDiCaL version: 2.1.3 % 202.54/29.20 % (2627245)Termination reason: Instruction limit % 202.54/29.20 % (2627245)Termination phase: Saturation % 202.54/29.20 % (2627245)Time elapsed: 1.193 s % 202.54/29.20 % (2627245)Peak memory usage: 136 MB % 202.54/29.20 % (2627245)Instructions burned: 2055 (million) % 202.54/29.20 % (2627253)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=2738555446:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2811 on theBenchmark for (2811ds/797Mi) % 202.54/29.20 % (2627253)Instruction limit reached! % 202.54/29.20 % (2627253)------------------------------ % 202.54/29.20 % (2627253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.54/29.20 % (2627253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/29.20 % (2627253)CaDiCaL version: 2.1.3 % 202.54/29.20 % (2627253)Termination reason: Instruction limit % 202.54/29.21 % (2627253)Termination phase: Saturation % 202.54/29.21 % (2627253)Time elapsed: 0.464 s % 202.54/29.21 % (2627253)Peak memory usage: 95 MB % 202.54/29.21 % (2627253)Instructions burned: 799 (million) % 202.54/29.21 % (2627242)Instruction limit reached! % 202.54/29.21 % (2627242)------------------------------ % 202.54/29.21 % (2627242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.54/29.21 % (2627242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.54/29.21 % (2627242)CaDiCaL version: 2.1.3 % 202.54/29.21 % (2627242)Termination reason: Instruction limit % 202.54/29.21 % (2627242)Termination phase: Saturation % 202.54/29.21 % (2627242)Time elapsed: 2.004 s % 202.54/29.21 % (2627242)Peak memory usage: 152 MB % 202.54/29.21 % (2627242)Instructions burned: 3223 (million) % 202.54/29.21 % (2627255)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2937435078:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2805 on theBenchmark for (2805ds/2326Mi) % 202.54/29.21 % (2627256)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4255811274:i=6038:nm=6_2805 on theBenchmark for (2805ds/6038Mi) % 287.66/41.24 % (2627255)Refutation not found, incomplete strategy % 287.66/41.24 % (2627255)------------------------------ % 287.66/41.24 % (2627255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.66/41.24 % (2627255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.66/41.24 % (2627255)CaDiCaL version: 2.1.3 % 287.66/41.24 % (2627255)Termination reason: Refutation not found, incomplete strategy % 287.66/41.24 % (2627255)Time elapsed: 0.089 s % 287.66/41.24 % (2627255)Peak memory usage: 92 MB % 287.66/41.24 % (2627255)Instructions burned: 154 (million) % 287.66/41.24 % (2627255)------------------------------ % 287.66/41.24 % (2627255)------------------------------ % 287.66/41.24 % (2627259)lrs+10_1_sil=32000:sp=occurrence:random_seed=3975559005:st=2:i=33334:sd=3:ss=included:sgt=32_2800 on theBenchmark for (2800ds/33334Mi) % 287.66/41.24 % (2627251)Instruction limit reached! % 287.66/41.24 % (2627251)------------------------------ % 287.66/41.24 % (2627251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.66/41.24 % (2627251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.66/41.24 % (2627251)CaDiCaL version: 2.1.3 % 287.66/41.24 % (2627251)Termination reason: Instruction limit % 287.66/41.24 % (2627251)Termination phase: Saturation % 287.66/41.24 % (2627251)Time elapsed: 2.566 s % 287.66/41.24 % (2627251)Peak memory usage: 112 MB % 287.66/41.24 % (2627251)Instructions burned: 4835 (million) % 287.66/41.24 % (2627261)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=675100407:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2786 on theBenchmark for (2786ds/1008Mi) % 287.66/41.24 % (2627261)Instruction limit reached! % 287.66/41.24 % (2627261)------------------------------ % 287.66/41.24 % (2627261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.66/41.24 % (2627261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.66/41.24 % (2627261)CaDiCaL version: 2.1.3 % 287.66/41.24 % (2627261)Termination reason: Instruction limit % 287.66/41.24 % (2627261)Termination phase: Saturation % 287.66/41.24 % (2627261)Time elapsed: 0.515 s % 287.66/41.24 % (2627261)Peak memory usage: 97 MB % 287.66/41.24 % (2627261)Instructions burned: 1010 (million) % 287.66/41.24 % (2627263)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=779460335:i=8327:s2at=5:bd=preordered_2779 on theBenchmark for (2779ds/8327Mi) % 287.66/41.24 % (2627256)Instruction limit reached! % 287.66/41.24 % (2627256)------------------------------ % 287.66/41.24 % (2627256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.66/41.24 % (2627256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.66/41.24 % (2627256)CaDiCaL version: 2.1.3 % 287.66/41.24 % (2627256)Termination reason: Instruction limit % 287.66/41.24 % (2627256)Termination phase: Saturation % 287.66/41.24 % (2627256)Time elapsed: 2.828 s % 287.66/41.24 % (2627256)Peak memory usage: 159 MB % 287.66/41.24 % (2627256)Instructions burned: 6039 (million) % 287.66/41.24 % (2627265)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=1608410756:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2775 on theBenchmark for (2775ds/1083Mi) % 287.66/41.24 % (2627265)Instruction limit reached! % 287.66/41.24 % (2627265)------------------------------ % 287.66/41.24 % (2627265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.66/41.24 % (2627265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.66/41.24 % (2627265)CaDiCaL version: 2.1.3 % 287.66/41.24 % (2627265)Termination reason: Instruction limit % 287.66/41.24 % (2627265)Termination phase: Saturation % 287.66/41.24 % (2627265)Time elapsed: 0.492 s % 287.66/41.24 % (2627265)Peak memory usage: 99 MB % 287.66/41.24 % (2627265)Instructions burned: 1085 (million) % 287.66/41.24 % (2627267)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=876672910:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2768 on theBenchmark for (2768ds/1084Mi) % 287.66/41.24 % (2627267)Instruction limit reached! % 287.66/41.24 % (2627267)------------------------------ % 287.66/41.24 % (2627267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.66/41.24 % (2627267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.06 % (2627267)CaDiCaL version: 2.1.3 % 300.67/43.06 % (2627267)Termination reason: Instruction limit % 300.67/43.06 % (2627267)Termination phase: Saturation % 300.67/43.06 % (2627267)Time elapsed: 0.640 s % 300.67/43.06 % (2627267)Peak memory usage: 97 MB % 300.67/43.06 % (2627267)Instructions burned: 1086 (million) % 300.67/43.06 % (2627269)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3935771976:i=6995:s2at=5:gtg=all_2760 on theBenchmark for (2760ds/6995Mi) % 300.67/43.06 % (2627249)Instruction limit reached! % 300.67/43.06 % (2627249)------------------------------ % 300.67/43.06 % (2627249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.06 % (2627249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.06 % (2627249)CaDiCaL version: 2.1.3 % 300.67/43.06 % (2627249)Termination reason: Instruction limit % 300.67/43.06 % (2627249)Termination phase: Saturation % 300.67/43.06 % (2627249)Time elapsed: 6.122 s % 300.67/43.06 % (2627249)Peak memory usage: 314 MB % 300.67/43.06 % (2627249)Instructions burned: 21616 (million) % 300.67/43.06 % (2627271)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3634759222:st=2:i=6225:sd=15:ss=axioms_2755 on theBenchmark for (2755ds/6225Mi) % 300.67/43.06 % (2627271)Instruction limit reached! % 300.67/43.06 % (2627271)------------------------------ % 300.67/43.06 % (2627271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.06 % (2627271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.06 % (2627271)CaDiCaL version: 2.1.3 % 300.67/43.06 % (2627271)Termination reason: Instruction limit % 300.67/43.06 % (2627271)Termination phase: Saturation % 300.67/43.06 % (2627271)Time elapsed: 1.446 s % 300.67/43.06 % (2627271)Peak memory usage: 120 MB % 300.67/43.06 % (2627271)Instructions burned: 6227 (million) % 300.67/43.06 % (2627273)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2301153389:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2739 on theBenchmark for (2739ds/3372Mi) % 300.67/43.06 % (2627273)Instruction limit reached! % 300.67/43.06 % (2627273)------------------------------ % 300.67/43.06 % (2627273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.06 % (2627273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.06 % (2627273)CaDiCaL version: 2.1.3 % 300.67/43.06 % (2627273)Termination reason: Instruction limit % 300.67/43.06 % (2627273)Termination phase: Saturation % 300.67/43.06 % (2627273)Time elapsed: 1.107 s % 300.67/43.06 % (2627273)Peak memory usage: 151 MB % 300.67/43.06 % (2627273)Instructions burned: 3374 (million) % 300.67/43.06 % (2627275)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3202396230:st=2.3:i=26457:sd=10:ss=included:sgt=8_2726 on theBenchmark for (2726ds/26457Mi) % 300.67/43.06 % (2627263)Instruction limit reached! % 300.67/43.06 % (2627263)------------------------------ % 300.67/43.06 % (2627263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.06 % (2627263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.06 % (2627263)CaDiCaL version: 2.1.3 % 300.67/43.06 % (2627263)Termination reason: Instruction limit % 300.67/43.06 % (2627263)Termination phase: Saturation % 300.67/43.06 % (2627263)Time elapsed: 5.259 s % 300.67/43.06 % (2627263)Peak memory usage: 185 MB % 300.67/43.06 % (2627263)Instructions burned: 8328 (million) % 300.67/43.06 % (2627277)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=2177376583:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2725 on theBenchmark for (2725ds/13494Mi) % 300.67/43.06 % (2627269)Instruction limit reached! % 300.67/43.06 % (2627269)------------------------------ % 300.67/43.06 % (2627269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.06 % (2627269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.06 % (2627269)CaDiCaL version: 2.1.3 % 300.67/43.06 % (2627269)Termination reason: Instruction limit % 300.67/43.06 % (2627269)Termination phase: Saturation % 300.67/43.06 % (2627269)Time elapsed: 4.256 s % 300.67/43.06 % (2627269)Peak memory usage: 186 MB % 300.67/43.06 % (2627269)Instructions burned: 6996 (million) % 300.67/43.06 % (2627279)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=2861839939:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2716 on theBenchmark for (2716ds/2503M % 300.67/43.07 Terminated %------------------------------------------------------------------------------