%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM923+7 : TPTP v9.3.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n008.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 12:17:28 PM UTC 2026 % Result : Timeout 300.58s 43.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM923+7 : TPTP v9.3.1. Released v5.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.42 % Computer : n008.cluster.edu % 0.17/0.42 % Model : x86_64 x86_64 % 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.42 % Memory : 8046.5625MB % 0.17/0.42 % OS : Linux 6.8.0-71-generic % 0.17/0.42 % CPULimit : 300 % 0.17/0.42 % WCLimit : 300 % 0.17/0.42 % DateTime : Sun Sep 27 21:41:24 UTC 2026 % 0.17/0.42 % CPUTime : % 0.17/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.22/0.48 Running first-order theorem proving % 0.22/0.48 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 % 17.89/3.73 % (1628405)Detected formulas, will run a generic FOF schedule. % 17.89/3.73 % (1628413)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=16958711:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi) % 17.89/3.73 % (1628413)Instruction limit reached! % 17.89/3.73 % (1628413)------------------------------ % 17.89/3.73 % (1628413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.73 % (1628413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.73 % (1628413)CaDiCaL version: 2.1.3 % 17.89/3.73 % (1628413)Termination reason: Instruction limit % 17.89/3.73 % (1628413)Termination phase: Saturation % 17.89/3.73 % (1628413)Time elapsed: 0.030 s % 17.89/3.73 % (1628413)Peak memory usage: 90 MB % 17.89/3.73 % (1628413)Instructions burned: 112 (million) % 17.89/3.73 % (1628415)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4249054727:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi) % 17.89/3.73 % (1628412)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=648114062:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi) % 17.89/3.73 % (1628411)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=1492201662:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi) % 17.89/3.73 % (1628416)dis-21_1_sil=8000:lcm=predicate:random_seed=3986389163:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi) % 17.89/3.73 % (1628410)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=4053030974:i=141193_2998 on theBenchmark for (2998ds/141193Mi) % 17.89/3.73 % (1628414)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2483756318:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi) % 17.89/3.73 % (1628418)lrs+10_1_sil=8000:sp=occurrence:random_seed=2144241075:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 17.89/3.73 % (1628416)Instruction limit reached! % 17.89/3.73 % (1628416)------------------------------ % 17.89/3.73 % (1628416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.73 % (1628416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.73 % (1628416)CaDiCaL version: 2.1.3 % 17.89/3.73 % (1628416)Termination reason: Instruction limit % 17.89/3.73 % (1628416)Termination phase: Property scanning % 17.89/3.73 % (1628416)Time elapsed: 0.099 s % 17.89/3.73 % (1628416)Peak memory usage: 88 MB % 17.89/3.73 % (1628416)Instructions burned: 129 (million) % 17.89/3.73 % (1628415)Instruction limit reached! % 17.89/3.73 % (1628415)------------------------------ % 17.89/3.73 % (1628415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.73 % (1628415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.73 % (1628415)CaDiCaL version: 2.1.3 % 17.89/3.73 % (1628415)Termination reason: Instruction limit % 17.89/3.73 % (1628415)Termination phase: Equality resolution with deletion % 17.89/3.73 % (1628415)Time elapsed: 0.103 s % 17.89/3.73 % (1628415)Peak memory usage: 88 MB % 17.89/3.73 % (1628415)Instructions burned: 140 (million) % 17.89/3.73 % (1628414)Instruction limit reached! % 17.89/3.73 % (1628414)------------------------------ % 17.89/3.73 % (1628414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.73 % (1628414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.73 % (1628414)CaDiCaL version: 2.1.3 % 17.89/3.73 % (1628414)Termination reason: Instruction limit % 17.89/3.73 % (1628414)Termination phase: Saturation % 17.89/3.73 % (1628414)Time elapsed: 0.107 s % 17.89/3.73 % (1628414)Peak memory usage: 89 MB % 17.89/3.73 % (1628414)Instructions burned: 119 (million) % 17.89/3.73 % (1628418)Instruction limit reached! % 17.89/3.73 % (1628418)------------------------------ % 17.89/3.73 % (1628418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.89/3.73 % (1628418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.89/3.73 % (1628418)CaDiCaL version: 2.1.3 % 17.89/3.73 % (1628418)Termination reason: Instruction limit % 17.89/3.73 % (1628418)Termination phase: Saturation % 17.89/3.73 % (1628418)Time elapsed: 0.143 s % 17.89/3.73 % (1628418)Peak memory usage: 91 MB % 17.89/3.73 % (1628418)Instructions burned: 287 (million) % 28.18/5.06 % (1628428)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1440970321:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi) % 28.18/5.06 % (1628428)Instruction limit reached! % 28.18/5.06 % (1628428)------------------------------ % 28.18/5.06 % (1628428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.18/5.06 % (1628428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.18/5.06 % (1628428)CaDiCaL version: 2.1.3 % 28.18/5.06 % (1628428)Termination reason: Instruction limit % 28.18/5.06 % (1628428)Termination phase: Saturation % 28.18/5.06 % (1628428)Time elapsed: 0.073 s % 28.18/5.06 % (1628428)Peak memory usage: 90 MB % 28.18/5.06 % (1628428)Instructions burned: 157 (million) % 28.18/5.06 % (1628429)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1151691571:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 28.18/5.06 % (1628430)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=3401052087:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi) % 28.18/5.06 % (1628431)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1984435645:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 28.18/5.06 % (1628433)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4224248207:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 28.18/5.06 % (1628430)Instruction limit reached! % 28.18/5.06 % (1628430)------------------------------ % 28.18/5.06 % (1628430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.18/5.06 % (1628430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.18/5.06 % (1628430)CaDiCaL version: 2.1.3 % 28.18/5.06 % (1628430)Termination reason: Instruction limit % 28.18/5.06 % (1628430)Termination phase: Saturation % 28.18/5.06 % (1628430)Time elapsed: 0.205 s % 28.18/5.06 % (1628430)Peak memory usage: 91 MB % 28.18/5.06 % (1628430)Instructions burned: 248 (million) % 28.18/5.06 % (1628429)Instruction limit reached! % 28.18/5.06 % (1628429)------------------------------ % 28.18/5.06 % (1628429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.18/5.06 % (1628429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.18/5.06 % (1628429)CaDiCaL version: 2.1.3 % 28.18/5.06 % (1628429)Termination reason: Instruction limit % 28.18/5.06 % (1628429)Termination phase: Saturation % 28.18/5.06 % (1628429)Time elapsed: 0.283 s % 28.18/5.06 % (1628429)Peak memory usage: 92 MB % 28.18/5.06 % (1628429)Instructions burned: 325 (million) % 28.18/5.06 % (1628431)Instruction limit reached! % 28.18/5.06 % (1628431)------------------------------ % 28.18/5.06 % (1628431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.18/5.06 % (1628431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.18/5.06 % (1628431)CaDiCaL version: 2.1.3 % 28.18/5.06 % (1628431)Termination reason: Instruction limit % 28.18/5.06 % (1628431)Termination phase: Saturation % 28.18/5.06 % (1628431)Time elapsed: 0.258 s % 28.18/5.06 % (1628431)Peak memory usage: 92 MB % 28.18/5.06 % (1628431)Instructions burned: 295 (million) % 28.18/5.06 % (1628438)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2213868117:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi) % 28.18/5.06 % (1628439)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1321263608:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi) % 28.18/5.06 % (1628438)Instruction limit reached! % 28.18/5.06 % (1628438)------------------------------ % 28.18/5.06 % (1628438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.18/5.06 % (1628438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.18/5.06 % (1628438)CaDiCaL version: 2.1.3 % 28.18/5.06 % (1628438)Termination reason: Instruction limit % 28.18/5.06 % (1628438)Termination phase: Saturation % 28.18/5.06 % (1628438)Time elapsed: 0.093 s % 28.18/5.06 % (1628438)Peak memory usage: 90 MB % 28.18/5.06 % (1628438)Instructions burned: 113 (million) % 28.18/5.06 % (1628439)Instruction limit reached! % 28.18/5.06 % (1628439)------------------------------ % 28.18/5.06 % (1628439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.18/5.06 % (1628439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.18/5.06 % (1628439)CaDiCaL version: 2.1.3 % 28.18/5.06 % (1628439)Termination reason: Instruction limit % 52.96/8.68 % (1628439)Termination phase: Property scanning % 52.96/8.68 % (1628439)Time elapsed: 0.104 s % 52.96/8.68 % (1628439)Peak memory usage: 89 MB % 52.96/8.68 % (1628439)Instructions burned: 128 (million) % 52.96/8.68 % (1628440)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1218918572:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi) % 52.96/8.68 % (1628440)Instruction limit reached! % 52.96/8.68 % (1628440)------------------------------ % 52.96/8.68 % (1628440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.68 % (1628440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.68 % (1628440)CaDiCaL version: 2.1.3 % 52.96/8.68 % (1628440)Termination reason: Instruction limit % 52.96/8.68 % (1628440)Termination phase: Property scanning % 52.96/8.68 % (1628440)Time elapsed: 0.090 s % 52.96/8.68 % (1628440)Peak memory usage: 87 MB % 52.96/8.68 % (1628440)Instructions burned: 114 (million) % 52.96/8.68 % (1628443)lrs+10_1_sil=8000:sp=occurrence:random_seed=2811395519:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi) % 52.96/8.68 % (1628446)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1037901277:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi) % 52.96/8.68 % (1628447)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1938399437:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi) % 52.96/8.68 % (1628446)Instruction limit reached! % 52.96/8.68 % (1628446)------------------------------ % 52.96/8.68 % (1628446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.68 % (1628446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.68 % (1628446)CaDiCaL version: 2.1.3 % 52.96/8.68 % (1628446)Termination reason: Instruction limit % 52.96/8.68 % (1628446)Termination phase: Saturation % 52.96/8.68 % (1628446)Time elapsed: 0.361 s % 52.96/8.68 % (1628446)Peak memory usage: 94 MB % 52.96/8.68 % (1628446)Instructions burned: 437 (million) % 52.96/8.68 % (1628433)Instruction limit reached! % 52.96/8.68 % (1628433)------------------------------ % 52.96/8.68 % (1628433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.68 % (1628433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.68 % (1628433)CaDiCaL version: 2.1.3 % 52.96/8.68 % (1628433)Termination reason: Instruction limit % 52.96/8.68 % (1628433)Termination phase: Saturation % 52.96/8.68 % (1628433)Time elapsed: 1.269 s % 52.96/8.68 % (1628433)Peak memory usage: 145 MB % 52.96/8.68 % (1628433)Instructions burned: 2351 (million) % 52.96/8.68 % (1628451)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3644024124:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi) % 52.96/8.68 % (1628451)Instruction limit reached! % 52.96/8.68 % (1628451)------------------------------ % 52.96/8.68 % (1628451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.68 % (1628451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.68 % (1628451)CaDiCaL version: 2.1.3 % 52.96/8.68 % (1628451)Termination reason: Instruction limit % 52.96/8.68 % (1628451)Termination phase: Property scanning % 52.96/8.68 % (1628451)Time elapsed: 0.108 s % 52.96/8.68 % (1628451)Peak memory usage: 88 MB % 52.96/8.68 % (1628451)Instructions burned: 135 (million) % 52.96/8.68 % (1628443)Instruction limit reached! % 52.96/8.68 % (1628443)------------------------------ % 52.96/8.68 % (1628443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.96/8.68 % (1628443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.96/8.68 % (1628443)CaDiCaL version: 2.1.3 % 52.96/8.68 % (1628443)Termination reason: Instruction limit % 52.96/8.68 % (1628443)Termination phase: Saturation % 52.96/8.68 % (1628443)Time elapsed: 0.803 s % 52.96/8.68 % (1628443)Peak memory usage: 96 MB % 52.96/8.68 % (1628443)Instructions burned: 908 (million) % 52.96/8.68 % (1628452)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=944366336:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi) % 52.96/8.68 % (1628454)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2922920714:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi) % 52.96/8.68 % (1628455)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=3763888568:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi) % 126.72/18.96 % (1628452)Instruction limit reached! % 126.72/18.96 % (1628452)------------------------------ % 126.72/18.96 % (1628452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.72/18.96 % (1628452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.72/18.96 % (1628452)CaDiCaL version: 2.1.3 % 126.72/18.96 % (1628452)Termination reason: Instruction limit % 126.72/18.96 % (1628452)Termination phase: Saturation % 126.72/18.96 % (1628452)Time elapsed: 0.247 s % 126.72/18.96 % (1628452)Peak memory usage: 96 MB % 126.72/18.96 % (1628452)Instructions burned: 592 (million) % 126.72/18.96 % (1628455)Instruction limit reached! % 126.72/18.96 % (1628455)------------------------------ % 126.72/18.96 % (1628455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.72/18.96 % (1628455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.72/18.96 % (1628455)CaDiCaL version: 2.1.3 % 126.72/18.96 % (1628455)Termination reason: Instruction limit % 126.72/18.96 % (1628455)Termination phase: Saturation % 126.72/18.96 % (1628455)Time elapsed: 0.102 s % 126.72/18.96 % (1628455)Peak memory usage: 90 MB % 126.72/18.96 % (1628455)Instructions burned: 125 (million) % 126.72/18.96 % (1628459)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1090194431:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi) % 126.72/18.96 % (1628459)Instruction limit reached! % 126.72/18.96 % (1628459)------------------------------ % 126.72/18.96 % (1628459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.72/18.96 % (1628459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.72/18.96 % (1628459)CaDiCaL version: 2.1.3 % 126.72/18.96 % (1628459)Termination reason: Instruction limit % 126.72/18.96 % (1628459)Termination phase: Property scanning % 126.72/18.96 % (1628459)Time elapsed: 0.107 s % 126.72/18.96 % (1628459)Peak memory usage: 87 MB % 126.72/18.96 % (1628459)Instructions burned: 135 (million) % 126.72/18.96 % (1628460)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=705682234:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/141Mi) % 126.72/18.96 % (1628460)Refutation not found, incomplete strategy % 126.72/18.96 % (1628460)------------------------------ % 126.72/18.96 % (1628460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.72/18.96 % (1628460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.72/18.96 % (1628460)CaDiCaL version: 2.1.3 % 126.72/18.96 % (1628460)Termination reason: Refutation not found, incomplete strategy % 126.72/18.96 % (1628460)Time elapsed: 0.022 s % 126.72/18.96 % (1628460)Peak memory usage: 90 MB % 126.72/18.96 % (1628460)Instructions burned: 50 (million) % 126.72/18.96 % (1628463)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=375809629:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi) % 126.72/18.96 % (1628460)------------------------------ % 126.72/18.96 % (1628460)------------------------------ % 126.72/18.96 % (1628465)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=29216029:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi) % 126.72/18.96 % (1628463)Instruction limit reached! % 126.72/18.96 % (1628463)------------------------------ % 126.72/18.96 % (1628463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.72/18.96 % (1628463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.72/18.96 % (1628463)CaDiCaL version: 2.1.3 % 126.72/18.96 % (1628463)Termination reason: Instruction limit % 126.72/18.96 % (1628463)Termination phase: Saturation % 126.72/18.96 % (1628463)Time elapsed: 0.352 s % 126.72/18.96 % (1628463)Peak memory usage: 91 MB % 126.72/18.96 % (1628463)Instructions burned: 432 (million) % 126.72/18.96 % (1628467)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=2542930081:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2963 on theBenchmark for (2963ds/150Mi) % 126.72/18.96 % (1628467)Instruction limit reached! % 126.72/18.96 % (1628467)------------------------------ % 126.72/18.96 % (1628467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.72/18.96 % (1628467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.72/18.96 % (1628467)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628467)Termination reason: Instruction limit % 146.40/21.79 % (1628467)Termination phase: Property scanning % 146.40/21.79 % (1628467)Time elapsed: 0.117 s % 146.40/21.79 % (1628467)Peak memory usage: 88 MB % 146.40/21.79 % (1628467)Instructions burned: 151 (million) % 146.40/21.79 % (1628469)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1576990197:i=14155:bd=all_2959 on theBenchmark for (2959ds/14155Mi) % 146.40/21.79 % (1628447)Instruction limit reached! % 146.40/21.79 % (1628447)------------------------------ % 146.40/21.79 % (1628447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.40/21.79 % (1628447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.40/21.79 % (1628447)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628447)Termination reason: Instruction limit % 146.40/21.79 % (1628447)Termination phase: Saturation % 146.40/21.79 % (1628447)Time elapsed: 4.701 s % 146.40/21.79 % (1628447)Peak memory usage: 151 MB % 146.40/21.79 % (1628447)Instructions burned: 5203 (million) % 146.40/21.79 % (1628471)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1251995709:i=667:av=off:fsr=off_2935 on theBenchmark for (2935ds/667Mi) % 146.40/21.79 % (1628471)Instruction limit reached! % 146.40/21.79 % (1628471)------------------------------ % 146.40/21.79 % (1628471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.40/21.79 % (1628471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.40/21.79 % (1628471)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628471)Termination reason: Instruction limit % 146.40/21.79 % (1628471)Termination phase: Saturation % 146.40/21.79 % (1628471)Time elapsed: 0.284 s % 146.40/21.79 % (1628471)Peak memory usage: 92 MB % 146.40/21.79 % (1628471)Instructions burned: 669 (million) % 146.40/21.79 % (1628473)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=2424575580:s2a=on:i=185:s2at=1.8:fdi=4_2930 on theBenchmark for (2930ds/185Mi) % 146.40/21.79 % (1628465)Instruction limit reached! % 146.40/21.79 % (1628465)------------------------------ % 146.40/21.79 % (1628465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.40/21.79 % (1628465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.40/21.79 % (1628465)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628465)Termination reason: Instruction limit % 146.40/21.79 % (1628465)Termination phase: Saturation % 146.40/21.79 % (1628465)Time elapsed: 3.716 s % 146.40/21.79 % (1628465)Peak memory usage: 176 MB % 146.40/21.79 % (1628465)Instructions burned: 6061 (million) % 146.40/21.79 % (1628473)Instruction limit reached! % 146.40/21.79 % (1628473)------------------------------ % 146.40/21.79 % (1628473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.40/21.79 % (1628473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.40/21.79 % (1628473)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628473)Termination reason: Instruction limit % 146.40/21.79 % (1628473)Termination phase: Saturation % 146.40/21.79 % (1628473)Time elapsed: 0.081 s % 146.40/21.79 % (1628473)Peak memory usage: 91 MB % 146.40/21.79 % (1628473)Instructions burned: 187 (million) % 146.40/21.79 % (1628477)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1540683928:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2927 on theBenchmark for (2927ds/193Mi) % 146.40/21.79 % (1628478)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3379305571:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2927 on theBenchmark for (2927ds/4850Mi) % 146.40/21.79 % (1628478)Refutation not found, incomplete strategy % 146.40/21.79 % (1628478)------------------------------ % 146.40/21.79 % (1628478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.40/21.79 % (1628478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.40/21.79 % (1628478)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628478)Termination reason: Refutation not found, incomplete strategy % 146.40/21.79 % (1628478)Time elapsed: 0.086 s % 146.40/21.79 % (1628478)Peak memory usage: 91 MB % 146.40/21.79 % (1628478)Instructions burned: 203 (million) % 146.40/21.79 % (1628477)Instruction limit reached! % 146.40/21.79 % (1628477)------------------------------ % 146.40/21.79 % (1628477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.40/21.79 % (1628477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.40/21.79 % (1628477)CaDiCaL version: 2.1.3 % 146.40/21.79 % (1628477)Termination reason: Instruction limit % 192.23/28.18 % (1628477)Termination phase: Saturation % 192.23/28.18 % (1628477)Time elapsed: 0.176 s % 192.23/28.18 % (1628477)Peak memory usage: 91 MB % 192.23/28.18 % (1628477)Instructions burned: 193 (million) % 192.23/28.18 % (1628478)------------------------------ % 192.23/28.18 % (1628478)------------------------------ % 192.23/28.18 % (1628481)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3353891885:i=12111:sd=1:ss=included_2923 on theBenchmark for (2923ds/12111Mi) % 192.23/28.18 % (1628482)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1556262547:i=319:kws=precedence:fsr=off_2921 on theBenchmark for (2921ds/319Mi) % 192.23/28.18 % (1628482)Instruction limit reached! % 192.23/28.18 % (1628482)------------------------------ % 192.23/28.18 % (1628482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.23/28.18 % (1628482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.23/28.18 % (1628482)CaDiCaL version: 2.1.3 % 192.23/28.18 % (1628482)Termination reason: Instruction limit % 192.23/28.18 % (1628482)Termination phase: Saturation % 192.23/28.18 % (1628482)Time elapsed: 0.146 s % 192.23/28.18 % (1628482)Peak memory usage: 93 MB % 192.23/28.18 % (1628482)Instructions burned: 320 (million) % 192.23/28.18 % (1628485)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3085738181:i=2064:ep=RST_2917 on theBenchmark for (2917ds/2064Mi) % 192.23/28.18 % (1628485)Instruction limit reached! % 192.23/28.18 % (1628485)------------------------------ % 192.23/28.18 % (1628485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.23/28.18 % (1628485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.23/28.18 % (1628485)CaDiCaL version: 2.1.3 % 192.23/28.18 % (1628485)Termination reason: Instruction limit % 192.23/28.18 % (1628485)Termination phase: Saturation % 192.23/28.18 % (1628485)Time elapsed: 0.868 s % 192.23/28.18 % (1628485)Peak memory usage: 98 MB % 192.23/28.18 % (1628485)Instructions burned: 2066 (million) % 192.23/28.18 % (1628487)dis-1011_128_sil=32000:random_seed=3952560284:i=3706:ep=RST:av=off_2906 on theBenchmark for (2906ds/3706Mi) % 192.23/28.18 % (1628487)Instruction limit reached! % 192.23/28.18 % (1628487)------------------------------ % 192.23/28.18 % (1628487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.23/28.18 % (1628487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.23/28.18 % (1628487)CaDiCaL version: 2.1.3 % 192.23/28.18 % (1628487)Termination reason: Instruction limit % 192.23/28.18 % (1628487)Termination phase: Saturation % 192.23/28.18 % (1628487)Time elapsed: 1.801 s % 192.23/28.18 % (1628487)Peak memory usage: 114 MB % 192.23/28.18 % (1628487)Instructions burned: 3707 (million) % 192.23/28.18 % (1628491)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1208256250:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2886 on theBenchmark for (2886ds/757Mi) % 192.23/28.18 % (1628491)Instruction limit reached! % 192.23/28.18 % (1628491)------------------------------ % 192.23/28.18 % (1628491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.23/28.18 % (1628491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.23/28.18 % (1628491)CaDiCaL version: 2.1.3 % 192.23/28.18 % (1628491)Termination reason: Instruction limit % 192.23/28.18 % (1628491)Termination phase: Saturation % 192.23/28.18 % (1628491)Time elapsed: 0.341 s % 192.23/28.18 % (1628491)Peak memory usage: 92 MB % 192.23/28.18 % (1628491)Instructions burned: 759 (million) % 192.23/28.18 % (1628495)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=209022049:i=13913:ss=axioms:sgt=8_2880 on theBenchmark for (2880ds/13913Mi) % 192.23/28.18 % (1628454)Instruction limit reached! % 192.23/28.18 % (1628454)------------------------------ % 192.23/28.18 % (1628454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.23/28.18 % (1628454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.23/28.18 % (1628454)CaDiCaL version: 2.1.3 % 192.23/28.18 % (1628454)Termination reason: Instruction limit % 192.23/28.18 % (1628454)Termination phase: Saturation % 192.23/28.18 % (1628454)Time elapsed: 12.491 s % 192.23/28.18 % (1628454)Peak memory usage: 224 MB % 192.23/28.18 % (1628454)Instructions burned: 13193 (million) % 192.23/28.18 % (1628497)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=855921023:i=9925:aac=none_2848 on theBenchmark for (2848ds/9925Mi) % 192.23/28.18 % (1628469)Instruction limit reached! % 192.23/28.18 % (1628469)------------------------------ % 216.67/31.61 % (1628469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.67/31.61 % (1628469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.67/31.61 % (1628469)CaDiCaL version: 2.1.3 % 216.67/31.61 % (1628469)Termination reason: Instruction limit % 216.67/31.61 % (1628469)Termination phase: Saturation % 216.67/31.61 % (1628469)Time elapsed: 13.602 s % 216.67/31.61 % (1628469)Peak memory usage: 224 MB % 216.67/31.61 % (1628469)Instructions burned: 14155 (million) % 216.67/31.61 % (1628503)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4257154600:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2820 on theBenchmark for (2820ds/2479Mi) % 216.67/31.61 % (1628503)Refutation not found, incomplete strategy % 216.67/31.61 % (1628503)------------------------------ % 216.67/31.61 % (1628503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.67/31.61 % (1628503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.67/31.61 % (1628503)CaDiCaL version: 2.1.3 % 216.67/31.61 % (1628503)Termination reason: Refutation not found, incomplete strategy % 216.67/31.61 % (1628503)Time elapsed: 0.696 s % 216.67/31.61 % (1628503)Peak memory usage: 93 MB % 216.67/31.61 % (1628503)Instructions burned: 821 (million) % 216.67/31.61 % (1628495)Instruction limit reached! % 216.67/31.61 % (1628495)------------------------------ % 216.67/31.61 % (1628495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.67/31.61 % (1628495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.67/31.61 % (1628495)CaDiCaL version: 2.1.3 % 216.67/31.61 % (1628495)Termination reason: Instruction limit % 216.67/31.61 % (1628495)Termination phase: Saturation % 216.67/31.61 % (1628495)Time elapsed: 6.947 s % 216.67/31.61 % (1628495)Peak memory usage: 210 MB % 216.67/31.61 % (1628495)Instructions burned: 13914 (million) % 216.67/31.61 % (1628481)Instruction limit reached! % 216.67/31.61 % (1628481)------------------------------ % 216.67/31.61 % (1628481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.67/31.61 % (1628481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.67/31.61 % (1628481)CaDiCaL version: 2.1.3 % 216.67/31.61 % (1628481)Termination reason: Instruction limit % 216.67/31.61 % (1628481)Termination phase: Saturation % 216.67/31.61 % (1628481)Time elapsed: 11.309 s % 216.67/31.61 % (1628481)Peak memory usage: 219 MB % 216.67/31.61 % (1628481)Instructions burned: 12111 (million) % 216.67/31.61 % (1628503)------------------------------ % 216.67/31.61 % (1628503)------------------------------ % 216.67/31.61 % (1628505)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3970986355:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2808 on theBenchmark for (2808ds/440Mi) % 216.67/31.61 % (1628506)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=929928248:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2808 on theBenchmark for (2808ds/11145Mi) % 216.67/31.61 % (1628509)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=3621506206:cts=off:i=3034:av=off:er=known:fsd=on_2806 on theBenchmark for (2806ds/3034Mi) % 216.67/31.61 % (1628505)Instruction limit reached! % 216.67/31.61 % (1628505)------------------------------ % 216.67/31.61 % (1628505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.67/31.61 % (1628505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.67/31.61 % (1628505)CaDiCaL version: 2.1.3 % 216.67/31.61 % (1628505)Termination reason: Instruction limit % 216.67/31.61 % (1628505)Termination phase: Saturation % 216.67/31.61 % (1628505)Time elapsed: 0.348 s % 216.67/31.61 % (1628505)Peak memory usage: 91 MB % 216.67/31.61 % (1628505)Instructions burned: 440 (million) % 216.67/31.61 % (1628513)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2136662233:st=2:s2a=on:i=524:s2at=2:ss=axioms_2802 on theBenchmark for (2802ds/524Mi) % 216.67/31.61 % (1628513)Instruction limit reached! % 216.67/31.61 % (1628513)------------------------------ % 216.67/31.61 % (1628513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.67/31.61 % (1628513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.67/31.61 % (1628513)CaDiCaL version: 2.1.3 % 216.67/31.61 % (1628513)Termination reason: Instruction limit % 216.67/31.61 % (1628513)Termination phase: Saturation % 216.67/31.61 % (1628513)Time elapsed: 0.453 s % 216.67/31.61 % (1628513)Peak memory usage: 93 MB % 216.67/31.61 % (1628513)Instructions burned: 524 (million) % 216.67/31.61 % (1628515)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1820849275:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2795 on theBenchmark for (2795ds/1016Mi) % 244.04/35.50 % (1628515)Instruction limit reached! % 244.04/35.50 % (1628515)------------------------------ % 244.04/35.50 % (1628515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.04/35.50 % (1628515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.04/35.50 % (1628515)CaDiCaL version: 2.1.3 % 244.04/35.50 % (1628515)Termination reason: Instruction limit % 244.04/35.50 % (1628515)Termination phase: Saturation % 244.04/35.50 % (1628515)Time elapsed: 0.820 s % 244.04/35.50 % (1628515)Peak memory usage: 93 MB % 244.04/35.50 % (1628515)Instructions burned: 1017 (million) % 244.04/35.50 % (1628517)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1090379631:i=14123:bd=preordered:ins=4_2784 on theBenchmark for (2784ds/14123Mi) % 244.04/35.50 % (1628509)Instruction limit reached! % 244.04/35.50 % (1628509)------------------------------ % 244.04/35.50 % (1628509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.04/35.50 % (1628509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.04/35.50 % (1628509)CaDiCaL version: 2.1.3 % 244.04/35.50 % (1628509)Termination reason: Instruction limit % 244.04/35.50 % (1628509)Termination phase: Saturation % 244.04/35.50 % (1628509)Time elapsed: 2.964 s % 244.04/35.50 % (1628509)Peak memory usage: 154 MB % 244.04/35.50 % (1628509)Instructions burned: 3035 (million) % 244.04/35.50 % (1628519)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2600669059:i=5781:kws=precedence:bd=all:rawr=on_2774 on theBenchmark for (2774ds/5781Mi) % 244.04/35.50 % (1628497)Instruction limit reached! % 244.04/35.50 % (1628497)------------------------------ % 244.04/35.50 % (1628497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.04/35.50 % (1628497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.04/35.50 % (1628497)CaDiCaL version: 2.1.3 % 244.04/35.50 % (1628497)Termination reason: Instruction limit % 244.04/35.50 % (1628497)Termination phase: Saturation % 244.04/35.50 % (1628497)Time elapsed: 8.844 s % 244.04/35.50 % (1628497)Peak memory usage: 174 MB % 244.04/35.50 % (1628497)Instructions burned: 9925 (million) % 244.04/35.50 % (1628525)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=2811614426:i=2448:gtgl=5:bd=preordered:gtg=all_2756 on theBenchmark for (2756ds/2448Mi) % 244.04/35.50 % (1628506)Instruction limit reached! % 244.04/35.50 % (1628506)------------------------------ % 244.04/35.50 % (1628506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.04/35.50 % (1628506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.04/35.50 % (1628506)CaDiCaL version: 2.1.3 % 244.04/35.50 % (1628506)Termination reason: Instruction limit % 244.04/35.50 % (1628506)Termination phase: Saturation % 244.04/35.50 % (1628506)Time elapsed: 5.865 s % 244.04/35.50 % (1628506)Peak memory usage: 208 MB % 244.04/35.50 % (1628506)Instructions burned: 11145 (million) % 244.04/35.50 % (1628527)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=135336025:i=3223:kws=precedence:fgj=on:av=off_2747 on theBenchmark for (2747ds/3223Mi) % 244.04/35.50 % (1628525)Instruction limit reached! % 244.04/35.50 % (1628525)------------------------------ % 244.04/35.50 % (1628525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.04/35.50 % (1628525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.04/35.50 % (1628525)CaDiCaL version: 2.1.3 % 244.04/35.50 % (1628525)Termination reason: Instruction limit % 244.04/35.50 % (1628525)Termination phase: Saturation % 244.04/35.50 % (1628525)Time elapsed: 2.387 s % 244.04/35.50 % (1628525)Peak memory usage: 147 MB % 244.04/35.50 % (1628525)Instructions burned: 2449 (million) % 244.04/35.50 % (1628527)Instruction limit reached! % 244.04/35.50 % (1628527)------------------------------ % 244.04/35.50 % (1628527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 244.04/35.50 % (1628527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 244.04/35.50 % (1628527)CaDiCaL version: 2.1.3 % 244.04/35.50 % (1628527)Termination reason: Instruction limit % 244.04/35.50 % (1628527)Termination phase: Saturation % 244.04/35.50 % (1628527)Time elapsed: 1.680 s % 244.04/35.50 % (1628527)Peak memory usage: 152 MB % 244.04/35.50 % (1628527)Instructions burned: 3225 (million) % 282.79/40.98 % (1628533)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=12899318:st=5.6:i=2033:sd=3:ss=axioms_2729 on theBenchmark for (2729ds/2033Mi) % 282.79/40.98 % (1628534)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=838370423:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2728 on theBenchmark for (2728ds/2055Mi) % 282.79/40.98 % (1628519)Instruction limit reached! % 282.79/40.98 % (1628519)------------------------------ % 282.79/40.98 % (1628519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.79/40.98 % (1628519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.79/40.98 % (1628519)CaDiCaL version: 2.1.3 % 282.79/40.98 % (1628519)Termination reason: Instruction limit % 282.79/40.98 % (1628519)Termination phase: Saturation % 282.79/40.98 % (1628519)Time elapsed: 4.523 s % 282.79/40.98 % (1628519)Peak memory usage: 103 MB % 282.79/40.98 % (1628519)Instructions burned: 5783 (million) % 282.79/40.98 % (1628537)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=3023713225:i=21611:sd=3:ss=axioms_2727 on theBenchmark for (2727ds/21611Mi) % 282.79/40.98 % (1628534)Instruction limit reached! % 282.79/40.98 % (1628534)------------------------------ % 282.79/40.98 % (1628534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.79/40.98 % (1628534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.79/40.98 % (1628534)CaDiCaL version: 2.1.3 % 282.79/40.98 % (1628534)Termination reason: Instruction limit % 282.79/40.98 % (1628534)Termination phase: Saturation % 282.79/40.98 % (1628534)Time elapsed: 0.699 s % 282.79/40.98 % (1628534)Peak memory usage: 139 MB % 282.79/40.98 % (1628534)Instructions burned: 2058 (million) % 282.79/40.98 % (1628692)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1275854490:i=4835:sd=13:ss=axioms:sgt=23_2720 on theBenchmark for (2720ds/4835Mi) % 282.79/40.98 % (1628533)Instruction limit reached! % 282.79/40.98 % (1628533)------------------------------ % 282.79/40.98 % (1628533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.79/40.98 % (1628533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.79/40.98 % (1628533)CaDiCaL version: 2.1.3 % 282.79/40.98 % (1628533)Termination reason: Instruction limit % 282.79/40.98 % (1628533)Termination phase: Saturation % 282.79/40.98 % (1628533)Time elapsed: 1.233 s % 282.79/40.98 % (1628533)Peak memory usage: 148 MB % 282.79/40.98 % (1628533)Instructions burned: 2033 (million) % 282.79/40.98 % (1628694)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=1985307282:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2715 on theBenchmark for (2715ds/797Mi) % 282.79/40.98 % (1628694)Instruction limit reached! % 282.79/40.98 % (1628694)------------------------------ % 282.79/40.98 % (1628694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.79/40.98 % (1628694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.79/40.98 % (1628694)CaDiCaL version: 2.1.3 % 282.79/40.98 % (1628694)Termination reason: Instruction limit % 282.79/40.98 % (1628694)Termination phase: Saturation % 282.79/40.98 % (1628694)Time elapsed: 0.413 s % 282.79/40.98 % (1628694)Peak memory usage: 95 MB % 282.79/40.98 % (1628694)Instructions burned: 797 (million) % 282.79/40.98 % (1628696)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3894039594:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2709 on theBenchmark for (2709ds/2326Mi) % 282.79/40.98 % (1628696)Instruction limit reached! % 282.79/40.98 % (1628696)------------------------------ % 282.79/40.98 % (1628696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.79/40.98 % (1628696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.79/40.98 % (1628696)CaDiCaL version: 2.1.3 % 282.79/40.98 % (1628696)Termination reason: Instruction limit % 282.79/40.98 % (1628696)Termination phase: Saturation % 282.79/40.98 % (1628696)Time elapsed: 1.216 s % 282.79/40.98 % (1628696)Peak memory usage: 101 MB % 282.79/40.98 % (1628696)Instructions burned: 2327 (million) % 282.79/40.98 % (1628692)Instruction limit reached! % 282.79/40.98 % (1628692)------------------------------ % 282.79/40.98 % (1628692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.79/40.98 % (1628692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.44 % (1628692)CaDiCaL version: 2.1.3 % 300.58/43.44 % (1628692)Termination reason: Instruction limit % 300.58/43.44 % (1628692)Termination phase: Saturation % 300.58/43.44 % (1628692)Time elapsed: 2.429 s % 300.58/43.44 % (1628692)Peak memory usage: 106 MB % 300.58/43.44 % (1628692)Instructions burned: 4836 (million) % 300.58/43.44 % (1628698)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1243744261:i=6038:nm=6_2695 on theBenchmark for (2695ds/6038Mi) % 300.58/43.44 % (1628699)lrs+10_1_sil=32000:sp=occurrence:random_seed=4229753215:st=2:i=33334:sd=3:ss=included:sgt=32_2694 on theBenchmark for (2694ds/33334Mi) % 300.58/43.44 % (1628517)Instruction limit reached! % 300.58/43.44 % (1628517)------------------------------ % 300.58/43.44 % (1628517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.44 % (1628517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.44 % (1628517)CaDiCaL version: 2.1.3 % 300.58/43.44 % (1628517)Termination reason: Instruction limit % 300.58/43.44 % (1628517)Termination phase: Saturation % 300.58/43.44 % (1628517)Time elapsed: 10.150 s % 300.58/43.44 % (1628517)Peak memory usage: 212 MB % 300.58/43.44 % (1628517)Instructions burned: 14123 (million) % 300.58/43.44 % (1628702)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1895835652:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2679 on theBenchmark for (2679ds/1008Mi) % 300.58/43.44 % (1628702)Instruction limit reached! % 300.58/43.44 % (1628702)------------------------------ % 300.58/43.44 % (1628702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.44 % (1628702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.44 % (1628702)CaDiCaL version: 2.1.3 % 300.58/43.44 % (1628702)Termination reason: Instruction limit % 300.58/43.44 % (1628702)Termination phase: Saturation % 300.58/43.44 % (1628702)Time elapsed: 0.573 s % 300.58/43.44 % (1628702)Peak memory usage: 97 MB % 300.58/43.44 % (1628702)Instructions burned: 1008 (million) % 300.58/43.44 % (1628704)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=2346749013:i=8327:s2at=5:bd=preordered_2672 on theBenchmark for (2672ds/8327Mi) % 300.58/43.44 % (1628698)Instruction limit reached! % 300.58/43.44 % (1628698)------------------------------ % 300.58/43.44 % (1628698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.44 % (1628698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.44 % (1628698)CaDiCaL version: 2.1.3 % 300.58/43.44 % (1628698)Termination reason: Instruction limit % 300.58/43.44 % (1628698)Termination phase: Saturation % 300.58/43.44 % (1628698)Time elapsed: 3.112 s % 300.58/43.44 % (1628698)Peak memory usage: 150 MB % 300.58/43.44 % (1628698)Instructions burned: 6040 (million) % 300.58/43.44 % (1628706)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=1089934144:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2662 on theBenchmark for (2662ds/1083Mi) % 300.58/43.44 % (1628537)Instruction limit reached! % 300.58/43.44 % (1628537)------------------------------ % 300.58/43.44 % (1628537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.44 % (1628537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.44 % (1628537)CaDiCaL version: 2.1.3 % 300.58/43.44 % (1628537)Termination reason: Instruction limit % 300.58/43.44 % (1628537)Termination phase: Saturation % 300.58/43.44 % (1628537)Time elapsed: 6.719 s % 300.58/43.44 % (1628537)Peak memory usage: 259 MB % 300.58/43.44 % (1628537)Instructions burned: 21613 (million) % 300.58/43.44 % (1628708)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2037337917:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2658 on theBenchmark for (2658ds/1084Mi) % 300.58/43.44 % (1628706)Instruction limit reached! % 300.58/43.44 % (1628706)------------------------------ % 300.58/43.44 % (1628706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.58/43.44 % (1628706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.58/43.44 % (1628706)CaDiCaL version: 2.1.3 % 300.58/43.44 % (1628706)Termination reason: Instruction limit % 300.58/43.44 % (1628706)Termination phase: Saturation % 300.58/43.44 % (1628706)Time elapsed: 0.439 s % 300.58/43.44 % (1628706)Peak memory usage: 94 MB % 300.58/43.44 % (1628706)Instructions burned: 1083 (million) % 300.58/43.44 % % 300.58/43.44 Terminated %------------------------------------------------------------------------------