%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : LAT293+2 : 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 : n011.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 11:46:36 AM UTC 2026 % Result : Timeout 300.13s 43.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LAT293+2 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.39 % Computer : n011.cluster.edu % 0.10/0.39 % Model : x86_64 x86_64 % 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.39 % Memory : 8046.5625MB % 0.10/0.39 % OS : Linux 6.8.0-71-generic % 0.10/0.39 % CPULimit : 300 % 0.10/0.39 % WCLimit : 300 % 0.10/0.39 % DateTime : Sun Sep 27 14:17:01 UTC 2026 % 0.10/0.39 % CPUTime : % 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.42 Running first-order theorem proving % 0.10/0.42 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 % 15.12/3.05 % (2464318)Detected formulas, will run a generic FOF schedule. % 15.12/3.05 % (2464323)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=4084753646:i=141193_2998 on theBenchmark for (2998ds/141193Mi) % 15.12/3.05 % (2464329)dis-21_1_sil=8000:lcm=predicate:random_seed=2109519734:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi) % 15.12/3.05 % (2464324)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=143894911:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi) % 15.12/3.05 % (2464326)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=600146336:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi) % 15.12/3.05 % (2464325)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=1826931523:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi) % 15.12/3.05 % (2464327)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=506603421:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi) % 15.12/3.05 % (2464328)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1993720620:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi) % 15.12/3.05 % (2464326)Instruction limit reached! % 15.12/3.05 % (2464326)------------------------------ % 15.12/3.05 % (2464326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/3.05 % (2464326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/3.05 % (2464326)CaDiCaL version: 2.1.3 % 15.12/3.05 % (2464326)Termination reason: Instruction limit % 15.12/3.05 % (2464326)Termination phase: Saturation % 15.12/3.05 % (2464326)Time elapsed: 0.066 s % 15.12/3.05 % (2464326)Peak memory usage: 92 MB % 15.12/3.05 % (2464326)Instructions burned: 111 (million) % 15.12/3.05 % (2464327)Instruction limit reached! % 15.12/3.05 % (2464327)------------------------------ % 15.12/3.05 % (2464327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/3.05 % (2464327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/3.05 % (2464327)CaDiCaL version: 2.1.3 % 15.12/3.05 % (2464327)Termination reason: Instruction limit % 15.12/3.05 % (2464327)Termination phase: Saturation % 15.12/3.05 % (2464327)Time elapsed: 0.076 s % 15.12/3.05 % (2464327)Peak memory usage: 93 MB % 15.12/3.05 % (2464327)Instructions burned: 122 (million) % 15.12/3.05 % (2464329)Instruction limit reached! % 15.12/3.05 % (2464329)------------------------------ % 15.12/3.05 % (2464329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/3.05 % (2464329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/3.05 % (2464329)CaDiCaL version: 2.1.3 % 15.12/3.05 % (2464329)Termination reason: Instruction limit % 15.12/3.05 % (2464329)Termination phase: Function definition elimination % 15.12/3.05 % (2464329)Time elapsed: 0.076 s % 15.12/3.05 % (2464329)Peak memory usage: 92 MB % 15.12/3.05 % (2464329)Instructions burned: 130 (million) % 15.12/3.05 % (2464328)Instruction limit reached! % 15.12/3.05 % (2464328)------------------------------ % 15.12/3.05 % (2464328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.12/3.05 % (2464328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.12/3.05 % (2464328)CaDiCaL version: 2.1.3 % 15.12/3.05 % (2464328)Termination reason: Instruction limit % 15.12/3.05 % (2464328)Termination phase: Property scanning % 15.12/3.05 % (2464328)Time elapsed: 0.084 s % 15.12/3.05 % (2464328)Peak memory usage: 94 MB % 15.12/3.05 % (2464328)Instructions burned: 140 (million) % 15.12/3.05 % (2464339)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3084681024:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 15.12/3.05 % (2464338)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2851250769:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 15.12/3.05 % (2464337)lrs+10_1_sil=8000:sp=occurrence:random_seed=4008200781:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 15.12/3.05 % (2464340)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=3359278651:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi) % 15.12/3.05 % (2464338)Instruction limit reached! % 20.67/3.99 % (2464338)------------------------------ % 20.67/3.99 % (2464338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464338)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464338)Termination reason: Instruction limit % 20.67/3.99 % (2464338)Termination phase: Saturation % 20.67/3.99 % (2464338)Time elapsed: 0.090 s % 20.67/3.99 % (2464338)Peak memory usage: 93 MB % 20.67/3.99 % (2464338)Instructions burned: 159 (million) % 20.67/3.99 % (2464337)Instruction limit reached! % 20.67/3.99 % (2464337)------------------------------ % 20.67/3.99 % (2464337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464337)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464337)Termination reason: Instruction limit % 20.67/3.99 % (2464337)Termination phase: Saturation % 20.67/3.99 % (2464337)Time elapsed: 0.188 s % 20.67/3.99 % (2464337)Peak memory usage: 96 MB % 20.67/3.99 % (2464337)Instructions burned: 286 (million) % 20.67/3.99 % (2464340)Instruction limit reached! % 20.67/3.99 % (2464340)------------------------------ % 20.67/3.99 % (2464340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464340)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464340)Termination reason: Instruction limit % 20.67/3.99 % (2464340)Termination phase: Saturation % 20.67/3.99 % (2464340)Time elapsed: 0.139 s % 20.67/3.99 % (2464340)Peak memory usage: 98 MB % 20.67/3.99 % (2464340)Instructions burned: 249 (million) % 20.67/3.99 % (2464339)Instruction limit reached! % 20.67/3.99 % (2464339)------------------------------ % 20.67/3.99 % (2464339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464339)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464339)Termination reason: Instruction limit % 20.67/3.99 % (2464339)Termination phase: Saturation % 20.67/3.99 % (2464339)Time elapsed: 0.211 s % 20.67/3.99 % (2464339)Peak memory usage: 94 MB % 20.67/3.99 % (2464339)Instructions burned: 325 (million) % 20.67/3.99 % (2464345)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=921554200:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 20.67/3.99 % (2464346)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3109572540:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 20.67/3.99 % (2464347)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3423319218:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 20.67/3.99 % (2464348)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2917540629:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 20.67/3.99 % (2464345)Instruction limit reached! % 20.67/3.99 % (2464345)------------------------------ % 20.67/3.99 % (2464345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464345)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464345)Termination reason: Instruction limit % 20.67/3.99 % (2464345)Termination phase: Saturation % 20.67/3.99 % (2464345)Time elapsed: 0.166 s % 20.67/3.99 % (2464345)Peak memory usage: 96 MB % 20.67/3.99 % (2464345)Instructions burned: 295 (million) % 20.67/3.99 % (2464347)Instruction limit reached! % 20.67/3.99 % (2464347)------------------------------ % 20.67/3.99 % (2464347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464347)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464347)Termination reason: Instruction limit % 20.67/3.99 % (2464347)Termination phase: Saturation % 20.67/3.99 % (2464347)Time elapsed: 0.064 s % 20.67/3.99 % (2464347)Peak memory usage: 93 MB % 20.67/3.99 % (2464347)Instructions burned: 113 (million) % 20.67/3.99 % (2464348)Instruction limit reached! % 20.67/3.99 % (2464348)------------------------------ % 20.67/3.99 % (2464348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.67/3.99 % (2464348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.67/3.99 % (2464348)CaDiCaL version: 2.1.3 % 20.67/3.99 % (2464348)Termination reason: Instruction limit % 56.72/8.96 % (2464348)Termination phase: Property scanning % 56.72/8.96 % (2464348)Time elapsed: 0.074 s % 56.72/8.96 % (2464348)Peak memory usage: 94 MB % 56.72/8.96 % (2464348)Instructions burned: 128 (million) % 56.72/8.96 % (2464353)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1564196412:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 56.72/8.96 % (2464354)lrs+10_1_sil=8000:sp=occurrence:random_seed=1479232320:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 56.72/8.96 % (2464355)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2420758929:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 56.72/8.96 % (2464353)Instruction limit reached! % 56.72/8.96 % (2464353)------------------------------ % 56.72/8.96 % (2464353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.72/8.96 % (2464353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.72/8.96 % (2464353)CaDiCaL version: 2.1.3 % 56.72/8.96 % (2464353)Termination reason: Instruction limit % 56.72/8.96 % (2464353)Termination phase: Property scanning % 56.72/8.96 % (2464353)Time elapsed: 0.057 s % 56.72/8.96 % (2464353)Peak memory usage: 91 MB % 56.72/8.96 % (2464353)Instructions burned: 117 (million) % 56.72/8.96 % (2464359)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1218548208:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 56.72/8.96 % (2464355)Instruction limit reached! % 56.72/8.96 % (2464355)------------------------------ % 56.72/8.96 % (2464355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.72/8.96 % (2464355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.72/8.96 % (2464355)CaDiCaL version: 2.1.3 % 56.72/8.96 % (2464355)Termination reason: Instruction limit % 56.72/8.96 % (2464355)Termination phase: Saturation % 56.72/8.96 % (2464355)Time elapsed: 0.221 s % 56.72/8.96 % (2464355)Peak memory usage: 94 MB % 56.72/8.96 % (2464355)Instructions burned: 439 (million) % 56.72/8.96 % (2464361)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2392299812:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi) % 56.72/8.96 % (2464361)Instruction limit reached! % 56.72/8.96 % (2464361)------------------------------ % 56.72/8.96 % (2464361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.72/8.96 % (2464361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.72/8.96 % (2464361)CaDiCaL version: 2.1.3 % 56.72/8.96 % (2464361)Termination reason: Instruction limit % 56.72/8.96 % (2464361)Termination phase: Saturation % 56.72/8.96 % (2464361)Time elapsed: 0.084 s % 56.72/8.96 % (2464361)Peak memory usage: 94 MB % 56.72/8.96 % (2464361)Instructions burned: 135 (million) % 56.72/8.96 % (2464354)Instruction limit reached! % 56.72/8.96 % (2464354)------------------------------ % 56.72/8.96 % (2464354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.72/8.96 % (2464354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.72/8.96 % (2464354)CaDiCaL version: 2.1.3 % 56.72/8.96 % (2464354)Termination reason: Instruction limit % 56.72/8.96 % (2464354)Termination phase: Saturation % 56.72/8.96 % (2464354)Time elapsed: 0.578 s % 56.72/8.96 % (2464354)Peak memory usage: 106 MB % 56.72/8.96 % (2464354)Instructions burned: 908 (million) % 56.72/8.96 % (2464363)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1252347268:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi) % 56.72/8.96 % (2464364)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=36487137:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi) % 56.72/8.96 % (2464363)Instruction limit reached! % 56.72/8.96 % (2464363)------------------------------ % 56.72/8.96 % (2464363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 56.72/8.96 % (2464363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 56.72/8.96 % (2464363)CaDiCaL version: 2.1.3 % 56.72/8.96 % (2464363)Termination reason: Instruction limit % 56.72/8.96 % (2464363)Termination phase: Saturation % 56.72/8.96 % (2464363)Time elapsed: 0.295 s % 56.72/8.96 % (2464363)Peak memory usage: 102 MB % 56.72/8.96 % (2464363)Instructions burned: 593 (million) % 56.72/8.96 % (2464367)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=1861589468:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi) % 84.36/12.84 % (2464367)Instruction limit reached! % 84.36/12.84 % (2464367)------------------------------ % 84.36/12.84 % (2464367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.36/12.84 % (2464367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.36/12.84 % (2464367)CaDiCaL version: 2.1.3 % 84.36/12.84 % (2464367)Termination reason: Instruction limit % 84.36/12.84 % (2464367)Termination phase: Saturation % 84.36/12.84 % (2464367)Time elapsed: 0.066 s % 84.36/12.84 % (2464367)Peak memory usage: 93 MB % 84.36/12.84 % (2464367)Instructions burned: 126 (million) % 84.36/12.84 % (2464346)Instruction limit reached! % 84.36/12.84 % (2464346)------------------------------ % 84.36/12.84 % (2464346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.36/12.84 % (2464346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.36/12.84 % (2464346)CaDiCaL version: 2.1.3 % 84.36/12.84 % (2464346)Termination reason: Instruction limit % 84.36/12.84 % (2464346)Termination phase: Saturation % 84.36/12.84 % (2464346)Time elapsed: 1.448 s % 84.36/12.84 % (2464346)Peak memory usage: 225 MB % 84.36/12.84 % (2464346)Instructions burned: 2351 (million) % 84.36/12.84 % (2464369)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3774376002:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi) % 84.36/12.84 % (2464370)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2815752593:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi) % 84.36/12.84 % (2464369)Instruction limit reached! % 84.36/12.84 % (2464369)------------------------------ % 84.36/12.84 % (2464369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.36/12.84 % (2464369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.36/12.84 % (2464369)CaDiCaL version: 2.1.3 % 84.36/12.84 % (2464369)Termination reason: Instruction limit % 84.36/12.84 % (2464369)Termination phase: Preprocessing 3 % 84.36/12.84 % (2464369)Time elapsed: 0.075 s % 84.36/12.84 % (2464369)Peak memory usage: 92 MB % 84.36/12.84 % (2464369)Instructions burned: 135 (million) % 84.36/12.84 % (2464370)Instruction limit reached! % 84.36/12.84 % (2464370)------------------------------ % 84.36/12.84 % (2464370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.36/12.84 % (2464370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.36/12.84 % (2464370)CaDiCaL version: 2.1.3 % 84.36/12.84 % (2464370)Termination reason: Instruction limit % 84.36/12.84 % (2464370)Termination phase: Saturation % 84.36/12.84 % (2464370)Time elapsed: 0.084 s % 84.36/12.84 % (2464370)Peak memory usage: 93 MB % 84.36/12.84 % (2464370)Instructions burned: 143 (million) % 84.36/12.84 % (2464373)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1532904240:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi) % 84.36/12.84 % (2464374)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=2937333888:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi) % 84.36/12.84 % (2464373)Instruction limit reached! % 84.36/12.84 % (2464373)------------------------------ % 84.36/12.84 % (2464373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.36/12.84 % (2464373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.36/12.84 % (2464373)CaDiCaL version: 2.1.3 % 84.36/12.84 % (2464373)Termination reason: Instruction limit % 84.36/12.84 % (2464373)Termination phase: Saturation % 84.36/12.84 % (2464373)Time elapsed: 0.243 s % 84.36/12.84 % (2464373)Peak memory usage: 99 MB % 84.36/12.84 % (2464373)Instructions burned: 431 (million) % 84.36/12.84 % (2464377)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=420457560:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi) % 84.36/12.84 % (2464377)Instruction limit reached! % 84.36/12.84 % (2464377)------------------------------ % 84.36/12.84 % (2464377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.36/12.84 % (2464377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.36/12.84 % (2464377)CaDiCaL version: 2.1.3 % 84.36/12.84 % (2464377)Termination reason: Instruction limit % 84.36/12.84 % (2464377)Termination phase: Property scanning % 116.33/17.31 % (2464377)Time elapsed: 0.084 s % 116.33/17.31 % (2464377)Peak memory usage: 94 MB % 116.33/17.31 % (2464377)Instructions burned: 152 (million) % 116.33/17.31 % (2464379)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1785400917:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi) % 116.33/17.31 % (2464359)Instruction limit reached! % 116.33/17.31 % (2464359)------------------------------ % 116.33/17.31 % (2464359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.33/17.31 % (2464359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.33/17.31 % (2464359)CaDiCaL version: 2.1.3 % 116.33/17.31 % (2464359)Termination reason: Instruction limit % 116.33/17.31 % (2464359)Termination phase: Saturation % 116.33/17.31 % (2464359)Time elapsed: 3.035 s % 116.33/17.31 % (2464359)Peak memory usage: 187 MB % 116.33/17.31 % (2464359)Instructions burned: 5203 (million) % 116.33/17.31 % (2464381)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1938152308:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi) % 116.33/17.31 % (2464381)Instruction limit reached! % 116.33/17.31 % (2464381)------------------------------ % 116.33/17.31 % (2464381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.33/17.31 % (2464381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.33/17.31 % (2464381)CaDiCaL version: 2.1.3 % 116.33/17.31 % (2464381)Termination reason: Instruction limit % 116.33/17.31 % (2464381)Termination phase: Saturation % 116.33/17.31 % (2464381)Time elapsed: 0.287 s % 116.33/17.31 % (2464381)Peak memory usage: 101 MB % 116.33/17.31 % (2464381)Instructions burned: 670 (million) % 116.33/17.31 % (2464383)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=1644900346:s2a=on:i=185:s2at=1.8:fdi=4_2952 on theBenchmark for (2952ds/185Mi) % 116.33/17.31 % (2464383)Instruction limit reached! % 116.33/17.31 % (2464383)------------------------------ % 116.33/17.31 % (2464383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.33/17.31 % (2464383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.33/17.31 % (2464383)CaDiCaL version: 2.1.3 % 116.33/17.31 % (2464383)Termination reason: Instruction limit % 116.33/17.31 % (2464383)Termination phase: Function definition elimination % 116.33/17.31 % (2464383)Time elapsed: 0.104 s % 116.33/17.31 % (2464383)Peak memory usage: 94 MB % 116.33/17.31 % (2464383)Instructions burned: 188 (million) % 116.33/17.31 % (2464385)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3492721201:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2949 on theBenchmark for (2949ds/193Mi) % 116.33/17.31 % (2464385)Instruction limit reached! % 116.33/17.31 % (2464385)------------------------------ % 116.33/17.31 % (2464385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.33/17.31 % (2464385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.33/17.31 % (2464385)CaDiCaL version: 2.1.3 % 116.33/17.31 % (2464385)Termination reason: Instruction limit % 116.33/17.31 % (2464385)Termination phase: Saturation % 116.33/17.31 % (2464385)Time elapsed: 0.113 s % 116.33/17.31 % (2464385)Peak memory usage: 96 MB % 116.33/17.31 % (2464385)Instructions burned: 194 (million) % 116.33/17.31 % (2464387)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1551779137:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2946 on theBenchmark for (2946ds/4850Mi) % 116.33/17.31 % (2464374)Instruction limit reached! % 116.33/17.31 % (2464374)------------------------------ % 116.33/17.31 % (2464374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.33/17.31 % (2464374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.33/17.31 % (2464374)CaDiCaL version: 2.1.3 % 116.33/17.31 % (2464374)Termination reason: Instruction limit % 116.33/17.31 % (2464374)Termination phase: Saturation % 116.33/17.31 % (2464374)Time elapsed: 3.646 s % 116.33/17.31 % (2464374)Peak memory usage: 241 MB % 116.33/17.31 % (2464374)Instructions burned: 6061 (million) % 116.33/17.31 % (2464389)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3640928428:i=12111:sd=1:ss=included_2936 on theBenchmark for (2936ds/12111Mi) % 116.33/17.31 % (2464387)Instruction limit reached! % 116.33/17.31 % (2464387)------------------------------ % 116.33/17.31 % (2464387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.33/17.31 % (2464387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.47/21.86 % (2464387)CaDiCaL version: 2.1.3 % 147.47/21.86 % (2464387)Termination reason: Instruction limit % 147.47/21.86 % (2464387)Termination phase: Saturation % 147.47/21.86 % (2464387)Time elapsed: 2.601 s % 147.47/21.86 % (2464387)Peak memory usage: 128 MB % 147.47/21.86 % (2464387)Instructions burned: 4851 (million) % 147.47/21.86 % (2464391)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1315464101:i=319:kws=precedence:fsr=off_2918 on theBenchmark for (2918ds/319Mi) % 147.47/21.86 % (2464391)Instruction limit reached! % 147.47/21.86 % (2464391)------------------------------ % 147.47/21.86 % (2464391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.47/21.86 % (2464391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.47/21.86 % (2464391)CaDiCaL version: 2.1.3 % 147.47/21.86 % (2464391)Termination reason: Instruction limit % 147.47/21.86 % (2464391)Termination phase: Saturation % 147.47/21.86 % (2464391)Time elapsed: 0.148 s % 147.47/21.86 % (2464391)Peak memory usage: 97 MB % 147.47/21.86 % (2464391)Instructions burned: 321 (million) % 147.47/21.86 % (2464393)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4067364471:i=2064:ep=RST_2915 on theBenchmark for (2915ds/2064Mi) % 147.47/21.86 % (2464393)Instruction limit reached! % 147.47/21.86 % (2464393)------------------------------ % 147.47/21.86 % (2464393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.47/21.86 % (2464393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.47/21.86 % (2464393)CaDiCaL version: 2.1.3 % 147.47/21.86 % (2464393)Termination reason: Instruction limit % 147.47/21.86 % (2464393)Termination phase: Saturation % 147.47/21.86 % (2464393)Time elapsed: 1.114 s % 147.47/21.86 % (2464393)Peak memory usage: 117 MB % 147.47/21.86 % (2464393)Instructions burned: 2065 (million) % 147.47/21.86 % (2464395)dis-1011_128_sil=32000:random_seed=1163894908:i=3706:ep=RST:av=off_2903 on theBenchmark for (2903ds/3706Mi) % 147.47/21.86 % (2464364)Instruction limit reached! % 147.47/21.86 % (2464364)------------------------------ % 147.47/21.86 % (2464364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.47/21.86 % (2464364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.47/21.86 % (2464364)CaDiCaL version: 2.1.3 % 147.47/21.86 % (2464364)Termination reason: Instruction limit % 147.47/21.86 % (2464364)Termination phase: Saturation % 147.47/21.86 % (2464364)Time elapsed: 8.074 s % 147.47/21.86 % (2464364)Peak memory usage: 233 MB % 147.47/21.86 % (2464364)Instructions burned: 13194 (million) % 147.47/21.86 % (2464397)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=993134555:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2900 on theBenchmark for (2900ds/757Mi) % 147.47/21.86 % (2464397)Instruction limit reached! % 147.47/21.86 % (2464397)------------------------------ % 147.47/21.86 % (2464397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.47/21.86 % (2464397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.47/21.86 % (2464397)CaDiCaL version: 2.1.3 % 147.47/21.86 % (2464397)Termination reason: Instruction limit % 147.47/21.86 % (2464397)Termination phase: Saturation % 147.47/21.86 % (2464397)Time elapsed: 0.520 s % 147.47/21.86 % (2464397)Peak memory usage: 110 MB % 147.47/21.86 % (2464397)Instructions burned: 757 (million) % 147.47/21.86 % (2464399)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2056116421:i=13913:ss=axioms:sgt=8_2893 on theBenchmark for (2893ds/13913Mi) % 147.47/21.86 % (2464379)Instruction limit reached! % 147.47/21.86 % (2464379)------------------------------ % 147.47/21.86 % (2464379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.47/21.86 % (2464379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 147.47/21.86 % (2464379)CaDiCaL version: 2.1.3 % 147.47/21.86 % (2464379)Termination reason: Instruction limit % 147.47/21.86 % (2464379)Termination phase: Saturation % 147.47/21.86 % (2464379)Time elapsed: 7.544 s % 147.47/21.86 % (2464379)Peak memory usage: 271 MB % 147.47/21.86 % (2464379)Instructions burned: 14157 (million) % 147.47/21.86 % (2464401)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1553842342:i=9925:aac=none_2891 on theBenchmark for (2891ds/9925Mi) % 147.47/21.86 % (2464395)Instruction limit reached! % 147.47/21.86 % (2464395)------------------------------ % 147.47/21.86 % (2464395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 147.47/21.86 % (2464395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.67 % (2464395)CaDiCaL version: 2.1.3 % 174.90/25.67 % (2464395)Termination reason: Instruction limit % 174.90/25.67 % (2464395)Termination phase: Saturation % 174.90/25.67 % (2464395)Time elapsed: 2.105 s % 174.90/25.67 % (2464395)Peak memory usage: 128 MB % 174.90/25.67 % (2464395)Instructions burned: 3706 (million) % 174.90/25.67 % (2464403)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=330037587:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2880 on theBenchmark for (2880ds/2479Mi) % 174.90/25.67 % (2464389)Instruction limit reached! % 174.90/25.67 % (2464389)------------------------------ % 174.90/25.67 % (2464389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.67 % (2464389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.67 % (2464389)CaDiCaL version: 2.1.3 % 174.90/25.67 % (2464389)Termination reason: Instruction limit % 174.90/25.67 % (2464389)Termination phase: Saturation % 174.90/25.67 % (2464389)Time elapsed: 6.493 s % 174.90/25.67 % (2464389)Peak memory usage: 268 MB % 174.90/25.67 % (2464389)Instructions burned: 12111 (million) % 174.90/25.67 % (2464405)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2503739242:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2869 on theBenchmark for (2869ds/440Mi) % 174.90/25.67 % (2464405)Instruction limit reached! % 174.90/25.67 % (2464405)------------------------------ % 174.90/25.67 % (2464405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.67 % (2464405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.67 % (2464405)CaDiCaL version: 2.1.3 % 174.90/25.67 % (2464405)Termination reason: Instruction limit % 174.90/25.67 % (2464405)Termination phase: Saturation % 174.90/25.67 % (2464405)Time elapsed: 0.208 s % 174.90/25.67 % (2464405)Peak memory usage: 99 MB % 174.90/25.67 % (2464405)Instructions burned: 440 (million) % 174.90/25.67 % (2464403)Instruction limit reached! % 174.90/25.67 % (2464403)------------------------------ % 174.90/25.67 % (2464403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.67 % (2464403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.67 % (2464403)CaDiCaL version: 2.1.3 % 174.90/25.67 % (2464403)Termination reason: Instruction limit % 174.90/25.67 % (2464403)Termination phase: Saturation % 174.90/25.67 % (2464403)Time elapsed: 1.367 s % 174.90/25.67 % (2464403)Peak memory usage: 117 MB % 174.90/25.67 % (2464403)Instructions burned: 2481 (million) % 174.90/25.67 % (2464407)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=281245722:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2865 on theBenchmark for (2865ds/11145Mi) % 174.90/25.67 % (2464408)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=2379136591:cts=off:i=3034:av=off:er=known:fsd=on_2864 on theBenchmark for (2864ds/3034Mi) % 174.90/25.67 % (2464408)Instruction limit reached! % 174.90/25.67 % (2464408)------------------------------ % 174.90/25.67 % (2464408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.67 % (2464408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.67 % (2464408)CaDiCaL version: 2.1.3 % 174.90/25.67 % (2464408)Termination reason: Instruction limit % 174.90/25.67 % (2464408)Termination phase: Saturation % 174.90/25.67 % (2464408)Time elapsed: 1.717 s % 174.90/25.67 % (2464408)Peak memory usage: 206 MB % 174.90/25.67 % (2464408)Instructions burned: 3034 (million) % 174.90/25.67 % (2464411)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1639361063:st=2:s2a=on:i=524:s2at=2:ss=axioms_2845 on theBenchmark for (2845ds/524Mi) % 174.90/25.67 % (2464411)Instruction limit reached! % 174.90/25.67 % (2464411)------------------------------ % 174.90/25.67 % (2464411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 174.90/25.67 % (2464411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 174.90/25.67 % (2464411)CaDiCaL version: 2.1.3 % 174.90/25.67 % (2464411)Termination reason: Instruction limit % 174.90/25.67 % (2464411)Termination phase: Saturation % 174.90/25.67 % (2464411)Time elapsed: 0.280 s % 174.90/25.67 % (2464411)Peak memory usage: 99 MB % 174.90/25.67 % (2464411)Instructions burned: 524 (million) % 174.90/25.67 % (2464413)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=15776964:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2841 on theBenchmark for (2841ds/1016Mi) % 174.90/25.67 % (2464401)Instruction limit reached! % 174.90/25.67 % (2464401)------------------------------ % 219.23/31.89 % (2464401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.23/31.89 % (2464401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.23/31.89 % (2464401)CaDiCaL version: 2.1.3 % 219.23/31.89 % (2464401)Termination reason: Instruction limit % 219.23/31.89 % (2464401)Termination phase: Saturation % 219.23/31.89 % (2464401)Time elapsed: 5.405 s % 219.23/31.89 % (2464401)Peak memory usage: 218 MB % 219.23/31.89 % (2464401)Instructions burned: 9925 (million) % 219.23/31.89 % (2464415)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1224736844:i=14123:bd=preordered:ins=4_2835 on theBenchmark for (2835ds/14123Mi) % 219.23/31.89 % (2464413)Instruction limit reached! % 219.23/31.89 % (2464413)------------------------------ % 219.23/31.89 % (2464413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.23/31.89 % (2464413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.23/31.89 % (2464413)CaDiCaL version: 2.1.3 % 219.23/31.89 % (2464413)Termination reason: Instruction limit % 219.23/31.89 % (2464413)Termination phase: Saturation % 219.23/31.89 % (2464413)Time elapsed: 0.608 s % 219.23/31.89 % (2464413)Peak memory usage: 113 MB % 219.23/31.89 % (2464413)Instructions burned: 1017 (million) % 219.23/31.89 % (2464417)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2627080249:i=5781:kws=precedence:bd=all:rawr=on_2833 on theBenchmark for (2833ds/5781Mi) % 219.23/31.89 % (2464399)Instruction limit reached! % 219.23/31.89 % (2464399)------------------------------ % 219.23/31.89 % (2464399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.23/31.89 % (2464399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.23/31.89 % (2464399)CaDiCaL version: 2.1.3 % 219.23/31.89 % (2464399)Termination reason: Instruction limit % 219.23/31.89 % (2464399)Termination phase: Saturation % 219.23/31.89 % (2464399)Time elapsed: 8.173 s % 219.23/31.89 % (2464399)Peak memory usage: 245 MB % 219.23/31.89 % (2464399)Instructions burned: 13915 (million) % 219.23/31.89 % (2464419)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=290223636:i=2448:gtgl=5:bd=preordered:gtg=all_2810 on theBenchmark for (2810ds/2448Mi) % 219.23/31.89 % (2464417)Instruction limit reached! % 219.23/31.89 % (2464417)------------------------------ % 219.23/31.89 % (2464417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.23/31.89 % (2464417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.23/31.89 % (2464417)CaDiCaL version: 2.1.3 % 219.23/31.89 % (2464417)Termination reason: Instruction limit % 219.23/31.89 % (2464417)Termination phase: Saturation % 219.23/31.89 % (2464417)Time elapsed: 3.674 s % 219.23/31.89 % (2464417)Peak memory usage: 121 MB % 219.23/31.89 % (2464417)Instructions burned: 5781 (million) % 219.23/31.89 % (2464419)Instruction limit reached! % 219.23/31.89 % (2464419)------------------------------ % 219.23/31.89 % (2464419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.23/31.89 % (2464419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.23/31.89 % (2464419)CaDiCaL version: 2.1.3 % 219.23/31.89 % (2464419)Termination reason: Instruction limit % 219.23/31.89 % (2464419)Termination phase: Saturation % 219.23/31.89 % (2464419)Time elapsed: 1.443 s % 219.23/31.89 % (2464419)Peak memory usage: 203 MB % 219.23/31.89 % (2464419)Instructions burned: 2449 (million) % 219.23/31.89 % (2464421)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=805727611:i=3223:kws=precedence:fgj=on:av=off_2794 on theBenchmark for (2794ds/3223Mi) % 219.23/31.89 % (2464422)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2634307810:st=5.6:i=2033:sd=3:ss=axioms_2793 on theBenchmark for (2793ds/2033Mi) % 219.23/31.89 % (2464407)Instruction limit reached! % 219.23/31.89 % (2464407)------------------------------ % 219.23/31.89 % (2464407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.23/31.89 % (2464407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.23/31.89 % (2464407)CaDiCaL version: 2.1.3 % 219.23/31.89 % (2464407)Termination reason: Instruction limit % 219.23/31.89 % (2464407)Termination phase: Saturation % 219.23/31.89 % (2464407)Time elapsed: 7.217 s % 219.23/31.89 % (2464407)Peak memory usage: 218 MB % 219.23/31.89 % (2464407)Instructions burned: 11146 (million) % 219.23/31.89 % (2464425)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1626530602:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2791 on theBenchmark for (2791ds/2055Mi) % 266.09/38.41 % (2464422)Instruction limit reached! % 266.09/38.41 % (2464422)------------------------------ % 266.09/38.41 % (2464422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.09/38.41 % (2464422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.09/38.41 % (2464422)CaDiCaL version: 2.1.3 % 266.09/38.41 % (2464422)Termination reason: Instruction limit % 266.09/38.41 % (2464422)Termination phase: Saturation % 266.09/38.41 % (2464422)Time elapsed: 1.260 s % 266.09/38.41 % (2464422)Peak memory usage: 224 MB % 266.09/38.41 % (2464422)Instructions burned: 2034 (million) % 266.09/38.41 % (2464427)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=4075751770:i=21611:sd=3:ss=axioms_2779 on theBenchmark for (2779ds/21611Mi) % 266.09/38.41 % (2464425)Instruction limit reached! % 266.09/38.41 % (2464425)------------------------------ % 266.09/38.41 % (2464425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.09/38.41 % (2464425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.09/38.41 % (2464425)CaDiCaL version: 2.1.3 % 266.09/38.41 % (2464425)Termination reason: Instruction limit % 266.09/38.41 % (2464425)Termination phase: Saturation % 266.09/38.41 % (2464425)Time elapsed: 1.240 s % 266.09/38.41 % (2464425)Peak memory usage: 153 MB % 266.09/38.41 % (2464425)Instructions burned: 2055 (million) % 266.09/38.41 % (2464429)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2929390432:i=4835:sd=13:ss=axioms:sgt=23_2777 on theBenchmark for (2777ds/4835Mi) % 266.09/38.41 % (2464421)Instruction limit reached! % 266.09/38.41 % (2464421)------------------------------ % 266.09/38.41 % (2464421)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.09/38.41 % (2464421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.09/38.41 % (2464421)CaDiCaL version: 2.1.3 % 266.09/38.41 % (2464421)Termination reason: Instruction limit % 266.09/38.41 % (2464421)Termination phase: Saturation % 266.09/38.41 % (2464421)Time elapsed: 1.848 s % 266.09/38.41 % (2464421)Peak memory usage: 223 MB % 266.09/38.41 % (2464421)Instructions burned: 3224 (million) % 266.09/38.41 % (2464431)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=1795567216:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2774 on theBenchmark for (2774ds/797Mi) % 266.09/38.41 % (2464431)Instruction limit reached! % 266.09/38.41 % (2464431)------------------------------ % 266.09/38.41 % (2464431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.09/38.41 % (2464431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.09/38.41 % (2464431)CaDiCaL version: 2.1.3 % 266.09/38.41 % (2464431)Termination reason: Instruction limit % 266.09/38.41 % (2464431)Termination phase: Saturation % 266.09/38.41 % (2464431)Time elapsed: 0.381 s % 266.09/38.41 % (2464431)Peak memory usage: 99 MB % 266.09/38.41 % (2464431)Instructions burned: 797 (million) % 266.09/38.41 % (2464433)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=489851144:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2768 on theBenchmark for (2768ds/2326Mi) % 266.09/38.41 % (2464433)Instruction limit reached! % 266.09/38.41 % (2464433)------------------------------ % 266.09/38.41 % (2464433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.09/38.41 % (2464433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.09/38.41 % (2464433)CaDiCaL version: 2.1.3 % 266.09/38.41 % (2464433)Termination reason: Instruction limit % 266.09/38.41 % (2464433)Termination phase: Saturation % 266.09/38.41 % (2464433)Time elapsed: 1.122 s % 266.09/38.41 % (2464433)Peak memory usage: 113 MB % 266.09/38.41 % (2464433)Instructions burned: 2326 (million) % 266.09/38.41 % (2464435)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=172211438:i=6038:nm=6_2755 on theBenchmark for (2755ds/6038Mi) % 266.09/38.41 % (2464415)Instruction limit reached! % 266.09/38.41 % (2464415)------------------------------ % 266.09/38.41 % (2464415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.09/38.41 % (2464415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.09/38.41 % (2464415)CaDiCaL version: 2.1.3 % 266.09/38.41 % (2464Terminated %------------------------------------------------------------------------------