%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW270+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n004.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:29:59 PM UTC 2026 % Result : Timeout 300.58s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW270+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.21 % Computer : n004.cluster.edu % 0.10/0.21 % Model : x86_64 x86_64 % 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.21 % Memory : 8046.5625MB % 0.10/0.21 % OS : Linux 6.8.0-71-generic % 0.10/0.21 % CPULimit : 300 % 0.10/0.21 % WCLimit : 300 % 0.10/0.21 % DateTime : Mon Sep 28 13:28:52 UTC 2026 % 0.10/0.21 % CPUTime : % 0.10/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.25 Running first-order theorem proving % 0.10/0.25 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 % 14.87/2.91 % (357646)Detected formulas, will run a generic FOF schedule. % 14.87/2.91 % (357651)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=454871816:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 14.87/2.91 % (357653)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=3234401006:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 14.87/2.91 % (357656)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1207840249:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 14.87/2.91 % (357654)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1267204283:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 14.87/2.91 % (357657)dis-21_1_sil=8000:lcm=predicate:random_seed=4052256496:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 14.87/2.91 % (357652)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=2814692693:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 14.87/2.91 % (357655)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2869211725:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 14.87/2.91 % (357655)Instruction limit reached! % 14.87/2.91 % (357655)------------------------------ % 14.87/2.91 % (357655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.87/2.91 % (357655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.87/2.91 % (357655)CaDiCaL version: 2.1.3 % 14.87/2.91 % (357655)Termination reason: Instruction limit % 14.87/2.91 % (357655)Termination phase: Saturation % 14.87/2.91 % (357655)Time elapsed: 0.059 s % 14.87/2.91 % (357655)Peak memory usage: 89 MB % 14.87/2.91 % (357655)Instructions burned: 119 (million) % 14.87/2.91 % (357654)Instruction limit reached! % 14.87/2.91 % (357654)------------------------------ % 14.87/2.91 % (357654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.87/2.91 % (357654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.87/2.91 % (357654)CaDiCaL version: 2.1.3 % 14.87/2.91 % (357654)Termination reason: Instruction limit % 14.87/2.91 % (357654)Termination phase: Saturation % 14.87/2.91 % (357654)Time elapsed: 0.065 s % 14.87/2.91 % (357654)Peak memory usage: 90 MB % 14.87/2.91 % (357654)Instructions burned: 109 (million) % 14.87/2.91 % (357657)Instruction limit reached! % 14.87/2.91 % (357657)------------------------------ % 14.87/2.91 % (357657)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.87/2.91 % (357657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.87/2.91 % (357657)CaDiCaL version: 2.1.3 % 14.87/2.91 % (357657)Termination reason: Instruction limit % 14.87/2.91 % (357657)Termination phase: Saturation % 14.87/2.91 % (357657)Time elapsed: 0.066 s % 14.87/2.91 % (357657)Peak memory usage: 91 MB % 14.87/2.91 % (357657)Instructions burned: 129 (million) % 14.87/2.91 % (357656)Instruction limit reached! % 14.87/2.91 % (357656)------------------------------ % 14.87/2.91 % (357656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.87/2.91 % (357656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.87/2.91 % (357656)CaDiCaL version: 2.1.3 % 14.87/2.91 % (357656)Termination reason: Instruction limit % 14.87/2.91 % (357656)Termination phase: Saturation % 14.87/2.91 % (357656)Time elapsed: 0.075 s % 14.87/2.91 % (357656)Peak memory usage: 91 MB % 14.87/2.91 % (357656)Instructions burned: 139 (million) % 14.87/2.91 % (357665)lrs+10_1_sil=8000:sp=occurrence:random_seed=1756539503:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 14.87/2.91 % (357667)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1603678214:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 14.87/2.91 % (357666)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2490972457:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 14.87/2.91 % (357668)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=4279800518:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 14.87/2.91 % (357666)Instruction limit reached! % 14.87/2.91 % (357666)------------------------------ % 14.87/2.91 % (357666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357666)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357666)Termination reason: Instruction limit % 21.99/3.92 % (357666)Termination phase: Saturation % 21.99/3.92 % (357666)Time elapsed: 0.075 s % 21.99/3.92 % (357666)Peak memory usage: 90 MB % 21.99/3.92 % (357666)Instructions burned: 158 (million) % 21.99/3.92 % (357668)Instruction limit reached! % 21.99/3.92 % (357668)------------------------------ % 21.99/3.92 % (357668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357668)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357668)Termination reason: Instruction limit % 21.99/3.92 % (357668)Termination phase: Saturation % 21.99/3.92 % (357668)Time elapsed: 0.137 s % 21.99/3.92 % (357668)Peak memory usage: 92 MB % 21.99/3.92 % (357668)Instructions burned: 249 (million) % 21.99/3.92 % (357665)Instruction limit reached! % 21.99/3.92 % (357665)------------------------------ % 21.99/3.92 % (357665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357665)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357665)Termination reason: Instruction limit % 21.99/3.92 % (357665)Termination phase: Saturation % 21.99/3.92 % (357665)Time elapsed: 0.182 s % 21.99/3.92 % (357665)Peak memory usage: 92 MB % 21.99/3.92 % (357665)Instructions burned: 286 (million) % 21.99/3.92 % (357667)Instruction limit reached! % 21.99/3.92 % (357667)------------------------------ % 21.99/3.92 % (357667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357667)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357667)Termination reason: Instruction limit % 21.99/3.92 % (357667)Termination phase: Saturation % 21.99/3.92 % (357667)Time elapsed: 0.198 s % 21.99/3.92 % (357667)Peak memory usage: 92 MB % 21.99/3.92 % (357667)Instructions burned: 326 (million) % 21.99/3.92 % (357673)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3756261721:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 21.99/3.92 % (357674)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3913062904:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 21.99/3.92 % (357675)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=118684973:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 21.99/3.92 % (357676)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3840232011:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 21.99/3.92 % (357675)Instruction limit reached! % 21.99/3.92 % (357675)------------------------------ % 21.99/3.92 % (357675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357675)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357675)Termination reason: Instruction limit % 21.99/3.92 % (357675)Termination phase: Saturation % 21.99/3.92 % (357675)Time elapsed: 0.062 s % 21.99/3.92 % (357675)Peak memory usage: 91 MB % 21.99/3.92 % (357675)Instructions burned: 114 (million) % 21.99/3.92 % (357676)Instruction limit reached! % 21.99/3.92 % (357676)------------------------------ % 21.99/3.92 % (357676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357676)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357676)Termination reason: Instruction limit % 21.99/3.92 % (357676)Termination phase: Saturation % 21.99/3.92 % (357676)Time elapsed: 0.063 s % 21.99/3.92 % (357676)Peak memory usage: 90 MB % 21.99/3.92 % (357676)Instructions burned: 129 (million) % 21.99/3.92 % (357673)Instruction limit reached! % 21.99/3.92 % (357673)------------------------------ % 21.99/3.92 % (357673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.99/3.92 % (357673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.99/3.92 % (357673)CaDiCaL version: 2.1.3 % 21.99/3.92 % (357673)Termination reason: Instruction limit % 21.99/3.92 % (357673)Termination phase: Saturation % 21.99/3.92 % (357673)Time elapsed: 0.171 s % 21.99/3.92 % (357673)Peak memory usage: 92 MB % 21.99/3.92 % (357673)Instructions burned: 295 (million) % 59.19/9.10 % (357681)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2584503864:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 59.19/9.10 % (357682)lrs+10_1_sil=8000:sp=occurrence:random_seed=3917865955:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 59.19/9.10 % (357683)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1446298550:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi) % 59.19/9.10 % (357681)Instruction limit reached! % 59.19/9.10 % (357681)------------------------------ % 59.19/9.10 % (357681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.19/9.10 % (357681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.10 % (357681)CaDiCaL version: 2.1.3 % 59.19/9.10 % (357681)Termination reason: Instruction limit % 59.19/9.10 % (357681)Termination phase: Saturation % 59.19/9.10 % (357681)Time elapsed: 0.057 s % 59.19/9.10 % (357681)Peak memory usage: 90 MB % 59.19/9.10 % (357681)Instructions burned: 114 (million) % 59.19/9.10 % (357687)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2734483350:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 59.19/9.10 % (357683)Instruction limit reached! % 59.19/9.10 % (357683)------------------------------ % 59.19/9.10 % (357683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.19/9.10 % (357683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.10 % (357683)CaDiCaL version: 2.1.3 % 59.19/9.10 % (357683)Termination reason: Instruction limit % 59.19/9.10 % (357683)Termination phase: Saturation % 59.19/9.10 % (357683)Time elapsed: 0.234 s % 59.19/9.10 % (357683)Peak memory usage: 93 MB % 59.19/9.10 % (357683)Instructions burned: 438 (million) % 59.19/9.10 % (357689)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2575364475:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 59.19/9.10 % (357689)Instruction limit reached! % 59.19/9.10 % (357689)------------------------------ % 59.19/9.10 % (357689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.19/9.10 % (357689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.10 % (357689)CaDiCaL version: 2.1.3 % 59.19/9.10 % (357689)Termination reason: Instruction limit % 59.19/9.10 % (357689)Termination phase: Saturation % 59.19/9.10 % (357689)Time elapsed: 0.069 s % 59.19/9.10 % (357689)Peak memory usage: 92 MB % 59.19/9.10 % (357689)Instructions burned: 135 (million) % 59.19/9.10 % (357682)Instruction limit reached! % 59.19/9.10 % (357682)------------------------------ % 59.19/9.10 % (357682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.19/9.10 % (357682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.10 % (357682)CaDiCaL version: 2.1.3 % 59.19/9.10 % (357682)Termination reason: Instruction limit % 59.19/9.10 % (357682)Termination phase: Saturation % 59.19/9.10 % (357682)Time elapsed: 0.571 s % 59.19/9.10 % (357682)Peak memory usage: 98 MB % 59.19/9.10 % (357682)Instructions burned: 908 (million) % 59.19/9.10 % (357691)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2250525103:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 59.19/9.10 % (357692)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3753235446:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi) % 59.19/9.10 % (357691)Instruction limit reached! % 59.19/9.10 % (357691)------------------------------ % 59.19/9.10 % (357691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.19/9.10 % (357691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.19/9.10 % (357691)CaDiCaL version: 2.1.3 % 59.19/9.10 % (357691)Termination reason: Instruction limit % 59.19/9.10 % (357691)Termination phase: Saturation % 59.19/9.10 % (357691)Time elapsed: 0.333 s % 59.19/9.10 % (357691)Peak memory usage: 94 MB % 59.19/9.10 % (357691)Instructions burned: 593 (million) % 59.19/9.10 % (357695)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=109000226:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi) % 59.19/9.10 % (357695)Instruction limit reached! % 59.19/9.10 % (357695)------------------------------ % 59.19/9.10 % (357695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.64/12.80 % (357695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.80 % (357695)CaDiCaL version: 2.1.3 % 85.64/12.80 % (357695)Termination reason: Instruction limit % 85.64/12.80 % (357695)Termination phase: Saturation % 85.64/12.80 % (357695)Time elapsed: 0.068 s % 85.64/12.80 % (357695)Peak memory usage: 91 MB % 85.64/12.80 % (357695)Instructions burned: 125 (million) % 85.64/12.80 % (357674)Instruction limit reached! % 85.64/12.80 % (357674)------------------------------ % 85.64/12.80 % (357674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.64/12.80 % (357674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.80 % (357674)CaDiCaL version: 2.1.3 % 85.64/12.80 % (357674)Termination reason: Instruction limit % 85.64/12.80 % (357674)Termination phase: Saturation % 85.64/12.80 % (357674)Time elapsed: 1.490 s % 85.64/12.80 % (357674)Peak memory usage: 149 MB % 85.64/12.80 % (357674)Instructions burned: 2351 (million) % 85.64/12.80 % (357697)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1372009065:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi) % 85.64/12.80 % (357698)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2957592669:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi) % 85.64/12.80 % (357697)Instruction limit reached! % 85.64/12.80 % (357697)------------------------------ % 85.64/12.80 % (357697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.64/12.80 % (357697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.80 % (357697)CaDiCaL version: 2.1.3 % 85.64/12.80 % (357697)Termination reason: Instruction limit % 85.64/12.80 % (357697)Termination phase: Saturation % 85.64/12.80 % (357697)Time elapsed: 0.064 s % 85.64/12.80 % (357697)Peak memory usage: 90 MB % 85.64/12.80 % (357697)Instructions burned: 134 (million) % 85.64/12.80 % (357698)Instruction limit reached! % 85.64/12.80 % (357698)------------------------------ % 85.64/12.80 % (357698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.64/12.80 % (357698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.80 % (357698)CaDiCaL version: 2.1.3 % 85.64/12.80 % (357698)Termination reason: Instruction limit % 85.64/12.80 % (357698)Termination phase: Saturation % 85.64/12.80 % (357698)Time elapsed: 0.080 s % 85.64/12.80 % (357698)Peak memory usage: 90 MB % 85.64/12.80 % (357698)Instructions burned: 141 (million) % 85.64/12.80 % (357701)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1286257000:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi) % 85.64/12.80 % (357702)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=228313379:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi) % 85.64/12.80 % (357701)Instruction limit reached! % 85.64/12.80 % (357701)------------------------------ % 85.64/12.80 % (357701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.64/12.80 % (357701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.80 % (357701)CaDiCaL version: 2.1.3 % 85.64/12.80 % (357701)Termination reason: Instruction limit % 85.64/12.80 % (357701)Termination phase: Saturation % 85.64/12.80 % (357701)Time elapsed: 0.216 s % 85.64/12.80 % (357701)Peak memory usage: 94 MB % 85.64/12.80 % (357701)Instructions burned: 433 (million) % 85.64/12.80 % (357705)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=3083284229:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi) % 85.64/12.80 % (357705)Instruction limit reached! % 85.64/12.80 % (357705)------------------------------ % 85.64/12.80 % (357705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.64/12.80 % (357705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.64/12.80 % (357705)CaDiCaL version: 2.1.3 % 85.64/12.80 % (357705)Termination reason: Instruction limit % 85.64/12.80 % (357705)Termination phase: Saturation % 85.64/12.80 % (357705)Time elapsed: 0.079 s % 85.64/12.80 % (357705)Peak memory usage: 91 MB % 85.64/12.80 % (357705)Instructions burned: 151 (million) % 85.64/12.80 % (357707)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3202340368:i=14155:bd=all_2969 on theBenchmark for (2969ds/14155Mi) % 120.63/17.74 % (357687)Instruction limit reached! % 120.63/17.74 % (357687)------------------------------ % 120.63/17.74 % (357687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.63/17.74 % (357687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.63/17.74 % (357687)CaDiCaL version: 2.1.3 % 120.63/17.74 % (357687)Termination reason: Instruction limit % 120.63/17.74 % (357687)Termination phase: Saturation % 120.63/17.74 % (357687)Time elapsed: 3.174 s % 120.63/17.74 % (357687)Peak memory usage: 158 MB % 120.63/17.74 % (357687)Instructions burned: 5204 (million) % 120.63/17.74 % (357709)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2414851039:i=667:av=off:fsr=off_2956 on theBenchmark for (2956ds/667Mi) % 120.63/17.74 % (357709)Instruction limit reached! % 120.63/17.74 % (357709)------------------------------ % 120.63/17.74 % (357709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.63/17.74 % (357709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.63/17.74 % (357709)CaDiCaL version: 2.1.3 % 120.63/17.74 % (357709)Termination reason: Instruction limit % 120.63/17.74 % (357709)Termination phase: Saturation % 120.63/17.74 % (357709)Time elapsed: 0.296 s % 120.63/17.74 % (357709)Peak memory usage: 94 MB % 120.63/17.74 % (357709)Instructions burned: 667 (million) % 120.63/17.74 % (357711)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=861880609:s2a=on:i=185:s2at=1.8:fdi=4_2951 on theBenchmark for (2951ds/185Mi) % 120.63/17.74 % (357711)Instruction limit reached! % 120.63/17.74 % (357711)------------------------------ % 120.63/17.74 % (357711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.63/17.74 % (357711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.63/17.74 % (357711)CaDiCaL version: 2.1.3 % 120.63/17.74 % (357711)Termination reason: Instruction limit % 120.63/17.74 % (357711)Termination phase: Saturation % 120.63/17.74 % (357711)Time elapsed: 0.091 s % 120.63/17.74 % (357711)Peak memory usage: 92 MB % 120.63/17.74 % (357711)Instructions burned: 185 (million) % 120.63/17.74 % (357713)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3946942242:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/193Mi) % 120.63/17.74 % (357713)Instruction limit reached! % 120.63/17.74 % (357713)------------------------------ % 120.63/17.74 % (357713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.63/17.74 % (357713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.63/17.74 % (357713)CaDiCaL version: 2.1.3 % 120.63/17.74 % (357713)Termination reason: Instruction limit % 120.63/17.74 % (357713)Termination phase: Saturation % 120.63/17.74 % (357713)Time elapsed: 0.108 s % 120.63/17.74 % (357713)Peak memory usage: 92 MB % 120.63/17.74 % (357713)Instructions burned: 194 (million) % 120.63/17.74 % (357715)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4262242225:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2946 on theBenchmark for (2946ds/4850Mi) % 120.63/17.74 % (357702)Instruction limit reached! % 120.63/17.74 % (357702)------------------------------ % 120.63/17.74 % (357702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.63/17.74 % (357702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.63/17.74 % (357702)CaDiCaL version: 2.1.3 % 120.63/17.74 % (357702)Termination reason: Instruction limit % 120.63/17.74 % (357702)Termination phase: Saturation % 120.63/17.74 % (357702)Time elapsed: 3.877 s % 120.63/17.74 % (357702)Peak memory usage: 172 MB % 120.63/17.74 % (357702)Instructions burned: 6060 (million) % 120.63/17.74 % (357717)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2924288443:i=12111:sd=1:ss=included_2934 on theBenchmark for (2934ds/12111Mi) % 120.63/17.74 % (357715)Instruction limit reached! % 120.63/17.74 % (357715)------------------------------ % 120.63/17.74 % (357715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.63/17.74 % (357715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.63/17.74 % (357715)CaDiCaL version: 2.1.3 % 120.63/17.74 % (357715)Termination reason: Instruction limit % 120.63/17.74 % (357715)Termination phase: Saturation % 120.63/17.74 % (357715)Time elapsed: 2.704 s % 120.63/17.74 % (357715)Peak memory usage: 113 MB % 120.63/17.74 % (357715)Instructions burned: 4851 (million) % 120.63/17.74 % (357719)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1307733286:i=319:kws=precedence:fsr=off_2917 on theBenchmark for (2917ds/319Mi) % 156.92/22.86 % (357719)Instruction limit reached! % 156.92/22.86 % (357719)------------------------------ % 156.92/22.86 % (357719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.92/22.86 % (357719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.92/22.86 % (357719)CaDiCaL version: 2.1.3 % 156.92/22.86 % (357719)Termination reason: Instruction limit % 156.92/22.86 % (357719)Termination phase: Saturation % 156.92/22.86 % (357719)Time elapsed: 0.174 s % 156.92/22.86 % (357719)Peak memory usage: 94 MB % 156.92/22.86 % (357719)Instructions burned: 320 (million) % 156.92/22.86 % (357721)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4161464927:i=2064:ep=RST_2914 on theBenchmark for (2914ds/2064Mi) % 156.92/22.86 % (357721)Instruction limit reached! % 156.92/22.86 % (357721)------------------------------ % 156.92/22.86 % (357721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.92/22.86 % (357721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.92/22.86 % (357721)CaDiCaL version: 2.1.3 % 156.92/22.86 % (357721)Termination reason: Instruction limit % 156.92/22.86 % (357721)Termination phase: Saturation % 156.92/22.86 % (357721)Time elapsed: 1.164 s % 156.92/22.86 % (357721)Peak memory usage: 104 MB % 156.92/22.86 % (357721)Instructions burned: 2065 (million) % 156.92/22.86 % (357723)dis-1011_128_sil=32000:random_seed=3764709635:i=3706:ep=RST:av=off_2900 on theBenchmark for (2900ds/3706Mi) % 156.92/22.86 % (357692)Instruction limit reached! % 156.92/22.86 % (357692)------------------------------ % 156.92/22.86 % (357692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.92/22.86 % (357692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.92/22.86 % (357692)CaDiCaL version: 2.1.3 % 156.92/22.86 % (357692)Termination reason: Instruction limit % 156.92/22.86 % (357692)Termination phase: Saturation % 156.92/22.86 % (357692)Time elapsed: 8.492 s % 156.92/22.86 % (357692)Peak memory usage: 214 MB % 156.92/22.86 % (357692)Instructions burned: 13194 (million) % 156.92/22.86 % (357725)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3888915461:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2897 on theBenchmark for (2897ds/757Mi) % 156.92/22.86 % (357725)Instruction limit reached! % 156.92/22.86 % (357725)------------------------------ % 156.92/22.86 % (357725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.92/22.86 % (357725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.92/22.86 % (357725)CaDiCaL version: 2.1.3 % 156.92/22.86 % (357725)Termination reason: Instruction limit % 156.92/22.86 % (357725)Termination phase: Saturation % 156.92/22.86 % (357725)Time elapsed: 0.516 s % 156.92/22.86 % (357725)Peak memory usage: 98 MB % 156.92/22.86 % (357725)Instructions burned: 759 (million) % 156.92/22.86 % (357727)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3573480444:i=13913:ss=axioms:sgt=8_2890 on theBenchmark for (2890ds/13913Mi) % 156.92/22.86 % (357723)Instruction limit reached! % 156.92/22.86 % (357723)------------------------------ % 156.92/22.86 % (357723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.92/22.86 % (357723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.92/22.86 % (357723)CaDiCaL version: 2.1.3 % 156.92/22.86 % (357723)Termination reason: Instruction limit % 156.92/22.86 % (357723)Termination phase: Saturation % 156.92/22.86 % (357723)Time elapsed: 1.861 s % 156.92/22.86 % (357723)Peak memory usage: 99 MB % 156.92/22.86 % (357723)Instructions burned: 3706 (million) % 156.92/22.86 % (357707)Instruction limit reached! % 156.92/22.86 % (357707)------------------------------ % 156.92/22.86 % (357707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.92/22.86 % (357707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.92/22.86 % (357707)CaDiCaL version: 2.1.3 % 156.92/22.86 % (357707)Termination reason: Instruction limit % 156.92/22.86 % (357707)Termination phase: Saturation % 156.92/22.86 % (357707)Time elapsed: 8.714 s % 156.92/22.86 % (357707)Peak memory usage: 194 MB % 156.92/22.86 % (357707)Instructions burned: 14156 (million) % 156.92/22.86 % (357729)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2925405341:i=9925:aac=none_2880 on theBenchmark for (2880ds/9925Mi) % 156.92/22.86 % (357730)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3604639799:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2880 on theBenchmark for (2880ds/2479Mi) % 180.61/26.13 % (357717)Instruction limit reached! % 180.61/26.13 % (357717)------------------------------ % 180.61/26.13 % (357717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.61/26.13 % (357717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.61/26.13 % (357717)CaDiCaL version: 2.1.3 % 180.61/26.13 % (357717)Termination reason: Instruction limit % 180.61/26.13 % (357717)Termination phase: Saturation % 180.61/26.13 % (357717)Time elapsed: 6.695 s % 180.61/26.13 % (357717)Peak memory usage: 264 MB % 180.61/26.13 % (357717)Instructions burned: 12113 (million) % 180.61/26.13 % (357730)Instruction limit reached! % 180.61/26.13 % (357730)------------------------------ % 180.61/26.13 % (357730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.61/26.13 % (357730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.61/26.13 % (357730)CaDiCaL version: 2.1.3 % 180.61/26.13 % (357730)Termination reason: Instruction limit % 180.61/26.13 % (357730)Termination phase: Saturation % 180.61/26.13 % (357730)Time elapsed: 1.371 s % 180.61/26.13 % (357730)Peak memory usage: 108 MB % 180.61/26.13 % (357730)Instructions burned: 2480 (million) % 180.61/26.13 % (357733)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2015412342:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2866 on theBenchmark for (2866ds/440Mi) % 180.61/26.13 % (357734)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2175661512:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2865 on theBenchmark for (2865ds/11145Mi) % 180.61/26.13 % (357733)Instruction limit reached! % 180.61/26.13 % (357733)------------------------------ % 180.61/26.13 % (357733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.61/26.13 % (357733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.61/26.13 % (357733)CaDiCaL version: 2.1.3 % 180.61/26.13 % (357733)Termination reason: Instruction limit % 180.61/26.13 % (357733)Termination phase: Saturation % 180.61/26.13 % (357733)Time elapsed: 0.233 s % 180.61/26.13 % (357733)Peak memory usage: 94 MB % 180.61/26.13 % (357733)Instructions burned: 441 (million) % 180.61/26.13 % (357737)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=1808558363:cts=off:i=3034:av=off:er=known:fsd=on_2862 on theBenchmark for (2862ds/3034Mi) % 180.61/26.13 % (357737)Instruction limit reached! % 180.61/26.13 % (357737)------------------------------ % 180.61/26.13 % (357737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.61/26.13 % (357737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.61/26.13 % (357737)CaDiCaL version: 2.1.3 % 180.61/26.13 % (357737)Termination reason: Instruction limit % 180.61/26.13 % (357737)Termination phase: Saturation % 180.61/26.13 % (357737)Time elapsed: 1.786 s % 180.61/26.13 % (357737)Peak memory usage: 151 MB % 180.61/26.13 % (357737)Instructions burned: 3035 (million) % 180.61/26.13 % (357739)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2344672381:st=2:s2a=on:i=524:s2at=2:ss=axioms_2842 on theBenchmark for (2842ds/524Mi) % 180.61/26.13 % (357739)Instruction limit reached! % 180.61/26.13 % (357739)------------------------------ % 180.61/26.13 % (357739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.61/26.13 % (357739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.61/26.13 % (357739)CaDiCaL version: 2.1.3 % 180.61/26.13 % (357739)Termination reason: Instruction limit % 180.61/26.13 % (357739)Termination phase: Saturation % 180.61/26.13 % (357739)Time elapsed: 0.272 s % 180.61/26.13 % (357739)Peak memory usage: 94 MB % 180.61/26.13 % (357739)Instructions burned: 526 (million) % 180.61/26.13 % (357741)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1822333552:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2838 on theBenchmark for (2838ds/1016Mi) % 180.61/26.13 % (357741)Instruction limit reached! % 180.61/26.13 % (357741)------------------------------ % 180.61/26.13 % (357741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.61/26.13 % (357741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.61/26.13 % (357741)CaDiCaL version: 2.1.3 % 180.61/26.13 % (357741)Termination reason: Instruction limit % 180.61/26.13 % (357741)Termination phase: Saturation % 180.61/26.13 % (357741)Time elapsed: 0.525 s % 180.61/26.13 % (357741)Peak memory usage: 109 MB % 180.61/26.13 % (357741)Instructions burned: 1017 (million) % 180.61/26.13 % (357743)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=608462823:i=14123:bd=preordered:ins=4_2831 on theBenchmark for (2831ds/14123Mi) % 236.66/34.05 % (357729)Instruction limit reached! % 236.66/34.05 % (357729)------------------------------ % 236.66/34.05 % (357729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.66/34.05 % (357729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.66/34.05 % (357729)CaDiCaL version: 2.1.3 % 236.66/34.05 % (357729)Termination reason: Instruction limit % 236.66/34.05 % (357729)Termination phase: Saturation % 236.66/34.05 % (357729)Time elapsed: 5.688 s % 236.66/34.05 % (357729)Peak memory usage: 184 MB % 236.66/34.05 % (357729)Instructions burned: 9927 (million) % 236.66/34.05 % (357745)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=849927402:i=5781:kws=precedence:bd=all:rawr=on_2822 on theBenchmark for (2822ds/5781Mi) % 236.66/34.05 % (357727)Instruction limit reached! % 236.66/34.05 % (357727)------------------------------ % 236.66/34.05 % (357727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.66/34.05 % (357727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.66/34.05 % (357727)CaDiCaL version: 2.1.3 % 236.66/34.05 % (357727)Termination reason: Instruction limit % 236.66/34.05 % (357727)Termination phase: Saturation % 236.66/34.05 % (357727)Time elapsed: 8.591 s % 236.66/34.05 % (357727)Peak memory usage: 184 MB % 236.66/34.05 % (357727)Instructions burned: 13913 (million) % 236.66/34.05 % (357747)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=1034489838:i=2448:gtgl=5:bd=preordered:gtg=all_2803 on theBenchmark for (2803ds/2448Mi) % 236.66/34.05 % (357734)Instruction limit reached! % 236.66/34.05 % (357734)------------------------------ % 236.66/34.05 % (357734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.66/34.05 % (357734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.66/34.05 % (357734)CaDiCaL version: 2.1.3 % 236.66/34.05 % (357734)Termination reason: Instruction limit % 236.66/34.05 % (357734)Termination phase: Saturation % 236.66/34.05 % (357734)Time elapsed: 6.647 s % 236.66/34.05 % (357734)Peak memory usage: 214 MB % 236.66/34.05 % (357734)Instructions burned: 11145 (million) % 236.66/34.05 % (357749)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2810637334:i=3223:kws=precedence:fgj=on:av=off_2796 on theBenchmark for (2796ds/3223Mi) % 236.66/34.05 % (357745)Instruction limit reached! % 236.66/34.05 % (357745)------------------------------ % 236.66/34.05 % (357745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.66/34.05 % (357745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.66/34.05 % (357745)CaDiCaL version: 2.1.3 % 236.66/34.05 % (357745)Termination reason: Instruction limit % 236.66/34.05 % (357745)Termination phase: Saturation % 236.66/34.05 % (357745)Time elapsed: 2.752 s % 236.66/34.05 % (357745)Peak memory usage: 113 MB % 236.66/34.05 % (357745)Instructions burned: 5783 (million) % 236.66/34.05 % (357751)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2050031354:st=5.6:i=2033:sd=3:ss=axioms_2792 on theBenchmark for (2792ds/2033Mi) % 236.66/34.05 % (357747)Instruction limit reached! % 236.66/34.05 % (357747)------------------------------ % 236.66/34.05 % (357747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.66/34.05 % (357747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.66/34.05 % (357747)CaDiCaL version: 2.1.3 % 236.66/34.05 % (357747)Termination reason: Instruction limit % 236.66/34.05 % (357747)Termination phase: Saturation % 236.66/34.05 % (357747)Time elapsed: 1.385 s % 236.66/34.05 % (357747)Peak memory usage: 149 MB % 236.66/34.05 % (357747)Instructions burned: 2448 (million) % 236.66/34.05 % (357753)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3077746246:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2787 on theBenchmark for (2787ds/2055Mi) % 236.66/34.05 % (357751)Instruction limit reached! % 236.66/34.05 % (357751)------------------------------ % 236.66/34.05 % (357751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.66/34.05 % (357751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.66/34.05 % (357751)CaDiCaL version: 2.1.3 % 236.66/34.05 % (357751)Termination reason: Instruction limit % 236.66/34.05 % (357751)Termination phase: Saturation % 236.66/34.05 % (357751)Time elapsed: 1.286 s % 236.66/34.05 % (357751)Peak memory usage: 142 MB % 278.21/39.91 % (357751)Instructions burned: 2034 (million) % 278.21/39.91 % (357755)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=3777573606:i=21611:sd=3:ss=axioms_2778 on theBenchmark for (2778ds/21611Mi) % 278.21/39.91 % (357749)Instruction limit reached! % 278.21/39.91 % (357749)------------------------------ % 278.21/39.91 % (357749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.21/39.91 % (357749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.21/39.91 % (357749)CaDiCaL version: 2.1.3 % 278.21/39.91 % (357749)Termination reason: Instruction limit % 278.21/39.91 % (357749)Termination phase: Saturation % 278.21/39.91 % (357749)Time elapsed: 2.027 s % 278.21/39.91 % (357749)Peak memory usage: 152 MB % 278.21/39.91 % (357749)Instructions burned: 3224 (million) % 278.21/39.91 % (357757)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3618612404:i=4835:sd=13:ss=axioms:sgt=23_2774 on theBenchmark for (2774ds/4835Mi) % 278.21/39.91 % (357753)Instruction limit reached! % 278.21/39.91 % (357753)------------------------------ % 278.21/39.91 % (357753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.21/39.91 % (357753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.21/39.91 % (357753)CaDiCaL version: 2.1.3 % 278.21/39.91 % (357753)Termination reason: Instruction limit % 278.21/39.91 % (357753)Termination phase: Saturation % 278.21/39.91 % (357753)Time elapsed: 1.333 s % 278.21/39.91 % (357753)Peak memory usage: 138 MB % 278.21/39.91 % (357753)Instructions burned: 2055 (million) % 278.21/39.91 % (357759)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=3634798918:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2772 on theBenchmark for (2772ds/797Mi) % 278.21/39.91 % (357759)Instruction limit reached! % 278.21/39.91 % (357759)------------------------------ % 278.21/39.91 % (357759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.21/39.91 % (357759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.21/39.91 % (357759)CaDiCaL version: 2.1.3 % 278.21/39.91 % (357759)Termination reason: Instruction limit % 278.21/39.91 % (357759)Termination phase: Saturation % 278.21/39.91 % (357759)Time elapsed: 0.479 s % 278.21/39.91 % (357759)Peak memory usage: 96 MB % 278.21/39.91 % (357759)Instructions burned: 797 (million) % 278.21/39.91 % (357761)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2701975608:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2766 on theBenchmark for (2766ds/2326Mi) % 278.21/39.91 % (357761)Instruction limit reached! % 278.21/39.91 % (357761)------------------------------ % 278.21/39.91 % (357761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.21/39.91 % (357761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.21/39.91 % (357761)CaDiCaL version: 2.1.3 % 278.21/39.91 % (357761)Termination reason: Instruction limit % 278.21/39.91 % (357761)Termination phase: Saturation % 278.21/39.91 % (357761)Time elapsed: 1.486 s % 278.21/39.91 % (357761)Peak memory usage: 102 MB % 278.21/39.91 % (357761)Instructions burned: 2328 (million) % 278.21/39.91 % (357763)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2107901349:i=6038:nm=6_2749 on theBenchmark for (2749ds/6038Mi) % 278.21/39.91 % (357757)Instruction limit reached! % 278.21/39.91 % (357757)------------------------------ % 278.21/39.91 % (357757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.21/39.91 % (357757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.21/39.91 % (357757)CaDiCaL version: 2.1.3 % 278.21/39.91 % (357757)Termination reason: Instruction limit % 278.21/39.91 % (357757)Termination phase: Saturation % 278.21/39.91 % (357757)Time elapsed: 2.549 s % 278.21/39.91 % (357757)Peak memory usage: 106 MB % 278.21/39.91 % (357757)Instructions burned: 4836 (million) % 278.21/39.91 % (357765)lrs+10_1_sil=32000:sp=occurrence:random_seed=4031573347:st=2:i=33334:sd=3:ss=included:sgt=32_2747 on theBenchmark for (2747ds/33334Mi) % 278.21/39.91 % (357743)Instruction limit reached! % 278.21/39.91 % (357743)------------------------------ % 278.21/39.91 % (357743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 278.21/39.91 % (357743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 278.21/39.91 % (357743)CaDiCaL vTerminated %------------------------------------------------------------------------------