%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX196+1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n019.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:46:07 PM UTC 2026 % Result : Timeout 300.09s 43.09s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX196+1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.20 % Computer : n019.cluster.edu % 0.08/0.20 % Model : x86_64 x86_64 % 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.20 % Memory : 8046.5625MB % 0.08/0.20 % OS : Linux 6.8.0-71-generic % 0.08/0.20 % CPULimit : 300 % 0.08/0.20 % WCLimit : 300 % 0.08/0.20 % DateTime : Mon Sep 28 15:06:48 UTC 2026 % 0.08/0.20 % CPUTime : % 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.23 Running first-order theorem proving % 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 21.23/3.81 % (4074885)Detected formulas, will run a generic FOF schedule. % 21.23/3.81 % (4075018)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=211320896:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 21.23/3.81 % (4075021)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=168503146:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 21.23/3.81 % (4075022)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=540415477:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 21.23/3.81 % (4075019)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=3951548746:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 21.23/3.81 % (4075017)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=3812114423:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 21.23/3.81 % (4075023)dis-21_1_sil=8000:lcm=predicate:random_seed=111988029: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) % 21.23/3.81 % (4075020)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2335701592:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 21.23/3.81 % (4075023)Refutation not found, incomplete strategy % 21.23/3.81 % (4075023)------------------------------ % 21.23/3.81 % (4075023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.23/3.81 % (4075023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.23/3.81 % (4075023)CaDiCaL version: 2.1.3 % 21.23/3.81 % (4075023)Termination reason: Refutation not found, incomplete strategy % 21.23/3.81 % (4075023)Time elapsed: 0.007 s % 21.23/3.81 % (4075023)Peak memory usage: 88 MB % 21.23/3.81 % (4075023)Instructions burned: 6 (million) % 21.23/3.81 % (4075021)Instruction limit reached! % 21.23/3.81 % (4075021)------------------------------ % 21.23/3.81 % (4075021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.23/3.81 % (4075021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.23/3.81 % (4075021)CaDiCaL version: 2.1.3 % 21.23/3.81 % (4075021)Termination reason: Instruction limit % 21.23/3.81 % (4075021)Termination phase: Saturation % 21.23/3.81 % (4075021)Time elapsed: 0.102 s % 21.23/3.81 % (4075021)Peak memory usage: 88 MB % 21.23/3.81 % (4075021)Instructions burned: 119 (million) % 21.23/3.81 % (4075020)Instruction limit reached! % 21.23/3.81 % (4075020)------------------------------ % 21.23/3.81 % (4075020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.23/3.81 % (4075020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.23/3.81 % (4075020)CaDiCaL version: 2.1.3 % 21.23/3.81 % (4075020)Termination reason: Instruction limit % 21.23/3.81 % (4075020)Termination phase: Saturation % 21.23/3.81 % (4075020)Time elapsed: 0.098 s % 21.23/3.81 % (4075020)Peak memory usage: 89 MB % 21.23/3.81 % (4075020)Instructions burned: 109 (million) % 21.23/3.81 % (4075022)Instruction limit reached! % 21.23/3.81 % (4075022)------------------------------ % 21.23/3.81 % (4075022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.23/3.81 % (4075022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.23/3.81 % (4075022)CaDiCaL version: 2.1.3 % 21.23/3.81 % (4075022)Termination reason: Instruction limit % 21.23/3.81 % (4075022)Termination phase: Saturation % 21.23/3.81 % (4075022)Time elapsed: 0.126 s % 21.23/3.81 % (4075022)Peak memory usage: 90 MB % 21.23/3.81 % (4075022)Instructions burned: 139 (million) % 21.23/3.81 % (4075037)lrs+10_1_sil=8000:sp=occurrence:random_seed=3053985068:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 21.23/3.81 % (4075023)------------------------------ % 21.23/3.81 % (4075023)------------------------------ % 21.23/3.81 % (4075038)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1420735629:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 21.23/3.81 % (4075039)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2114289019:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 21.23/3.81 % (4075038)Instruction limit reached! % 21.23/3.81 % (4075038)------------------------------ % 21.23/3.81 % (4075038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.71 % (4075038)CaDiCaL version: 2.1.3 % 35.14/5.71 % (4075038)Termination reason: Instruction limit % 35.14/5.71 % (4075038)Termination phase: Saturation % 35.14/5.71 % (4075038)Time elapsed: 0.145 s % 35.14/5.71 % (4075038)Peak memory usage: 91 MB % 35.14/5.71 % (4075038)Instructions burned: 157 (million) % 35.14/5.71 % (4075037)Instruction limit reached! % 35.14/5.71 % (4075037)------------------------------ % 35.14/5.71 % (4075037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.71 % (4075037)CaDiCaL version: 2.1.3 % 35.14/5.71 % (4075037)Termination reason: Instruction limit % 35.14/5.71 % (4075037)Termination phase: Saturation % 35.14/5.71 % (4075037)Time elapsed: 0.275 s % 35.14/5.71 % (4075037)Peak memory usage: 91 MB % 35.14/5.71 % (4075037)Instructions burned: 285 (million) % 35.14/5.71 % (4075048)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=2159009148:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 35.14/5.71 % (4075050)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3164056153:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi) % 35.14/5.71 % (4075039)Instruction limit reached! % 35.14/5.71 % (4075039)------------------------------ % 35.14/5.71 % (4075039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.71 % (4075039)CaDiCaL version: 2.1.3 % 35.14/5.71 % (4075039)Termination reason: Instruction limit % 35.14/5.71 % (4075039)Termination phase: Saturation % 35.14/5.71 % (4075039)Time elapsed: 0.305 s % 35.14/5.71 % (4075039)Peak memory usage: 92 MB % 35.14/5.71 % (4075039)Instructions burned: 326 (million) % 35.14/5.71 % (4075048)Instruction limit reached! % 35.14/5.71 % (4075048)------------------------------ % 35.14/5.71 % (4075048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.71 % (4075048)CaDiCaL version: 2.1.3 % 35.14/5.71 % (4075048)Termination reason: Instruction limit % 35.14/5.71 % (4075048)Termination phase: Saturation % 35.14/5.71 % (4075048)Time elapsed: 0.228 s % 35.14/5.71 % (4075048)Peak memory usage: 91 MB % 35.14/5.71 % (4075048)Instructions burned: 248 (million) % 35.14/5.71 % (4075051)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2359414970:i=2350_2991 on theBenchmark for (2991ds/2350Mi) % 35.14/5.71 % (4075050)Instruction limit reached! % 35.14/5.71 % (4075050)------------------------------ % 35.14/5.71 % (4075050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.71 % (4075050)CaDiCaL version: 2.1.3 % 35.14/5.71 % (4075050)Termination reason: Instruction limit % 35.14/5.71 % (4075050)Termination phase: Saturation % 35.14/5.71 % (4075050)Time elapsed: 0.210 s % 35.14/5.71 % (4075050)Peak memory usage: 91 MB % 35.14/5.71 % (4075050)Instructions burned: 294 (million) % 35.14/5.71 % (4075054)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3238910765:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi) % 35.14/5.71 % (4075054)Instruction limit reached! % 35.14/5.71 % (4075054)------------------------------ % 35.14/5.71 % (4075054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.14/5.71 % (4075054)CaDiCaL version: 2.1.3 % 35.14/5.71 % (4075054)Termination reason: Instruction limit % 35.14/5.71 % (4075054)Termination phase: Saturation % 35.14/5.71 % (4075054)Time elapsed: 0.110 s % 35.14/5.71 % (4075054)Peak memory usage: 89 MB % 35.14/5.71 % (4075054)Instructions burned: 114 (million) % 35.14/5.71 % (4075058)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2023722950:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi) % 35.14/5.71 % (4075058)Refutation not found, incomplete strategy % 35.14/5.71 % (4075058)------------------------------ % 35.14/5.71 % (4075058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.14/5.71 % (4075058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/10.18 % (4075058)CaDiCaL version: 2.1.3 % 67.24/10.18 % (4075058)Termination reason: Refutation not found, incomplete strategy % 67.24/10.18 % (4075058)Time elapsed: 0.003 s % 67.24/10.18 % (4075058)Peak memory usage: 87 MB % 67.24/10.18 % (4075058)Instructions burned: 2 (million) % 67.24/10.18 % (4075061)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2408837539:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi) % 67.24/10.18 % (4075061)Instruction limit reached! % 67.24/10.18 % (4075061)------------------------------ % 67.24/10.18 % (4075061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/10.18 % (4075061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/10.18 % (4075061)CaDiCaL version: 2.1.3 % 67.24/10.18 % (4075061)Termination reason: Instruction limit % 67.24/10.18 % (4075061)Termination phase: Saturation % 67.24/10.18 % (4075061)Time elapsed: 0.098 s % 67.24/10.18 % (4075061)Peak memory usage: 88 MB % 67.24/10.18 % (4075061)Instructions burned: 115 (million) % 67.24/10.18 % (4075067)lrs+10_1_sil=8000:sp=occurrence:random_seed=2326189717:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi) % 67.24/10.18 % (4075070)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1718629029:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi) % 67.24/10.18 % (4075058)------------------------------ % 67.24/10.18 % (4075058)------------------------------ % 67.24/10.18 % (4075073)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1199082118:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi) % 67.24/10.18 % (4075070)Instruction limit reached! % 67.24/10.18 % (4075070)------------------------------ % 67.24/10.18 % (4075070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/10.18 % (4075070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/10.18 % (4075070)CaDiCaL version: 2.1.3 % 67.24/10.18 % (4075070)Termination reason: Instruction limit % 67.24/10.18 % (4075070)Termination phase: Saturation % 67.24/10.18 % (4075070)Time elapsed: 0.379 s % 67.24/10.18 % (4075070)Peak memory usage: 91 MB % 67.24/10.18 % (4075070)Instructions burned: 441 (million) % 67.24/10.18 % (4075077)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2721509566:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi) % 67.24/10.18 % (4075077)Refutation not found, incomplete strategy % 67.24/10.18 % (4075077)------------------------------ % 67.24/10.18 % (4075077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/10.18 % (4075077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/10.18 % (4075077)CaDiCaL version: 2.1.3 % 67.24/10.18 % (4075077)Termination reason: Refutation not found, incomplete strategy % 67.24/10.18 % (4075077)Time elapsed: 0.014 s % 67.24/10.18 % (4075077)Peak memory usage: 88 MB % 67.24/10.18 % (4075077)Instructions burned: 13 (million) % 67.24/10.18 % (4075067)Instruction limit reached! % 67.24/10.18 % (4075067)------------------------------ % 67.24/10.18 % (4075067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/10.18 % (4075067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/10.18 % (4075067)CaDiCaL version: 2.1.3 % 67.24/10.18 % (4075067)Termination reason: Instruction limit % 67.24/10.18 % (4075067)Termination phase: Saturation % 67.24/10.18 % (4075067)Time elapsed: 0.851 s % 67.24/10.18 % (4075067)Peak memory usage: 99 MB % 67.24/10.18 % (4075067)Instructions burned: 907 (million) % 67.24/10.18 % (4075079)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4108864749:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi) % 67.24/10.18 % (4075079)Refutation not found, incomplete strategy % 67.24/10.18 % (4075079)------------------------------ % 67.24/10.18 % (4075079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.24/10.18 % (4075079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.24/10.18 % (4075079)CaDiCaL version: 2.1.3 % 67.24/10.18 % (4075079)Termination reason: Refutation not found, incomplete strategy % 67.24/10.18 % (4075079)Time elapsed: 0.005 s % 67.24/10.18 % (4075079)Peak memory usage: 88 MB % 67.24/10.18 % (4075079)Instructions burned: 3 (million) % 67.24/10.18 % (4075077)------------------------------ % 67.24/10.18 % (4075077)------------------------------ % 67.24/10.18 % (4075081)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4021161503:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi) % 114.33/16.97 % (4075079)------------------------------ % 114.33/16.97 % (4075079)------------------------------ % 114.33/16.97 % (4075084)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=151308840:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi) % 114.33/16.97 % (4075051)Instruction limit reached! % 114.33/16.97 % (4075051)------------------------------ % 114.33/16.97 % (4075051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.33/16.97 % (4075051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.33/16.97 % (4075051)CaDiCaL version: 2.1.3 % 114.33/16.97 % (4075051)Termination reason: Instruction limit % 114.33/16.97 % (4075051)Termination phase: Saturation % 114.33/16.97 % (4075051)Time elapsed: 2.345 s % 114.33/16.97 % (4075051)Peak memory usage: 142 MB % 114.33/16.97 % (4075051)Instructions burned: 2350 (million) % 114.33/16.97 % (4075084)Instruction limit reached! % 114.33/16.97 % (4075084)------------------------------ % 114.33/16.97 % (4075084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.33/16.97 % (4075084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.33/16.97 % (4075084)CaDiCaL version: 2.1.3 % 114.33/16.97 % (4075084)Termination reason: Instruction limit % 114.33/16.97 % (4075084)Termination phase: Saturation % 114.33/16.97 % (4075084)Time elapsed: 0.132 s % 114.33/16.97 % (4075084)Peak memory usage: 90 MB % 114.33/16.97 % (4075084)Instructions burned: 125 (million) % 114.33/16.97 % (4075087)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=813257699:i=134:gtgl=5:slsql=off:gtg=exists_sym_2965 on theBenchmark for (2965ds/134Mi) % 114.33/16.97 % (4075088)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1539481859:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/141Mi) % 114.33/16.97 % (4075088)Refutation not found, incomplete strategy % 114.33/16.97 % (4075088)------------------------------ % 114.33/16.97 % (4075088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.33/16.97 % (4075088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.33/16.97 % (4075088)CaDiCaL version: 2.1.3 % 114.33/16.97 % (4075088)Termination reason: Refutation not found, incomplete strategy % 114.33/16.97 % (4075088)Time elapsed: 0.002 s % 114.33/16.97 % (4075088)Peak memory usage: 88 MB % 114.33/16.97 % (4075087)Instruction limit reached! % 114.33/16.97 % (4075087)------------------------------ % 114.33/16.97 % (4075087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.33/16.97 % (4075087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.33/16.97 % (4075087)CaDiCaL version: 2.1.3 % 114.33/16.97 % (4075087)Termination reason: Instruction limit % 114.33/16.97 % (4075087)Termination phase: Saturation % 114.33/16.97 % (4075087)Time elapsed: 0.130 s % 114.33/16.97 % (4075087)Peak memory usage: 90 MB % 114.33/16.97 % (4075087)Instructions burned: 134 (million) % 114.33/16.97 % (4075091)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4171945870:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2961 on theBenchmark for (2961ds/431Mi) % 114.33/16.97 % (4075091)Refutation not found, incomplete strategy % 114.33/16.97 % (4075091)------------------------------ % 114.33/16.97 % (4075091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.33/16.97 % (4075091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.33/16.97 % (4075091)CaDiCaL version: 2.1.3 % 114.33/16.97 % (4075091)Termination reason: Refutation not found, incomplete strategy % 114.33/16.97 % (4075091)Time elapsed: 0.002 s % 114.33/16.97 % (4075091)Peak memory usage: 88 MB % 114.33/16.97 % (4075088)------------------------------ % 114.33/16.97 % (4075088)------------------------------ % 114.33/16.97 % (4075093)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=1770539480:i=6060:aac=none:ins=25_2957 on theBenchmark for (2957ds/6060Mi) % 114.33/16.97 % (4075091)------------------------------ % 114.33/16.97 % (4075091)------------------------------ % 114.33/16.97 % (4075095)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=2785210385:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi) % 114.33/16.97 % (4075095)Instruction limit reached! % 114.33/16.97 % (4075095)------------------------------ % 177.59/25.83 % (4075095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.83 % (4075095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.83 % (4075095)CaDiCaL version: 2.1.3 % 177.59/25.83 % (4075095)Termination reason: Instruction limit % 177.59/25.83 % (4075095)Termination phase: Saturation % 177.59/25.83 % (4075095)Time elapsed: 0.144 s % 177.59/25.83 % (4075095)Peak memory usage: 91 MB % 177.59/25.83 % (4075095)Instructions burned: 150 (million) % 177.59/25.83 % (4075097)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3247194136:i=14155:bd=all_2950 on theBenchmark for (2950ds/14155Mi) % 177.59/25.83 % (4075073)Instruction limit reached! % 177.59/25.83 % (4075073)------------------------------ % 177.59/25.83 % (4075073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.83 % (4075073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.83 % (4075073)CaDiCaL version: 2.1.3 % 177.59/25.83 % (4075073)Termination reason: Instruction limit % 177.59/25.83 % (4075073)Termination phase: Saturation % 177.59/25.83 % (4075073)Time elapsed: 4.830 s % 177.59/25.83 % (4075073)Peak memory usage: 150 MB % 177.59/25.83 % (4075073)Instructions burned: 5203 (million) % 177.59/25.83 % (4075101)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4127423783:i=667:av=off:fsr=off_2931 on theBenchmark for (2931ds/667Mi) % 177.59/25.83 % (4075101)Instruction limit reached! % 177.59/25.83 % (4075101)------------------------------ % 177.59/25.83 % (4075101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.83 % (4075101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.83 % (4075101)CaDiCaL version: 2.1.3 % 177.59/25.83 % (4075101)Termination reason: Instruction limit % 177.59/25.83 % (4075101)Termination phase: Saturation % 177.59/25.83 % (4075101)Time elapsed: 0.526 s % 177.59/25.83 % (4075101)Peak memory usage: 88 MB % 177.59/25.83 % (4075101)Instructions burned: 667 (million) % 177.59/25.83 % (4075107)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=2829623055:s2a=on:i=185:s2at=1.8:fdi=4_2923 on theBenchmark for (2923ds/185Mi) % 177.59/25.83 % (4075107)Instruction limit reached! % 177.59/25.83 % (4075107)------------------------------ % 177.59/25.83 % (4075107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.83 % (4075107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.83 % (4075107)CaDiCaL version: 2.1.3 % 177.59/25.83 % (4075107)Termination reason: Instruction limit % 177.59/25.83 % (4075107)Termination phase: Saturation % 177.59/25.83 % (4075107)Time elapsed: 0.177 s % 177.59/25.83 % (4075107)Peak memory usage: 91 MB % 177.59/25.83 % (4075107)Instructions burned: 186 (million) % 177.59/25.83 % (4075113)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3076086478:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2919 on theBenchmark for (2919ds/193Mi) % 177.59/25.83 % (4075113)Instruction limit reached! % 177.59/25.83 % (4075113)------------------------------ % 177.59/25.83 % (4075113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.83 % (4075113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.83 % (4075113)CaDiCaL version: 2.1.3 % 177.59/25.83 % (4075113)Termination reason: Instruction limit % 177.59/25.83 % (4075113)Termination phase: Saturation % 177.59/25.83 % (4075113)Time elapsed: 0.158 s % 177.59/25.83 % (4075113)Peak memory usage: 89 MB % 177.59/25.83 % (4075113)Instructions burned: 194 (million) % 177.59/25.83 % (4075115)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=376056143:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2915 on theBenchmark for (2915ds/4850Mi) % 177.59/25.83 % (4075115)Refutation not found, incomplete strategy % 177.59/25.83 % (4075115)------------------------------ % 177.59/25.83 % (4075115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.59/25.83 % (4075115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.59/25.83 % (4075115)CaDiCaL version: 2.1.3 % 177.59/25.83 % (4075115)Termination reason: Refutation not found, incomplete strategy % 177.59/25.83 % (4075115)Time elapsed: 0.003 s % 177.59/25.83 % (4075115)Peak memory usage: 87 MB % 177.59/25.83 % (4075115)Instructions burned: 2 (million) % 177.59/25.83 % (4075115)------------------------------ % 177.59/25.83 % (4075115)------------------------------ % 177.59/25.83 % (4075117)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1668731554:i=12111:sd=1:ss=included_2908 on theBenchmark for (2908ds/12111Mi) % 229.85/33.06 % (4075093)Instruction limit reached! % 229.85/33.06 % (4075093)------------------------------ % 229.85/33.06 % (4075093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.85/33.06 % (4075093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.85/33.06 % (4075093)CaDiCaL version: 2.1.3 % 229.85/33.06 % (4075093)Termination reason: Instruction limit % 229.85/33.06 % (4075093)Termination phase: Saturation % 229.85/33.06 % (4075093)Time elapsed: 6.045 s % 229.85/33.06 % (4075093)Peak memory usage: 184 MB % 229.85/33.06 % (4075093)Instructions burned: 6061 (million) % 229.85/33.06 % (4075119)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1259545134:i=319:kws=precedence:fsr=off_2894 on theBenchmark for (2894ds/319Mi) % 229.85/33.06 % (4075119)Instruction limit reached! % 229.85/33.06 % (4075119)------------------------------ % 229.85/33.06 % (4075119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.85/33.06 % (4075119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.85/33.06 % (4075119)CaDiCaL version: 2.1.3 % 229.85/33.06 % (4075119)Termination reason: Instruction limit % 229.85/33.06 % (4075119)Termination phase: Saturation % 229.85/33.06 % (4075119)Time elapsed: 0.324 s % 229.85/33.06 % (4075119)Peak memory usage: 93 MB % 229.85/33.06 % (4075119)Instructions burned: 320 (million) % 229.85/33.06 % (4075123)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1565616029:i=2064:ep=RST_2887 on theBenchmark for (2887ds/2064Mi) % 229.85/33.06 % (4075123)Refutation not found, incomplete strategy % 229.85/33.06 % (4075123)------------------------------ % 229.85/33.06 % (4075123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.85/33.06 % (4075123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.85/33.06 % (4075123)CaDiCaL version: 2.1.3 % 229.85/33.06 % (4075123)Termination reason: Refutation not found, incomplete strategy % 229.85/33.06 % (4075123)Time elapsed: 0.004 s % 229.85/33.06 % (4075123)Peak memory usage: 88 MB % 229.85/33.06 % (4075123)Instructions burned: 3 (million) % 229.85/33.06 % (4075123)------------------------------ % 229.85/33.06 % (4075123)------------------------------ % 229.85/33.06 % (4075125)dis-1011_128_sil=32000:random_seed=3265575602:i=3706:ep=RST:av=off_2880 on theBenchmark for (2880ds/3706Mi) % 229.85/33.06 % (4075081)Instruction limit reached! % 229.85/33.06 % (4075081)------------------------------ % 229.85/33.06 % (4075081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.85/33.06 % (4075081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.85/33.06 % (4075081)CaDiCaL version: 2.1.3 % 229.85/33.06 % (4075081)Termination reason: Instruction limit % 229.85/33.06 % (4075081)Termination phase: Saturation % 229.85/33.06 % (4075081)Time elapsed: 12.295 s % 229.85/33.06 % (4075081)Peak memory usage: 249 MB % 229.85/33.06 % (4075081)Instructions burned: 13193 (million) % 229.85/33.06 % (4075134)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4091611134:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2845 on theBenchmark for (2845ds/757Mi) % 229.85/33.06 % (4075125)Instruction limit reached! % 229.85/33.06 % (4075125)------------------------------ % 229.85/33.06 % (4075125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.85/33.06 % (4075125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.85/33.06 % (4075125)CaDiCaL version: 2.1.3 % 229.85/33.06 % (4075125)Termination reason: Instruction limit % 229.85/33.06 % (4075125)Termination phase: Saturation % 229.85/33.06 % (4075125)Time elapsed: 3.734 s % 229.85/33.06 % (4075125)Peak memory usage: 133 MB % 229.85/33.06 % (4075125)Instructions burned: 3706 (million) % 229.85/33.06 % (4075134)Instruction limit reached! % 229.85/33.06 % (4075134)------------------------------ % 229.85/33.06 % (4075134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 229.85/33.06 % (4075134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 229.85/33.06 % (4075134)CaDiCaL version: 2.1.3 % 229.85/33.06 % (4075134)Termination reason: Instruction limit % 229.85/33.06 % (4075134)Termination phase: Saturation % 229.85/33.06 % (4075134)Time elapsed: 0.575 s % 229.85/33.06 % (4075134)Peak memory usage: 91 MB % 229.85/33.06 % (4075134)Instructions burned: 757 (million) % 229.85/33.06 % (4075136)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2621751173:i=13913:ss=axioms:sgt=8_2840 on theBenchmark for (2840ds/13913Mi) % 272.71/39.21 % (4075137)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1955820952:i=9925:aac=none_2837 on theBenchmark for (2837ds/9925Mi) % 272.71/39.21 % (4075097)Instruction limit reached! % 272.71/39.21 % (4075097)------------------------------ % 272.71/39.21 % (4075097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.71/39.21 % (4075097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.71/39.21 % (4075097)CaDiCaL version: 2.1.3 % 272.71/39.21 % (4075097)Termination reason: Instruction limit % 272.71/39.21 % (4075097)Termination phase: Saturation % 272.71/39.21 % (4075097)Time elapsed: 13.746 s % 272.71/39.21 % (4075097)Peak memory usage: 246 MB % 272.71/39.21 % (4075097)Instructions burned: 14155 (million) % 272.71/39.21 % (4075144)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1891848191:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2809 on theBenchmark for (2809ds/2479Mi) % 272.71/39.21 % (4075117)Instruction limit reached! % 272.71/39.21 % (4075117)------------------------------ % 272.71/39.21 % (4075117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.71/39.21 % (4075117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.71/39.21 % (4075117)CaDiCaL version: 2.1.3 % 272.71/39.21 % (4075117)Termination reason: Instruction limit % 272.71/39.21 % (4075117)Termination phase: Saturation % 272.71/39.21 % (4075117)Time elapsed: 11.257 s % 272.71/39.21 % (4075117)Peak memory usage: 238 MB % 272.71/39.21 % (4075117)Instructions burned: 12111 (million) % 272.71/39.21 % (4075146)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2448016459:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2792 on theBenchmark for (2792ds/440Mi) % 272.71/39.21 % (4075144)Instruction limit reached! % 272.71/39.21 % (4075144)------------------------------ % 272.71/39.21 % (4075144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.71/39.21 % (4075144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.71/39.21 % (4075144)CaDiCaL version: 2.1.3 % 272.71/39.21 % (4075144)Termination reason: Instruction limit % 272.71/39.21 % (4075144)Termination phase: Saturation % 272.71/39.21 % (4075144)Time elapsed: 2.108 s % 272.71/39.21 % (4075144)Peak memory usage: 112 MB % 272.71/39.21 % (4075144)Instructions burned: 2480 (million) % 272.71/39.21 % (4075146)Instruction limit reached! % 272.71/39.21 % (4075146)------------------------------ % 272.71/39.21 % (4075146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.71/39.21 % (4075146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.71/39.21 % (4075146)CaDiCaL version: 2.1.3 % 272.71/39.21 % (4075146)Termination reason: Instruction limit % 272.71/39.21 % (4075146)Termination phase: Saturation % 272.71/39.21 % (4075146)Time elapsed: 0.391 s % 272.71/39.21 % (4075146)Peak memory usage: 93 MB % 272.71/39.21 % (4075146)Instructions burned: 441 (million) % 272.71/39.21 % (4075148)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1230910551:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2785 on theBenchmark for (2785ds/11145Mi) % 272.71/39.21 % (4075149)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=177949230:cts=off:i=3034:av=off:er=known:fsd=on_2785 on theBenchmark for (2785ds/3034Mi) % 272.71/39.21 % (4075149)Instruction limit reached! % 272.71/39.21 % (4075149)------------------------------ % 272.71/39.21 % (4075149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.71/39.21 % (4075149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.71/39.21 % (4075149)CaDiCaL version: 2.1.3 % 272.71/39.21 % (4075149)Termination reason: Instruction limit % 272.71/39.21 % (4075149)Termination phase: Saturation % 272.71/39.21 % (4075149)Time elapsed: 2.589 s % 272.71/39.21 % (4075149)Peak memory usage: 135 MB % 272.71/39.21 % (4075149)Instructions burned: 3034 (million) % 272.71/39.21 % (4075154)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3675390599:st=2:s2a=on:i=524:s2at=2:ss=axioms_2756 on theBenchmark for (2756ds/524Mi) % 272.71/39.21 % (4075154)Instruction limit reached! % 272.71/39.21 % (4075154)------------------------------ % 272.71/39.21 % (4075154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.71/39.21 % (4075154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.09 % (4075154)CaDiCaL version: 2.1.3 % 300.09/43.09 % (4075154)Termination reason: Instruction limit % 300.09/43.09 % (4075154)Termination phase: Saturation % 300.09/43.09 % (4075154)Time elapsed: 0.495 s % 300.09/43.09 % (4075154)Peak memory usage: 95 MB % 300.09/43.09 % (4075154)Instructions burned: 525 (million) % 300.09/43.09 % (4075156)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3000126746:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2748 on theBenchmark for (2748ds/1016Mi) % 300.09/43.09 % (4075137)Instruction limit reached! % 300.09/43.09 % (4075137)------------------------------ % 300.09/43.09 % (4075137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.09 % (4075137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.09 % (4075137)CaDiCaL version: 2.1.3 % 300.09/43.09 % (4075137)Termination reason: Instruction limit % 300.09/43.09 % (4075137)Termination phase: Saturation % 300.09/43.09 % (4075137)Time elapsed: 9.161 s % 300.09/43.09 % (4075137)Peak memory usage: 217 MB % 300.09/43.09 % (4075137)Instructions burned: 9926 (million) % 300.09/43.09 % (4075158)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=729274070:i=14123:bd=preordered:ins=4_2743 on theBenchmark for (2743ds/14123Mi) % 300.09/43.09 % (4075156)Instruction limit reached! % 300.09/43.09 % (4075156)------------------------------ % 300.09/43.09 % (4075156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.09 % (4075156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.09 % (4075156)CaDiCaL version: 2.1.3 % 300.09/43.09 % (4075156)Termination reason: Instruction limit % 300.09/43.09 % (4075156)Termination phase: Saturation % 300.09/43.09 % (4075156)Time elapsed: 0.896 s % 300.09/43.09 % (4075156)Peak memory usage: 102 MB % 300.09/43.09 % (4075156)Instructions burned: 1016 (million) % 300.09/43.09 % (4075160)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=985452641:i=5781:kws=precedence:bd=all:rawr=on_2737 on theBenchmark for (2737ds/5781Mi) % 300.09/43.09 % (4075136)Instruction limit reached! % 300.09/43.09 % (4075136)------------------------------ % 300.09/43.09 % (4075136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.09 % (4075136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.09 % (4075136)CaDiCaL version: 2.1.3 % 300.09/43.09 % (4075136)Termination reason: Instruction limit % 300.09/43.09 % (4075136)Termination phase: Saturation % 300.09/43.09 % (4075136)Time elapsed: 13.268 s % 300.09/43.09 % (4075136)Peak memory usage: 255 MB % 300.09/43.09 % (4075136)Instructions burned: 13913 (million) % 300.09/43.09 % (4075164)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=3716217768:i=2448:gtgl=5:bd=preordered:gtg=all_2704 on theBenchmark for (2704ds/2448Mi) % 300.09/43.09 % (4075160)Instruction limit reached! % 300.09/43.09 % (4075160)------------------------------ % 300.09/43.09 % (4075160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.09 % (4075160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.09 % (4075160)CaDiCaL version: 2.1.3 % 300.09/43.09 % (4075160)Termination reason: Instruction limit % 300.09/43.09 % (4075160)Termination phase: Saturation % 300.09/43.09 % (4075160)Time elapsed: 4.919 s % 300.09/43.09 % (4075160)Peak memory usage: 145 MB % 300.09/43.09 % (4075160)Instructions burned: 5782 (million) % 300.09/43.09 % (4075166)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2825350809:i=3223:kws=precedence:fgj=on:av=off_2684 on theBenchmark for (2684ds/3223Mi) % 300.09/43.09 % (4075148)Instruction limit reached! % 300.09/43.09 % (4075148)------------------------------ % 300.09/43.09 % (4075148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.09 % (4075148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.09/43.09 % (4075148)CaDiCaL version: 2.1.3 % 300.09/43.09 % (4075148)Termination reason: Instruction limit % 300.09/43.09 % (4075148)Termination phase: Saturation % 300.09/43.09 % (4075148)Time elapsed: 10.431 s % 300.09/43.09 % (4075148)Peak memory usage: 219 MB % 300.09/43.09 % (4075148)Instructions burned: 11145 (million) % 300.09/43.09 % (4075164)Instruction limit reached! % 300.09/43.09 % (4075164)------------------------------ % 300.09/43.09 % (4075164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.09/43.09 % (4075164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c % 300.09/43.09 Terminated %------------------------------------------------------------------------------