%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW476+1 : TPTP v9.3.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n010.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:34 PM UTC 2026 % Result : Timeout 301.22s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW476+1 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n010.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:10:47 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.08/0.21 Running first-order theorem proving % 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 13.49/2.64 % (1940010)Detected formulas, will run a generic FOF schedule. % 13.49/2.64 % (1940017)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=1309325290:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 13.49/2.64 % (1940021)dis-21_1_sil=8000:lcm=predicate:random_seed=2046066763: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) % 13.49/2.64 % (1940016)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=627657754:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 13.49/2.64 % (1940015)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=3759340856:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 13.49/2.64 % (1940020)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2122065120:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 13.49/2.64 % (1940019)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4212658991:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 13.49/2.64 % (1940018)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3473334137:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 13.49/2.64 % (1940018)Instruction limit reached! % 13.49/2.64 % (1940018)------------------------------ % 13.49/2.64 % (1940018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/2.64 % (1940018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/2.64 % (1940018)CaDiCaL version: 2.1.3 % 13.49/2.64 % (1940018)Termination reason: Instruction limit % 13.49/2.64 % (1940018)Termination phase: Saturation % 13.49/2.64 % (1940018)Time elapsed: 0.047 s % 13.49/2.64 % (1940018)Peak memory usage: 89 MB % 13.49/2.64 % (1940018)Instructions burned: 111 (million) % 13.49/2.64 % (1940021)Instruction limit reached! % 13.49/2.64 % (1940021)------------------------------ % 13.49/2.64 % (1940021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/2.64 % (1940021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/2.64 % (1940021)CaDiCaL version: 2.1.3 % 13.49/2.64 % (1940021)Termination reason: Instruction limit % 13.49/2.64 % (1940021)Termination phase: Saturation % 13.49/2.64 % (1940021)Time elapsed: 0.064 s % 13.49/2.64 % (1940021)Peak memory usage: 90 MB % 13.49/2.64 % (1940021)Instructions burned: 131 (million) % 13.49/2.64 % (1940019)Instruction limit reached! % 13.49/2.64 % (1940019)------------------------------ % 13.49/2.64 % (1940019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/2.64 % (1940019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/2.64 % (1940019)CaDiCaL version: 2.1.3 % 13.49/2.64 % (1940019)Termination reason: Instruction limit % 13.49/2.64 % (1940019)Termination phase: Saturation % 13.49/2.64 % (1940019)Time elapsed: 0.071 s % 13.49/2.64 % (1940019)Peak memory usage: 89 MB % 13.49/2.64 % (1940019)Instructions burned: 119 (million) % 13.49/2.64 % (1940020)Instruction limit reached! % 13.49/2.64 % (1940020)------------------------------ % 13.49/2.64 % (1940020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.49/2.64 % (1940020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.49/2.64 % (1940020)CaDiCaL version: 2.1.3 % 13.49/2.64 % (1940020)Termination reason: Instruction limit % 13.49/2.64 % (1940020)Termination phase: Saturation % 13.49/2.64 % (1940020)Time elapsed: 0.104 s % 13.49/2.64 % (1940020)Peak memory usage: 90 MB % 13.49/2.64 % (1940020)Instructions burned: 140 (million) % 13.49/2.64 % (1940029)lrs+10_1_sil=8000:sp=occurrence:random_seed=1285298238:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 13.49/2.64 % (1940031)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4245847142:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 13.49/2.64 % (1940030)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2694218506:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 13.49/2.64 % (1940032)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=1954409508:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 13.49/2.64 % (1940030)Instruction limit reached! % 19.87/3.57 % (1940030)------------------------------ % 19.87/3.57 % (1940030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940030)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940030)Termination reason: Instruction limit % 19.87/3.57 % (1940030)Termination phase: Saturation % 19.87/3.57 % (1940030)Time elapsed: 0.089 s % 19.87/3.57 % (1940030)Peak memory usage: 90 MB % 19.87/3.57 % (1940030)Instructions burned: 157 (million) % 19.87/3.57 % (1940029)Instruction limit reached! % 19.87/3.57 % (1940029)------------------------------ % 19.87/3.57 % (1940029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940029)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940029)Termination reason: Instruction limit % 19.87/3.57 % (1940029)Termination phase: Saturation % 19.87/3.57 % (1940029)Time elapsed: 0.180 s % 19.87/3.57 % (1940029)Peak memory usage: 92 MB % 19.87/3.57 % (1940029)Instructions burned: 285 (million) % 19.87/3.57 % (1940032)Instruction limit reached! % 19.87/3.57 % (1940032)------------------------------ % 19.87/3.57 % (1940032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940032)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940032)Termination reason: Instruction limit % 19.87/3.57 % (1940032)Termination phase: Saturation % 19.87/3.57 % (1940032)Time elapsed: 0.124 s % 19.87/3.57 % (1940032)Peak memory usage: 92 MB % 19.87/3.57 % (1940032)Instructions burned: 248 (million) % 19.87/3.57 % (1940031)Instruction limit reached! % 19.87/3.57 % (1940031)------------------------------ % 19.87/3.57 % (1940031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940031)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940031)Termination reason: Instruction limit % 19.87/3.57 % (1940031)Termination phase: Saturation % 19.87/3.57 % (1940031)Time elapsed: 0.209 s % 19.87/3.57 % (1940031)Peak memory usage: 92 MB % 19.87/3.57 % (1940031)Instructions burned: 326 (million) % 19.87/3.57 % (1940037)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2897609417:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 19.87/3.57 % (1940038)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2841700681:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 19.87/3.57 % (1940039)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3948489655:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 19.87/3.57 % (1940037)Instruction limit reached! % 19.87/3.57 % (1940037)------------------------------ % 19.87/3.57 % (1940037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940037)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940037)Termination reason: Instruction limit % 19.87/3.57 % (1940037)Termination phase: Saturation % 19.87/3.57 % (1940037)Time elapsed: 0.122 s % 19.87/3.57 % (1940037)Peak memory usage: 89 MB % 19.87/3.57 % (1940037)Instructions burned: 297 (million) % 19.87/3.57 % (1940040)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2331762158:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 19.87/3.57 % (1940039)Instruction limit reached! % 19.87/3.57 % (1940039)------------------------------ % 19.87/3.57 % (1940039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940039)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940039)Termination reason: Instruction limit % 19.87/3.57 % (1940039)Termination phase: Saturation % 19.87/3.57 % (1940039)Time elapsed: 0.065 s % 19.87/3.57 % (1940039)Peak memory usage: 90 MB % 19.87/3.57 % (1940039)Instructions burned: 113 (million) % 19.87/3.57 % (1940040)Instruction limit reached! % 19.87/3.57 % (1940040)------------------------------ % 19.87/3.57 % (1940040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.87/3.57 % (1940040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.87/3.57 % (1940040)CaDiCaL version: 2.1.3 % 19.87/3.57 % (1940040)Termination reason: Instruction limit % 57.33/8.77 % (1940040)Termination phase: Saturation % 57.33/8.77 % (1940040)Time elapsed: 0.059 s % 57.33/8.77 % (1940040)Peak memory usage: 89 MB % 57.33/8.77 % (1940040)Instructions burned: 128 (million) % 57.33/8.77 % (1940045)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3035093596:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 57.33/8.77 % (1940046)lrs+10_1_sil=8000:sp=occurrence:random_seed=3833721687:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi) % 57.33/8.77 % (1940045)Instruction limit reached! % 57.33/8.77 % (1940045)------------------------------ % 57.33/8.77 % (1940045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.33/8.77 % (1940045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.33/8.77 % (1940045)CaDiCaL version: 2.1.3 % 57.33/8.77 % (1940045)Termination reason: Instruction limit % 57.33/8.77 % (1940045)Termination phase: Saturation % 57.33/8.77 % (1940045)Time elapsed: 0.055 s % 57.33/8.77 % (1940045)Peak memory usage: 89 MB % 57.33/8.77 % (1940045)Instructions burned: 115 (million) % 57.33/8.77 % (1940047)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=528563308:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi) % 57.33/8.77 % (1940050)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1599470351:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 57.33/8.77 % (1940047)Instruction limit reached! % 57.33/8.77 % (1940047)------------------------------ % 57.33/8.77 % (1940047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.33/8.77 % (1940047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.33/8.77 % (1940047)CaDiCaL version: 2.1.3 % 57.33/8.77 % (1940047)Termination reason: Instruction limit % 57.33/8.77 % (1940047)Termination phase: Saturation % 57.33/8.77 % (1940047)Time elapsed: 0.222 s % 57.33/8.77 % (1940047)Peak memory usage: 91 MB % 57.33/8.77 % (1940047)Instructions burned: 437 (million) % 57.33/8.77 % (1940053)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2006111294:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 57.33/8.77 % (1940046)Instruction limit reached! % 57.33/8.77 % (1940046)------------------------------ % 57.33/8.77 % (1940046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.33/8.77 % (1940046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.33/8.77 % (1940046)CaDiCaL version: 2.1.3 % 57.33/8.77 % (1940046)Termination reason: Instruction limit % 57.33/8.77 % (1940046)Termination phase: Saturation % 57.33/8.77 % (1940046)Time elapsed: 0.516 s % 57.33/8.77 % (1940046)Peak memory usage: 95 MB % 57.33/8.77 % (1940046)Instructions burned: 907 (million) % 57.33/8.77 % (1940053)Instruction limit reached! % 57.33/8.77 % (1940053)------------------------------ % 57.33/8.77 % (1940053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.33/8.77 % (1940053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.33/8.77 % (1940053)CaDiCaL version: 2.1.3 % 57.33/8.77 % (1940053)Termination reason: Instruction limit % 57.33/8.77 % (1940053)Termination phase: Saturation % 57.33/8.77 % (1940053)Time elapsed: 0.080 s % 57.33/8.77 % (1940053)Peak memory usage: 90 MB % 57.33/8.77 % (1940053)Instructions burned: 134 (million) % 57.33/8.77 % (1940055)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3828535601:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 57.33/8.77 % (1940056)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=702487168:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 57.33/8.77 % (1940055)Instruction limit reached! % 57.33/8.77 % (1940055)------------------------------ % 57.33/8.77 % (1940055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 57.33/8.77 % (1940055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 57.33/8.77 % (1940055)CaDiCaL version: 2.1.3 % 57.33/8.77 % (1940055)Termination reason: Instruction limit % 57.33/8.77 % (1940055)Termination phase: Saturation % 57.33/8.77 % (1940055)Time elapsed: 0.209 s % 57.33/8.77 % (1940055)Peak memory usage: 89 MB % 57.33/8.77 % (1940055)Instructions burned: 594 (million) % 57.33/8.77 % (1940059)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=4034305071:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi) % 76.49/11.48 % (1940059)Instruction limit reached! % 76.49/11.48 % (1940059)------------------------------ % 76.49/11.48 % (1940059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.49/11.48 % (1940059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.49/11.48 % (1940059)CaDiCaL version: 2.1.3 % 76.49/11.48 % (1940059)Termination reason: Instruction limit % 76.49/11.48 % (1940059)Termination phase: Saturation % 76.49/11.48 % (1940059)Time elapsed: 0.068 s % 76.49/11.48 % (1940059)Peak memory usage: 91 MB % 76.49/11.48 % (1940059)Instructions burned: 126 (million) % 76.49/11.48 % (1940038)Instruction limit reached! % 76.49/11.48 % (1940038)------------------------------ % 76.49/11.48 % (1940038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.49/11.48 % (1940038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.49/11.48 % (1940038)CaDiCaL version: 2.1.3 % 76.49/11.48 % (1940038)Termination reason: Instruction limit % 76.49/11.48 % (1940038)Termination phase: Saturation % 76.49/11.48 % (1940038)Time elapsed: 1.489 s % 76.49/11.48 % (1940038)Peak memory usage: 140 MB % 76.49/11.48 % (1940038)Instructions burned: 2350 (million) % 76.49/11.48 % (1940061)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=277299161:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi) % 76.49/11.48 % (1940061)Instruction limit reached! % 76.49/11.48 % (1940061)------------------------------ % 76.49/11.48 % (1940061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.49/11.48 % (1940061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.49/11.48 % (1940061)CaDiCaL version: 2.1.3 % 76.49/11.48 % (1940061)Termination reason: Instruction limit % 76.49/11.48 % (1940061)Termination phase: Saturation % 76.49/11.48 % (1940061)Time elapsed: 0.076 s % 76.49/11.48 % (1940061)Peak memory usage: 91 MB % 76.49/11.48 % (1940061)Instructions burned: 134 (million) % 76.49/11.48 % (1940062)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2661259736:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi) % 76.49/11.48 % (1940062)Instruction limit reached! % 76.49/11.48 % (1940062)------------------------------ % 76.49/11.48 % (1940062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.49/11.48 % (1940062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.49/11.48 % (1940062)CaDiCaL version: 2.1.3 % 76.49/11.48 % (1940062)Termination reason: Instruction limit % 76.49/11.48 % (1940062)Termination phase: Saturation % 76.49/11.48 % (1940062)Time elapsed: 0.059 s % 76.49/11.48 % (1940062)Peak memory usage: 89 MB % 76.49/11.48 % (1940062)Instructions burned: 143 (million) % 76.49/11.48 % (1940064)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3557927026:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi) % 76.49/11.48 % (1940066)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=2406364947:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi) % 76.49/11.48 % (1940064)Instruction limit reached! % 76.49/11.48 % (1940064)------------------------------ % 76.49/11.48 % (1940064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.49/11.48 % (1940064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.49/11.48 % (1940064)CaDiCaL version: 2.1.3 % 76.49/11.48 % (1940064)Termination reason: Instruction limit % 76.49/11.48 % (1940064)Termination phase: Saturation % 76.49/11.48 % (1940064)Time elapsed: 0.212 s % 76.49/11.48 % (1940064)Peak memory usage: 92 MB % 76.49/11.48 % (1940064)Instructions burned: 431 (million) % 76.49/11.48 % (1940069)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=3590310043:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi) % 76.49/11.48 % (1940069)Instruction limit reached! % 76.49/11.48 % (1940069)------------------------------ % 76.49/11.48 % (1940069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.49/11.48 % (1940069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.49/11.48 % (1940069)CaDiCaL version: 2.1.3 % 76.49/11.48 % (1940069)Termination reason: Instruction limit % 76.49/11.48 % (1940069)Termination phase: Saturation % 76.49/11.48 % (1940069)Time elapsed: 0.092 s % 76.49/11.48 % (1940069)Peak memory usage: 91 MB % 112.79/16.63 % (1940069)Instructions burned: 151 (million) % 112.79/16.63 % (1940071)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=330593717:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi) % 112.79/16.63 % (1940050)Instruction limit reached! % 112.79/16.63 % (1940050)------------------------------ % 112.79/16.63 % (1940050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.79/16.63 % (1940050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.79/16.63 % (1940050)CaDiCaL version: 2.1.3 % 112.79/16.63 % (1940050)Termination reason: Instruction limit % 112.79/16.63 % (1940050)Termination phase: Saturation % 112.79/16.63 % (1940050)Time elapsed: 3.019 s % 112.79/16.63 % (1940050)Peak memory usage: 161 MB % 112.79/16.63 % (1940050)Instructions burned: 5202 (million) % 112.79/16.63 % (1940073)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3085963997:i=667:av=off:fsr=off_2958 on theBenchmark for (2958ds/667Mi) % 112.79/16.63 % (1940073)Instruction limit reached! % 112.79/16.63 % (1940073)------------------------------ % 112.79/16.63 % (1940073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.79/16.63 % (1940073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.79/16.63 % (1940073)CaDiCaL version: 2.1.3 % 112.79/16.63 % (1940073)Termination reason: Instruction limit % 112.79/16.63 % (1940073)Termination phase: Saturation % 112.79/16.63 % (1940073)Time elapsed: 0.282 s % 112.79/16.63 % (1940073)Peak memory usage: 90 MB % 112.79/16.63 % (1940073)Instructions burned: 667 (million) % 112.79/16.63 % (1940075)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=3194404602:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi) % 112.79/16.63 % (1940075)Instruction limit reached! % 112.79/16.63 % (1940075)------------------------------ % 112.79/16.63 % (1940075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.79/16.63 % (1940075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.79/16.63 % (1940075)CaDiCaL version: 2.1.3 % 112.79/16.63 % (1940075)Termination reason: Instruction limit % 112.79/16.63 % (1940075)Termination phase: Saturation % 112.79/16.63 % (1940075)Time elapsed: 0.101 s % 112.79/16.63 % (1940075)Peak memory usage: 92 MB % 112.79/16.63 % (1940075)Instructions burned: 186 (million) % 112.79/16.63 % (1940077)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1648074508:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2951 on theBenchmark for (2951ds/193Mi) % 112.79/16.63 % (1940077)Instruction limit reached! % 112.79/16.63 % (1940077)------------------------------ % 112.79/16.63 % (1940077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.79/16.63 % (1940077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.79/16.63 % (1940077)CaDiCaL version: 2.1.3 % 112.79/16.63 % (1940077)Termination reason: Instruction limit % 112.79/16.63 % (1940077)Termination phase: Saturation % 112.79/16.63 % (1940077)Time elapsed: 0.110 s % 112.79/16.63 % (1940077)Peak memory usage: 90 MB % 112.79/16.63 % (1940077)Instructions burned: 193 (million) % 112.79/16.63 % (1940079)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=752394385:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2948 on theBenchmark for (2948ds/4850Mi) % 112.79/16.63 % (1940066)Instruction limit reached! % 112.79/16.63 % (1940066)------------------------------ % 112.79/16.63 % (1940066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.79/16.63 % (1940066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.79/16.63 % (1940066)CaDiCaL version: 2.1.3 % 112.79/16.63 % (1940066)Termination reason: Instruction limit % 112.79/16.63 % (1940066)Termination phase: Saturation % 112.79/16.63 % (1940066)Time elapsed: 3.273 s % 112.79/16.63 % (1940066)Peak memory usage: 145 MB % 112.79/16.63 % (1940066)Instructions burned: 6062 (million) % 112.79/16.63 % (1940081)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=4100949705:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi) % 112.79/16.63 % (1940079)Instruction limit reached! % 112.79/16.63 % (1940079)------------------------------ % 112.79/16.63 % (1940079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.79/16.63 % (1940079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.79/16.63 % (1940079)CaDiCaL version: 2.1.3 % 143.23/21.01 % (1940079)Termination reason: Instruction limit % 143.23/21.01 % (1940079)Termination phase: Saturation % 143.23/21.01 % (1940079)Time elapsed: 2.760 s % 143.23/21.01 % (1940079)Peak memory usage: 117 MB % 143.23/21.01 % (1940079)Instructions burned: 4851 (million) % 143.23/21.01 % (1940083)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=336825405:i=319:kws=precedence:fsr=off_2918 on theBenchmark for (2918ds/319Mi) % 143.23/21.01 % (1940083)Instruction limit reached! % 143.23/21.01 % (1940083)------------------------------ % 143.23/21.01 % (1940083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.23/21.01 % (1940083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/21.01 % (1940083)CaDiCaL version: 2.1.3 % 143.23/21.01 % (1940083)Termination reason: Instruction limit % 143.23/21.01 % (1940083)Termination phase: Saturation % 143.23/21.01 % (1940083)Time elapsed: 0.173 s % 143.23/21.01 % (1940083)Peak memory usage: 92 MB % 143.23/21.01 % (1940083)Instructions burned: 321 (million) % 143.23/21.01 % (1940085)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2134671521:i=2064:ep=RST_2915 on theBenchmark for (2915ds/2064Mi) % 143.23/21.01 % (1940056)Instruction limit reached! % 143.23/21.01 % (1940056)------------------------------ % 143.23/21.01 % (1940056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.23/21.01 % (1940056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/21.01 % (1940056)CaDiCaL version: 2.1.3 % 143.23/21.01 % (1940056)Termination reason: Instruction limit % 143.23/21.01 % (1940056)Termination phase: Saturation % 143.23/21.01 % (1940056)Time elapsed: 7.269 s % 143.23/21.01 % (1940056)Peak memory usage: 170 MB % 143.23/21.01 % (1940056)Instructions burned: 13193 (million) % 143.23/21.01 % (1940087)dis-1011_128_sil=32000:random_seed=1052549099:i=3706:ep=RST:av=off_2910 on theBenchmark for (2910ds/3706Mi) % 143.23/21.01 % (1940085)Instruction limit reached! % 143.23/21.01 % (1940085)------------------------------ % 143.23/21.01 % (1940085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.23/21.01 % (1940085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/21.01 % (1940085)CaDiCaL version: 2.1.3 % 143.23/21.01 % (1940085)Termination reason: Instruction limit % 143.23/21.01 % (1940085)Termination phase: Saturation % 143.23/21.01 % (1940085)Time elapsed: 1.078 s % 143.23/21.01 % (1940085)Peak memory usage: 108 MB % 143.23/21.01 % (1940085)Instructions burned: 2066 (million) % 143.23/21.01 % (1940089)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=966013866:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2902 on theBenchmark for (2902ds/757Mi) % 143.23/21.01 % (1940089)Instruction limit reached! % 143.23/21.01 % (1940089)------------------------------ % 143.23/21.01 % (1940089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.23/21.01 % (1940089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/21.01 % (1940089)CaDiCaL version: 2.1.3 % 143.23/21.01 % (1940089)Termination reason: Instruction limit % 143.23/21.01 % (1940089)Termination phase: Saturation % 143.23/21.01 % (1940089)Time elapsed: 0.336 s % 143.23/21.01 % (1940089)Peak memory usage: 93 MB % 143.23/21.01 % (1940089)Instructions burned: 757 (million) % 143.23/21.01 % (1940087)Instruction limit reached! % 143.23/21.01 % (1940087)------------------------------ % 143.23/21.01 % (1940087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.23/21.01 % (1940087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/21.01 % (1940087)CaDiCaL version: 2.1.3 % 143.23/21.01 % (1940087)Termination reason: Instruction limit % 143.23/21.01 % (1940087)Termination phase: Saturation % 143.23/21.01 % (1940087)Time elapsed: 1.226 s % 143.23/21.01 % (1940087)Peak memory usage: 89 MB % 143.23/21.01 % (1940087)Instructions burned: 3708 (million) % 143.23/21.01 % (1940091)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4202586129:i=13913:ss=axioms:sgt=8_2897 on theBenchmark for (2897ds/13913Mi) % 143.23/21.01 % (1940092)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=136627721:i=9925:aac=none_2897 on theBenchmark for (2897ds/9925Mi) % 143.23/21.01 % (1940071)Instruction limit reached! % 143.23/21.01 % (1940071)------------------------------ % 143.23/21.01 % (1940071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.23/21.01 % (1940071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.23/21.01 % (1940071)CaDiCaL version: 2.1.3 % 169.47/24.51 % (1940071)Termination reason: Instruction limit % 169.47/24.51 % (1940071)Termination phase: Saturation % 169.47/24.51 % (1940071)Time elapsed: 7.756 s % 169.47/24.51 % (1940071)Peak memory usage: 191 MB % 169.47/24.51 % (1940071)Instructions burned: 14156 (million) % 169.47/24.51 % (1940095)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2596823790:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2891 on theBenchmark for (2891ds/2479Mi) % 169.47/24.51 % (1940095)Instruction limit reached! % 169.47/24.51 % (1940095)------------------------------ % 169.47/24.51 % (1940095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.47/24.51 % (1940095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.51 % (1940095)CaDiCaL version: 2.1.3 % 169.47/24.51 % (1940095)Termination reason: Instruction limit % 169.47/24.51 % (1940095)Termination phase: Saturation % 169.47/24.51 % (1940095)Time elapsed: 0.877 s % 169.47/24.51 % (1940095)Peak memory usage: 90 MB % 169.47/24.51 % (1940095)Instructions burned: 2480 (million) % 169.47/24.51 % (1940097)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=608647654:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2881 on theBenchmark for (2881ds/440Mi) % 169.47/24.51 % (1940097)Instruction limit reached! % 169.47/24.51 % (1940097)------------------------------ % 169.47/24.51 % (1940097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.47/24.51 % (1940097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.51 % (1940097)CaDiCaL version: 2.1.3 % 169.47/24.51 % (1940097)Termination reason: Instruction limit % 169.47/24.51 % (1940097)Termination phase: Saturation % 169.47/24.51 % (1940097)Time elapsed: 0.248 s % 169.47/24.51 % (1940097)Peak memory usage: 92 MB % 169.47/24.51 % (1940097)Instructions burned: 440 (million) % 169.47/24.51 % (1940099)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1781630490:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2876 on theBenchmark for (2876ds/11145Mi) % 169.47/24.51 % (1940081)Instruction limit reached! % 169.47/24.51 % (1940081)------------------------------ % 169.47/24.51 % (1940081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.47/24.51 % (1940081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.51 % (1940081)CaDiCaL version: 2.1.3 % 169.47/24.51 % (1940081)Termination reason: Instruction limit % 169.47/24.51 % (1940081)Termination phase: Saturation % 169.47/24.51 % (1940081)Time elapsed: 7.222 s % 169.47/24.51 % (1940081)Peak memory usage: 226 MB % 169.47/24.51 % (1940081)Instructions burned: 12112 (million) % 169.47/24.51 % (1940101)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=3193420443:cts=off:i=3034:av=off:er=known:fsd=on_2867 on theBenchmark for (2867ds/3034Mi) % 169.47/24.51 % (1940101)Instruction limit reached! % 169.47/24.51 % (1940101)------------------------------ % 169.47/24.51 % (1940101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.47/24.51 % (1940101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.51 % (1940101)CaDiCaL version: 2.1.3 % 169.47/24.51 % (1940101)Termination reason: Instruction limit % 169.47/24.51 % (1940101)Termination phase: Saturation % 169.47/24.51 % (1940101)Time elapsed: 1.464 s % 169.47/24.51 % (1940101)Peak memory usage: 139 MB % 169.47/24.51 % (1940101)Instructions burned: 3036 (million) % 169.47/24.52 % (1940255)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1054319933:st=2:s2a=on:i=524:s2at=2:ss=axioms_2850 on theBenchmark for (2850ds/524Mi) % 169.47/24.52 % (1940255)Instruction limit reached! % 169.47/24.52 % (1940255)------------------------------ % 169.47/24.52 % (1940255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.47/24.52 % (1940255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.47/24.52 % (1940255)CaDiCaL version: 2.1.3 % 169.47/24.52 % (1940255)Termination reason: Instruction limit % 169.47/24.52 % (1940255)Termination phase: Saturation % 169.47/24.52 % (1940255)Time elapsed: 0.233 s % 169.47/24.52 % (1940255)Peak memory usage: 92 MB % 169.47/24.52 % (1940255)Instructions burned: 525 (million) % 169.47/24.52 % (1940257)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=295909111:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2846 on theBenchmark for (2846ds/1016Mi) % 169.47/24.52 % (1940257)Instruction limit reached! % 169.47/24.52 % (1940257)------------------------------ % 169.47/24.52 % (1940257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.93/26.73 % (1940257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.93/26.73 % (1940257)CaDiCaL version: 2.1.3 % 184.93/26.73 % (1940257)Termination reason: Instruction limit % 184.93/26.73 % (1940257)Termination phase: Saturation % 184.93/26.73 % (1940257)Time elapsed: 0.468 s % 184.93/26.73 % (1940257)Peak memory usage: 93 MB % 184.93/26.73 % (1940257)Instructions burned: 1016 (million) % 184.93/26.73 % (1940092)Instruction limit reached! % 184.93/26.73 % (1940092)------------------------------ % 184.93/26.73 % (1940092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.93/26.73 % (1940092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.93/26.73 % (1940092)CaDiCaL version: 2.1.3 % 184.93/26.73 % (1940092)Termination reason: Instruction limit % 184.93/26.73 % (1940092)Termination phase: Saturation % 184.93/26.73 % (1940092)Time elapsed: 5.665 s % 184.93/26.73 % (1940092)Peak memory usage: 180 MB % 184.93/26.73 % (1940092)Instructions burned: 9926 (million) % 184.93/26.73 % (1940259)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3545698737:i=14123:bd=preordered:ins=4_2840 on theBenchmark for (2840ds/14123Mi) % 184.93/26.73 % (1940261)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=669318423:i=5781:kws=precedence:bd=all:rawr=on_2838 on theBenchmark for (2838ds/5781Mi) % 184.93/26.73 % (1940091)Instruction limit reached! % 184.93/26.73 % (1940091)------------------------------ % 184.93/26.73 % (1940091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.93/26.73 % (1940091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.93/26.73 % (1940091)CaDiCaL version: 2.1.3 % 184.93/26.73 % (1940091)Termination reason: Instruction limit % 184.93/26.73 % (1940091)Termination phase: Saturation % 184.93/26.73 % (1940091)Time elapsed: 8.233 s % 184.93/26.73 % (1940091)Peak memory usage: 231 MB % 184.93/26.73 % (1940091)Instructions burned: 13915 (million) % 184.93/26.73 % (1940263)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=2126968588:i=2448:gtgl=5:bd=preordered:gtg=all_2813 on theBenchmark for (2813ds/2448Mi) % 184.93/26.73 % (1940099)Instruction limit reached! % 184.93/26.73 % (1940099)------------------------------ % 184.93/26.73 % (1940099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.93/26.73 % (1940099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.93/26.73 % (1940099)CaDiCaL version: 2.1.3 % 184.93/26.73 % (1940099)Termination reason: Instruction limit % 184.93/26.73 % (1940099)Termination phase: Saturation % 184.93/26.73 % (1940099)Time elapsed: 7.268 s % 184.93/26.73 % (1940099)Peak memory usage: 197 MB % 184.93/26.73 % (1940099)Instructions burned: 11146 (million) % 184.93/26.73 % (1940265)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2293248915:i=3223:kws=precedence:fgj=on:av=off_2802 on theBenchmark for (2802ds/3223Mi) % 184.93/26.73 % (1940261)Instruction limit reached! % 184.93/26.73 % (1940261)------------------------------ % 184.93/26.73 % (1940261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.93/26.73 % (1940261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.93/26.73 % (1940261)CaDiCaL version: 2.1.3 % 184.93/26.73 % (1940261)Termination reason: Instruction limit % 184.93/26.73 % (1940261)Termination phase: Saturation % 184.93/26.73 % (1940261)Time elapsed: 3.738 s % 184.93/26.73 % (1940261)Peak memory usage: 141 MB % 184.93/26.73 % (1940261)Instructions burned: 5781 (million) % 184.93/26.73 % (1940263)Instruction limit reached! % 184.93/26.73 % (1940263)------------------------------ % 184.93/26.73 % (1940263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 184.93/26.73 % (1940263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 184.93/26.73 % (1940263)CaDiCaL version: 2.1.3 % 184.93/26.73 % (1940263)Termination reason: Instruction limit % 184.93/26.73 % (1940263)Termination phase: Saturation % 184.93/26.73 % (1940263)Time elapsed: 1.361 s % 184.93/26.73 % (1940263)Peak memory usage: 143 MB % 184.93/26.73 % (1940263)Instructions burned: 2449 (million) % 184.93/26.73 % (1940267)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1396082727:st=5.6:i=2033:sd=3:ss=axioms_2799 on theBenchmark for (2799ds/2033Mi) % 184.93/26.73 % (1940268)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3919205548:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2798 on theBenchmark for (2798ds/2055Mi) % 237.17/34.07 % (1940265)Instruction limit reached! % 237.17/34.07 % (1940265)------------------------------ % 237.17/34.07 % (1940265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.17/34.07 % (1940265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.17/34.07 % (1940265)CaDiCaL version: 2.1.3 % 237.17/34.07 % (1940265)Termination reason: Instruction limit % 237.17/34.07 % (1940265)Termination phase: Saturation % 237.17/34.07 % (1940265)Time elapsed: 1.408 s % 237.17/34.07 % (1940265)Peak memory usage: 147 MB % 237.17/34.07 % (1940265)Instructions burned: 3225 (million) % 237.17/34.07 % (1940267)Instruction limit reached! % 237.17/34.07 % (1940267)------------------------------ % 237.17/34.07 % (1940267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.17/34.07 % (1940267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.17/34.07 % (1940267)CaDiCaL version: 2.1.3 % 237.17/34.07 % (1940267)Termination reason: Instruction limit % 237.17/34.07 % (1940267)Termination phase: Saturation % 237.17/34.07 % (1940267)Time elapsed: 1.199 s % 237.17/34.07 % (1940267)Peak memory usage: 137 MB % 237.17/34.07 % (1940267)Instructions burned: 2035 (million) % 237.17/34.07 % (1940271)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=971505107:i=21611:sd=3:ss=axioms_2786 on theBenchmark for (2786ds/21611Mi) % 237.17/34.07 % (1940272)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=4190686091:i=4835:sd=13:ss=axioms:sgt=23_2785 on theBenchmark for (2785ds/4835Mi) % 237.17/34.07 % (1940268)Instruction limit reached! % 237.17/34.07 % (1940268)------------------------------ % 237.17/34.07 % (1940268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.17/34.07 % (1940268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.17/34.07 % (1940268)CaDiCaL version: 2.1.3 % 237.17/34.07 % (1940268)Termination reason: Instruction limit % 237.17/34.07 % (1940268)Termination phase: Saturation % 237.17/34.07 % (1940268)Time elapsed: 1.294 s % 237.17/34.07 % (1940268)Peak memory usage: 135 MB % 237.17/34.07 % (1940268)Instructions burned: 2057 (million) % 237.17/34.07 % (1940275)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=4181645620:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2783 on theBenchmark for (2783ds/797Mi) % 237.17/34.07 % (1940275)Instruction limit reached! % 237.17/34.07 % (1940275)------------------------------ % 237.17/34.07 % (1940275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.17/34.07 % (1940275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.17/34.07 % (1940275)CaDiCaL version: 2.1.3 % 237.17/34.07 % (1940275)Termination reason: Instruction limit % 237.17/34.07 % (1940275)Termination phase: Saturation % 237.17/34.07 % (1940275)Time elapsed: 0.503 s % 237.17/34.07 % (1940275)Peak memory usage: 96 MB % 237.17/34.07 % (1940275)Instructions burned: 797 (million) % 237.17/34.07 % (1940277)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2478897867:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2776 on theBenchmark for (2776ds/2326Mi) % 237.17/34.07 % (1940277)Instruction limit reached! % 237.17/34.07 % (1940277)------------------------------ % 237.17/34.07 % (1940277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.17/34.07 % (1940277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.17/34.07 % (1940277)CaDiCaL version: 2.1.3 % 237.17/34.07 % (1940277)Termination reason: Instruction limit % 237.17/34.07 % (1940277)Termination phase: Saturation % 237.17/34.07 % (1940277)Time elapsed: 0.785 s % 237.17/34.07 % (1940277)Peak memory usage: 90 MB % 237.17/34.07 % (1940277)Instructions burned: 2326 (million) % 237.17/34.07 % (1940280)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=483592358:i=6038:nm=6_2767 on theBenchmark for (2767ds/6038Mi) % 237.17/34.07 % (1940259)Instruction limit reached! % 237.17/34.07 % (1940259)------------------------------ % 237.17/34.07 % (1940259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.17/34.07 % (1940259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.17/34.07 % (1940259)CaDiCaL version: 2.1.3 % 237.17/34.07 % (1940259)Termination reason: Instruction limit % 237.17/34.07 % (1940259)Termination phase: SaturatioTerminated %------------------------------------------------------------------------------