%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWV100+1 : TPTP v9.3.1. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n013.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:08:08 PM UTC 2026 % Result : Timeout 301.05s 43.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWV100+1 : TPTP v9.3.1. Bugfixed v3.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.20 % Computer : n013.cluster.edu % 0.09/0.20 % Model : x86_64 x86_64 % 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.20 % Memory : 8046.5625MB % 0.09/0.20 % OS : Linux 6.8.0-71-generic % 0.09/0.20 % CPULimit : 300 % 0.09/0.20 % WCLimit : 300 % 0.09/0.20 % DateTime : Mon Sep 28 09:53:22 UTC 2026 % 0.09/0.20 % CPUTime : % 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.23 Running first-order theorem proving % 0.09/0.23 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 % 10.97/2.26 % (1064808)Detected formulas, will run a generic FOF schedule. % 10.97/2.26 % (1064817)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2191830183:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.97/2.26 % (1064816)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1203247833:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.97/2.26 % (1064814)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=1890327637:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.97/2.26 % (1064815)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=384222032:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.97/2.26 % (1064813)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=3945734522:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.97/2.26 % (1064817)Instruction limit reached! % 10.97/2.26 % (1064817)------------------------------ % 10.97/2.26 % (1064817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.26 % (1064817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.26 % (1064817)CaDiCaL version: 2.1.3 % 10.97/2.26 % (1064817)Termination reason: Instruction limit % 10.97/2.26 % (1064817)Termination phase: Saturation % 10.97/2.26 % (1064817)Time elapsed: 0.031 s % 10.97/2.26 % (1064817)Peak memory usage: 88 MB % 10.97/2.26 % (1064817)Instructions burned: 122 (million) % 10.97/2.26 % (1064818)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=768159748:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.97/2.26 % (1064819)dis-21_1_sil=8000:lcm=predicate:random_seed=2227125885: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) % 10.97/2.26 % (1064816)Instruction limit reached! % 10.97/2.26 % (1064816)------------------------------ % 10.97/2.26 % (1064816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.26 % (1064816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.26 % (1064816)CaDiCaL version: 2.1.3 % 10.97/2.26 % (1064816)Termination reason: Instruction limit % 10.97/2.26 % (1064816)Termination phase: Saturation % 10.97/2.26 % (1064816)Time elapsed: 0.056 s % 10.97/2.26 % (1064816)Peak memory usage: 90 MB % 10.97/2.26 % (1064816)Instructions burned: 111 (million) % 10.97/2.26 % (1064819)Instruction limit reached! % 10.97/2.26 % (1064819)------------------------------ % 10.97/2.26 % (1064819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.26 % (1064819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.26 % (1064819)CaDiCaL version: 2.1.3 % 10.97/2.26 % (1064819)Termination reason: Instruction limit % 10.97/2.26 % (1064819)Termination phase: Saturation % 10.97/2.26 % (1064819)Time elapsed: 0.072 s % 10.97/2.26 % (1064819)Peak memory usage: 89 MB % 10.97/2.26 % (1064819)Instructions burned: 130 (million) % 10.97/2.26 % (1064818)Instruction limit reached! % 10.97/2.26 % (1064818)------------------------------ % 10.97/2.26 % (1064818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.26 % (1064818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.26 % (1064818)CaDiCaL version: 2.1.3 % 10.97/2.26 % (1064818)Termination reason: Instruction limit % 10.97/2.26 % (1064818)Termination phase: Saturation % 10.97/2.26 % (1064818)Time elapsed: 0.082 s % 10.97/2.26 % (1064818)Peak memory usage: 90 MB % 10.97/2.26 % (1064818)Instructions burned: 140 (million) % 10.97/2.26 % (1064825)lrs+10_1_sil=8000:sp=occurrence:random_seed=90306144:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 10.97/2.26 % (1064828)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3944479474:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 10.97/2.26 % (1064825)Instruction limit reached! % 10.97/2.26 % (1064825)------------------------------ % 10.97/2.26 % (1064825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.97/2.26 % (1064825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.97/2.26 % (1064825)CaDiCaL version: 2.1.3 % 10.97/2.26 % (1064825)Termination reason: Instruction limit % 10.97/2.26 % (1064825)Termination phase: Saturation % 18.84/3.36 % (1064825)Time elapsed: 0.084 s % 18.84/3.36 % (1064825)Peak memory usage: 91 MB % 18.84/3.36 % (1064825)Instructions burned: 286 (million) % 18.84/3.36 % (1064829)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2564838360:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 18.84/3.36 % (1064830)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=2537624064:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 18.84/3.36 % (1064828)Instruction limit reached! % 18.84/3.36 % (1064828)------------------------------ % 18.84/3.36 % (1064828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.36 % (1064828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.36 % (1064828)CaDiCaL version: 2.1.3 % 18.84/3.36 % (1064828)Termination reason: Instruction limit % 18.84/3.36 % (1064828)Termination phase: Saturation % 18.84/3.36 % (1064828)Time elapsed: 0.070 s % 18.84/3.36 % (1064828)Peak memory usage: 89 MB % 18.84/3.36 % (1064828)Instructions burned: 157 (million) % 18.84/3.36 % (1064833)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3330809955:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 18.84/3.36 % (1064830)Instruction limit reached! % 18.84/3.36 % (1064830)------------------------------ % 18.84/3.36 % (1064830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.36 % (1064830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.36 % (1064830)CaDiCaL version: 2.1.3 % 18.84/3.36 % (1064830)Termination reason: Instruction limit % 18.84/3.36 % (1064830)Termination phase: Saturation % 18.84/3.36 % (1064830)Time elapsed: 0.126 s % 18.84/3.36 % (1064830)Peak memory usage: 92 MB % 18.84/3.36 % (1064830)Instructions burned: 249 (million) % 18.84/3.36 % (1064836)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=118875002:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 18.84/3.36 % (1064833)Instruction limit reached! % 18.84/3.36 % (1064833)------------------------------ % 18.84/3.36 % (1064833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.36 % (1064833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.36 % (1064833)CaDiCaL version: 2.1.3 % 18.84/3.36 % (1064833)Termination reason: Instruction limit % 18.84/3.36 % (1064833)Termination phase: Saturation % 18.84/3.36 % (1064833)Time elapsed: 0.086 s % 18.84/3.36 % (1064833)Peak memory usage: 90 MB % 18.84/3.36 % (1064833)Instructions burned: 298 (million) % 18.84/3.36 % (1064829)Instruction limit reached! % 18.84/3.36 % (1064829)------------------------------ % 18.84/3.36 % (1064829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.36 % (1064829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.36 % (1064829)CaDiCaL version: 2.1.3 % 18.84/3.36 % (1064829)Termination reason: Instruction limit % 18.84/3.36 % (1064829)Termination phase: Saturation % 18.84/3.36 % (1064829)Time elapsed: 0.180 s % 18.84/3.36 % (1064829)Peak memory usage: 91 MB % 18.84/3.36 % (1064829)Instructions burned: 325 (million) % 18.84/3.36 % (1064838)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2120985155:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi) % 18.84/3.36 % (1064840)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2938300625:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 18.84/3.36 % (1064840)Instruction limit reached! % 18.84/3.36 % (1064840)------------------------------ % 18.84/3.36 % (1064840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.36 % (1064840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.36 % (1064840)CaDiCaL version: 2.1.3 % 18.84/3.36 % (1064840)Termination reason: Instruction limit % 18.84/3.36 % (1064840)Termination phase: Saturation % 18.84/3.36 % (1064840)Time elapsed: 0.030 s % 18.84/3.36 % (1064840)Peak memory usage: 89 MB % 18.84/3.36 % (1064840)Instructions burned: 128 (million) % 18.84/3.36 % (1064838)Instruction limit reached! % 18.84/3.36 % (1064838)------------------------------ % 18.84/3.36 % (1064838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.84/3.36 % (1064838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.84/3.36 % (1064838)CaDiCaL version: 2.1.3 % 18.84/3.36 % (1064838)Termination reason: Instruction limit % 18.84/3.36 % (1064838)Termination phase: Saturation % 43.86/6.80 % (1064838)Time elapsed: 0.053 s % 43.86/6.80 % (1064838)Peak memory usage: 89 MB % 43.86/6.80 % (1064838)Instructions burned: 113 (million) % 43.86/6.80 % (1064841)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3284878567:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi) % 43.86/6.80 % (1064844)lrs+10_1_sil=8000:sp=occurrence:random_seed=88971577:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi) % 43.86/6.80 % (1064841)Instruction limit reached! % 43.86/6.80 % (1064841)------------------------------ % 43.86/6.80 % (1064841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.86/6.80 % (1064841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.86/6.80 % (1064841)CaDiCaL version: 2.1.3 % 43.86/6.80 % (1064841)Termination reason: Instruction limit % 43.86/6.80 % (1064841)Termination phase: Clausification % 43.86/6.80 % (1064841)Time elapsed: 0.138 s % 43.86/6.80 % (1064841)Peak memory usage: 167 MB % 43.86/6.80 % (1064841)Instructions burned: 114 (million) % 43.86/6.80 % (1064846)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2597193541:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi) % 43.86/6.80 % (1064848)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=704654585:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 43.86/6.80 % (1064846)Instruction limit reached! % 43.86/6.80 % (1064846)------------------------------ % 43.86/6.80 % (1064846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.86/6.80 % (1064846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.86/6.80 % (1064846)CaDiCaL version: 2.1.3 % 43.86/6.80 % (1064846)Termination reason: Instruction limit % 43.86/6.80 % (1064846)Termination phase: Saturation % 43.86/6.80 % (1064846)Time elapsed: 0.234 s % 43.86/6.80 % (1064846)Peak memory usage: 91 MB % 43.86/6.80 % (1064846)Instructions burned: 439 (million) % 43.86/6.80 % (1064844)Instruction limit reached! % 43.86/6.80 % (1064844)------------------------------ % 43.86/6.80 % (1064844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.86/6.80 % (1064844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.86/6.80 % (1064844)CaDiCaL version: 2.1.3 % 43.86/6.80 % (1064844)Termination reason: Instruction limit % 43.86/6.80 % (1064844)Termination phase: Saturation % 43.86/6.80 % (1064844)Time elapsed: 0.297 s % 43.86/6.80 % (1064844)Peak memory usage: 96 MB % 43.86/6.80 % (1064844)Instructions burned: 908 (million) % 43.86/6.80 % (1064852)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2501463173:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 43.86/6.80 % (1064851)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=335165292:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 43.86/6.80 % (1064852)Refutation not found, incomplete strategy % 43.86/6.80 % (1064852)------------------------------ % 43.86/6.80 % (1064852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.86/6.80 % (1064852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.86/6.80 % (1064852)CaDiCaL version: 2.1.3 % 43.86/6.80 % (1064852)Termination reason: Refutation not found, incomplete strategy % 43.86/6.80 % (1064852)Time elapsed: 0.013 s % 43.86/6.80 % (1064852)Peak memory usage: 89 MB % 43.86/6.80 % (1064852)Instructions burned: 60 (million) % 43.86/6.80 % (1064851)Instruction limit reached! % 43.86/6.80 % (1064851)------------------------------ % 43.86/6.80 % (1064851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.86/6.80 % (1064851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.86/6.80 % (1064851)CaDiCaL version: 2.1.3 % 43.86/6.80 % (1064851)Termination reason: Instruction limit % 43.86/6.80 % (1064851)Termination phase: Saturation % 43.86/6.80 % (1064851)Time elapsed: 0.055 s % 43.86/6.80 % (1064851)Peak memory usage: 89 MB % 43.86/6.80 % (1064851)Instructions burned: 135 (million) % 43.86/6.80 % (1064852)------------------------------ % 43.86/6.80 % (1064852)------------------------------ % 43.86/6.80 % (1064855)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=223139637:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 43.86/6.80 % (1064856)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=2052195894:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi) % 70.12/10.52 % (1064856)Instruction limit reached! % 70.12/10.52 % (1064856)------------------------------ % 70.12/10.52 % (1064856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.12/10.52 % (1064856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.12/10.52 % (1064856)CaDiCaL version: 2.1.3 % 70.12/10.52 % (1064856)Termination reason: Instruction limit % 70.12/10.52 % (1064856)Termination phase: Saturation % 70.12/10.52 % (1064856)Time elapsed: 0.037 s % 70.12/10.52 % (1064856)Peak memory usage: 90 MB % 70.12/10.52 % (1064856)Instructions burned: 128 (million) % 70.12/10.52 % (1064859)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3200003415:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi) % 70.12/10.52 % (1064859)Instruction limit reached! % 70.12/10.52 % (1064859)------------------------------ % 70.12/10.52 % (1064859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.12/10.52 % (1064859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.12/10.52 % (1064859)CaDiCaL version: 2.1.3 % 70.12/10.52 % (1064859)Termination reason: Instruction limit % 70.12/10.52 % (1064859)Termination phase: Saturation % 70.12/10.52 % (1064859)Time elapsed: 0.059 s % 70.12/10.52 % (1064859)Peak memory usage: 90 MB % 70.12/10.52 % (1064859)Instructions burned: 135 (million) % 70.12/10.52 % (1064861)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2614172188:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi) % 70.12/10.52 % (1064861)Instruction limit reached! % 70.12/10.52 % (1064861)------------------------------ % 70.12/10.52 % (1064861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.12/10.52 % (1064861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.12/10.52 % (1064861)CaDiCaL version: 2.1.3 % 70.12/10.52 % (1064861)Termination reason: Instruction limit % 70.12/10.52 % (1064861)Termination phase: Saturation % 70.12/10.52 % (1064861)Time elapsed: 0.063 s % 70.12/10.52 % (1064861)Peak memory usage: 89 MB % 70.12/10.52 % (1064861)Instructions burned: 141 (million) % 70.12/10.52 % (1064836)Instruction limit reached! % 70.12/10.52 % (1064836)------------------------------ % 70.12/10.52 % (1064836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.12/10.52 % (1064836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.12/10.52 % (1064836)CaDiCaL version: 2.1.3 % 70.12/10.52 % (1064836)Termination reason: Instruction limit % 70.12/10.52 % (1064836)Termination phase: Saturation % 70.12/10.52 % (1064836)Time elapsed: 1.568 s % 70.12/10.52 % (1064836)Peak memory usage: 141 MB % 70.12/10.52 % (1064836)Instructions burned: 2351 (million) % 70.12/10.52 % (1064863)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3964013295:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi) % 70.12/10.52 % (1064864)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=2222206782:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi) % 70.12/10.52 % (1064863)Instruction limit reached! % 70.12/10.52 % (1064863)------------------------------ % 70.12/10.52 % (1064863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.12/10.52 % (1064863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.12/10.52 % (1064863)CaDiCaL version: 2.1.3 % 70.12/10.52 % (1064863)Termination reason: Instruction limit % 70.12/10.52 % (1064863)Termination phase: Saturation % 70.12/10.52 % (1064863)Time elapsed: 0.219 s % 70.12/10.52 % (1064863)Peak memory usage: 93 MB % 70.12/10.52 % (1064863)Instructions burned: 432 (million) % 70.12/10.52 % (1064867)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=812020197:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2975 on theBenchmark for (2975ds/150Mi) % 70.12/10.52 % (1064867)Instruction limit reached! % 70.12/10.52 % (1064867)------------------------------ % 70.12/10.52 % (1064867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.12/10.52 % (1064867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.12/10.52 % (1064867)CaDiCaL version: 2.1.3 % 70.12/10.52 % (1064867)Termination reason: Instruction limit % 70.12/10.52 % (1064867)Termination phase: Saturation % 92.10/13.63 % (1064867)Time elapsed: 0.069 s % 92.10/13.63 % (1064867)Peak memory usage: 90 MB % 92.10/13.63 % (1064867)Instructions burned: 151 (million) % 92.10/13.63 % (1064869)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1987533965:i=14155:bd=all_2973 on theBenchmark for (2973ds/14155Mi) % 92.10/13.63 % (1064848)Instruction limit reached! % 92.10/13.63 % (1064848)------------------------------ % 92.10/13.63 % (1064848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.10/13.63 % (1064848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.10/13.63 % (1064848)CaDiCaL version: 2.1.3 % 92.10/13.63 % (1064848)Termination reason: Instruction limit % 92.10/13.63 % (1064848)Termination phase: Saturation % 92.10/13.63 % (1064848)Time elapsed: 2.061 s % 92.10/13.63 % (1064848)Peak memory usage: 165 MB % 92.10/13.63 % (1064848)Instructions burned: 5202 (million) % 92.10/13.63 % (1064871)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=783777660:i=667:av=off:fsr=off_2968 on theBenchmark for (2968ds/667Mi) % 92.10/13.63 % (1064871)Instruction limit reached! % 92.10/13.63 % (1064871)------------------------------ % 92.10/13.63 % (1064871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.10/13.63 % (1064871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.10/13.63 % (1064871)CaDiCaL version: 2.1.3 % 92.10/13.63 % (1064871)Termination reason: Instruction limit % 92.10/13.63 % (1064871)Termination phase: Saturation % 92.10/13.63 % (1064871)Time elapsed: 0.168 s % 92.10/13.63 % (1064871)Peak memory usage: 93 MB % 92.10/13.63 % (1064871)Instructions burned: 671 (million) % 92.10/13.63 % (1064873)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=3040797675:s2a=on:i=185:s2at=1.8:fdi=4_2965 on theBenchmark for (2965ds/185Mi) % 92.10/13.63 % (1064873)Instruction limit reached! % 92.10/13.63 % (1064873)------------------------------ % 92.10/13.63 % (1064873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.10/13.63 % (1064873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.10/13.63 % (1064873)CaDiCaL version: 2.1.3 % 92.10/13.63 % (1064873)Termination reason: Instruction limit % 92.10/13.63 % (1064873)Termination phase: Saturation % 92.10/13.63 % (1064873)Time elapsed: 0.050 s % 92.10/13.63 % (1064873)Peak memory usage: 91 MB % 92.10/13.63 % (1064873)Instructions burned: 187 (million) % 92.10/13.63 % (1064875)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1609437760:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2963 on theBenchmark for (2963ds/193Mi) % 92.10/13.63 % (1064875)Instruction limit reached! % 92.10/13.63 % (1064875)------------------------------ % 92.10/13.63 % (1064875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.10/13.63 % (1064875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.10/13.63 % (1064875)CaDiCaL version: 2.1.3 % 92.10/13.63 % (1064875)Termination reason: Instruction limit % 92.10/13.63 % (1064875)Termination phase: Saturation % 92.10/13.63 % (1064875)Time elapsed: 0.064 s % 92.10/13.63 % (1064875)Peak memory usage: 92 MB % 92.10/13.63 % (1064875)Instructions burned: 195 (million) % 92.10/13.63 % (1064877)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=464100266:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2961 on theBenchmark for (2961ds/4850Mi) % 92.10/13.63 % (1064877)Instruction limit reached! % 92.10/13.63 % (1064877)------------------------------ % 92.10/13.63 % (1064877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.10/13.63 % (1064877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.10/13.63 % (1064877)CaDiCaL version: 2.1.3 % 92.10/13.63 % (1064877)Termination reason: Instruction limit % 92.10/13.63 % (1064877)Termination phase: Saturation % 92.10/13.63 % (1064877)Time elapsed: 1.100 s % 92.10/13.63 % (1064877)Peak memory usage: 102 MB % 92.10/13.63 % (1064877)Instructions burned: 4853 (million) % 92.10/13.63 % (1064879)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1813091957:i=12111:sd=1:ss=included_2949 on theBenchmark for (2949ds/12111Mi) % 92.10/13.63 % (1064864)Instruction limit reached! % 92.10/13.63 % (1064864)------------------------------ % 92.10/13.63 % (1064864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.10/13.63 % (1064864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.44/16.80 % (1064864)CaDiCaL version: 2.1.3 % 114.44/16.80 % (1064864)Termination reason: Instruction limit % 114.44/16.80 % (1064864)Termination phase: Saturation % 114.44/16.80 % (1064864)Time elapsed: 3.811 s % 114.44/16.80 % (1064864)Peak memory usage: 167 MB % 114.44/16.80 % (1064864)Instructions burned: 6061 (million) % 114.44/16.80 % (1064881)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2768126474:i=319:kws=precedence:fsr=off_2938 on theBenchmark for (2938ds/319Mi) % 114.44/16.80 % (1064881)Instruction limit reached! % 114.44/16.80 % (1064881)------------------------------ % 114.44/16.80 % (1064881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.44/16.80 % (1064881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.44/16.80 % (1064881)CaDiCaL version: 2.1.3 % 114.44/16.80 % (1064881)Termination reason: Instruction limit % 114.44/16.80 % (1064881)Termination phase: Saturation % 114.44/16.80 % (1064881)Time elapsed: 0.156 s % 114.44/16.80 % (1064881)Peak memory usage: 92 MB % 114.44/16.80 % (1064881)Instructions burned: 319 (million) % 114.44/16.80 % (1064883)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3712662824:i=2064:ep=RST_2935 on theBenchmark for (2935ds/2064Mi) % 114.44/16.80 % (1064883)Instruction limit reached! % 114.44/16.80 % (1064883)------------------------------ % 114.44/16.80 % (1064883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.44/16.80 % (1064883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.44/16.80 % (1064883)CaDiCaL version: 2.1.3 % 114.44/16.80 % (1064883)Termination reason: Instruction limit % 114.44/16.80 % (1064883)Termination phase: Saturation % 114.44/16.80 % (1064883)Time elapsed: 0.703 s % 114.44/16.80 % (1064883)Peak memory usage: 89 MB % 114.44/16.80 % (1064883)Instructions burned: 2067 (million) % 114.44/16.80 % (1064885)dis-1011_128_sil=32000:random_seed=1611515438:i=3706:ep=RST:av=off_2926 on theBenchmark for (2926ds/3706Mi) % 114.44/16.80 % (1064879)Instruction limit reached! % 114.44/16.80 % (1064879)------------------------------ % 114.44/16.80 % (1064879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.44/16.80 % (1064879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.44/16.80 % (1064879)CaDiCaL version: 2.1.3 % 114.44/16.80 % (1064879)Termination reason: Instruction limit % 114.44/16.80 % (1064879)Termination phase: Saturation % 114.44/16.80 % (1064879)Time elapsed: 3.380 s % 114.44/16.80 % (1064879)Peak memory usage: 164 MB % 114.44/16.80 % (1064879)Instructions burned: 12116 (million) % 114.44/16.80 % (1064887)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3974933966:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2914 on theBenchmark for (2914ds/757Mi) % 114.44/16.80 % (1064887)Instruction limit reached! % 114.44/16.80 % (1064887)------------------------------ % 114.44/16.80 % (1064887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.44/16.80 % (1064887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.44/16.80 % (1064887)CaDiCaL version: 2.1.3 % 114.44/16.80 % (1064887)Termination reason: Instruction limit % 114.44/16.80 % (1064887)Termination phase: Saturation % 114.44/16.80 % (1064887)Time elapsed: 0.250 s % 114.44/16.80 % (1064887)Peak memory usage: 98 MB % 114.44/16.80 % (1064887)Instructions burned: 759 (million) % 114.44/16.80 % (1064889)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1860269073:i=13913:ss=axioms:sgt=8_2910 on theBenchmark for (2910ds/13913Mi) % 114.44/16.80 % (1064855)Instruction limit reached! % 114.44/16.80 % (1064855)------------------------------ % 114.44/16.80 % (1064855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.44/16.80 % (1064855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.44/16.80 % (1064855)CaDiCaL version: 2.1.3 % 114.44/16.80 % (1064855)Termination reason: Instruction limit % 114.44/16.80 % (1064855)Termination phase: Saturation % 114.44/16.80 % (1064855)Time elapsed: 7.731 s % 114.44/16.80 % (1064855)Peak memory usage: 204 MB % 114.44/16.80 % (1064855)Instructions burned: 13195 (million) % 114.44/16.80 % (1064891)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3082375293:i=9925:aac=none_2907 on theBenchmark for (2907ds/9925Mi) % 114.44/16.80 % (1064885)Instruction limit reached! % 114.44/16.80 % (1064885)------------------------------ % 114.44/16.80 % (1064885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.44/16.80 % (1064885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.06/20.50 % (1064885)CaDiCaL version: 2.1.3 % 141.06/20.50 % (1064885)Termination reason: Instruction limit % 141.06/20.50 % (1064885)Termination phase: Saturation % 141.06/20.50 % (1064885)Time elapsed: 2.368 s % 141.06/20.50 % (1064885)Peak memory usage: 107 MB % 141.06/20.50 % (1064885)Instructions burned: 3706 (million) % 141.06/20.50 % (1064893)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1224387423:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2901 on theBenchmark for (2901ds/2479Mi) % 141.06/20.50 % (1064893)Instruction limit reached! % 141.06/20.50 % (1064893)------------------------------ % 141.06/20.50 % (1064893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.06/20.50 % (1064893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.06/20.50 % (1064893)CaDiCaL version: 2.1.3 % 141.06/20.50 % (1064893)Termination reason: Instruction limit % 141.06/20.50 % (1064893)Termination phase: Saturation % 141.06/20.50 % (1064893)Time elapsed: 1.268 s % 141.06/20.50 % (1064893)Peak memory usage: 104 MB % 141.06/20.50 % (1064893)Instructions burned: 2480 (million) % 141.06/20.50 % (1064869)Instruction limit reached! % 141.06/20.50 % (1064869)------------------------------ % 141.06/20.50 % (1064869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.06/20.50 % (1064869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.06/20.50 % (1064869)CaDiCaL version: 2.1.3 % 141.06/20.50 % (1064869)Termination reason: Instruction limit % 141.06/20.50 % (1064869)Termination phase: Saturation % 141.06/20.50 % (1064869)Time elapsed: 8.530 s % 141.06/20.50 % (1064869)Peak memory usage: 190 MB % 141.06/20.50 % (1064869)Instructions burned: 14156 (million) % 141.06/20.50 % (1064895)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2416574612:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2887 on theBenchmark for (2887ds/440Mi) % 141.06/20.50 % (1064896)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1919258884:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2886 on theBenchmark for (2886ds/11145Mi) % 141.06/20.50 % (1064895)Instruction limit reached! % 141.06/20.50 % (1064895)------------------------------ % 141.06/20.50 % (1064895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.06/20.50 % (1064895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.06/20.50 % (1064895)CaDiCaL version: 2.1.3 % 141.06/20.50 % (1064895)Termination reason: Instruction limit % 141.06/20.50 % (1064895)Termination phase: Saturation % 141.06/20.50 % (1064895)Time elapsed: 0.195 s % 141.06/20.50 % (1064895)Peak memory usage: 91 MB % 141.06/20.50 % (1064895)Instructions burned: 440 (million) % 141.06/20.50 % (1064899)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=3577825547:cts=off:i=3034:av=off:er=known:fsd=on_2883 on theBenchmark for (2883ds/3034Mi) % 141.06/20.50 % (1064889)Instruction limit reached! % 141.06/20.50 % (1064889)------------------------------ % 141.06/20.50 % (1064889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.06/20.50 % (1064889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.06/20.50 % (1064889)CaDiCaL version: 2.1.3 % 141.06/20.50 % (1064889)Termination reason: Instruction limit % 141.06/20.50 % (1064889)Termination phase: Saturation % 141.06/20.50 % (1064889)Time elapsed: 2.901 s % 141.06/20.50 % (1064889)Peak memory usage: 147 MB % 141.06/20.50 % (1064889)Instructions burned: 13914 (million) % 141.06/20.50 % (1064901)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1535931749:st=2:s2a=on:i=524:s2at=2:ss=axioms_2880 on theBenchmark for (2880ds/524Mi) % 141.06/20.50 % (1064901)Instruction limit reached! % 141.06/20.50 % (1064901)------------------------------ % 141.06/20.50 % (1064901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.06/20.50 % (1064901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.06/20.50 % (1064901)CaDiCaL version: 2.1.3 % 141.06/20.50 % (1064901)Termination reason: Instruction limit % 141.06/20.50 % (1064901)Termination phase: Saturation % 141.06/20.50 % (1064901)Time elapsed: 0.137 s % 141.06/20.50 % (1064901)Peak memory usage: 92 MB % 141.06/20.50 % (1064901)Instructions burned: 526 (million) % 141.06/20.50 % (1064903)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=957948223:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2877 on theBenchmark for (2877ds/1016Mi) % 141.06/20.50 % (1064903)Instruction limit reached! % 141.06/20.50 % (1064903)------------------------------ % 181.07/26.14 % (1064903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.07/26.14 % (1064903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.07/26.14 % (1064903)CaDiCaL version: 2.1.3 % 181.07/26.14 % (1064903)Termination reason: Instruction limit % 181.07/26.14 % (1064903)Termination phase: Saturation % 181.07/26.14 % (1064903)Time elapsed: 0.545 s % 181.07/26.14 % (1064903)Peak memory usage: 93 MB % 181.07/26.14 % (1064903)Instructions burned: 1017 (million) % 181.07/26.14 % (1064899)Instruction limit reached! % 181.07/26.14 % (1064899)------------------------------ % 181.07/26.14 % (1064899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.07/26.14 % (1064899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.07/26.14 % (1064899)CaDiCaL version: 2.1.3 % 181.07/26.14 % (1064899)Termination reason: Instruction limit % 181.07/26.14 % (1064899)Termination phase: Saturation % 181.07/26.14 % (1064899)Time elapsed: 1.185 s % 181.07/26.14 % (1064899)Peak memory usage: 136 MB % 181.07/26.14 % (1064899)Instructions burned: 3037 (million) % 181.07/26.14 % (1064905)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4023369019:i=14123:bd=preordered:ins=4_2870 on theBenchmark for (2870ds/14123Mi) % 181.07/26.14 % (1064906)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2657537834:i=5781:kws=precedence:bd=all:rawr=on_2870 on theBenchmark for (2870ds/5781Mi) % 181.07/26.14 % (1064891)Instruction limit reached! % 181.07/26.14 % (1064891)------------------------------ % 181.07/26.14 % (1064891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.07/26.14 % (1064891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.07/26.14 % (1064891)CaDiCaL version: 2.1.3 % 181.07/26.14 % (1064891)Termination reason: Instruction limit % 181.07/26.14 % (1064891)Termination phase: Saturation % 181.07/26.14 % (1064891)Time elapsed: 4.895 s % 181.07/26.14 % (1064891)Peak memory usage: 169 MB % 181.07/26.14 % (1064891)Instructions burned: 9926 (million) % 181.07/26.14 % (1064909)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=2731758662:i=2448:gtgl=5:bd=preordered:gtg=all_2856 on theBenchmark for (2856ds/2448Mi) % 181.07/26.14 % (1064906)Instruction limit reached! % 181.07/26.14 % (1064906)------------------------------ % 181.07/26.14 % (1064906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.07/26.14 % (1064906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.07/26.14 % (1064906)CaDiCaL version: 2.1.3 % 181.07/26.14 % (1064906)Termination reason: Instruction limit % 181.07/26.14 % (1064906)Termination phase: Saturation % 181.07/26.14 % (1064906)Time elapsed: 1.679 s % 181.07/26.14 % (1064906)Peak memory usage: 116 MB % 181.07/26.14 % (1064906)Instructions burned: 5782 (million) % 181.07/26.14 % (1064911)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2683599367:i=3223:kws=precedence:fgj=on:av=off_2852 on theBenchmark for (2852ds/3223Mi) % 181.07/26.14 % (1064909)Instruction limit reached! % 181.07/26.14 % (1064909)------------------------------ % 181.07/26.14 % (1064909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.07/26.14 % (1064909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.07/26.14 % (1064909)CaDiCaL version: 2.1.3 % 181.07/26.14 % (1064909)Termination reason: Instruction limit % 181.07/26.14 % (1064909)Termination phase: Saturation % 181.07/26.14 % (1064909)Time elapsed: 1.347 s % 181.07/26.14 % (1064909)Peak memory usage: 138 MB % 181.07/26.14 % (1064909)Instructions burned: 2448 (million) % 181.07/26.14 % (1064911)Instruction limit reached! % 181.07/26.14 % (1064911)------------------------------ % 181.07/26.14 % (1064911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 181.07/26.14 % (1064911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 181.07/26.14 % (1064911)CaDiCaL version: 2.1.3 % 181.07/26.14 % (1064911)Termination reason: Instruction limit % 181.07/26.14 % (1064911)Termination phase: Saturation % 181.07/26.14 % (1064911)Time elapsed: 1.077 s % 181.07/26.14 % (1064911)Peak memory usage: 143 MB % 181.07/26.14 % (1064911)Instructions burned: 3223 (million) % 181.07/26.14 % (1064913)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2078907606:st=5.6:i=2033:sd=3:ss=axioms_2841 on theBenchmark for (2841ds/2033Mi) % 181.07/26.14 % (1064915)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4066256474:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2839 on theBenchmark for (2839ds/2055Mi) % 214.89/30.99 % (1064915)Instruction limit reached! % 214.89/30.99 % (1064915)------------------------------ % 214.89/30.99 % (1064915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.89/30.99 % (1064915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.89/30.99 % (1064915)CaDiCaL version: 2.1.3 % 214.89/30.99 % (1064915)Termination reason: Instruction limit % 214.89/30.99 % (1064915)Termination phase: Saturation % 214.89/30.99 % (1064915)Time elapsed: 0.787 s % 214.89/30.99 % (1064915)Peak memory usage: 137 MB % 214.89/30.99 % (1064915)Instructions burned: 2055 (million) % 214.89/30.99 % (1064917)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=1358209251:i=21611:sd=3:ss=axioms_2830 on theBenchmark for (2830ds/21611Mi) % 214.89/30.99 % (1064913)Instruction limit reached! % 214.89/30.99 % (1064913)------------------------------ % 214.89/30.99 % (1064913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.89/30.99 % (1064913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.89/30.99 % (1064913)CaDiCaL version: 2.1.3 % 214.89/30.99 % (1064913)Termination reason: Instruction limit % 214.89/30.99 % (1064913)Termination phase: Saturation % 214.89/30.99 % (1064913)Time elapsed: 1.342 s % 214.89/30.99 % (1064913)Peak memory usage: 137 MB % 214.89/30.99 % (1064913)Instructions burned: 2033 (million) % 214.89/30.99 % (1064919)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=53492734:i=4835:sd=13:ss=axioms:sgt=23_2826 on theBenchmark for (2826ds/4835Mi) % 214.89/30.99 % (1064896)Instruction limit reached! % 214.89/30.99 % (1064896)------------------------------ % 214.89/30.99 % (1064896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.89/30.99 % (1064896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.89/30.99 % (1064896)CaDiCaL version: 2.1.3 % 214.89/30.99 % (1064896)Termination reason: Instruction limit % 214.89/30.99 % (1064896)Termination phase: Saturation % 214.89/30.99 % (1064896)Time elapsed: 7.172 s % 214.89/30.99 % (1064896)Peak memory usage: 199 MB % 214.89/30.99 % (1064896)Instructions burned: 11146 (million) % 214.89/30.99 % (1064921)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=3807977953:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2812 on theBenchmark for (2812ds/797Mi) % 214.89/30.99 % (1064905)Instruction limit reached! % 214.89/30.99 % (1064905)------------------------------ % 214.89/30.99 % (1064905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.89/30.99 % (1064905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.89/30.99 % (1064905)CaDiCaL version: 2.1.3 % 214.89/30.99 % (1064905)Termination reason: Instruction limit % 214.89/30.99 % (1064905)Termination phase: Saturation % 214.89/30.99 % (1064905)Time elapsed: 5.838 s % 214.89/30.99 % (1064905)Peak memory usage: 146 MB % 214.89/30.99 % (1064905)Instructions burned: 14125 (million) % 214.89/30.99 % (1064923)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3656107661:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2810 on theBenchmark for (2810ds/2326Mi) % 214.89/30.99 % (1064921)Instruction limit reached! % 214.89/30.99 % (1064921)------------------------------ % 214.89/30.99 % (1064921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.89/30.99 % (1064921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.89/30.99 % (1064921)CaDiCaL version: 2.1.3 % 214.89/30.99 % (1064921)Termination reason: Instruction limit % 214.89/30.99 % (1064921)Termination phase: Saturation % 214.89/30.99 % (1064921)Time elapsed: 0.376 s % 214.89/30.99 % (1064921)Peak memory usage: 91 MB % 214.89/30.99 % (1064921)Instructions burned: 798 (million) % 214.89/30.99 % (1064925)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1027262016:i=6038:nm=6_2807 on theBenchmark for (2807ds/6038Mi) % 214.89/30.99 % (1064919)Instruction limit reached! % 214.89/30.99 % (1064919)------------------------------ % 214.89/30.99 % (1064919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 214.89/30.99 % (1064919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 214.89/30.99 % (1064919)CaDiCaL version: 2.1.3 % 214.89/30.99 % (1064919)Termination reason: Instruction limit % 282.37/40.50 % (1064919)Termination phase: Saturation % 282.37/40.50 % (1064919)Time elapsed: 2.306 s % 282.37/40.50 % (1064919)Peak memory usage: 108 MB % 282.37/40.50 % (1064919)Instructions burned: 4835 (million) % 282.37/40.50 % (1064927)lrs+10_1_sil=32000:sp=occurrence:random_seed=3432659177:st=2:i=33334:sd=3:ss=included:sgt=32_2801 on theBenchmark for (2801ds/33334Mi) % 282.37/40.50 % (1064923)Instruction limit reached! % 282.37/40.50 % (1064923)------------------------------ % 282.37/40.50 % (1064923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.50 % (1064923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.50 % (1064923)CaDiCaL version: 2.1.3 % 282.37/40.50 % (1064923)Termination reason: Instruction limit % 282.37/40.50 % (1064923)Termination phase: Saturation % 282.37/40.50 % (1064923)Time elapsed: 1.385 s % 282.37/40.50 % (1064923)Peak memory usage: 104 MB % 282.37/40.50 % (1064923)Instructions burned: 2328 (million) % 282.37/40.50 % (1064929)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3931867757:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2795 on theBenchmark for (2795ds/1008Mi) % 282.37/40.50 % (1064929)Instruction limit reached! % 282.37/40.50 % (1064929)------------------------------ % 282.37/40.50 % (1064929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.50 % (1064929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.50 % (1064929)CaDiCaL version: 2.1.3 % 282.37/40.50 % (1064929)Termination reason: Instruction limit % 282.37/40.50 % (1064929)Termination phase: Saturation % 282.37/40.50 % (1064929)Time elapsed: 0.495 s % 282.37/40.50 % (1064929)Peak memory usage: 103 MB % 282.37/40.50 % (1064929)Instructions burned: 1008 (million) % 282.37/40.50 % (1064931)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=2290668098:i=8327:s2at=5:bd=preordered_2788 on theBenchmark for (2788ds/8327Mi) % 282.37/40.50 % (1064925)Instruction limit reached! % 282.37/40.50 % (1064925)------------------------------ % 282.37/40.50 % (1064925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.50 % (1064925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.50 % (1064925)CaDiCaL version: 2.1.3 % 282.37/40.50 % (1064925)Termination reason: Instruction limit % 282.37/40.50 % (1064925)Termination phase: Saturation % 282.37/40.50 % (1064925)Time elapsed: 3.105 s % 282.37/40.50 % (1064925)Peak memory usage: 182 MB % 282.37/40.50 % (1064925)Instructions burned: 6039 (million) % 282.37/40.50 % (1064933)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=1988444030:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2774 on theBenchmark for (2774ds/1083Mi) % 282.37/40.50 % (1064933)Instruction limit reached! % 282.37/40.50 % (1064933)------------------------------ % 282.37/40.50 % (1064933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.50 % (1064933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.50 % (1064933)CaDiCaL version: 2.1.3 % 282.37/40.50 % (1064933)Termination reason: Instruction limit % 282.37/40.50 % (1064933)Termination phase: Saturation % 282.37/40.50 % (1064933)Time elapsed: 0.443 s % 282.37/40.50 % (1064933)Peak memory usage: 97 MB % 282.37/40.50 % (1064933)Instructions burned: 1085 (million) % 282.37/40.50 % (1064935)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1395774945:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2768 on theBenchmark for (2768ds/1084Mi) % 282.37/40.50 % (1064935)Instruction limit reached! % 282.37/40.50 % (1064935)------------------------------ % 282.37/40.50 % (1064935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.37/40.50 % (1064935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.37/40.50 % (1064935)CaDiCaL version: 2.1.3 % 282.37/40.50 % (1064935)Termination reason: Instruction limit % 282.37/40.50 % (1064935)Termination phase: Saturation % 282.37/40.50 % (1064935)Time elapsed: 0.566 s % 282.37/40.50 % (1064935)Peak memory usage: 99 MB % 282.37/40.50 % (1064935)Instructions burned: 1085 (million) % 282.37/40.50 % (1064937)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3526984015:i=6995:s2at=5:gtg=all_2760 on theBenchmark for (2760ds/6995Mi) % 282.37/40.50 % (1064917)Instruction limTerminated %------------------------------------------------------------------------------