%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW251+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 : 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 01:29:56 PM UTC 2026 % Result : Timeout 295.07s 42.39s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWW251+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.25/0.28 % Computer : n011.cluster.edu % 0.25/0.28 % Model : x86_64 x86_64 % 0.25/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.25/0.28 % Memory : 8046.5625MB % 0.25/0.28 % OS : Linux 6.8.0-71-generic % 0.25/0.28 % CPULimit : 300 % 0.25/0.28 % WCLimit : 300 % 0.25/0.28 % DateTime : Mon Sep 28 13:24:45 UTC 2026 % 0.25/0.28 % CPUTime : % 0.25/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.25/0.33 Running first-order theorem proving % 0.25/0.33 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 % 23.62/4.14 % (3381193)Detected formulas, will run a generic FOF schedule. % 23.62/4.14 % (3381198)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=1714580277:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 23.62/4.14 % (3381201)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1808837244:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 23.62/4.14 % (3381203)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=995845199:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 23.62/4.14 % (3381202)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1649883752:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 23.62/4.14 % (3381204)dis-21_1_sil=8000:lcm=predicate:random_seed=197858062: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) % 23.62/4.14 % (3381199)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=2291181585:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 23.62/4.14 % (3381200)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=323121550:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 23.62/4.14 % (3381201)Refutation not found, incomplete strategy % 23.62/4.14 % (3381201)------------------------------ % 23.62/4.14 % (3381201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.14 % (3381201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.14 % (3381201)CaDiCaL version: 2.1.3 % 23.62/4.14 % (3381201)Termination reason: Refutation not found, incomplete strategy % 23.62/4.14 % (3381201)Time elapsed: 0.007 s % 23.62/4.14 % (3381201)Peak memory usage: 89 MB % 23.62/4.14 % (3381201)Instructions burned: 4 (million) % 23.62/4.14 % (3381202)Instruction limit reached! % 23.62/4.14 % (3381202)------------------------------ % 23.62/4.14 % (3381202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.14 % (3381202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.14 % (3381202)CaDiCaL version: 2.1.3 % 23.62/4.14 % (3381202)Termination reason: Instruction limit % 23.62/4.14 % (3381202)Termination phase: Saturation % 23.62/4.14 % (3381202)Time elapsed: 0.117 s % 23.62/4.14 % (3381202)Peak memory usage: 90 MB % 23.62/4.14 % (3381202)Instructions burned: 119 (million) % 23.62/4.14 % (3381204)Instruction limit reached! % 23.62/4.14 % (3381204)------------------------------ % 23.62/4.14 % (3381204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.14 % (3381204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.14 % (3381204)CaDiCaL version: 2.1.3 % 23.62/4.14 % (3381204)Termination reason: Instruction limit % 23.62/4.14 % (3381204)Termination phase: Saturation % 23.62/4.14 % (3381204)Time elapsed: 0.119 s % 23.62/4.14 % (3381204)Peak memory usage: 91 MB % 23.62/4.14 % (3381204)Instructions burned: 129 (million) % 23.62/4.14 % (3381203)Instruction limit reached! % 23.62/4.14 % (3381203)------------------------------ % 23.62/4.14 % (3381203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.62/4.14 % (3381203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.62/4.14 % (3381203)CaDiCaL version: 2.1.3 % 23.62/4.14 % (3381203)Termination reason: Instruction limit % 23.62/4.14 % (3381203)Termination phase: Saturation % 23.62/4.14 % (3381203)Time elapsed: 0.133 s % 23.62/4.14 % (3381203)Peak memory usage: 91 MB % 23.62/4.14 % (3381203)Instructions burned: 139 (million) % 23.62/4.14 % (3381212)lrs+10_1_sil=8000:sp=occurrence:random_seed=1073799022:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi) % 23.62/4.14 % (3381213)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4040350469:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi) % 23.62/4.14 % (3381201)------------------------------ % 23.62/4.14 % (3381201)------------------------------ % 23.62/4.14 % (3381214)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1016136528:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 23.62/4.14 % (3381212)Instruction limit reached! % 23.62/4.14 % (3381212)------------------------------ % 23.62/4.14 % (3381212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.52 % (3381212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.52 % (3381212)CaDiCaL version: 2.1.3 % 33.03/5.52 % (3381212)Termination reason: Instruction limit % 33.03/5.52 % (3381212)Termination phase: Saturation % 33.03/5.52 % (3381212)Time elapsed: 0.151 s % 33.03/5.52 % (3381212)Peak memory usage: 92 MB % 33.03/5.52 % (3381212)Instructions burned: 286 (million) % 33.03/5.52 % (3381213)Instruction limit reached! % 33.03/5.52 % (3381213)------------------------------ % 33.03/5.52 % (3381213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.52 % (3381213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.52 % (3381213)CaDiCaL version: 2.1.3 % 33.03/5.52 % (3381213)Termination reason: Instruction limit % 33.03/5.52 % (3381213)Termination phase: Saturation % 33.03/5.52 % (3381213)Time elapsed: 0.126 s % 33.03/5.52 % (3381213)Peak memory usage: 93 MB % 33.03/5.52 % (3381213)Instructions burned: 157 (million) % 33.03/5.52 % (3381218)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=1348208236:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi) % 33.03/5.52 % (3381219)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3811139745:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi) % 33.03/5.52 % (3381214)Instruction limit reached! % 33.03/5.52 % (3381214)------------------------------ % 33.03/5.52 % (3381214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.52 % (3381214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.52 % (3381214)CaDiCaL version: 2.1.3 % 33.03/5.52 % (3381214)Termination reason: Instruction limit % 33.03/5.52 % (3381214)Termination phase: Saturation % 33.03/5.52 % (3381214)Time elapsed: 0.295 s % 33.03/5.52 % (3381214)Peak memory usage: 91 MB % 33.03/5.52 % (3381214)Instructions burned: 326 (million) % 33.03/5.52 % (3381218)Instruction limit reached! % 33.03/5.52 % (3381218)------------------------------ % 33.03/5.52 % (3381218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.52 % (3381218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.52 % (3381218)CaDiCaL version: 2.1.3 % 33.03/5.52 % (3381218)Termination reason: Instruction limit % 33.03/5.52 % (3381218)Termination phase: Saturation % 33.03/5.52 % (3381218)Time elapsed: 0.185 s % 33.03/5.52 % (3381218)Peak memory usage: 91 MB % 33.03/5.52 % (3381218)Instructions burned: 249 (million) % 33.03/5.52 % (3381220)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=387000603:i=2350_2991 on theBenchmark for (2991ds/2350Mi) % 33.03/5.52 % (3381219)Instruction limit reached! % 33.03/5.52 % (3381219)------------------------------ % 33.03/5.52 % (3381219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.52 % (3381219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.52 % (3381219)CaDiCaL version: 2.1.3 % 33.03/5.52 % (3381219)Termination reason: Instruction limit % 33.03/5.52 % (3381219)Termination phase: Saturation % 33.03/5.52 % (3381219)Time elapsed: 0.122 s % 33.03/5.52 % (3381219)Peak memory usage: 90 MB % 33.03/5.52 % (3381219)Instructions burned: 297 (million) % 33.03/5.52 % (3381223)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=811267504:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi) % 33.03/5.52 % (3381225)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1061570877:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi) % 33.03/5.52 % (3381226)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=702156557:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi) % 33.03/5.52 % (3381223)Instruction limit reached! % 33.03/5.52 % (3381223)------------------------------ % 33.03/5.52 % (3381223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.03/5.52 % (3381223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.03/5.52 % (3381223)CaDiCaL version: 2.1.3 % 33.03/5.52 % (3381223)Termination reason: Instruction limit % 33.03/5.52 % (3381223)Termination phase: Saturation % 33.03/5.52 % (3381223)Time elapsed: 0.105 s % 33.03/5.52 % (3381223)Peak memory usage: 90 MB % 33.03/5.52 % (3381223)Instructions burned: 113 (million) % 33.03/5.52 % (3381225)Refutation not found, incomplete strategy % 33.03/5.52 % (3381225)------------------------------ % 33.03/5.52 % (3381225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.13/10.56 % (3381225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.13/10.56 % (3381225)CaDiCaL version: 2.1.3 % 69.13/10.56 % (3381225)Termination reason: Refutation not found, incomplete strategy % 69.13/10.56 % (3381225)Time elapsed: 0.099 s % 69.13/10.56 % (3381225)Peak memory usage: 90 MB % 69.13/10.56 % (3381225)Instructions burned: 118 (million) % 69.13/10.56 % (3381226)Instruction limit reached! % 69.13/10.56 % (3381226)------------------------------ % 69.13/10.56 % (3381226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.13/10.56 % (3381226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.13/10.56 % (3381226)CaDiCaL version: 2.1.3 % 69.13/10.56 % (3381226)Termination reason: Instruction limit % 69.13/10.56 % (3381226)Termination phase: Saturation % 69.13/10.56 % (3381226)Time elapsed: 0.102 s % 69.13/10.56 % (3381226)Peak memory usage: 90 MB % 69.13/10.56 % (3381226)Instructions burned: 114 (million) % 69.13/10.56 % (3381232)lrs+10_1_sil=8000:sp=occurrence:random_seed=3395320050:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi) % 69.13/10.57 % (3381235)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2916452387:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi) % 69.13/10.57 % (3381225)------------------------------ % 69.13/10.57 % (3381225)------------------------------ % 69.13/10.57 % (3381238)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2287242032:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi) % 69.13/10.57 % (3381235)Instruction limit reached! % 69.13/10.57 % (3381235)------------------------------ % 69.13/10.57 % (3381235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.13/10.57 % (3381235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.13/10.57 % (3381235)CaDiCaL version: 2.1.3 % 69.13/10.57 % (3381235)Termination reason: Instruction limit % 69.13/10.57 % (3381235)Termination phase: Saturation % 69.13/10.57 % (3381235)Time elapsed: 0.392 s % 69.13/10.57 % (3381235)Peak memory usage: 94 MB % 69.13/10.57 % (3381235)Instructions burned: 437 (million) % 69.13/10.57 % (3381240)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1405927522:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi) % 69.13/10.57 % (3381240)Instruction limit reached! % 69.13/10.57 % (3381240)------------------------------ % 69.13/10.57 % (3381240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.13/10.57 % (3381240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.13/10.57 % (3381240)CaDiCaL version: 2.1.3 % 69.13/10.57 % (3381240)Termination reason: Instruction limit % 69.13/10.57 % (3381240)Termination phase: Saturation % 69.13/10.57 % (3381240)Time elapsed: 0.122 s % 69.13/10.57 % (3381240)Peak memory usage: 92 MB % 69.13/10.57 % (3381240)Instructions burned: 136 (million) % 69.13/10.57 % (3381232)Instruction limit reached! % 69.13/10.57 % (3381232)------------------------------ % 69.13/10.57 % (3381232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.13/10.57 % (3381232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.13/10.57 % (3381232)CaDiCaL version: 2.1.3 % 69.13/10.57 % (3381232)Termination reason: Instruction limit % 69.13/10.57 % (3381232)Termination phase: Saturation % 69.13/10.57 % (3381232)Time elapsed: 0.860 s % 69.13/10.57 % (3381232)Peak memory usage: 97 MB % 69.13/10.57 % (3381232)Instructions burned: 908 (million) % 69.13/10.57 % (3381242)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=547808354:st=8:i=592:sd=3:ep=RST:ss=axioms_2974 on theBenchmark for (2974ds/592Mi) % 69.13/10.57 % (3381243)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3507883696:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi) % 69.13/10.57 % (3381242)Instruction limit reached! % 69.13/10.57 % (3381242)------------------------------ % 69.13/10.57 % (3381242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.13/10.57 % (3381242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.13/10.57 % (3381242)CaDiCaL version: 2.1.3 % 69.13/10.57 % (3381242)Termination reason: Instruction limit % 69.13/10.57 % (3381242)Termination phase: Saturation % 69.13/10.57 % (3381242)Time elapsed: 0.548 s % 69.13/10.57 % (3381242)Peak memory usage: 98 MB % 69.13/10.57 % (3381242)Instructions burned: 593 (million) % 69.13/10.57 % (3381220)Instruction limit reached! % 69.13/10.57 % (3381220)------------------------------ % 111.19/16.45 % (3381220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.19/16.45 % (3381220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.19/16.45 % (3381220)CaDiCaL version: 2.1.3 % 111.19/16.45 % (3381220)Termination reason: Instruction limit % 111.19/16.45 % (3381220)Termination phase: Saturation % 111.19/16.45 % (3381220)Time elapsed: 2.297 s % 111.19/16.45 % (3381220)Peak memory usage: 148 MB % 111.19/16.45 % (3381220)Instructions burned: 2350 (million) % 111.19/16.45 % (3381246)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=3630904836:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/125Mi) % 111.19/16.45 % (3381246)Instruction limit reached! % 111.19/16.45 % (3381246)------------------------------ % 111.19/16.45 % (3381246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.19/16.45 % (3381246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.19/16.45 % (3381246)CaDiCaL version: 2.1.3 % 111.19/16.45 % (3381246)Termination reason: Instruction limit % 111.19/16.45 % (3381246)Termination phase: Saturation % 111.19/16.45 % (3381246)Time elapsed: 0.071 s % 111.19/16.45 % (3381246)Peak memory usage: 91 MB % 111.19/16.45 % (3381246)Instructions burned: 125 (million) % 111.19/16.45 % (3381247)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1671425001:i=134:gtgl=5:slsql=off:gtg=exists_sym_2965 on theBenchmark for (2965ds/134Mi) % 111.19/16.45 % (3381247)Instruction limit reached! % 111.19/16.45 % (3381247)------------------------------ % 111.19/16.45 % (3381247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.19/16.45 % (3381247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.19/16.45 % (3381247)CaDiCaL version: 2.1.3 % 111.19/16.45 % (3381247)Termination reason: Instruction limit % 111.19/16.45 % (3381247)Termination phase: Saturation % 111.19/16.45 % (3381247)Time elapsed: 0.120 s % 111.19/16.45 % (3381247)Peak memory usage: 90 MB % 111.19/16.45 % (3381247)Instructions burned: 134 (million) % 111.19/16.45 % (3381251)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=448748652:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/141Mi) % 111.19/16.45 % (3381251)Refutation not found, incomplete strategy % 111.19/16.45 % (3381251)------------------------------ % 111.19/16.45 % (3381251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.19/16.45 % (3381251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.19/16.45 % (3381251)CaDiCaL version: 2.1.3 % 111.19/16.45 % (3381251)Termination reason: Refutation not found, incomplete strategy % 111.19/16.45 % (3381251)Time elapsed: 0.007 s % 111.19/16.45 % (3381251)Peak memory usage: 89 MB % 111.19/16.45 % (3381251)Instructions burned: 4 (million) % 111.19/16.45 % (3381253)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=433836313:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi) % 111.19/16.45 % (3381253)Refutation not found, incomplete strategy % 111.19/16.45 % (3381253)------------------------------ % 111.19/16.45 % (3381253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.19/16.45 % (3381253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.19/16.45 % (3381253)CaDiCaL version: 2.1.3 % 111.19/16.45 % (3381253)Termination reason: Refutation not found, incomplete strategy % 111.19/16.45 % (3381253)Time elapsed: 0.010 s % 111.19/16.45 % (3381253)Peak memory usage: 89 MB % 111.19/16.45 % (3381253)Instructions burned: 7 (million) % 111.19/16.45 % (3381251)------------------------------ % 111.19/16.45 % (3381251)------------------------------ % 111.19/16.45 % (3381253)------------------------------ % 111.19/16.45 % (3381253)------------------------------ % 111.19/16.45 % (3381256)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=2846208139:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi) % 111.19/16.45 % (3381257)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=2601857861:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2955 on theBenchmark for (2955ds/150Mi) % 111.19/16.45 % (3381257)Instruction limit reached! % 111.19/16.45 % (3381257)------------------------------ % 111.19/16.45 % (3381257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.34 % (3381257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.34 % (3381257)CaDiCaL version: 2.1.3 % 146.04/21.34 % (3381257)Termination reason: Instruction limit % 146.04/21.34 % (3381257)Termination phase: Saturation % 146.04/21.34 % (3381257)Time elapsed: 0.137 s % 146.04/21.34 % (3381257)Peak memory usage: 91 MB % 146.04/21.34 % (3381257)Instructions burned: 151 (million) % 146.04/21.34 % (3381260)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=381866988:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi) % 146.04/21.34 % (3381238)Instruction limit reached! % 146.04/21.34 % (3381238)------------------------------ % 146.04/21.34 % (3381238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.34 % (3381238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.34 % (3381238)CaDiCaL version: 2.1.3 % 146.04/21.34 % (3381238)Termination reason: Instruction limit % 146.04/21.34 % (3381238)Termination phase: Saturation % 146.04/21.34 % (3381238)Time elapsed: 4.881 s % 146.04/21.34 % (3381238)Peak memory usage: 152 MB % 146.04/21.34 % (3381238)Instructions burned: 5203 (million) % 146.04/21.34 % (3381266)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=375914886:i=667:av=off:fsr=off_2929 on theBenchmark for (2929ds/667Mi) % 146.04/21.34 % (3381266)Refutation not found, incomplete strategy % 146.04/21.34 % (3381266)------------------------------ % 146.04/21.34 % (3381266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.34 % (3381266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.34 % (3381266)CaDiCaL version: 2.1.3 % 146.04/21.34 % (3381266)Termination reason: Refutation not found, incomplete strategy % 146.04/21.34 % (3381266)Time elapsed: 0.102 s % 146.04/21.34 % (3381266)Peak memory usage: 91 MB % 146.04/21.34 % (3381266)Instructions burned: 110 (million) % 146.04/21.34 % (3381266)------------------------------ % 146.04/21.34 % (3381266)------------------------------ % 146.04/21.34 % (3381268)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=2969602098:s2a=on:i=185:s2at=1.8:fdi=4_2921 on theBenchmark for (2921ds/185Mi) % 146.04/21.34 % (3381268)Instruction limit reached! % 146.04/21.34 % (3381268)------------------------------ % 146.04/21.34 % (3381268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.34 % (3381268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.34 % (3381268)CaDiCaL version: 2.1.3 % 146.04/21.34 % (3381268)Termination reason: Instruction limit % 146.04/21.34 % (3381268)Termination phase: Saturation % 146.04/21.34 % (3381268)Time elapsed: 0.164 s % 146.04/21.34 % (3381268)Peak memory usage: 92 MB % 146.04/21.34 % (3381268)Instructions burned: 186 (million) % 146.04/21.34 % (3381270)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=249889466:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2917 on theBenchmark for (2917ds/193Mi) % 146.04/21.34 % (3381270)Instruction limit reached! % 146.04/21.34 % (3381270)------------------------------ % 146.04/21.34 % (3381270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.34 % (3381270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.34 % (3381270)CaDiCaL version: 2.1.3 % 146.04/21.34 % (3381270)Termination reason: Instruction limit % 146.04/21.34 % (3381270)Termination phase: Saturation % 146.04/21.34 % (3381270)Time elapsed: 0.194 s % 146.04/21.34 % (3381270)Peak memory usage: 93 MB % 146.04/21.34 % (3381270)Instructions burned: 193 (million) % 146.04/21.34 % (3381272)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1835064520:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2912 on theBenchmark for (2912ds/4850Mi) % 146.04/21.34 % (3381272)Refutation not found, incomplete strategy % 146.04/21.34 % (3381272)------------------------------ % 146.04/21.34 % (3381272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.34 % (3381272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.34 % (3381272)CaDiCaL version: 2.1.3 % 146.04/21.34 % (3381272)Termination reason: Refutation not found, incomplete strategy % 146.04/21.34 % (3381272)Time elapsed: 0.085 s % 146.04/21.34 % (3381272)Peak memory usage: 91 MB % 146.04/21.34 % (3381272)Instructions burned: 95 (million) % 146.04/21.34 % (3381272)------------------------------ % 146.04/21.34 % (3381272)------------------------------ % 146.04/21.34 % (3381274)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=15589514:i=12111:sd=1:ss=included_2904 on theBenchmark for (2904ds/12111Mi) % 171.53/25.00 % (3381256)Instruction limit reached! % 171.53/25.00 % (3381256)------------------------------ % 171.53/25.00 % (3381256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.53/25.00 % (3381256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.53/25.00 % (3381256)CaDiCaL version: 2.1.3 % 171.53/25.00 % (3381256)Termination reason: Instruction limit % 171.53/25.00 % (3381256)Termination phase: Saturation % 171.53/25.00 % (3381256)Time elapsed: 6.092 s % 171.53/25.00 % (3381256)Peak memory usage: 178 MB % 171.53/25.00 % (3381256)Instructions burned: 6060 (million) % 171.53/25.00 % (3381278)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1998028779:i=319:kws=precedence:fsr=off_2893 on theBenchmark for (2893ds/319Mi) % 171.53/25.00 % (3381278)Instruction limit reached! % 171.53/25.00 % (3381278)------------------------------ % 171.53/25.00 % (3381278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.53/25.00 % (3381278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.53/25.00 % (3381278)CaDiCaL version: 2.1.3 % 171.53/25.00 % (3381278)Termination reason: Instruction limit % 171.53/25.00 % (3381278)Termination phase: Saturation % 171.53/25.00 % (3381278)Time elapsed: 0.293 s % 171.53/25.00 % (3381278)Peak memory usage: 94 MB % 171.53/25.00 % (3381278)Instructions burned: 320 (million) % 171.53/25.00 % (3381280)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2842870951:i=2064:ep=RST_2887 on theBenchmark for (2887ds/2064Mi) % 171.53/25.00 % (3381280)Instruction limit reached! % 171.53/25.00 % (3381280)------------------------------ % 171.53/25.00 % (3381280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.53/25.00 % (3381280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.53/25.00 % (3381280)CaDiCaL version: 2.1.3 % 171.53/25.00 % (3381280)Termination reason: Instruction limit % 171.53/25.00 % (3381280)Termination phase: Saturation % 171.53/25.00 % (3381280)Time elapsed: 1.634 s % 171.53/25.00 % (3381280)Peak memory usage: 106 MB % 171.53/25.00 % (3381280)Instructions burned: 2065 (million) % 171.53/25.00 % (3381285)dis-1011_128_sil=32000:random_seed=3219391607:i=3706:ep=RST:av=off_2868 on theBenchmark for (2868ds/3706Mi) % 171.53/25.00 % (3381243)Instruction limit reached! % 171.53/25.00 % (3381243)------------------------------ % 171.53/25.00 % (3381243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.53/25.00 % (3381243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.53/25.00 % (3381243)CaDiCaL version: 2.1.3 % 171.53/25.00 % (3381243)Termination reason: Instruction limit % 171.53/25.00 % (3381243)Termination phase: Saturation % 171.53/25.00 % (3381243)Time elapsed: 11.755 s % 171.53/25.00 % (3381243)Peak memory usage: 215 MB % 171.53/25.00 % (3381243)Instructions burned: 13194 (million) % 171.53/25.00 % (3381440)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=496885361:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2854 on theBenchmark for (2854ds/757Mi) % 171.53/25.00 % (3381440)Instruction limit reached! % 171.53/25.00 % (3381440)------------------------------ % 171.53/25.00 % (3381440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.53/25.00 % (3381440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.53/25.00 % (3381440)CaDiCaL version: 2.1.3 % 171.53/25.00 % (3381440)Termination reason: Instruction limit % 171.53/25.00 % (3381440)Termination phase: Saturation % 171.53/25.00 % (3381440)Time elapsed: 0.414 s % 171.53/25.00 % (3381440)Peak memory usage: 96 MB % 171.53/25.00 % (3381440)Instructions burned: 757 (million) % 171.53/25.00 % (3381442)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3785063843:i=13913:ss=axioms:sgt=8_2848 on theBenchmark for (2848ds/13913Mi) % 171.53/25.00 % (3381285)Instruction limit reached! % 171.53/25.00 % (3381285)------------------------------ % 171.53/25.00 % (3381285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 171.53/25.00 % (3381285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 171.53/25.00 % (3381285)CaDiCaL version: 2.1.3 % 171.53/25.00 % (3381285)Termination reason: Instruction limit % 171.53/25.00 % (3381285)Termination phase: Saturation % 171.53/25.00 % (3381285)Time elapsed: 2.184 s % 171.53/25.00 % (3381285)Peak memory usage: 123 MB % 171.53/25.00 % (3381285)Instructions burned: 3707 (million) % 171.53/25.00 % (3381444)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2893406384:i=9925:aac=none_2844 on theBenchmark for (2844ds/9925Mi) % 202.11/29.26 % (3381260)Instruction limit reached! % 202.11/29.26 % (3381260)------------------------------ % 202.11/29.26 % (3381260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.11/29.26 % (3381260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.11/29.26 % (3381260)CaDiCaL version: 2.1.3 % 202.11/29.26 % (3381260)Termination reason: Instruction limit % 202.11/29.26 % (3381260)Termination phase: Saturation % 202.11/29.26 % (3381260)Time elapsed: 11.701 s % 202.11/29.26 % (3381260)Peak memory usage: 243 MB % 202.11/29.26 % (3381260)Instructions burned: 14156 (million) % 202.11/29.26 % (3381446)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1484484228:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2832 on theBenchmark for (2832ds/2479Mi) % 202.11/29.26 % (3381446)Refutation not found, incomplete strategy % 202.11/29.26 % (3381446)------------------------------ % 202.11/29.26 % (3381446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.11/29.26 % (3381446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.11/29.26 % (3381446)CaDiCaL version: 2.1.3 % 202.11/29.26 % (3381446)Termination reason: Refutation not found, incomplete strategy % 202.11/29.26 % (3381446)Time elapsed: 0.026 s % 202.11/29.26 % (3381446)Peak memory usage: 90 MB % 202.11/29.26 % (3381446)Instructions burned: 44 (million) % 202.11/29.26 % (3381446)------------------------------ % 202.11/29.26 % (3381446)------------------------------ % 202.11/29.26 % (3381448)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=837490854:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2828 on theBenchmark for (2828ds/440Mi) % 202.11/29.26 % (3381448)Instruction limit reached! % 202.11/29.26 % (3381448)------------------------------ % 202.11/29.26 % (3381448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.11/29.26 % (3381448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.11/29.26 % (3381448)CaDiCaL version: 2.1.3 % 202.11/29.26 % (3381448)Termination reason: Instruction limit % 202.11/29.26 % (3381448)Termination phase: Saturation % 202.11/29.26 % (3381448)Time elapsed: 0.235 s % 202.11/29.26 % (3381448)Peak memory usage: 94 MB % 202.11/29.26 % (3381448)Instructions burned: 441 (million) % 202.11/29.26 % (3381450)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3147512542:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2823 on theBenchmark for (2823ds/11145Mi) % 202.11/29.26 % (3381274)Instruction limit reached! % 202.11/29.26 % (3381274)------------------------------ % 202.11/29.26 % (3381274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.11/29.26 % (3381274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.11/29.26 % (3381274)CaDiCaL version: 2.1.3 % 202.11/29.26 % (3381274)Termination reason: Instruction limit % 202.11/29.26 % (3381274)Termination phase: Saturation % 202.11/29.26 % (3381274)Time elapsed: 8.440 s % 202.11/29.26 % (3381274)Peak memory usage: 230 MB % 202.11/29.26 % (3381274)Instructions burned: 12112 (million) % 202.11/29.26 % (3381452)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=3102024883:cts=off:i=3034:av=off:er=known:fsd=on_2817 on theBenchmark for (2817ds/3034Mi) % 202.11/29.26 % (3381452)Instruction limit reached! % 202.11/29.26 % (3381452)------------------------------ % 202.11/29.26 % (3381452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.11/29.26 % (3381452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.11/29.26 % (3381452)CaDiCaL version: 2.1.3 % 202.11/29.26 % (3381452)Termination reason: Instruction limit % 202.11/29.26 % (3381452)Termination phase: Saturation % 202.11/29.26 % (3381452)Time elapsed: 1.716 s % 202.11/29.26 % (3381452)Peak memory usage: 144 MB % 202.11/29.26 % (3381452)Instructions burned: 3036 (million) % 202.11/29.26 % (3381454)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2255012694:st=2:s2a=on:i=524:s2at=2:ss=axioms_2798 on theBenchmark for (2798ds/524Mi) % 202.11/29.26 % (3381454)Instruction limit reached! % 202.11/29.26 % (3381454)------------------------------ % 202.11/29.26 % (3381454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.11/29.26 % (3381454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381454)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381454)Termination reason: Instruction limit % 236.38/34.08 % (3381454)Termination phase: Saturation % 236.38/34.08 % (3381454)Time elapsed: 0.275 s % 236.38/34.08 % (3381454)Peak memory usage: 97 MB % 236.38/34.08 % (3381454)Instructions burned: 524 (million) % 236.38/34.08 % (3381456)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1999535853:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2794 on theBenchmark for (2794ds/1016Mi) % 236.38/34.08 % (3381444)Instruction limit reached! % 236.38/34.08 % (3381444)------------------------------ % 236.38/34.08 % (3381444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.38/34.08 % (3381444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381444)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381444)Termination reason: Instruction limit % 236.38/34.08 % (3381444)Termination phase: Saturation % 236.38/34.08 % (3381444)Time elapsed: 5.484 s % 236.38/34.08 % (3381444)Peak memory usage: 193 MB % 236.38/34.08 % (3381444)Instructions burned: 9927 (million) % 236.38/34.08 % (3381456)Instruction limit reached! % 236.38/34.08 % (3381456)------------------------------ % 236.38/34.08 % (3381456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.38/34.08 % (3381456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381456)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381456)Termination reason: Instruction limit % 236.38/34.08 % (3381456)Termination phase: Saturation % 236.38/34.08 % (3381456)Time elapsed: 0.445 s % 236.38/34.08 % (3381456)Peak memory usage: 123 MB % 236.38/34.08 % (3381456)Instructions burned: 1018 (million) % 236.38/34.08 % (3381458)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=775405811:i=14123:bd=preordered:ins=4_2788 on theBenchmark for (2788ds/14123Mi) % 236.38/34.08 % (3381459)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2087839080:i=5781:kws=precedence:bd=all:rawr=on_2787 on theBenchmark for (2787ds/5781Mi) % 236.38/34.08 % (3381442)Instruction limit reached! % 236.38/34.08 % (3381442)------------------------------ % 236.38/34.08 % (3381442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.38/34.08 % (3381442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381442)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381442)Termination reason: Instruction limit % 236.38/34.08 % (3381442)Termination phase: Saturation % 236.38/34.08 % (3381442)Time elapsed: 7.229 s % 236.38/34.08 % (3381442)Peak memory usage: 208 MB % 236.38/34.08 % (3381442)Instructions burned: 13915 (million) % 236.38/34.08 % (3381462)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=3573305124:i=2448:gtgl=5:bd=preordered:gtg=all_2774 on theBenchmark for (2774ds/2448Mi) % 236.38/34.08 % (3381450)Instruction limit reached! % 236.38/34.08 % (3381450)------------------------------ % 236.38/34.08 % (3381450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.38/34.08 % (3381450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381450)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381450)Termination reason: Instruction limit % 236.38/34.08 % (3381450)Termination phase: Saturation % 236.38/34.08 % (3381450)Time elapsed: 6.299 s % 236.38/34.08 % (3381450)Peak memory usage: 208 MB % 236.38/34.08 % (3381450)Instructions burned: 11145 (million) % 236.38/34.08 % (3381459)Instruction limit reached! % 236.38/34.08 % (3381459)------------------------------ % 236.38/34.08 % (3381459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.38/34.08 % (3381459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381459)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381459)Termination reason: Instruction limit % 236.38/34.08 % (3381459)Termination phase: Saturation % 236.38/34.08 % (3381459)Time elapsed: 2.878 s % 236.38/34.08 % (3381459)Peak memory usage: 144 MB % 236.38/34.08 % (3381459)Instructions burned: 5781 (million) % 236.38/34.08 % (3381462)Instruction limit reached! % 236.38/34.08 % (3381462)------------------------------ % 236.38/34.08 % (3381462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.38/34.08 % (3381462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.38/34.08 % (3381462)CaDiCaL version: 2.1.3 % 236.38/34.08 % (3381462)Termination reason: Instruction limit % 236.38/34.08 % (3381462)Termination phase: Saturation % 236.38/34.08 % (3381462)Time elapsed: 1.512 s % 236.38/34.08 % (3381462)Peak memory usage: 148 MB % 295.07/42.39 % (3381462)Instructions burned: 2449 (million) % 295.07/42.39 % (3381464)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2465869285:i=3223:kws=precedence:fgj=on:av=off_2759 on theBenchmark for (2759ds/3223Mi) % 295.07/42.39 % (3381467)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1260640184:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2757 on theBenchmark for (2757ds/2055Mi) % 295.07/42.39 % (3381466)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4053523030:st=5.6:i=2033:sd=3:ss=axioms_2757 on theBenchmark for (2757ds/2033Mi) % 295.07/42.39 % (3381467)Instruction limit reached! % 295.07/42.39 % (3381467)------------------------------ % 295.07/42.39 % (3381467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.39 % (3381467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.39 % (3381467)CaDiCaL version: 2.1.3 % 295.07/42.39 % (3381467)Termination reason: Instruction limit % 295.07/42.39 % (3381467)Termination phase: Saturation % 295.07/42.39 % (3381467)Time elapsed: 1.193 s % 295.07/42.39 % (3381467)Peak memory usage: 136 MB % 295.07/42.39 % (3381467)Instructions burned: 2056 (million) % 295.07/42.39 % (3381466)Instruction limit reached! % 295.07/42.39 % (3381466)------------------------------ % 295.07/42.39 % (3381466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.39 % (3381466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.39 % (3381466)CaDiCaL version: 2.1.3 % 295.07/42.39 % (3381466)Termination reason: Instruction limit % 295.07/42.39 % (3381466)Termination phase: Saturation % 295.07/42.39 % (3381466)Time elapsed: 1.247 s % 295.07/42.39 % (3381466)Peak memory usage: 141 MB % 295.07/42.39 % (3381466)Instructions burned: 2034 (million) % 295.07/42.39 % (3381470)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=3494257985:i=21611:sd=3:ss=axioms_2743 on theBenchmark for (2743ds/21611Mi) % 295.07/42.39 % (3381471)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3286740855:i=4835:sd=13:ss=axioms:sgt=23_2743 on theBenchmark for (2743ds/4835Mi) % 295.07/42.39 % (3381464)Instruction limit reached! % 295.07/42.39 % (3381464)------------------------------ % 295.07/42.39 % (3381464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.39 % (3381464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.39 % (3381464)CaDiCaL version: 2.1.3 % 295.07/42.39 % (3381464)Termination reason: Instruction limit % 295.07/42.39 % (3381464)Termination phase: Saturation % 295.07/42.39 % (3381464)Time elapsed: 1.946 s % 295.07/42.39 % (3381464)Peak memory usage: 153 MB % 295.07/42.39 % (3381464)Instructions burned: 3223 (million) % 295.07/42.39 % (3381474)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=362756687:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2737 on theBenchmark for (2737ds/797Mi) % 295.07/42.39 % (3381474)Instruction limit reached! % 295.07/42.39 % (3381474)------------------------------ % 295.07/42.39 % (3381474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.39 % (3381474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.39 % (3381474)CaDiCaL version: 2.1.3 % 295.07/42.39 % (3381474)Termination reason: Instruction limit % 295.07/42.39 % (3381474)Termination phase: Saturation % 295.07/42.39 % (3381474)Time elapsed: 0.490 s % 295.07/42.39 % (3381474)Peak memory usage: 96 MB % 295.07/42.39 % (3381474)Instructions burned: 797 (million) % 295.07/42.39 % (3381476)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3714100440:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2731 on theBenchmark for (2731ds/2326Mi) % 295.07/42.39 % (3381476)Instruction limit reached! % 295.07/42.39 % (3381476)------------------------------ % 295.07/42.39 % (3381476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.39 % (3381476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.39 % (3381476)CaDiCaL version: 2.1.3 % 295.07/42.39 % (3381476)Termination reason: Instruction limit % 295.07/42.39 % (3381476)Termination phase: Saturation % 295.07/42.39 % (3381476)Time elapsed: 1.418 s % 295.07/42.39 % (3381476)Peak memory usage: 102 MB % 295.07/42.39 % (3381476)Instructions burned: 2326 (million) % 295.07/42.39 % (3381471)Instruction limit reached! % 300.28/43.07 % (3381471)------------------------------ % 300.28/43.07 % (3381471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.07 % (3381471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.07 % (3381471)CaDiCaL version: 2.1.3 % 300.28/43.07 % (3381471)Termination reason: Instruction limit % 300.28/43.07 % (3381471)Termination phase: Saturation % 300.28/43.07 % (3381471)Time elapsed: 2.682 s % 300.28/43.07 % (3381471)Peak memory usage: 111 MB % 300.28/43.07 % (3381471)Instructions burned: 4835 (million) % 300.28/43.07 % (3381478)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=433818413:i=6038:nm=6_2715 on theBenchmark for (2715ds/6038Mi) % 300.28/43.07 % (3381480)lrs+10_1_sil=32000:sp=occurrence:random_seed=2791118278:st=2:i=33334:sd=3:ss=included:sgt=32_2714 on theBenchmark for (2714ds/33334Mi) % 300.28/43.07 % (3381458)Instruction limit reached! % 300.28/43.07 % (3381458)------------------------------ % 300.28/43.07 % (3381458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.07 % (3381458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.07 % (3381458)CaDiCaL version: 2.1.3 % 300.28/43.07 % (3381458)Termination reason: Instruction limit % 300.28/43.07 % (3381458)Termination phase: Saturation % 300.28/43.07 % (3381458)Time elapsed: 8.641 s % 300.28/43.07 % (3381458)Peak memory usage: 237 MB % 300.28/43.07 % (3381458)Instructions burned: 14124 (million) % 300.28/43.07 % (3381757)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1215277480:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2699 on theBenchmark for (2699ds/1008Mi) % 300.28/43.07 % (3381757)Instruction limit reached! % 300.28/43.07 % (3381757)------------------------------ % 300.28/43.07 % (3381757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.07 % (3381757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.07 % (3381757)CaDiCaL version: 2.1.3 % 300.28/43.07 % (3381757)Termination reason: Instruction limit % 300.28/43.07 % (3381757)Termination phase: Saturation % 300.28/43.07 % (3381757)Time elapsed: 0.520 s % 300.28/43.07 % (3381757)Peak memory usage: 97 MB % 300.28/43.07 % (3381757)Instructions burned: 1011 (million) % 300.28/43.07 % (3381759)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=4106157310:i=8327:s2at=5:bd=preordered_2691 on theBenchmark for (2691ds/8327Mi) % 300.28/43.07 % (3381478)Instruction limit reached! % 300.28/43.07 % (3381478)------------------------------ % 300.28/43.07 % (3381478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.07 % (3381478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.07 % (3381478)CaDiCaL version: 2.1.3 % 300.28/43.07 % (3381478)Termination reason: Instruction limit % 300.28/43.07 % (3381478)Termination phase: Saturation % 300.28/43.07 % (3381478)Time elapsed: 3.370 s % 300.28/43.07 % (3381478)Peak memory usage: 163 MB % 300.28/43.07 % (3381478)Instructions burned: 6040 (million) % 300.28/43.07 % (3381761)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1712868130:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2680 on theBenchmark for (2680ds/1083Mi) % 300.28/43.07 % (3381761)Instruction limit reached! % 300.28/43.07 % (3381761)------------------------------ % 300.28/43.07 % (3381761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.07 % (3381761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.28/43.07 % (3381761)CaDiCaL version: 2.1.3 % 300.28/43.07 % (3381761)Termination reason: Instruction limit % 300.28/43.07 % (3381761)Termination phase: Saturation % 300.28/43.07 % (3381761)Time elapsed: 0.461 s % 300.28/43.07 % (3381761)Peak memory usage: 97 MB % 300.28/43.07 % (3381761)Instructions burned: 1085 (million) % 300.28/43.07 % (3381763)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1004299233:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2673 on theBenchmark for (2673ds/1084Mi) % 300.28/43.07 % (3381763)Instruction limit reached! % 300.28/43.07 % (3381763)------------------------------ % 300.28/43.07 % (3381763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.28/43.07 % (3381763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47f % 300.28/43.08 Terminated %------------------------------------------------------------------------------