%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : CAT024+4 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/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 09:36:41 AM UTC 2026 % Result : Timeout 300.35s 44.43s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : CAT024+4 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.17 % Computer : n015.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 21:19:56 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.21 Running first-order theorem proving % 0.07/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 % 16.22/4.42 % (3038377)Detected formulas, will run a generic FOF schedule. % 16.22/4.42 % (3038385)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=77831430:i=109:sd=1:ins=1:gsp=on:ss=axioms_2982 on theBenchmark for (2982ds/109Mi) % 16.22/4.42 % (3038384)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=2993910380:i=141695:sd=1:nm=32:gsp=on:ss=included_2982 on theBenchmark for (2982ds/141695Mi) % 16.22/4.42 % (3038383)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=3202395844:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2982 on theBenchmark for (2982ds/134677Mi) % 16.22/4.42 % (3038382)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=3188672056:i=141193_2982 on theBenchmark for (2982ds/141193Mi) % 16.22/4.42 % (3038386)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=530339589:i=119:av=off:ss=axioms_2982 on theBenchmark for (2982ds/119Mi) % 16.22/4.42 % (3038387)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1419742016:s2a=on:i=139:gtg=position_2982 on theBenchmark for (2982ds/139Mi) % 16.22/4.42 % (3038385)Instruction limit reached! % 16.22/4.42 % (3038385)------------------------------ % 16.22/4.42 % (3038385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/4.42 % (3038385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/4.42 % (3038385)CaDiCaL version: 2.1.3 % 16.22/4.42 % (3038385)Termination reason: Instruction limit % 16.22/4.42 % (3038385)Termination phase: SInE selection % 16.22/4.42 % (3038385)Time elapsed: 0.051 s % 16.22/4.42 % (3038385)Peak memory usage: 127 MB % 16.22/4.42 % (3038385)Instructions burned: 110 (million) % 16.22/4.42 % (3038388)dis-21_1_sil=8000:lcm=predicate:random_seed=1598447022:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2982 on theBenchmark for (2982ds/129Mi) % 16.22/4.42 % (3038387)Instruction limit reached! % 16.22/4.42 % (3038387)------------------------------ % 16.22/4.42 % (3038387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/4.42 % (3038387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/4.42 % (3038387)CaDiCaL version: 2.1.3 % 16.22/4.42 % (3038387)Termination reason: Instruction limit % 16.22/4.42 % (3038387)Termination phase: Property scanning % 16.22/4.42 % (3038387)Time elapsed: 0.061 s % 16.22/4.42 % (3038387)Peak memory usage: 127 MB % 16.22/4.42 % (3038387)Instructions burned: 141 (million) % 16.22/4.42 % (3038386)Instruction limit reached! % 16.22/4.42 % (3038386)------------------------------ % 16.22/4.42 % (3038386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/4.42 % (3038386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/4.42 % (3038386)CaDiCaL version: 2.1.3 % 16.22/4.42 % (3038386)Termination reason: Instruction limit % 16.22/4.42 % (3038386)Termination phase: SInE selection % 16.22/4.42 % (3038386)Time elapsed: 0.094 s % 16.22/4.42 % (3038386)Peak memory usage: 126 MB % 16.22/4.42 % (3038386)Instructions burned: 120 (million) % 16.22/4.42 % (3038388)Instruction limit reached! % 16.22/4.42 % (3038388)------------------------------ % 16.22/4.42 % (3038388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/4.42 % (3038388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/4.42 % (3038388)CaDiCaL version: 2.1.3 % 16.22/4.42 % (3038388)Termination reason: Instruction limit % 16.22/4.42 % (3038388)Termination phase: SInE selection % 16.22/4.42 % (3038388)Time elapsed: 0.095 s % 16.22/4.42 % (3038388)Peak memory usage: 127 MB % 16.22/4.42 % (3038388)Instructions burned: 129 (million) % 16.22/4.42 % (3038396)lrs+10_1_sil=8000:sp=occurrence:random_seed=2681785864:i=285:sd=3:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/285Mi) % 16.22/4.42 % (3038397)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1229521428:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/157Mi) % 16.22/4.42 % (3038396)Instruction limit reached! % 16.22/4.42 % (3038396)------------------------------ % 16.22/4.42 % (3038396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.22/4.42 % (3038396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.22/4.42 % (3038396)CaDiCaL version: 2.1.3 % 16.22/4.42 % (3038396)Termination reason: Instruction limit % 21.53/5.15 % (3038396)Termination phase: Saturation % 21.53/5.15 % (3038396)Time elapsed: 0.124 s % 21.53/5.15 % (3038396)Peak memory usage: 132 MB % 21.53/5.15 % (3038396)Instructions burned: 287 (million) % 21.53/5.15 % (3038399)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=3885453646:s2a=on:i=248:s2at=1.23:gtg=position_2979 on theBenchmark for (2979ds/248Mi) % 21.53/5.15 % (3038398)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2977637582:i=325:sd=1:ss=axioms:sgt=32_2979 on theBenchmark for (2979ds/325Mi) % 21.53/5.15 % (3038397)Instruction limit reached! % 21.53/5.15 % (3038397)------------------------------ % 21.53/5.15 % (3038397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.53/5.15 % (3038397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.53/5.15 % (3038397)CaDiCaL version: 2.1.3 % 21.53/5.15 % (3038397)Termination reason: Instruction limit % 21.53/5.15 % (3038397)Termination phase: Property scanning % 21.53/5.15 % (3038397)Time elapsed: 0.070 s % 21.53/5.15 % (3038397)Peak memory usage: 127 MB % 21.53/5.15 % (3038397)Instructions burned: 158 (million) % 21.53/5.15 % (3038399)Instruction limit reached! % 21.53/5.15 % (3038399)------------------------------ % 21.53/5.15 % (3038399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.53/5.15 % (3038399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.53/5.15 % (3038399)CaDiCaL version: 2.1.3 % 21.53/5.15 % (3038399)Termination reason: Instruction limit % 21.53/5.15 % (3038399)Termination phase: Property scanning % 21.53/5.15 % (3038399)Time elapsed: 0.107 s % 21.53/5.15 % (3038399)Peak memory usage: 127 MB % 21.53/5.15 % (3038399)Instructions burned: 249 (million) % 21.53/5.15 % (3038404)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1776979213:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2978 on theBenchmark for (2978ds/294Mi) % 21.53/5.15 % (3038405)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=168138082:i=2350_2977 on theBenchmark for (2977ds/2350Mi) % 21.53/5.15 % (3038404)Instruction limit reached! % 21.53/5.15 % (3038404)------------------------------ % 21.53/5.15 % (3038404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.53/5.15 % (3038404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.53/5.15 % (3038404)CaDiCaL version: 2.1.3 % 21.53/5.15 % (3038404)Termination reason: Instruction limit % 21.53/5.15 % (3038404)Termination phase: Preprocessing 3 % 21.53/5.15 % (3038404)Time elapsed: 0.122 s % 21.53/5.15 % (3038404)Peak memory usage: 130 MB % 21.53/5.15 % (3038404)Instructions burned: 294 (million) % 21.53/5.15 % (3038398)Instruction limit reached! % 21.53/5.15 % (3038398)------------------------------ % 21.53/5.15 % (3038398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.53/5.15 % (3038398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.53/5.15 % (3038398)CaDiCaL version: 2.1.3 % 21.53/5.15 % (3038398)Termination reason: Instruction limit % 21.53/5.15 % (3038398)Termination phase: Saturation % 21.53/5.15 % (3038398)Time elapsed: 0.246 s % 21.53/5.15 % (3038398)Peak memory usage: 133 MB % 21.53/5.15 % (3038398)Instructions burned: 325 (million) % 21.53/5.15 % (3038406)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1936530431:cts=off:i=113:fsr=off:ss=included:sgt=4_2977 on theBenchmark for (2977ds/113Mi) % 21.53/5.15 % (3038409)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=841208625:i=127:av=off:fsr=off:sup=off_2975 on theBenchmark for (2975ds/127Mi) % 21.53/5.15 % (3038406)Instruction limit reached! % 21.53/5.15 % (3038406)------------------------------ % 21.53/5.15 % (3038406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.53/5.15 % (3038406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.53/5.15 % (3038406)CaDiCaL version: 2.1.3 % 21.53/5.15 % (3038406)Termination reason: Instruction limit % 21.53/5.15 % (3038406)Termination phase: SInE selection % 21.53/5.15 % (3038406)Time elapsed: 0.091 s % 21.53/5.15 % (3038406)Peak memory usage: 127 MB % 21.53/5.15 % (3038406)Instructions burned: 113 (million) % 21.53/5.15 % (3038410)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4058310652:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2975 on theBenchmark for (2975ds/114Mi) % 21.53/5.15 % (3038409)Instruction limit reached! % 21.53/5.15 % (3038409)------------------------------ % 21.53/5.15 % (3038409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.61/11.24 % (3038409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/11.24 % (3038409)CaDiCaL version: 2.1.3 % 64.61/11.24 % (3038409)Termination reason: Instruction limit % 64.61/11.24 % (3038409)Termination phase: Preprocessing 1 % 64.61/11.24 % (3038409)Time elapsed: 0.058 s % 64.61/11.24 % (3038409)Peak memory usage: 128 MB % 64.61/11.24 % (3038409)Instructions burned: 129 (million) % 64.61/11.24 % (3038410)Instruction limit reached! % 64.61/11.24 % (3038410)------------------------------ % 64.61/11.24 % (3038410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.61/11.24 % (3038410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/11.24 % (3038410)CaDiCaL version: 2.1.3 % 64.61/11.24 % (3038410)Termination reason: Instruction limit % 64.61/11.24 % (3038410)Termination phase: Property scanning % 64.61/11.24 % (3038410)Time elapsed: 0.051 s % 64.61/11.24 % (3038410)Peak memory usage: 127 MB % 64.61/11.24 % (3038410)Instructions burned: 115 (million) % 64.61/11.24 % (3038413)lrs+10_1_sil=8000:sp=occurrence:random_seed=3698814740:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi) % 64.61/11.24 % (3038415)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=910043314:i=437:sd=1:aac=none:ss=included_2973 on theBenchmark for (2973ds/437Mi) % 64.61/11.24 % (3038416)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4018360451:i=5202:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/5202Mi) % 64.61/11.24 % (3038415)Refutation not found, incomplete strategy % 64.61/11.24 % (3038415)------------------------------ % 64.61/11.24 % (3038415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.61/11.24 % (3038415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/11.24 % (3038415)CaDiCaL version: 2.1.3 % 64.61/11.24 % (3038415)Termination reason: Refutation not found, incomplete strategy % 64.61/11.24 % (3038415)Time elapsed: 0.117 s % 64.61/11.24 % (3038415)Peak memory usage: 133 MB % 64.61/11.24 % (3038415)Instructions burned: 265 (million) % 64.61/11.24 % (3038415)------------------------------ % 64.61/11.24 % (3038415)------------------------------ % 64.61/11.24 % (3038420)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=252651618:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2969 on theBenchmark for (2969ds/134Mi) % 64.61/11.24 % (3038420)Instruction limit reached! % 64.61/11.24 % (3038420)------------------------------ % 64.61/11.24 % (3038420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.61/11.24 % (3038420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/11.24 % (3038420)CaDiCaL version: 2.1.3 % 64.61/11.24 % (3038420)Termination reason: Instruction limit % 64.61/11.24 % (3038420)Termination phase: SInE selection % 64.61/11.24 % (3038420)Time elapsed: 0.059 s % 64.61/11.24 % (3038420)Peak memory usage: 127 MB % 64.61/11.24 % (3038420)Instructions burned: 136 (million) % 64.61/11.24 % (3038413)Instruction limit reached! % 64.61/11.24 % (3038413)------------------------------ % 64.61/11.24 % (3038413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.61/11.24 % (3038413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/11.24 % (3038413)CaDiCaL version: 2.1.3 % 64.61/11.24 % (3038413)Termination reason: Instruction limit % 64.61/11.24 % (3038413)Termination phase: Property scanning % 64.61/11.24 % (3038413)Time elapsed: 0.580 s % 64.61/11.24 % (3038413)Peak memory usage: 149 MB % 64.61/11.24 % (3038413)Instructions burned: 909 (million) % 64.61/11.24 % (3038422)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=106241658:st=8:i=592:sd=3:ep=RST:ss=axioms_2967 on theBenchmark for (2967ds/592Mi) % 64.61/11.24 % (3038423)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=692841533:st=3:i=13193:sd=3:ss=axioms_2966 on theBenchmark for (2966ds/13193Mi) % 64.61/11.24 % (3038422)Instruction limit reached! % 64.61/11.24 % (3038422)------------------------------ % 64.61/11.24 % (3038422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 64.61/11.24 % (3038422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 64.61/11.24 % (3038422)CaDiCaL version: 2.1.3 % 64.61/11.24 % (3038422)Termination reason: Instruction limit % 64.61/11.24 % (3038422)Termination phase: Preprocessing 3 % 64.61/11.24 % (3038422)Time elapsed: 0.272 s % 64.61/11.24 % (3038422)Peak memory usage: 146 MB % 64.61/11.24 % (3038422)Instructions burned: 593 (million) % 64.61/11.24 % (3038426)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=3448489272:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/125Mi) % 83.04/13.86 % (3038426)Instruction limit reached! % 83.04/13.86 % (3038426)------------------------------ % 83.04/13.86 % (3038426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/13.86 % (3038426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/13.86 % (3038426)CaDiCaL version: 2.1.3 % 83.04/13.86 % (3038426)Termination reason: Instruction limit % 83.04/13.86 % (3038426)Termination phase: Property scanning % 83.04/13.86 % (3038426)Time elapsed: 0.032 s % 83.04/13.86 % (3038426)Peak memory usage: 127 MB % 83.04/13.86 % (3038426)Instructions burned: 129 (million) % 83.04/13.86 % (3038405)Instruction limit reached! % 83.04/13.86 % (3038405)------------------------------ % 83.04/13.86 % (3038405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/13.86 % (3038405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/13.86 % (3038405)CaDiCaL version: 2.1.3 % 83.04/13.86 % (3038405)Termination reason: Instruction limit % 83.04/13.86 % (3038405)Termination phase: Property scanning % 83.04/13.86 % (3038405)Time elapsed: 1.421 s % 83.04/13.86 % (3038405)Peak memory usage: 208 MB % 83.04/13.86 % (3038405)Instructions burned: 2351 (million) % 83.04/13.86 % (3038428)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4196642356:i=134:gtgl=5:slsql=off:gtg=exists_sym_2961 on theBenchmark for (2961ds/134Mi) % 83.04/13.86 % (3038428)Instruction limit reached! % 83.04/13.86 % (3038428)------------------------------ % 83.04/13.86 % (3038428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/13.86 % (3038428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/13.86 % (3038428)CaDiCaL version: 2.1.3 % 83.04/13.86 % (3038428)Termination reason: Instruction limit % 83.04/13.86 % (3038428)Termination phase: Property scanning % 83.04/13.86 % (3038428)Time elapsed: 0.034 s % 83.04/13.86 % (3038428)Peak memory usage: 127 MB % 83.04/13.86 % (3038428)Instructions burned: 136 (million) % 83.04/13.86 % (3038429)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3313476096:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/141Mi) % 83.04/13.86 % (3038431)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1271890148:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2960 on theBenchmark for (2960ds/431Mi) % 83.04/13.86 % (3038429)Instruction limit reached! % 83.04/13.86 % (3038429)------------------------------ % 83.04/13.86 % (3038429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/13.86 % (3038429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/13.86 % (3038429)CaDiCaL version: 2.1.3 % 83.04/13.86 % (3038429)Termination reason: Instruction limit % 83.04/13.86 % (3038429)Termination phase: SInE selection % 83.04/13.86 % (3038429)Time elapsed: 0.113 s % 83.04/13.86 % (3038429)Peak memory usage: 127 MB % 83.04/13.86 % (3038429)Instructions burned: 141 (million) % 83.04/13.86 % (3038431)Instruction limit reached! % 83.04/13.86 % (3038431)------------------------------ % 83.04/13.86 % (3038431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/13.86 % (3038431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.04/13.86 % (3038431)CaDiCaL version: 2.1.3 % 83.04/13.86 % (3038431)Termination reason: Instruction limit % 83.04/13.86 % (3038431)Termination phase: Saturation % 83.04/13.86 % (3038431)Time elapsed: 0.173 s % 83.04/13.86 % (3038431)Peak memory usage: 135 MB % 83.04/13.86 % (3038431)Instructions burned: 434 (million) % 83.04/13.86 % (3038434)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=3084428104:i=6060:aac=none:ins=25_2958 on theBenchmark for (2958ds/6060Mi) % 83.04/13.86 % (3038438)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=1357938426:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2957 on theBenchmark for (2957ds/150Mi) % 83.04/13.86 % (3038438)Instruction limit reached! % 83.04/13.86 % (3038438)------------------------------ % 83.04/13.86 % (3038438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.04/13.86 % (3038438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.31/17.82 % (3038438)CaDiCaL version: 2.1.3 % 111.31/17.82 % (3038438)Termination reason: Instruction limit % 111.31/17.82 % (3038438)Termination phase: SInE selection % 111.31/17.82 % (3038438)Time elapsed: 0.075 s % 111.31/17.82 % (3038438)Peak memory usage: 127 MB % 111.31/17.82 % (3038438)Instructions burned: 152 (million) % 111.31/17.82 % (3038464)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2839251935:i=14155:bd=all_2955 on theBenchmark for (2955ds/14155Mi) % 111.31/17.82 % (3038416)Instruction limit reached! % 111.31/17.82 % (3038416)------------------------------ % 111.31/17.82 % (3038416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.31/17.82 % (3038416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.31/17.82 % (3038416)CaDiCaL version: 2.1.3 % 111.31/17.82 % (3038416)Termination reason: Instruction limit % 111.31/17.82 % (3038416)Termination phase: Saturation % 111.31/17.82 % (3038416)Time elapsed: 3.842 s % 111.31/17.82 % (3038416)Peak memory usage: 443 MB % 111.31/17.82 % (3038416)Instructions burned: 5202 (million) % 111.31/17.82 % (3038715)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=327595701:i=667:av=off:fsr=off_2933 on theBenchmark for (2933ds/667Mi) % 111.31/17.82 % (3038715)Instruction limit reached! % 111.31/17.82 % (3038715)------------------------------ % 111.31/17.82 % (3038715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.31/17.82 % (3038715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.31/17.82 % (3038715)CaDiCaL version: 2.1.3 % 111.31/17.82 % (3038715)Termination reason: Instruction limit % 111.31/17.82 % (3038715)Termination phase: NewCNF % 111.31/17.82 % (3038715)Time elapsed: 0.550 s % 111.31/17.82 % (3038715)Peak memory usage: 172 MB % 111.31/17.82 % (3038715)Instructions burned: 667 (million) % 111.31/17.82 % (3038717)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=4281103182:s2a=on:i=185:s2at=1.8:fdi=4_2925 on theBenchmark for (2925ds/185Mi) % 111.31/17.82 % (3038717)Instruction limit reached! % 111.31/17.82 % (3038717)------------------------------ % 111.31/17.82 % (3038717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.31/17.82 % (3038717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.31/17.82 % (3038717)CaDiCaL version: 2.1.3 % 111.31/17.82 % (3038717)Termination reason: Instruction limit % 111.31/17.82 % (3038717)Termination phase: SInE selection % 111.31/17.82 % (3038717)Time elapsed: 0.139 s % 111.31/17.82 % (3038717)Peak memory usage: 127 MB % 111.31/17.82 % (3038717)Instructions burned: 186 (million) % 111.31/17.82 % (3038719)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2513881998:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2922 on theBenchmark for (2922ds/193Mi) % 111.31/17.82 % (3038434)Instruction limit reached! % 111.31/17.82 % (3038434)------------------------------ % 111.31/17.82 % (3038434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.31/17.82 % (3038434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.31/17.82 % (3038434)CaDiCaL version: 2.1.3 % 111.31/17.82 % (3038434)Termination reason: Instruction limit % 111.31/17.82 % (3038434)Termination phase: Property scanning % 111.31/17.82 % (3038434)Time elapsed: 3.710 s % 111.31/17.82 % (3038434)Peak memory usage: 227 MB % 111.31/17.82 % (3038434)Instructions burned: 6060 (million) % 111.31/17.82 % (3038719)Instruction limit reached! % 111.31/17.82 % (3038719)------------------------------ % 111.31/17.82 % (3038719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.31/17.82 % (3038719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.31/17.82 % (3038719)CaDiCaL version: 2.1.3 % 111.31/17.82 % (3038719)Termination reason: Instruction limit % 111.31/17.82 % (3038719)Termination phase: SInE selection % 111.31/17.82 % (3038719)Time elapsed: 0.168 s % 111.31/17.82 % (3038719)Peak memory usage: 127 MB % 111.31/17.82 % (3038719)Instructions burned: 193 (million) % 111.31/17.82 % (3038721)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1441051917:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2919 on theBenchmark for (2919ds/4850Mi) % 111.31/17.82 % (3038722)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1914623609:i=12111:sd=1:ss=included_2918 on theBenchmark for (2918ds/12111Mi) % 111.31/17.82 % (3038721)Instruction limit reached! % 111.31/17.82 % (3038721)------------------------------ % 133.18/21.04 % (3038721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.18/21.04 % (3038721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.18/21.04 % (3038721)CaDiCaL version: 2.1.3 % 133.18/21.04 % (3038721)Termination reason: Instruction limit % 133.18/21.04 % (3038721)Termination phase: Property scanning % 133.18/21.04 % (3038721)Time elapsed: 2.394 s % 133.18/21.04 % (3038721)Peak memory usage: 198 MB % 133.18/21.04 % (3038721)Instructions burned: 4851 (million) % 133.18/21.04 % (3038423)Instruction limit reached! % 133.18/21.04 % (3038423)------------------------------ % 133.18/21.04 % (3038423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.18/21.04 % (3038423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.18/21.04 % (3038423)CaDiCaL version: 2.1.3 % 133.18/21.04 % (3038423)Termination reason: Instruction limit % 133.18/21.04 % (3038423)Termination phase: Saturation % 133.18/21.04 % (3038423)Time elapsed: 7.168 s % 133.18/21.04 % (3038423)Peak memory usage: 272 MB % 133.18/21.04 % (3038423)Instructions burned: 13193 (million) % 133.18/21.04 % (3038725)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1414926234:i=319:kws=precedence:fsr=off_2893 on theBenchmark for (2893ds/319Mi) % 133.18/21.04 % (3038726)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=633214880:i=2064:ep=RST_2893 on theBenchmark for (2893ds/2064Mi) % 133.18/21.04 % (3038725)Instruction limit reached! % 133.18/21.04 % (3038725)------------------------------ % 133.18/21.04 % (3038725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.18/21.04 % (3038725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.18/21.04 % (3038725)CaDiCaL version: 2.1.3 % 133.18/21.04 % (3038725)Termination reason: Instruction limit % 133.18/21.04 % (3038725)Termination phase: Preprocessing 2 % 133.18/21.04 % (3038725)Time elapsed: 0.271 s % 133.18/21.04 % (3038725)Peak memory usage: 138 MB % 133.18/21.04 % (3038725)Instructions burned: 320 (million) % 133.18/21.04 % (3038729)dis-1011_128_sil=32000:random_seed=2973075710:i=3706:ep=RST:av=off_2889 on theBenchmark for (2889ds/3706Mi) % 133.18/21.04 % (3038464)Instruction limit reached! % 133.18/21.04 % (3038464)------------------------------ % 133.18/21.04 % (3038464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.18/21.04 % (3038464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.18/21.04 % (3038464)CaDiCaL version: 2.1.3 % 133.18/21.04 % (3038464)Termination reason: Instruction limit % 133.18/21.04 % (3038464)Termination phase: Saturation % 133.18/21.04 % (3038464)Time elapsed: 6.793 s % 133.18/21.04 % (3038464)Peak memory usage: 1258 MB % 133.18/21.04 % (3038464)Instructions burned: 14161 (million) % 133.18/21.04 % (3038731)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2897927840:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2885 on theBenchmark for (2885ds/757Mi) % 133.18/21.04 % (3038731)Instruction limit reached! % 133.18/21.04 % (3038731)------------------------------ % 133.18/21.04 % (3038731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.18/21.04 % (3038731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.18/21.04 % (3038731)CaDiCaL version: 2.1.3 % 133.18/21.04 % (3038731)Termination reason: Instruction limit % 133.18/21.04 % (3038731)Termination phase: Saturation % 133.18/21.04 % (3038731)Time elapsed: 0.287 s % 133.18/21.04 % (3038731)Peak memory usage: 136 MB % 133.18/21.04 % (3038731)Instructions burned: 758 (million) % 133.18/21.04 % (3038733)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3572555436:i=13913:ss=axioms:sgt=8_2880 on theBenchmark for (2880ds/13913Mi) % 133.18/21.04 % (3038726)Instruction limit reached! % 133.18/21.04 % (3038726)------------------------------ % 133.18/21.04 % (3038726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.18/21.04 % (3038726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.18/21.04 % (3038726)CaDiCaL version: 2.1.3 % 133.18/21.04 % (3038726)Termination reason: Instruction limit % 133.18/21.04 % (3038726)Termination phase: Property scanning % 133.18/21.04 % (3038726)Time elapsed: 1.274 s % 133.18/21.04 % (3038726)Peak memory usage: 208 MB % 133.18/21.04 % (3038726)Instructions burned: 2066 (million) % 133.18/21.04 % (3038735)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1935505862:i=9925:aac=none_2878 on theBenchmark for (2878ds/9925Mi) % 133.18/21.04 % (3038729)Instruction limit reached! % 133.18/21.04 % (3038729)------------------------------ % 161.84/25.02 % (3038729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.84/25.02 % (3038729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.84/25.02 % (3038729)CaDiCaL version: 2.1.3 % 161.84/25.02 % (3038729)Termination reason: Instruction limit % 161.84/25.02 % (3038729)Termination phase: Property scanning % 161.84/25.02 % (3038729)Time elapsed: 1.970 s % 161.84/25.02 % (3038729)Peak memory usage: 218 MB % 161.84/25.02 % (3038729)Instructions burned: 3707 (million) % 161.84/25.02 % (3038737)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1935153580:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2867 on theBenchmark for (2867ds/2479Mi) % 161.84/25.02 % (3038737)Refutation not found, incomplete strategy % 161.84/25.02 % (3038737)------------------------------ % 161.84/25.02 % (3038737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.84/25.02 % (3038737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.84/25.02 % (3038737)CaDiCaL version: 2.1.3 % 161.84/25.02 % (3038737)Termination reason: Refutation not found, incomplete strategy % 161.84/25.02 % (3038737)Time elapsed: 0.399 s % 161.84/25.02 % (3038737)Peak memory usage: 134 MB % 161.84/25.02 % (3038737)Instructions burned: 537 (million) % 161.84/25.02 % (3038737)------------------------------ % 161.84/25.02 % (3038737)------------------------------ % 161.84/25.02 % (3038739)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=721871743:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2859 on theBenchmark for (2859ds/440Mi) % 161.84/25.02 % (3038739)Instruction limit reached! % 161.84/25.02 % (3038739)------------------------------ % 161.84/25.02 % (3038739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.84/25.02 % (3038739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.84/25.02 % (3038739)CaDiCaL version: 2.1.3 % 161.84/25.02 % (3038739)Termination reason: Instruction limit % 161.84/25.02 % (3038739)Termination phase: Property scanning % 161.84/25.02 % (3038739)Time elapsed: 0.183 s % 161.84/25.02 % (3038739)Peak memory usage: 127 MB % 161.84/25.02 % (3038739)Instructions burned: 442 (million) % 161.84/25.02 % (3038741)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1852071029:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2855 on theBenchmark for (2855ds/11145Mi) % 161.84/25.02 % (3038722)Instruction limit reached! % 161.84/25.02 % (3038722)------------------------------ % 161.84/25.02 % (3038722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.84/25.02 % (3038722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.84/25.02 % (3038722)CaDiCaL version: 2.1.3 % 161.84/25.02 % (3038722)Termination reason: Instruction limit % 161.84/25.02 % (3038722)Termination phase: Saturation % 161.84/25.02 % (3038722)Time elapsed: 6.753 s % 161.84/25.02 % (3038722)Peak memory usage: 344 MB % 161.84/25.02 % (3038722)Instructions burned: 12112 (million) % 161.84/25.02 % (3038743)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=565070847:cts=off:i=3034:av=off:er=known:fsd=on_2849 on theBenchmark for (2849ds/3034Mi) % 161.84/25.02 % (3038743)Instruction limit reached! % 161.84/25.02 % (3038743)------------------------------ % 161.84/25.02 % (3038743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.84/25.02 % (3038743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.84/25.02 % (3038743)CaDiCaL version: 2.1.3 % 161.84/25.02 % (3038743)Termination reason: Instruction limit % 161.84/25.02 % (3038743)Termination phase: Function definition elimination % 161.84/25.02 % (3038743)Time elapsed: 1.732 s % 161.84/25.02 % (3038743)Peak memory usage: 211 MB % 161.84/25.02 % (3038743)Instructions burned: 3037 (million) % 161.84/25.02 % (3038733)Instruction limit reached! % 161.84/25.02 % (3038733)------------------------------ % 161.84/25.02 % (3038733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 161.84/25.02 % (3038733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 161.84/25.02 % (3038733)CaDiCaL version: 2.1.3 % 161.84/25.02 % (3038733)Termination reason: Instruction limit % 161.84/25.02 % (3038733)Termination phase: Saturation % 161.84/25.02 % (3038733)Time elapsed: 5.037 s % 161.84/25.02 % (3038733)Peak memory usage: 281 MB % 161.84/25.02 % (3038733)Instructions burned: 13914 (million) % 161.84/25.02 % (3038745)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1699590190:st=2:s2a=on:i=524:s2at=2:ss=axioms_2830 on theBenchmark for (2830ds/524Mi) % 195.23/29.62 % (3038746)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3584127986:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2828 on theBenchmark for (2828ds/1016Mi) % 195.23/29.62 % (3038745)Instruction limit reached! % 195.23/29.62 % (3038745)------------------------------ % 195.23/29.62 % (3038745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.23/29.62 % (3038745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.23/29.62 % (3038745)CaDiCaL version: 2.1.3 % 195.23/29.62 % (3038745)Termination reason: Instruction limit % 195.23/29.62 % (3038745)Termination phase: SInE selection % 195.23/29.62 % (3038745)Time elapsed: 0.404 s % 195.23/29.62 % (3038745)Peak memory usage: 128 MB % 195.23/29.62 % (3038745)Instructions burned: 525 (million) % 195.23/29.62 % (3038746)Instruction limit reached! % 195.23/29.62 % (3038746)------------------------------ % 195.23/29.62 % (3038746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.23/29.62 % (3038746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.23/29.62 % (3038746)CaDiCaL version: 2.1.3 % 195.23/29.62 % (3038746)Termination reason: Instruction limit % 195.23/29.62 % (3038746)Termination phase: Saturation % 195.23/29.62 % (3038746)Time elapsed: 0.380 s % 195.23/29.62 % (3038746)Peak memory usage: 163 MB % 195.23/29.62 % (3038746)Instructions burned: 1017 (million) % 195.23/29.62 % (3038749)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3293360930:i=14123:bd=preordered:ins=4_2824 on theBenchmark for (2824ds/14123Mi) % 195.23/29.62 % (3038750)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2321416769:i=5781:kws=precedence:bd=all:rawr=on_2823 on theBenchmark for (2823ds/5781Mi) % 195.23/29.62 % (3038735)Instruction limit reached! % 195.23/29.62 % (3038735)------------------------------ % 195.23/29.62 % (3038735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.23/29.62 % (3038735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.23/29.62 % (3038735)CaDiCaL version: 2.1.3 % 195.23/29.62 % (3038735)Termination reason: Instruction limit % 195.23/29.62 % (3038735)Termination phase: Saturation % 195.23/29.62 % (3038735)Time elapsed: 5.950 s % 195.23/29.62 % (3038735)Peak memory usage: 857 MB % 195.23/29.62 % (3038735)Instructions burned: 9928 (million) % 195.23/29.62 % (3038753)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=3047355646:i=2448:gtgl=5:bd=preordered:gtg=all_2816 on theBenchmark for (2816ds/2448Mi) % 195.23/29.62 % (3038750)Instruction limit reached! % 195.23/29.62 % (3038750)------------------------------ % 195.23/29.62 % (3038750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.23/29.62 % (3038750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.23/29.62 % (3038750)CaDiCaL version: 2.1.3 % 195.23/29.62 % (3038750)Termination reason: Instruction limit % 195.23/29.62 % (3038750)Termination phase: Property scanning % 195.23/29.62 % (3038750)Time elapsed: 1.465 s % 195.23/29.62 % (3038750)Peak memory usage: 219 MB % 195.23/29.62 % (3038750)Instructions burned: 5784 (million) % 195.23/29.62 % (3038755)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3433960875:i=3223:kws=precedence:fgj=on:av=off_2807 on theBenchmark for (2807ds/3223Mi) % 195.23/29.62 % (3038753)Instruction limit reached! % 195.23/29.62 % (3038753)------------------------------ % 195.23/29.62 % (3038753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.23/29.62 % (3038753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 195.23/29.62 % (3038753)CaDiCaL version: 2.1.3 % 195.23/29.62 % (3038753)Termination reason: Instruction limit % 195.23/29.62 % (3038753)Termination phase: Preprocessing 3 % 195.23/29.62 % (3038753)Time elapsed: 1.397 s % 195.23/29.62 % (3038753)Peak memory usage: 187 MB % 195.23/29.62 % (3038753)Instructions burned: 2448 (million) % 195.23/29.62 % (3038757)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=293197049:st=5.6:i=2033:sd=3:ss=axioms_2800 on theBenchmark for (2800ds/2033Mi) % 195.23/29.62 % (3038755)Instruction limit reached! % 195.23/29.62 % (3038755)------------------------------ % 195.23/29.62 % (3038755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 195.23/29.62 % (3038755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.84/35.66 % (3038755)CaDiCaL version: 2.1.3 % 237.84/35.66 % (3038755)Termination reason: Instruction limit % 237.84/35.66 % (3038755)Termination phase: Function definition elimination % 237.84/35.66 % (3038755)Time elapsed: 0.985 s % 237.84/35.66 % (3038755)Peak memory usage: 215 MB % 237.84/35.66 % (3038755)Instructions burned: 3224 (million) % 237.84/35.66 % (3038759)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1442787546:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2796 on theBenchmark for (2796ds/2055Mi) % 237.84/35.66 % (3038759)Instruction limit reached! % 237.84/35.66 % (3038759)------------------------------ % 237.84/35.66 % (3038759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.84/35.66 % (3038759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.84/35.66 % (3038759)CaDiCaL version: 2.1.3 % 237.84/35.66 % (3038759)Termination reason: Instruction limit % 237.84/35.66 % (3038759)Termination phase: Saturation % 237.84/35.66 % (3038759)Time elapsed: 0.728 s % 237.84/35.66 % (3038759)Peak memory usage: 195 MB % 237.84/35.66 % (3038759)Instructions burned: 2056 (million) % 237.84/35.66 % (3038761)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=1054886855:i=21611:sd=3:ss=axioms_2787 on theBenchmark for (2787ds/21611Mi) % 237.84/35.66 % (3038757)Instruction limit reached! % 237.84/35.66 % (3038757)------------------------------ % 237.84/35.66 % (3038757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.84/35.66 % (3038757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.84/35.66 % (3038757)CaDiCaL version: 2.1.3 % 237.84/35.66 % (3038757)Termination reason: Instruction limit % 237.84/35.66 % (3038757)Termination phase: Saturation % 237.84/35.66 % (3038757)Time elapsed: 1.280 s % 237.84/35.66 % (3038757)Peak memory usage: 173 MB % 237.84/35.66 % (3038757)Instructions burned: 2034 (million) % 237.84/35.66 % (3038763)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=880841819:i=4835:sd=13:ss=axioms:sgt=23_2785 on theBenchmark for (2785ds/4835Mi) % 237.84/35.66 % (3038741)Instruction limit reached! % 237.84/35.66 % (3038741)------------------------------ % 237.84/35.66 % (3038741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.84/35.66 % (3038741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.84/35.66 % (3038741)CaDiCaL version: 2.1.3 % 237.84/35.66 % (3038741)Termination reason: Instruction limit % 237.84/35.66 % (3038741)Termination phase: Saturation % 237.84/35.66 % (3038741)Time elapsed: 7.256 s % 237.84/35.66 % (3038741)Peak memory usage: 240 MB % 237.84/35.66 % (3038741)Instructions burned: 11146 (million) % 237.84/35.66 % (3038765)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=1166386935:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2781 on theBenchmark for (2781ds/797Mi) % 237.84/35.66 % (3038765)Instruction limit reached! % 237.84/35.66 % (3038765)------------------------------ % 237.84/35.66 % (3038765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.84/35.66 % (3038765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.84/35.66 % (3038765)CaDiCaL version: 2.1.3 % 237.84/35.66 % (3038765)Termination reason: Instruction limit % 237.84/35.66 % (3038765)Termination phase: Unused predicate definition removal % 237.84/35.66 % (3038765)Time elapsed: 0.596 s % 237.84/35.66 % (3038765)Peak memory usage: 130 MB % 237.84/35.66 % (3038765)Instructions burned: 798 (million) % 237.84/35.66 % (3038767)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=102536490:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2773 on theBenchmark for (2773ds/2326Mi) % 237.84/35.66 % (3038767)Instruction limit reached! % 237.84/35.66 % (3038767)------------------------------ % 237.84/35.66 % (3038767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.84/35.66 % (3038767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.84/35.66 % (3038767)CaDiCaL version: 2.1.3 % 237.84/35.66 % (3038767)Termination reason: Instruction limit % 237.84/35.66 % (3038767)Termination phase: Property scanning % 237.84/35.66 % (3038767)Time elapsed: 1.334 s % 237.84/35.66 % (3038767)Peak memory usage: 206 MB % 237.84/35.66 % (3038767)Instructions burned: 2328 (million) % 237.84/35.66 % (3038769)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=832644777:i=6038:nm=6_2758 on theBenchmark for (2758ds/6038Mi) % 300.35/44.43 % (3038763)Instruction limit reached! % 300.35/44.43 % (3038763)------------------------------ % 300.35/44.43 % (3038763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.35/44.43 % (3038763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/44.43 % (3038763)CaDiCaL version: 2.1.3 % 300.35/44.43 % (3038763)Termination reason: Instruction limit % 300.35/44.43 % (3038763)Termination phase: Saturation % 300.35/44.43 % (3038763)Time elapsed: 2.796 s % 300.35/44.43 % (3038763)Peak memory usage: 241 MB % 300.35/44.43 % (3038763)Instructions burned: 4835 (million) % 300.35/44.43 % (3038771)lrs+10_1_sil=32000:sp=occurrence:random_seed=3052653262:st=2:i=33334:sd=3:ss=included:sgt=32_2755 on theBenchmark for (2755ds/33334Mi) % 300.35/44.43 % (3038769)Instruction limit reached! % 300.35/44.43 % (3038769)------------------------------ % 300.35/44.43 % (3038769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.35/44.43 % (3038769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/44.43 % (3038769)CaDiCaL version: 2.1.3 % 300.35/44.43 % (3038769)Termination reason: Instruction limit % 300.35/44.43 % (3038769)Termination phase: Property scanning % 300.35/44.43 % (3038769)Time elapsed: 2.784 s % 300.35/44.43 % (3038769)Peak memory usage: 220 MB % 300.35/44.43 % (3038769)Instructions burned: 6039 (million) % 300.35/44.43 % (3038773)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1402038713:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2728 on theBenchmark for (2728ds/1008Mi) % 300.35/44.43 % (3038761)Instruction limit reached! % 300.35/44.43 % (3038761)------------------------------ % 300.35/44.43 % (3038761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.35/44.43 % (3038761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/44.43 % (3038761)CaDiCaL version: 2.1.3 % 300.35/44.43 % (3038761)Termination reason: Instruction limit % 300.35/44.43 % (3038761)Termination phase: Saturation % 300.35/44.43 % (3038761)Time elapsed: 6.015 s % 300.35/44.43 % (3038761)Peak memory usage: 279 MB % 300.35/44.43 % (3038761)Instructions burned: 21614 (million) % 300.35/44.43 % (3038775)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=3991871386:i=8327:s2at=5:bd=preordered_2725 on theBenchmark for (2725ds/8327Mi) % 300.35/44.44 % (3038773)Instruction limit reached! % 300.35/44.44 % (3038773)------------------------------ % 300.35/44.44 % (3038773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.35/44.44 % (3038773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/44.44 % (3038773)CaDiCaL version: 2.1.3 % 300.35/44.44 % (3038773)Termination reason: Instruction limit % 300.35/44.44 % (3038773)Termination phase: Property scanning % 300.35/44.44 % (3038773)Time elapsed: 0.647 s % 300.35/44.44 % (3038773)Peak memory usage: 141 MB % 300.35/44.44 % (3038773)Instructions burned: 1011 (million) % 300.35/44.44 % (3038777)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=1295150118:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2720 on theBenchmark for (2720ds/1083Mi) % 300.35/44.44 % (3038749)Instruction limit reached! % 300.35/44.44 % (3038749)------------------------------ % 300.35/44.44 % (3038749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.35/44.44 % (3038749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/44.44 % (3038749)CaDiCaL version: 2.1.3 % 300.35/44.44 % (3038749)Termination reason: Instruction limit % 300.35/44.44 % (3038749)Termination phase: Saturation % 300.35/44.44 % (3038749)Time elapsed: 10.492 s % 300.35/44.44 % (3038749)Peak memory usage: 723 MB % 300.35/44.44 % (3038749)Instructions burned: 14124 (million) % 300.35/44.44 % (3038779)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=783584849:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2717 on theBenchmark for (2717ds/1084Mi) % 300.35/44.44 % (3038777)Instruction limit reached! % 300.35/44.44 % (3038777)------------------------------ % 300.35/44.44 % (3038777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.35/44.44 % (3038777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.35/44.44 % (3038777)CaDiCaL version: 2.1.3 % 300.35/44.44 % (3038777)Termination reason: Instruction limit % 300.35/44.44 % (3038777)Termination pha % 300.35/44.44 Terminated %------------------------------------------------------------------------------