%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NLP073+1 : TPTP v9.3.1. Released v2.4.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 12:07:15 PM UTC 2026 % Result : Timeout 290.98s 42.19s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP073+1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.37 % Computer : n019.cluster.edu % 0.08/0.37 % Model : x86_64 x86_64 % 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.37 % Memory : 8046.5625MB % 0.08/0.37 % OS : Linux 6.8.0-71-generic % 0.08/0.37 % CPULimit : 300 % 0.08/0.37 % WCLimit : 300 % 0.08/0.37 % DateTime : Sun Sep 27 17:57:19 UTC 2026 % 0.08/0.37 % CPUTime : % 0.08/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.41 Running first-order theorem proving % 0.08/0.41 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 % 9.76/2.29 % (3305703)Detected formulas, will run a generic FOF schedule. % 9.76/2.29 % (3305711)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4198330072:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 9.76/2.29 % (3305711)Refutation not found, incomplete strategy % 9.76/2.29 % (3305711)------------------------------ % 9.76/2.29 % (3305711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.29 % (3305711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.29 % (3305711)CaDiCaL version: 2.1.3 % 9.76/2.29 % (3305711)Termination reason: Refutation not found, incomplete strategy % 9.76/2.29 % (3305711)Time elapsed: 0.0000 s % 9.76/2.29 % (3305711)Peak memory usage: 86 MB % 9.76/2.29 % (3305713)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3243559837:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 9.76/2.29 % (3305712)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=660546250:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 9.76/2.29 % (3305714)dis-21_1_sil=8000:lcm=predicate:random_seed=3622420561: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) % 9.76/2.29 % (3305708)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=2437318582:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 9.76/2.29 % (3305709)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=2676820374:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 9.76/2.29 % (3305710)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=3906011441:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 9.76/2.29 % (3305712)Instruction limit reached! % 9.76/2.29 % (3305712)------------------------------ % 9.76/2.29 % (3305712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.29 % (3305712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.29 % (3305712)CaDiCaL version: 2.1.3 % 9.76/2.29 % (3305712)Termination reason: Instruction limit % 9.76/2.29 % (3305712)Termination phase: Saturation % 9.76/2.29 % (3305712)Time elapsed: 0.049 s % 9.76/2.29 % (3305712)Peak memory usage: 88 MB % 9.76/2.29 % (3305712)Instructions burned: 121 (million) % 9.76/2.29 % (3305714)Instruction limit reached! % 9.76/2.29 % (3305714)------------------------------ % 9.76/2.29 % (3305714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.29 % (3305714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.29 % (3305714)CaDiCaL version: 2.1.3 % 9.76/2.29 % (3305714)Termination reason: Instruction limit % 9.76/2.29 % (3305714)Termination phase: Saturation % 9.76/2.29 % (3305714)Time elapsed: 0.060 s % 9.76/2.29 % (3305714)Peak memory usage: 88 MB % 9.76/2.29 % (3305714)Instructions burned: 130 (million) % 9.76/2.29 % (3305713)Instruction limit reached! % 9.76/2.29 % (3305713)------------------------------ % 9.76/2.29 % (3305713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.76/2.29 % (3305713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.76/2.29 % (3305713)CaDiCaL version: 2.1.3 % 9.76/2.29 % (3305713)Termination reason: Instruction limit % 9.76/2.29 % (3305713)Termination phase: Saturation % 9.76/2.29 % (3305713)Time elapsed: 0.066 s % 9.76/2.29 % (3305713)Peak memory usage: 89 MB % 9.76/2.29 % (3305713)Instructions burned: 141 (million) % 9.76/2.29 % (3305711)------------------------------ % 9.76/2.29 % (3305711)------------------------------ % 9.76/2.29 % (3305722)lrs+10_1_sil=8000:sp=occurrence:random_seed=2976016577:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 9.76/2.29 % (3305724)lrs+1011_1_sil=32000:sp=occurrence:random_seed=926906314:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 9.76/2.29 % (3305723)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1486577712:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 9.76/2.29 % (3305725)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=758140996:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 15.89/3.08 % (3305724)Refutation not found, incomplete strategy % 15.89/3.08 % (3305724)------------------------------ % 15.89/3.08 % (3305724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.08 % (3305724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.08 % (3305724)CaDiCaL version: 2.1.3 % 15.89/3.08 % (3305724)Termination reason: Refutation not found, incomplete strategy % 15.89/3.08 % (3305724)Time elapsed: 0.005 s % 15.89/3.08 % (3305724)Peak memory usage: 88 MB % 15.89/3.08 % (3305724)Instructions burned: 6 (million) % 15.89/3.08 % (3305725)Instruction limit reached! % 15.89/3.08 % (3305725)------------------------------ % 15.89/3.08 % (3305725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.08 % (3305725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.08 % (3305725)CaDiCaL version: 2.1.3 % 15.89/3.08 % (3305725)Termination reason: Instruction limit % 15.89/3.08 % (3305725)Termination phase: Saturation % 15.89/3.08 % (3305725)Time elapsed: 0.057 s % 15.89/3.08 % (3305725)Peak memory usage: 89 MB % 15.89/3.08 % (3305725)Instructions burned: 248 (million) % 15.89/3.08 % (3305723)Instruction limit reached! % 15.89/3.08 % (3305723)------------------------------ % 15.89/3.08 % (3305723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.08 % (3305723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.08 % (3305723)CaDiCaL version: 2.1.3 % 15.89/3.08 % (3305723)Termination reason: Instruction limit % 15.89/3.08 % (3305723)Termination phase: Saturation % 15.89/3.08 % (3305723)Time elapsed: 0.070 s % 15.89/3.08 % (3305723)Peak memory usage: 90 MB % 15.89/3.08 % (3305723)Instructions burned: 158 (million) % 15.89/3.08 % (3305722)Instruction limit reached! % 15.89/3.08 % (3305722)------------------------------ % 15.89/3.08 % (3305722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.08 % (3305722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.08 % (3305722)CaDiCaL version: 2.1.3 % 15.89/3.08 % (3305722)Termination reason: Instruction limit % 15.89/3.08 % (3305722)Termination phase: Saturation % 15.89/3.08 % (3305722)Time elapsed: 0.127 s % 15.89/3.08 % (3305722)Peak memory usage: 90 MB % 15.89/3.08 % (3305722)Instructions burned: 287 (million) % 15.89/3.08 % (3305730)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1074210613:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 15.89/3.08 % (3305730)Refutation not found, incomplete strategy % 15.89/3.08 % (3305730)------------------------------ % 15.89/3.08 % (3305730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.08 % (3305730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.08 % (3305730)CaDiCaL version: 2.1.3 % 15.89/3.08 % (3305730)Termination reason: Refutation not found, incomplete strategy % 15.89/3.08 % (3305730)Time elapsed: 0.008 s % 15.89/3.08 % (3305730)Peak memory usage: 88 MB % 15.89/3.08 % (3305730)Instructions burned: 27 (million) % 15.89/3.08 % (3305731)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1002804140:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 15.89/3.08 % (3305724)------------------------------ % 15.89/3.08 % (3305724)------------------------------ % 15.89/3.08 % (3305732)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1298012292:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 15.89/3.08 % (3305730)------------------------------ % 15.89/3.08 % (3305730)------------------------------ % 15.89/3.08 % (3305732)Instruction limit reached! % 15.89/3.08 % (3305732)------------------------------ % 15.89/3.08 % (3305732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.89/3.08 % (3305732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.89/3.08 % (3305732)CaDiCaL version: 2.1.3 % 15.89/3.08 % (3305732)Termination reason: Instruction limit % 15.89/3.08 % (3305732)Termination phase: Saturation % 15.89/3.08 % (3305732)Time elapsed: 0.057 s % 15.89/3.08 % (3305732)Peak memory usage: 89 MB % 15.89/3.08 % (3305732)Instructions burned: 114 (million) % 15.89/3.08 % (3305735)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=59436179:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 15.89/3.08 % (3305737)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=885284439:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi) % 15.89/3.08 % (3305737)Refutation not found, incomplete strategy % 25.94/4.50 % (3305737)------------------------------ % 25.94/4.50 % (3305737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.94/4.50 % (3305737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.50 % (3305737)CaDiCaL version: 2.1.3 % 25.94/4.50 % (3305737)Termination reason: Refutation not found, incomplete strategy % 25.94/4.50 % (3305737)Time elapsed: 0.0000 s % 25.94/4.50 % (3305737)Peak memory usage: 87 MB % 25.94/4.50 % (3305738)lrs+10_1_sil=8000:sp=occurrence:random_seed=4063644736:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 25.94/4.50 % (3305735)Instruction limit reached! % 25.94/4.50 % (3305735)------------------------------ % 25.94/4.50 % (3305735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.94/4.50 % (3305735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.50 % (3305735)CaDiCaL version: 2.1.3 % 25.94/4.50 % (3305735)Termination reason: Instruction limit % 25.94/4.50 % (3305735)Termination phase: Saturation % 25.94/4.50 % (3305735)Time elapsed: 0.059 s % 25.94/4.50 % (3305735)Peak memory usage: 88 MB % 25.94/4.50 % (3305735)Instructions burned: 128 (million) % 25.94/4.50 % (3305737)------------------------------ % 25.94/4.50 % (3305737)------------------------------ % 25.94/4.50 % (3305742)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3351417579:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi) % 25.94/4.50 % (3305742)Refutation not found, incomplete strategy % 25.94/4.50 % (3305742)------------------------------ % 25.94/4.50 % (3305742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.94/4.50 % (3305742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.50 % (3305742)CaDiCaL version: 2.1.3 % 25.94/4.50 % (3305742)Termination reason: Refutation not found, incomplete strategy % 25.94/4.50 % (3305742)Time elapsed: 0.003 s % 25.94/4.50 % (3305742)Peak memory usage: 88 MB % 25.94/4.50 % (3305742)Instructions burned: 3 (million) % 25.94/4.50 % (3305743)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3320689600:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi) % 25.94/4.50 % (3305742)------------------------------ % 25.94/4.50 % (3305742)------------------------------ % 25.94/4.50 % (3305738)Instruction limit reached! % 25.94/4.50 % (3305738)------------------------------ % 25.94/4.50 % (3305738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.94/4.50 % (3305738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.50 % (3305738)CaDiCaL version: 2.1.3 % 25.94/4.50 % (3305738)Termination reason: Instruction limit % 25.94/4.50 % (3305738)Termination phase: Saturation % 25.94/4.50 % (3305738)Time elapsed: 0.385 s % 25.94/4.50 % (3305738)Peak memory usage: 95 MB % 25.94/4.50 % (3305738)Instructions burned: 909 (million) % 25.94/4.50 % (3305746)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=563812410:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 25.94/4.50 % (3305747)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3164423400:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 25.94/4.50 % (3305747)Refutation not found, incomplete strategy % 25.94/4.50 % (3305747)------------------------------ % 25.94/4.50 % (3305747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.94/4.50 % (3305747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.50 % (3305747)CaDiCaL version: 2.1.3 % 25.94/4.50 % (3305747)Termination reason: Refutation not found, incomplete strategy % 25.94/4.50 % (3305747)Time elapsed: 0.003 s % 25.94/4.50 % (3305747)Peak memory usage: 88 MB % 25.94/4.50 % (3305747)Instructions burned: 4 (million) % 25.94/4.50 % (3305746)Instruction limit reached! % 25.94/4.50 % (3305746)------------------------------ % 25.94/4.50 % (3305746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.94/4.50 % (3305746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.94/4.50 % (3305746)CaDiCaL version: 2.1.3 % 25.94/4.50 % (3305746)Termination reason: Instruction limit % 25.94/4.50 % (3305746)Termination phase: Saturation % 25.94/4.50 % (3305746)Time elapsed: 0.060 s % 25.94/4.50 % (3305746)Peak memory usage: 89 MB % 25.94/4.50 % (3305746)Instructions burned: 135 (million) % 25.94/4.50 % (3305750)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=443575513:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 53.25/8.34 % (3305747)------------------------------ % 53.25/8.34 % (3305747)------------------------------ % 53.25/8.34 % (3305752)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=2599678837:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi) % 53.25/8.34 % (3305752)Instruction limit reached! % 53.25/8.34 % (3305752)------------------------------ % 53.25/8.34 % (3305752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.34 % (3305752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.34 % (3305752)CaDiCaL version: 2.1.3 % 53.25/8.34 % (3305752)Termination reason: Instruction limit % 53.25/8.34 % (3305752)Termination phase: Saturation % 53.25/8.34 % (3305752)Time elapsed: 0.061 s % 53.25/8.34 % (3305752)Peak memory usage: 89 MB % 53.25/8.34 % (3305752)Instructions burned: 125 (million) % 53.25/8.34 % (3305754)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2801573425:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi) % 53.25/8.34 % (3305754)Instruction limit reached! % 53.25/8.34 % (3305754)------------------------------ % 53.25/8.34 % (3305754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.34 % (3305754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.34 % (3305754)CaDiCaL version: 2.1.3 % 53.25/8.34 % (3305754)Termination reason: Instruction limit % 53.25/8.34 % (3305754)Termination phase: Saturation % 53.25/8.34 % (3305754)Time elapsed: 0.061 s % 53.25/8.34 % (3305754)Peak memory usage: 89 MB % 53.25/8.34 % (3305754)Instructions burned: 135 (million) % 53.25/8.34 % (3305731)Instruction limit reached! % 53.25/8.34 % (3305731)------------------------------ % 53.25/8.34 % (3305731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.34 % (3305731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.34 % (3305731)CaDiCaL version: 2.1.3 % 53.25/8.34 % (3305731)Termination reason: Instruction limit % 53.25/8.34 % (3305731)Termination phase: Saturation % 53.25/8.34 % (3305731)Time elapsed: 1.456 s % 53.25/8.34 % (3305731)Peak memory usage: 137 MB % 53.25/8.34 % (3305731)Instructions burned: 2351 (million) % 53.25/8.34 % (3305756)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=954575078:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 53.25/8.34 % (3305756)Refutation not found, incomplete strategy % 53.25/8.34 % (3305756)------------------------------ % 53.25/8.34 % (3305756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.34 % (3305756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.34 % (3305756)CaDiCaL version: 2.1.3 % 53.25/8.34 % (3305756)Termination reason: Refutation not found, incomplete strategy % 53.25/8.34 % (3305756)Time elapsed: 0.002 s % 53.25/8.34 % (3305756)Peak memory usage: 88 MB % 53.25/8.34 % (3305756)Instructions burned: 1 (million) % 53.25/8.34 % (3305757)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=869034763:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi) % 53.25/8.34 % (3305757)Refutation not found, incomplete strategy % 53.25/8.34 % (3305757)------------------------------ % 53.25/8.34 % (3305757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.34 % (3305757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.34 % (3305757)CaDiCaL version: 2.1.3 % 53.25/8.34 % (3305757)Termination reason: Refutation not found, incomplete strategy % 53.25/8.34 % (3305757)Time elapsed: 0.002 s % 53.25/8.34 % (3305757)Peak memory usage: 88 MB % 53.25/8.34 % (3305757)Instructions burned: 2 (million) % 53.25/8.34 % (3305743)Instruction limit reached! % 53.25/8.34 % (3305743)------------------------------ % 53.25/8.34 % (3305743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.25/8.34 % (3305743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.25/8.34 % (3305743)CaDiCaL version: 2.1.3 % 53.25/8.34 % (3305743)Termination reason: Instruction limit % 53.25/8.34 % (3305743)Termination phase: Saturation % 53.25/8.34 % (3305743)Time elapsed: 1.182 s % 53.25/8.34 % (3305743)Peak memory usage: 133 MB % 53.25/8.34 % (3305743)Instructions burned: 5206 (million) % 53.25/8.34 % (3305760)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=843236190:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi) % 77.82/11.88 % (3305756)------------------------------ % 77.82/11.88 % (3305756)------------------------------ % 77.82/11.88 % (3305757)------------------------------ % 77.82/11.88 % (3305757)------------------------------ % 77.82/11.88 % (3305762)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=493722685:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi) % 77.82/11.88 % (3305762)Instruction limit reached! % 77.82/11.88 % (3305762)------------------------------ % 77.82/11.88 % (3305762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.82/11.88 % (3305762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.82/11.88 % (3305762)CaDiCaL version: 2.1.3 % 77.82/11.88 % (3305762)Termination reason: Instruction limit % 77.82/11.88 % (3305762)Termination phase: Saturation % 77.82/11.88 % (3305762)Time elapsed: 0.071 s % 77.82/11.88 % (3305762)Peak memory usage: 89 MB % 77.82/11.88 % (3305762)Instructions burned: 152 (million) % 77.82/11.88 % (3305763)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2472455110:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi) % 77.82/11.88 % (3305765)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=529917818:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi) % 77.82/11.88 % (3305765)Refutation not found, incomplete strategy % 77.82/11.88 % (3305765)------------------------------ % 77.82/11.88 % (3305765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.82/11.88 % (3305765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.82/11.88 % (3305765)CaDiCaL version: 2.1.3 % 77.82/11.88 % (3305765)Termination reason: Refutation not found, incomplete strategy % 77.82/11.88 % (3305765)Time elapsed: 0.025 s % 77.82/11.88 % (3305765)Peak memory usage: 88 MB % 77.82/11.88 % (3305765)Instructions burned: 68 (million) % 77.82/11.88 % (3305765)------------------------------ % 77.82/11.88 % (3305765)------------------------------ % 77.82/11.88 % (3305768)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=1192771014:s2a=on:i=185:s2at=1.8:fdi=4_2971 on theBenchmark for (2971ds/185Mi) % 77.82/11.88 % (3305768)Instruction limit reached! % 77.82/11.88 % (3305768)------------------------------ % 77.82/11.88 % (3305768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.82/11.88 % (3305768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.82/11.88 % (3305768)CaDiCaL version: 2.1.3 % 77.82/11.88 % (3305768)Termination reason: Instruction limit % 77.82/11.88 % (3305768)Termination phase: Saturation % 77.82/11.88 % (3305768)Time elapsed: 0.084 s % 77.82/11.88 % (3305768)Peak memory usage: 89 MB % 77.82/11.88 % (3305768)Instructions burned: 187 (million) % 77.82/11.88 % (3305770)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3127216619:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2969 on theBenchmark for (2969ds/193Mi) % 77.82/11.88 % (3305770)Instruction limit reached! % 77.82/11.88 % (3305770)------------------------------ % 77.82/11.88 % (3305770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.82/11.88 % (3305770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.82/11.88 % (3305770)CaDiCaL version: 2.1.3 % 77.82/11.88 % (3305770)Termination reason: Instruction limit % 77.82/11.88 % (3305770)Termination phase: Saturation % 77.82/11.88 % (3305770)Time elapsed: 0.095 s % 77.82/11.88 % (3305770)Peak memory usage: 90 MB % 77.82/11.88 % (3305770)Instructions burned: 195 (million) % 77.82/11.88 % (3305772)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4183019191:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2966 on theBenchmark for (2966ds/4850Mi) % 77.82/11.88 % (3305760)Instruction limit reached! % 77.82/11.88 % (3305760)------------------------------ % 77.82/11.88 % (3305760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.82/11.88 % (3305760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.82/11.88 % (3305760)CaDiCaL version: 2.1.3 % 77.82/11.88 % (3305760)Termination reason: Instruction limit % 77.82/11.88 % (3305760)Termination phase: Saturation % 96.37/14.42 % (3305760)Time elapsed: 1.426 s % 96.37/14.42 % (3305760)Peak memory usage: 135 MB % 96.37/14.42 % (3305760)Instructions burned: 6063 (million) % 96.37/14.42 % (3305772)Refutation not found, incomplete strategy % 96.37/14.42 % (3305772)------------------------------ % 96.37/14.42 % (3305772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (3305772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (3305772)CaDiCaL version: 2.1.3 % 96.37/14.42 % (3305772)Termination reason: Refutation not found, incomplete strategy % 96.37/14.42 % (3305772)Time elapsed: 0.278 s % 96.37/14.42 % (3305772)Peak memory usage: 92 MB % 96.37/14.42 % (3305772)Instructions burned: 560 (million) % 96.37/14.42 % (3305774)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1894093201:i=12111:sd=1:ss=included_2963 on theBenchmark for (2963ds/12111Mi) % 96.37/14.42 % (3305772)------------------------------ % 96.37/14.42 % (3305772)------------------------------ % 96.37/14.42 % (3305776)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2218212021:i=319:kws=precedence:fsr=off_2960 on theBenchmark for (2960ds/319Mi) % 96.37/14.42 % (3305776)Instruction limit reached! % 96.37/14.42 % (3305776)------------------------------ % 96.37/14.42 % (3305776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (3305776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (3305776)CaDiCaL version: 2.1.3 % 96.37/14.42 % (3305776)Termination reason: Instruction limit % 96.37/14.42 % (3305776)Termination phase: Saturation % 96.37/14.42 % (3305776)Time elapsed: 0.149 s % 96.37/14.42 % (3305776)Peak memory usage: 91 MB % 96.37/14.42 % (3305776)Instructions burned: 320 (million) % 96.37/14.42 % (3305778)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1640206201:i=2064:ep=RST_2957 on theBenchmark for (2957ds/2064Mi) % 96.37/14.42 % (3305778)Instruction limit reached! % 96.37/14.42 % (3305778)------------------------------ % 96.37/14.42 % (3305778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (3305778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (3305778)CaDiCaL version: 2.1.3 % 96.37/14.42 % (3305778)Termination reason: Instruction limit % 96.37/14.42 % (3305778)Termination phase: Saturation % 96.37/14.42 % (3305778)Time elapsed: 0.981 s % 96.37/14.42 % (3305778)Peak memory usage: 105 MB % 96.37/14.42 % (3305778)Instructions burned: 2066 (million) % 96.37/14.42 % (3305780)dis-1011_128_sil=32000:random_seed=3853346846:i=3706:ep=RST:av=off_2946 on theBenchmark for (2946ds/3706Mi) % 96.37/14.42 % (3305780)Instruction limit reached! % 96.37/14.42 % (3305780)------------------------------ % 96.37/14.42 % (3305780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (3305780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (3305780)CaDiCaL version: 2.1.3 % 96.37/14.42 % (3305780)Termination reason: Instruction limit % 96.37/14.42 % (3305780)Termination phase: Saturation % 96.37/14.42 % (3305780)Time elapsed: 1.502 s % 96.37/14.42 % (3305780)Peak memory usage: 92 MB % 96.37/14.42 % (3305780)Instructions burned: 3706 (million) % 96.37/14.42 % (3305782)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4273670841:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2930 on theBenchmark for (2930ds/757Mi) % 96.37/14.42 % (3305774)Instruction limit reached! % 96.37/14.42 % (3305774)------------------------------ % 96.37/14.42 % (3305774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (3305774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (3305774)CaDiCaL version: 2.1.3 % 96.37/14.42 % (3305774)Termination reason: Instruction limit % 96.37/14.42 % (3305774)Termination phase: Saturation % 96.37/14.42 % (3305774)Time elapsed: 3.727 s % 96.37/14.42 % (3305774)Peak memory usage: 190 MB % 96.37/14.42 % (3305774)Instructions burned: 12114 (million) % 96.37/14.42 % (3305782)Instruction limit reached! % 96.37/14.42 % (3305782)------------------------------ % 96.37/14.42 % (3305782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.37/14.42 % (3305782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.37/14.42 % (3305782)CaDiCaL version: 2.1.3 % 96.37/14.42 % (3305782)Termination reason: Instruction limit % 96.37/14.42 % (3305782)Termination phase: Saturation % 96.37/14.42 % (3305782)Time elapsed: 0.398 s % 96.37/14.42 % (3305782)Peak memory usage: 96 MB % 108.10/16.07 % (3305782)Instructions burned: 759 (million) % 108.10/16.07 % (3305784)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2958597683:i=13913:ss=axioms:sgt=8_2925 on theBenchmark for (2925ds/13913Mi) % 108.10/16.07 % (3305785)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1156381175:i=9925:aac=none_2925 on theBenchmark for (2925ds/9925Mi) % 108.10/16.07 % (3305750)Instruction limit reached! % 108.10/16.07 % (3305750)------------------------------ % 108.10/16.07 % (3305750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.10/16.07 % (3305750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.10/16.07 % (3305750)CaDiCaL version: 2.1.3 % 108.10/16.07 % (3305750)Termination reason: Instruction limit % 108.10/16.07 % (3305750)Termination phase: Saturation % 108.10/16.07 % (3305750)Time elapsed: 6.618 s % 108.10/16.07 % (3305750)Peak memory usage: 185 MB % 108.10/16.07 % (3305750)Instructions burned: 13194 (million) % 108.10/16.07 % (3305788)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4249882150:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2919 on theBenchmark for (2919ds/2479Mi) % 108.10/16.07 % (3305788)Refutation not found, incomplete strategy % 108.10/16.07 % (3305788)------------------------------ % 108.10/16.07 % (3305788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.10/16.07 % (3305788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.10/16.07 % (3305788)CaDiCaL version: 2.1.3 % 108.10/16.07 % (3305788)Termination reason: Refutation not found, incomplete strategy % 108.10/16.07 % (3305788)Time elapsed: 0.002 s % 108.10/16.07 % (3305788)Peak memory usage: 88 MB % 108.10/16.07 % (3305788)Instructions burned: 2 (million) % 108.10/16.07 % (3305788)------------------------------ % 108.10/16.07 % (3305788)------------------------------ % 108.10/16.07 % (3305790)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2277312023:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2915 on theBenchmark for (2915ds/440Mi) % 108.10/16.07 % (3305790)Instruction limit reached! % 108.10/16.07 % (3305790)------------------------------ % 108.10/16.07 % (3305790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.10/16.07 % (3305790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.10/16.07 % (3305790)CaDiCaL version: 2.1.3 % 108.10/16.07 % (3305790)Termination reason: Instruction limit % 108.10/16.07 % (3305790)Termination phase: Saturation % 108.10/16.07 % (3305790)Time elapsed: 0.186 s % 108.10/16.07 % (3305790)Peak memory usage: 88 MB % 108.10/16.07 % (3305790)Instructions burned: 440 (million) % 108.10/16.07 % (3305792)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=816656909:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2912 on theBenchmark for (2912ds/11145Mi) % 108.10/16.07 % (3305763)Instruction limit reached! % 108.10/16.07 % (3305763)------------------------------ % 108.10/16.07 % (3305763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.10/16.07 % (3305763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.10/16.07 % (3305763)CaDiCaL version: 2.1.3 % 108.10/16.07 % (3305763)Termination reason: Instruction limit % 108.10/16.07 % (3305763)Termination phase: Saturation % 108.10/16.07 % (3305763)Time elapsed: 6.489 s % 108.10/16.07 % (3305763)Peak memory usage: 205 MB % 108.10/16.07 % (3305763)Instructions burned: 14157 (million) % 108.10/16.07 % (3305794)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=3673593215:cts=off:i=3034:av=off:er=known:fsd=on_2909 on theBenchmark for (2909ds/3034Mi) % 108.10/16.07 % (3305794)Instruction limit reached! % 108.10/16.07 % (3305794)------------------------------ % 108.10/16.07 % (3305794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.10/16.07 % (3305794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.10/16.07 % (3305794)CaDiCaL version: 2.1.3 % 108.10/16.07 % (3305794)Termination reason: Instruction limit % 108.10/16.07 % (3305794)Termination phase: Saturation % 108.10/16.07 % (3305794)Time elapsed: 1.547 s % 108.10/16.07 % (3305794)Peak memory usage: 138 MB % 108.10/16.07 % (3305794)Instructions burned: 3034 (million) % 108.10/16.07 % (3305796)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2513099648:st=2:s2a=on:i=524:s2at=2:ss=axioms_2893 on theBenchmark for (2893ds/524Mi) % 108.10/16.07 % (3305796)Instruction limit reached! % 108.10/16.07 % (3305796)------------------------------ % 130.99/19.35 % (3305796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.99/19.35 % (3305796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.99/19.35 % (3305796)CaDiCaL version: 2.1.3 % 130.99/19.35 % (3305796)Termination reason: Instruction limit % 130.99/19.35 % (3305796)Termination phase: Saturation % 130.99/19.35 % (3305796)Time elapsed: 0.225 s % 130.99/19.35 % (3305796)Peak memory usage: 91 MB % 130.99/19.35 % (3305796)Instructions burned: 525 (million) % 130.99/19.35 % (3305798)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2263186057:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2889 on theBenchmark for (2889ds/1016Mi) % 130.99/19.35 % (3305798)Refutation not found, incomplete strategy % 130.99/19.35 % (3305798)------------------------------ % 130.99/19.35 % (3305798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.99/19.35 % (3305798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.99/19.35 % (3305798)CaDiCaL version: 2.1.3 % 130.99/19.35 % (3305798)Termination reason: Refutation not found, incomplete strategy % 130.99/19.35 % (3305798)Time elapsed: 0.001 s % 130.99/19.35 % (3305798)Peak memory usage: 87 MB % 130.99/19.35 % (3305784)Instruction limit reached! % 130.99/19.35 % (3305784)------------------------------ % 130.99/19.35 % (3305784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.99/19.35 % (3305784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.99/19.35 % (3305784)CaDiCaL version: 2.1.3 % 130.99/19.35 % (3305784)Termination reason: Instruction limit % 130.99/19.35 % (3305784)Termination phase: Saturation % 130.99/19.35 % (3305784)Time elapsed: 3.731 s % 130.99/19.35 % (3305784)Peak memory usage: 186 MB % 130.99/19.35 % (3305784)Instructions burned: 13914 (million) % 130.99/19.35 % (3305800)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2467833394:i=14123:bd=preordered:ins=4_2886 on theBenchmark for (2886ds/14123Mi) % 130.99/19.35 % (3305798)------------------------------ % 130.99/19.35 % (3305798)------------------------------ % 130.99/19.35 % (3305802)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=117765039:i=5781:kws=precedence:bd=all:rawr=on_2885 on theBenchmark for (2885ds/5781Mi) % 130.99/19.35 % (3305785)Instruction limit reached! % 130.99/19.35 % (3305785)------------------------------ % 130.99/19.35 % (3305785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.99/19.35 % (3305785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.99/19.35 % (3305785)CaDiCaL version: 2.1.3 % 130.99/19.35 % (3305785)Termination reason: Instruction limit % 130.99/19.35 % (3305785)Termination phase: Saturation % 130.99/19.35 % (3305785)Time elapsed: 4.700 s % 130.99/19.35 % (3305785)Peak memory usage: 153 MB % 130.99/19.35 % (3305785)Instructions burned: 9927 (million) % 130.99/19.35 % (3305804)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=3729935189:i=2448:gtgl=5:bd=preordered:gtg=all_2876 on theBenchmark for (2876ds/2448Mi) % 130.99/19.35 % (3305804)Refutation not found, incomplete strategy % 130.99/19.35 % (3305804)------------------------------ % 130.99/19.35 % (3305804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.99/19.35 % (3305804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.99/19.36 % (3305804)CaDiCaL version: 2.1.3 % 130.99/19.36 % (3305804)Termination reason: Refutation not found, incomplete strategy % 130.99/19.36 % (3305804)Time elapsed: 0.877 s % 130.99/19.36 % (3305804)Peak memory usage: 135 MB % 130.99/19.36 % (3305804)Instructions burned: 1493 (million) % 130.99/19.36 % (3305792)Instruction limit reached! % 130.99/19.36 % (3305792)------------------------------ % 130.99/19.36 % (3305792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.99/19.36 % (3305792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 130.99/19.36 % (3305792)CaDiCaL version: 2.1.3 % 130.99/19.36 % (3305792)Termination reason: Instruction limit % 130.99/19.36 % (3305792)Termination phase: Saturation % 130.99/19.36 % (3305792)Time elapsed: 4.495 s % 130.99/19.36 % (3305792)Peak memory usage: 141 MB % 130.99/19.36 % (3305792)Instructions burned: 11147 (million) % 130.99/19.36 % (3305806)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=646769416:i=3223:kws=precedence:fgj=on:av=off_2866 on theBenchmark for (2866ds/3223Mi) % 130.99/19.36 % (3305804)------------------------------ % 144.58/21.29 % (3305804)------------------------------ % 144.58/21.29 % (3305808)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=895320007:st=5.6:i=2033:sd=3:ss=axioms_2864 on theBenchmark for (2864ds/2033Mi) % 144.58/21.29 % (3305802)Instruction limit reached! % 144.58/21.29 % (3305802)------------------------------ % 144.58/21.29 % (3305802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.58/21.29 % (3305802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.58/21.29 % (3305802)CaDiCaL version: 2.1.3 % 144.58/21.29 % (3305802)Termination reason: Instruction limit % 144.58/21.29 % (3305802)Termination phase: Saturation % 144.58/21.29 % (3305802)Time elapsed: 2.391 s % 144.58/21.29 % (3305802)Peak memory usage: 103 MB % 144.58/21.29 % (3305802)Instructions burned: 5782 (million) % 144.58/21.29 % (3305810)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4085135169:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2860 on theBenchmark for (2860ds/2055Mi) % 144.58/21.29 % (3305800)Instruction limit reached! % 144.58/21.29 % (3305800)------------------------------ % 144.58/21.29 % (3305800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.58/21.29 % (3305800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.58/21.29 % (3305800)CaDiCaL version: 2.1.3 % 144.58/21.29 % (3305800)Termination reason: Instruction limit % 144.58/21.29 % (3305800)Termination phase: Saturation % 144.58/21.29 % (3305800)Time elapsed: 2.812 s % 144.58/21.29 % (3305800)Peak memory usage: 135 MB % 144.58/21.29 % (3305800)Instructions burned: 14126 (million) % 144.58/21.29 % (3305812)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=3038925756:i=21611:sd=3:ss=axioms_2857 on theBenchmark for (2857ds/21611Mi) % 144.58/21.29 % (3305808)Refutation not found, incomplete strategy % 144.58/21.29 % (3305808)------------------------------ % 144.58/21.29 % (3305808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.58/21.29 % (3305808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.58/21.29 % (3305808)CaDiCaL version: 2.1.3 % 144.58/21.29 % (3305808)Termination reason: Refutation not found, incomplete strategy % 144.58/21.29 % (3305808)Time elapsed: 0.665 s % 144.58/21.29 % (3305808)Peak memory usage: 128 MB % 144.58/21.29 % (3305808)Instructions burned: 1025 (million) % 144.58/21.29 % (3305808)------------------------------ % 144.58/21.29 % (3305808)------------------------------ % 144.58/21.29 % (3305814)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2172119967:i=4835:sd=13:ss=axioms:sgt=23_2853 on theBenchmark for (2853ds/4835Mi) % 144.58/21.29 % (3305810)Instruction limit reached! % 144.58/21.29 % (3305810)------------------------------ % 144.58/21.29 % (3305810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.58/21.29 % (3305810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.58/21.29 % (3305810)CaDiCaL version: 2.1.3 % 144.58/21.29 % (3305810)Termination reason: Instruction limit % 144.58/21.29 % (3305810)Termination phase: Saturation % 144.58/21.29 % (3305810)Time elapsed: 1.033 s % 144.58/21.29 % (3305810)Peak memory usage: 130 MB % 144.58/21.29 % (3305810)Instructions burned: 2056 (million) % 144.58/21.29 % (3305806)Instruction limit reached! % 144.58/21.29 % (3305806)------------------------------ % 144.58/21.29 % (3305806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.58/21.29 % (3305806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.58/21.29 % (3305806)CaDiCaL version: 2.1.3 % 144.58/21.29 % (3305806)Termination reason: Instruction limit % 144.58/21.29 % (3305806)Termination phase: Saturation % 144.58/21.29 % (3305806)Time elapsed: 1.686 s % 144.58/21.29 % (3305806)Peak memory usage: 137 MB % 144.58/21.29 % (3305806)Instructions burned: 3225 (million) % 144.58/21.29 % (3305816)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=831271087:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2849 on theBenchmark for (2849ds/797Mi) % 144.58/21.29 % (3305816)Refutation not found, incomplete strategy % 144.58/21.29 % (3305816)------------------------------ % 144.58/21.29 % (3305816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 144.58/21.29 % (3305816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 144.58/21.29 % (3305816)CaDiCaL version: 2.1.3 % 144.58/21.29 % (3305816)Termination reason: Refutation not found, incomplete strategy % 153.07/22.46 % (3305816)Time elapsed: 0.005 s % 153.07/22.46 % (3305816)Peak memory usage: 88 MB % 153.07/22.46 % (3305816)Instructions burned: 8 (million) % 153.07/22.46 % (3305817)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3210229161:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2847 on theBenchmark for (2847ds/2326Mi) % 153.07/22.46 % (3305817)Refutation not found, incomplete strategy % 153.07/22.46 % (3305817)------------------------------ % 153.07/22.46 % (3305817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.07/22.46 % (3305817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.07/22.46 % (3305817)CaDiCaL version: 2.1.3 % 153.07/22.46 % (3305817)Termination reason: Refutation not found, incomplete strategy % 153.07/22.46 % (3305817)Time elapsed: 0.007 s % 153.07/22.46 % (3305817)Peak memory usage: 88 MB % 153.07/22.46 % (3305817)Instructions burned: 10 (million) % 153.07/22.46 % (3305816)------------------------------ % 153.07/22.46 % (3305816)------------------------------ % 153.07/22.46 % (3305817)------------------------------ % 153.07/22.46 % (3305817)------------------------------ % 153.07/22.46 % (3305820)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=794140654:i=6038:nm=6_2845 on theBenchmark for (2845ds/6038Mi) % 153.07/22.46 % (3305821)lrs+10_1_sil=32000:sp=occurrence:random_seed=928370066:st=2:i=33334:sd=3:ss=included:sgt=32_2844 on theBenchmark for (2844ds/33334Mi) % 153.07/22.46 % (3305814)Instruction limit reached! % 153.07/22.46 % (3305814)------------------------------ % 153.07/22.46 % (3305814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.07/22.46 % (3305814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.07/22.46 % (3305814)CaDiCaL version: 2.1.3 % 153.07/22.46 % (3305814)Termination reason: Instruction limit % 153.07/22.46 % (3305814)Termination phase: Saturation % 153.07/22.46 % (3305814)Time elapsed: 2.017 s % 153.07/22.46 % (3305814)Peak memory usage: 106 MB % 153.07/22.46 % (3305814)Instructions burned: 4835 (million) % 153.07/22.46 % (3305824)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3020768401:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2832 on theBenchmark for (2832ds/1008Mi) % 153.07/22.46 % (3305824)Refutation not found, incomplete strategy % 153.07/22.46 % (3305824)------------------------------ % 153.07/22.46 % (3305824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.07/22.46 % (3305824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.07/22.46 % (3305824)CaDiCaL version: 2.1.3 % 153.07/22.46 % (3305824)Termination reason: Refutation not found, incomplete strategy % 153.07/22.46 % (3305824)Time elapsed: 0.230 s % 153.07/22.46 % (3305824)Peak memory usage: 91 MB % 153.07/22.46 % (3305824)Instructions burned: 537 (million) % 153.07/22.46 % (3305824)------------------------------ % 153.07/22.46 % (3305824)------------------------------ % 153.07/22.46 % (3305826)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=826228190:i=8327:s2at=5:bd=preordered_2826 on theBenchmark for (2826ds/8327Mi) % 153.07/22.46 % (3305812)Instruction limit reached! % 153.07/22.46 % (3305812)------------------------------ % 153.07/22.46 % (3305812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.07/22.46 % (3305812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.07/22.46 % (3305812)CaDiCaL version: 2.1.3 % 153.07/22.46 % (3305812)Termination reason: Instruction limit % 153.07/22.46 % (3305812)Termination phase: Saturation % 153.07/22.46 % (3305812)Time elapsed: 3.874 s % 153.07/22.46 % (3305812)Peak memory usage: 142 MB % 153.07/22.46 % (3305812)Instructions burned: 21618 (million) % 153.07/22.46 % (3305828)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=61195793:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2818 on theBenchmark for (2818ds/1083Mi) % 153.07/22.46 % (3305828)Instruction limit reached! % 153.07/22.46 % (3305828)------------------------------ % 153.07/22.46 % (3305828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.07/22.46 % (3305828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.07/22.46 % (3305828)CaDiCaL version: 2.1.3 % 153.07/22.46 % (3305828)Termination reason: Instruction limit % 166.76/24.34 % (3305828)Termination phase: Saturation % 166.76/24.34 % (3305828)Time elapsed: 0.255 s % 166.76/24.34 % (3305828)Peak memory usage: 98 MB % 166.76/24.34 % (3305828)Instructions burned: 1088 (million) % 166.76/24.34 % (3305830)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=288227325:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2814 on theBenchmark for (2814ds/1084Mi) % 166.76/24.34 % (3305830)Refutation not found, incomplete strategy % 166.76/24.34 % (3305830)------------------------------ % 166.76/24.34 % (3305830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.76/24.34 % (3305830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.76/24.34 % (3305830)CaDiCaL version: 2.1.3 % 166.76/24.34 % (3305830)Termination reason: Refutation not found, incomplete strategy % 166.76/24.34 % (3305830)Time elapsed: 0.002 s % 166.76/24.34 % (3305830)Peak memory usage: 88 MB % 166.76/24.34 % (3305830)Instructions burned: 5 (million) % 166.76/24.34 % (3305820)Instruction limit reached! % 166.76/24.34 % (3305820)------------------------------ % 166.76/24.34 % (3305820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.76/24.34 % (3305820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.76/24.34 % (3305820)CaDiCaL version: 2.1.3 % 166.76/24.34 % (3305820)Termination reason: Instruction limit % 166.76/24.34 % (3305820)Termination phase: Saturation % 166.76/24.34 % (3305820)Time elapsed: 3.028 s % 166.76/24.34 % (3305820)Peak memory usage: 175 MB % 166.76/24.34 % (3305820)Instructions burned: 6039 (million) % 166.76/24.34 % (3305830)------------------------------ % 166.76/24.34 % (3305830)------------------------------ % 166.76/24.34 % (3305832)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1883989124:i=6995:s2at=5:gtg=all_2813 on theBenchmark for (2813ds/6995Mi) % 166.76/24.34 % (3305833)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1644429656:st=2:i=6225:sd=15:ss=axioms_2812 on theBenchmark for (2812ds/6225Mi) % 166.76/24.34 % (3305833)Instruction limit reached! % 166.76/24.34 % (3305833)------------------------------ % 166.76/24.34 % (3305833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.76/24.34 % (3305833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.76/24.34 % (3305833)CaDiCaL version: 2.1.3 % 166.76/24.34 % (3305833)Termination reason: Instruction limit % 166.76/24.34 % (3305833)Termination phase: Saturation % 166.76/24.34 % (3305833)Time elapsed: 1.328 s % 166.76/24.34 % (3305833)Peak memory usage: 115 MB % 166.76/24.34 % (3305833)Instructions burned: 6228 (million) % 166.76/24.34 % (3305836)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2230289037:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2798 on theBenchmark for (2798ds/3372Mi) % 166.76/24.34 [W927 17:57:40.435867921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.76/24.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.76/24.34 [W927 17:57:40.435909153 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.76/24.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.76/24.34 [W927 17:57:40.435929407 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.76/24.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.76/24.34 [W927 17:57:40.435935433 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.76/24.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.76/24.34 [W927 17:57:40.435948712 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 166.76/24.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.435955267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.435981559 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.435986869 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.435999345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.436011123 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.436024626 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 [W927 17:57:40.436030175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.67/29.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.67/29.50 % (3305836)Refutation not found, incomplete strategy % 203.67/29.50 % (3305836)------------------------------ % 203.67/29.50 % (3305836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.67/29.50 % (3305836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.67/29.50 % (3305836)CaDiCaL version: 2.1.3 % 203.67/29.50 % (3305836)Termination reason: Refutation not found, incomplete strategy % 203.67/29.50 % (3305836)Time elapsed: 0.291 s % 203.67/29.50 % (3305836)Peak memory usage: 126 MB % 203.67/29.50 % (3305836)Instructions burned: 822 (million) % 203.67/29.50 % (3305836)------------------------------ % 203.67/29.50 % (3305836)------------------------------ % 203.67/29.50 % (3305838)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3164634014:st=2.3:i=26457:sd=10:ss=included:sgt=8_2793 on theBenchmark for (2793ds/26457Mi) % 203.67/29.50 % (3305832)Instruction limit reached! % 203.67/29.50 % (3305832)------------------------------ % 203.67/29.50 % (3305832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.67/29.50 % (3305832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.67/29.50 % (3305832)CaDiCaL version: 2.1.3 % 203.67/29.50 % (3305832)Termination reason: Instruction limit % 203.67/29.50 % (3305832)Termination phase: Saturation % 203.67/29.50 % (3305832)Time elapsed: 2.555 s % 203.67/29.50 % (3305832)Peak memory usage: 131 MB % 203.67/29.50 % (3305832)Instructions burned: 6998 (million) % 203.67/29.50 % (3305840)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=3314385796:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2786 on theBenchmark for (2786ds/13494Mi) % 203.67/29.50 % (3305826)Instruction limit reached! % 203.67/29.50 % (3305826)------------------------------ % 203.67/29.50 % (3305826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.67/29.50 % (3305826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.67/29.50 % (3305826)CaDiCaL version: 2.1.3 % 216.39/31.31 % (3305826)Termination reason: Instruction limit % 216.39/31.31 % (3305826)Termination phase: Saturation % 216.39/31.31 % (3305826)Time elapsed: 4.116 s % 216.39/31.31 % (3305826)Peak memory usage: 154 MB % 216.39/31.31 % (3305826)Instructions burned: 8328 (million) % 216.39/31.31 % (3305842)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=815489456:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2783 on theBenchmark for (2783ds/2503Mi) % 216.39/31.31 % (3305842)Instruction limit reached! % 216.39/31.31 % (3305842)------------------------------ % 216.39/31.31 % (3305842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.39/31.31 % (3305842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.39/31.31 % (3305842)CaDiCaL version: 2.1.3 % 216.39/31.31 % (3305842)Termination reason: Instruction limit % 216.39/31.31 % (3305842)Termination phase: Saturation % 216.39/31.31 % (3305842)Time elapsed: 1.247 s % 216.39/31.31 % (3305842)Peak memory usage: 130 MB % 216.39/31.31 % (3305842)Instructions burned: 2505 (million) % 216.39/31.31 % (3305844)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=128629443:i=2559:sd=1:ep=RSTC:ss=axioms_2769 on theBenchmark for (2769ds/2559Mi) % 216.39/31.31 [W927 17:57:43.478189734 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478221711 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478260151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478273198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478298604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478310201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478336818 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478348068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478373761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.39/31.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.39/31.31 [W927 17:57:43.478385261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.73/33.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.73/33.01 [W927 17:57:43.478410618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.73/33.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.73/33.01 [W927 17:57:43.478420994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 225.73/33.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 225.73/33.01 % (3305844)Refutation not found, incomplete strategy % 225.73/33.01 % (3305844)------------------------------ % 225.73/33.01 % (3305844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.73/33.01 % (3305844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.73/33.01 % (3305844)CaDiCaL version: 2.1.3 % 225.73/33.01 % (3305844)Termination reason: Refutation not found, incomplete strategy % 225.73/33.01 % (3305844)Time elapsed: 0.535 s % 225.73/33.01 % (3305844)Peak memory usage: 125 MB % 225.73/33.01 % (3305844)Instructions burned: 823 (million) % 225.73/33.01 % (3305844)------------------------------ % 225.73/33.01 % (3305844)------------------------------ % 225.73/33.01 % (3305846)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2923821446:i=30753:av=off:ss=included_2760 on theBenchmark for (2760ds/30753Mi) % 225.73/33.01 % (3305838)Instruction limit reached! % 225.73/33.01 % (3305838)------------------------------ % 225.73/33.01 % (3305838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.73/33.01 % (3305838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.73/33.01 % (3305838)CaDiCaL version: 2.1.3 % 225.73/33.01 % (3305838)Termination reason: Instruction limit % 225.73/33.01 % (3305838)Termination phase: Saturation % 225.73/33.01 % (3305838)Time elapsed: 5.482 s % 225.73/33.01 % (3305838)Peak memory usage: 134 MB % 225.73/33.01 % (3305838)Instructions burned: 26459 (million) % 225.73/33.01 % (3305848)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2181044495:i=26473:ep=RSTC_2737 on theBenchmark for (2737ds/26473Mi) % 225.73/33.01 % (3305848)Refutation not found, incomplete strategy % 225.73/33.01 % (3305848)------------------------------ % 225.73/33.01 % (3305848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.73/33.01 % (3305848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.73/33.01 % (3305848)CaDiCaL version: 2.1.3 % 225.73/33.01 % (3305848)Termination reason: Refutation not found, incomplete strategy % 225.73/33.01 % (3305848)Time elapsed: 0.599 s % 225.73/33.01 % (3305848)Peak memory usage: 120 MB % 225.73/33.01 % (3305848)Instructions burned: 2281 (million) % 225.73/33.01 % (3305848)------------------------------ % 225.73/33.01 % (3305848)------------------------------ % 225.73/33.01 % (3305850)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=1027528892:cts=off:i=2759:kws=inv_arity:fgj=on_2729 on theBenchmark for (2729ds/2759Mi) % 225.73/33.01 % (3305850)Refutation not found, incomplete strategy % 225.73/33.01 % (3305850)------------------------------ % 225.73/33.01 % (3305850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.73/33.01 % (3305850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.73/33.01 % (3305850)CaDiCaL version: 2.1.3 % 225.73/33.01 % (3305850)Termination reason: Refutation not found, incomplete strategy % 225.73/33.01 % (3305850)Time elapsed: 0.323 s % 225.73/33.01 % (3305850)Peak memory usage: 128 MB % 225.73/33.01 % (3305850)Instructions burned: 907 (million) % 225.73/33.01 % (3305850)------------------------------ % 225.73/33.01 % (3305850)------------------------------ % 225.73/33.01 % (3305852)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=177676900:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2723 on theBenchmark for (2723ds/5665Mi) % 225.73/33.01 % (3305821)Instruction limit reached! % 225.73/33.01 % (3305821)------------------------------ % 225.73/33.01 % (3305821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.31/35.16 % (3305821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.31/35.16 % (3305821)CaDiCaL version: 2.1.3 % 241.31/35.16 % (3305821)Termination reason: Instruction limit % 241.31/35.16 % (3305821)Termination phase: Saturation % 241.31/35.16 % (3305821)Time elapsed: 12.953 s % 241.31/35.16 % (3305821)Peak memory usage: 165 MB % 241.31/35.16 % (3305821)Instructions burned: 33334 (million) % 241.31/35.16 % (3305854)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=1404062205:i=1532:ep=RS:ss=axioms_2713 on theBenchmark for (2713ds/1532Mi) % 241.31/35.16 % (3305854)Refutation not found, incomplete strategy % 241.31/35.16 % (3305854)------------------------------ % 241.31/35.16 % (3305854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.31/35.16 % (3305854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.31/35.16 % (3305854)CaDiCaL version: 2.1.3 % 241.31/35.16 % (3305854)Termination reason: Refutation not found, incomplete strategy % 241.31/35.16 % (3305854)Time elapsed: 0.707 s % 241.31/35.16 % (3305854)Peak memory usage: 131 MB % 241.31/35.16 % (3305854)Instructions burned: 1128 (million) % 241.31/35.16 % (3305840)Instruction limit reached! % 241.31/35.16 % (3305840)------------------------------ % 241.31/35.16 % (3305840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.31/35.16 % (3305840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.31/35.16 % (3305840)CaDiCaL version: 2.1.3 % 241.31/35.16 % (3305840)Termination reason: Instruction limit % 241.31/35.16 % (3305840)Termination phase: Saturation % 241.31/35.16 % (3305840)Time elapsed: 8.152 s % 241.31/35.16 % (3305840)Peak memory usage: 217 MB % 241.31/35.16 % (3305840)Instructions burned: 13496 (million) % 241.31/35.16 % (3305854)------------------------------ % 241.31/35.16 % (3305854)------------------------------ % 241.31/35.16 % (3305856)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=414406532:i=1565:sd=2:ss=axioms:sgt=32_2703 on theBenchmark for (2703ds/1565Mi) % 241.31/35.16 % (3305852)Instruction limit reached! % 241.31/35.16 % (3305852)------------------------------ % 241.31/35.16 % (3305852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.31/35.16 % (3305852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.31/35.16 % (3305852)CaDiCaL version: 2.1.3 % 241.31/35.16 % (3305852)Termination reason: Instruction limit % 241.31/35.16 % (3305852)Termination phase: Saturation % 241.31/35.16 % (3305852)Time elapsed: 2.051 s % 241.31/35.16 % (3305852)Peak memory usage: 166 MB % 241.31/35.16 % (3305852)Instructions burned: 5667 (million) % 241.31/35.16 % (3305859)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3331937579:i=6052:sd=4:ss=axioms:sgt=24_2702 on theBenchmark for (2702ds/6052Mi) % 241.31/35.16 % (3305857)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=1293321740:i=1572:fgj=on:gsp=on_2702 on theBenchmark for (2702ds/1572Mi) % 241.31/35.16 % (3305859)Refutation not found, incomplete strategy % 241.31/35.16 % (3305859)------------------------------ % 241.31/35.16 % (3305859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.31/35.16 % (3305859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.31/35.16 % (3305859)CaDiCaL version: 2.1.3 % 241.31/35.16 % (3305859)Termination reason: Refutation not found, incomplete strategy % 241.31/35.16 % (3305859)Time elapsed: 0.347 s % 241.31/35.16 % (3305859)Peak memory usage: 128 MB % 241.31/35.16 % (3305859)Instructions burned: 968 (million) % 241.31/35.16 % (3305859)------------------------------ % 241.31/35.16 % (3305859)------------------------------ % 241.31/35.16 % (3305856)Refutation not found, incomplete strategy % 241.31/35.16 % (3305856)------------------------------ % 241.31/35.16 % (3305856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 241.31/35.16 % (3305856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.31/35.16 % (3305856)CaDiCaL version: 2.1.3 % 241.31/35.16 % (3305856)Termination reason: Refutation not found, incomplete strategy % 241.31/35.16 % (3305856)Time elapsed: 0.615 s % 241.31/35.16 % (3305856)Peak memory usage: 128 MB % 241.31/35.16 % (3305856)Instructions burned: 922 (million) % 241.31/35.16 % (3305862)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=2854235814:i=3500:sd=1:bd=preordered:sup=off:ss=included_2696 on theBenchmark for (2696ds/3500Mi) % 255.87/37.23 % (3305856)------------------------------ % 255.87/37.23 % (3305856)------------------------------ % 255.87/37.23 % (3305864)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=2073573316:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2693 on theBenchmark for (2693ds/1842Mi) % 255.87/37.23 % (3305862)Refutation not found, incomplete strategy % 255.87/37.23 % (3305862)------------------------------ % 255.87/37.23 % (3305862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.87/37.23 % (3305862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.87/37.23 % (3305862)CaDiCaL version: 2.1.3 % 255.87/37.23 % (3305862)Termination reason: Refutation not found, incomplete strategy % 255.87/37.23 % (3305862)Time elapsed: 0.373 s % 255.87/37.23 % (3305862)Peak memory usage: 128 MB % 255.87/37.23 % (3305862)Instructions burned: 914 (million) % 255.87/37.23 % (3305857)Instruction limit reached! % 255.87/37.23 % (3305857)------------------------------ % 255.87/37.23 % (3305857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.87/37.23 % (3305857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.87/37.23 % (3305857)CaDiCaL version: 2.1.3 % 255.87/37.23 % (3305857)Termination reason: Instruction limit % 255.87/37.23 % (3305857)Termination phase: Saturation % 255.87/37.23 % (3305857)Time elapsed: 0.999 s % 255.87/37.23 % (3305857)Peak memory usage: 132 MB % 255.87/37.23 % (3305857)Instructions burned: 1573 (million) % 255.87/37.23 % (3305866)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=357935728:i=66096:add=on_2691 on theBenchmark for (2691ds/66096Mi) % 255.87/37.23 % (3305862)------------------------------ % 255.87/37.23 % (3305862)------------------------------ % 255.87/37.23 % (3305868)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3377549694:i=1884:sd=1:nm=60:ss=axioms_2683 on theBenchmark for (2683ds/1884Mi) % 255.87/37.23 % (3305864)Refutation not found, incomplete strategy % 255.87/37.23 % (3305864)------------------------------ % 255.87/37.23 % (3305864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.87/37.23 % (3305864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.87/37.23 % (3305864)CaDiCaL version: 2.1.3 % 255.87/37.23 % (3305864)Termination reason: Refutation not found, incomplete strategy % 255.87/37.23 % (3305864)Time elapsed: 1.023 s % 255.87/37.23 % (3305864)Peak memory usage: 128 MB % 255.87/37.23 % (3305864)Instructions burned: 983 (million) % 255.87/37.23 % (3305864)------------------------------ % 255.87/37.23 % (3305864)------------------------------ % 255.87/37.23 % (3305870)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3360827815:cts=off:i=5469:bs=on:fsr=off_2680 on theBenchmark for (2680ds/5469Mi) % 255.87/37.23 [W927 17:57:52.148475970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.87/37.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.87/37.23 [W927 17:57:52.148516297 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.87/37.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.87/37.23 [W927 17:57:52.148554127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.87/37.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.87/37.23 [W927 17:57:52.148565391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 255.87/37.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 255.87/37.23 [W927 17:57:52.148590127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148600694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148626671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148637257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148662244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148672807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148697761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 [W927 17:57:52.148708087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.98/42.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.98/42.19 % (3305868)Refutation not found, incomplete strategy % 290.98/42.19 % (3305868)------------------------------ % 290.98/42.19 % (3305868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.98/42.19 % (3305868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/42.19 % (3305868)CaDiCaL version: 2.1.3 % 290.98/42.19 % (3305868)Termination reason: Refutation not found, incomplete strategy % 290.98/42.19 % (3305868)Time elapsed: 0.542 s % 290.98/42.19 % (3305868)Peak memory usage: 125 MB % 290.98/42.19 % (3305868)Instructions burned: 826 (million) % 290.98/42.19 % (3305868)------------------------------ % 290.98/42.19 % (3305868)------------------------------ % 290.98/42.19 % (3305872)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=1076456477:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2674 on theBenchmark for (2674ds/2037Mi) % 290.98/42.19 % (3305870)Instruction limit reached! % 290.98/42.19 % (3305870)------------------------------ % 290.98/42.19 % (3305870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.98/42.19 % (3305870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.98/42.19 % (3305870)CaDiCaL version: 2.1.3 % 290.98/42.19 % (3305870)Termination reason: Instruction limit % 290.98/42.19 % (3305870)Termination phase: Saturation % 290.98/42.19 % (3305870)Time elapsed: 1.686 s % 290.98/42.19 % (3305870)Peak memory usage: 97 MB % 290.98/42.19 % (3305870)Instructions burned: 8896 (million) % 290.98/42.19 % (3305874)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=253418150:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2662 on theBenchmark for (2662ds/2110Mi) % 290.98/42.19 % (3305874)Refutation not found, incomplete strategy % 290.98/42.19 % (3305874)------------------------------ % 293.37/42.59 % (3305874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.37/42.59 % (3305874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.37/42.59 % (3305874)CaDiCaL version: 2.1.3 % 293.37/42.59 % (3305874)Termination reason: Refutation not found, incomplete strategy % 293.37/42.59 % (3305874)Time elapsed: 0.515 s % 293.37/42.59 % (3305874)Peak memory usage: 135 MB % 293.37/42.59 % (3305874)Instructions burned: 1489 (million) % 293.37/42.59 % (3305874)------------------------------ % 293.37/42.59 % (3305874)------------------------------ % 293.37/42.59 % (3305872)Instruction limit reached! % 293.37/42.59 % (3305872)------------------------------ % 293.37/42.59 % (3305872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.37/42.59 % (3305872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.37/42.59 % (3305872)CaDiCaL version: 2.1.3 % 293.37/42.59 % (3305872)Termination reason: Instruction limit % 293.37/42.59 % (3305872)Termination phase: Saturation % 293.37/42.59 % (3305872)Time elapsed: 1.833 s % 293.37/42.59 % (3305872)Peak memory usage: 134 MB % 293.37/42.59 % (3305872)Instructions burned: 2037 (million) % 293.37/42.59 % (3305876)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=2974467484:i=2430:add=off:aac=none:nm=16_2655 on theBenchmark for (2655ds/2430Mi) % 293.37/42.59 % (3305878)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=3479582870:cond=fast:i=4891_2654 on theBenchmark for (2654ds/4891Mi) % 293.37/42.59 % (3305876)Instruction limit reached! % 293.37/42.59 % (3305876)------------------------------ % 293.37/42.59 % (3305876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.37/42.59 % (3305876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.37/42.59 % (3305876)CaDiCaL version: 2.1.3 % 293.37/42.59 % (3305876)Termination reason: Instruction limit % 293.37/42.59 % (3305876)Termination phase: Saturation % 293.37/42.59 % (3305876)Time elapsed: 0.623 s % 293.37/42.59 % (3305876)Peak memory usage: 130 MB % 293.37/42.59 % (3305876)Instructions burned: 2435 (million) % 293.37/42.59 % (3305880)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=203239603:st=2:i=14845:sd=2:ss=included:fsd=on_2648 on theBenchmark for (2648ds/14845Mi) % 293.37/42.59 % (3305880)Refutation not found, incomplete strategy % 293.37/42.59 % (3305880)------------------------------ % 293.37/42.59 % (3305880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.37/42.59 % (3305880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.37/42.59 % (3305880)CaDiCaL version: 2.1.3 % 293.37/42.59 % (3305880)Termination reason: Refutation not found, incomplete strategy % 293.37/42.59 % (3305880)Time elapsed: 0.633 s % 293.37/42.59 % (3305880)Peak memory usage: 129 MB % 293.37/42.59 % (3305880)Instructions burned: 948 (million) % 293.37/42.59 % (3305878)Instruction limit reached! % 293.37/42.59 % (3305878)------------------------------ % 293.37/42.59 % (3305878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.37/42.59 % (3305878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 293.37/42.59 % (3305878)CaDiCaL version: 2.1.3 % 293.37/42.59 % (3305878)Termination reason: Instruction limit % 293.37/42.59 % (3305878)Termination phase: Saturation % 293.37/42.59 % (3305878)Time elapsed: 1.279 s % 293.37/42.59 % (3305878)Peak memory usage: 132 MB % 293.37/42.59 % (3305878)Instructions burned: 4904 (million) % 293.37/42.59 % (3305883)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=831224650:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2640 on theBenchmark for (2640ds/7534Mi) % 293.37/42.59 % (3305880)------------------------------ % 293.37/42.59 % (3305880)------------------------------ % 293.37/42.59 % (3305885)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=2913099312:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2638 on theBenchmark for (2638ds/10353Mi) % 293.37/42.59 % (3305883)Refutation not found, incomplete strategy % 293.37/42.59 % (3305883)------------------------------ % 293.37/42.59 % (3305883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 293.37/42.59 % (3305883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.53 % (3305883)CaDiCaL version: 2.1.3 % 300.66/43.53 % (3305883)Termination reason: Refutation not found, incomplete strategy % 300.66/43.53 % (3305883)Time elapsed: 0.343 s % 300.66/43.53 % (3305883)Peak memory usage: 129 MB % 300.66/43.53 % (3305883)Instructions burned: 916 (million) % 300.66/43.53 % (3305883)------------------------------ % 300.66/43.53 % (3305883)------------------------------ % 300.66/43.53 % (3305887)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1717756198:i=7860_2634 on theBenchmark for (2634ds/7860Mi) % 300.66/43.53 % (3305887)Instruction limit reached! % 300.66/43.53 % (3305887)------------------------------ % 300.66/43.53 % (3305887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.53 % (3305887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.53 % (3305887)CaDiCaL version: 2.1.3 % 300.66/43.53 % (3305887)Termination reason: Instruction limit % 300.66/43.53 % (3305887)Termination phase: Saturation % 300.66/43.53 % (3305887)Time elapsed: 1.686 s % 300.66/43.53 % (3305887)Peak memory usage: 102 MB % 300.66/43.53 % (3305887)Instructions burned: 7861 (million) % 300.66/43.53 % (3305889)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=3921643261:i=7896:sd=2:bs=on:ss=included:sgt=20_2616 on theBenchmark for (2616ds/7896Mi) % 300.66/43.53 % (3305846)Instruction limit reached! % 300.66/43.53 % (3305846)------------------------------ % 300.66/43.53 % (3305846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.53 % (3305846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.53 % (3305846)CaDiCaL version: 2.1.3 % 300.66/43.53 % (3305846)Termination reason: Instruction limit % 300.66/43.53 % (3305846)Termination phase: Saturation % 300.66/43.53 % (3305846)Time elapsed: 15.804 s % 300.66/43.53 % (3305846)Peak memory usage: 273 MB % 300.66/43.53 % (3305846)Instructions burned: 30755 (million) % 300.66/43.53 % (3305891)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2584692272:i=5812:gtgl=2:gtg=all_2601 on theBenchmark for (2601ds/5812Mi) % 300.66/43.53 % (3305889)Instruction limit reached! % 300.66/43.53 % (3305889)------------------------------ % 300.66/43.53 % (3305889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.53 % (3305889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.53 % (3305889)CaDiCaL version: 2.1.3 % 300.66/43.53 % (3305889)Termination reason: Instruction limit % 300.66/43.53 % (3305889)Termination phase: Saturation % 300.66/43.53 % (3305889)Time elapsed: 2.388 s % 300.66/43.53 % (3305889)Peak memory usage: 156 MB % 300.66/43.53 % (3305889)Instructions burned: 7897 (million) % 300.66/43.53 % (3305893)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=2644375385:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2592 on theBenchmark for (2592ds/2965Mi) % 300.66/43.53 % (3305885)Instruction limit reached! % 300.66/43.53 % (3305885)------------------------------ % 300.66/43.53 % (3305885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.53 % (3305885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.53 % (3305885)CaDiCaL version: 2.1.3 % 300.66/43.53 % (3305885)Termination reason: Instruction limit % 300.66/43.53 % (3305885)Termination phase: Saturation % 300.66/43.53 % (3305885)Time elapsed: 4.601 s % 300.66/43.53 % (3305885)Peak memory usage: 137 MB % 300.66/43.53 % (3305885)Instructions burned: 10354 (million) % 300.66/43.53 % (3305895)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3319857694:i=2967:kws=precedence:bd=preordered:av=off_2590 on theBenchmark for (2590ds/2967Mi) % 300.66/43.53 % (3305893)Refutation not found, incomplete strategy % 300.66/43.53 % (3305893)------------------------------ % 300.66/43.53 % (3305893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.66/43.53 % (3305893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.66/43.53 % (3305893)CaDiCaL version: 2.1.3 % 300.66/43.53 % (3305893)Termination reason: Refutation not found, incomplete strategy % 300.66/43.53 % (3305893)Time elapsed: 0.331 s % 300.66/43.53 % (3305893)Peak memory usage: 128 MB % 300.66/43.53 % (3305893)Instructions burned: 905 (million) % 300.66/43.53 % (3305893)------------------------------ % 300.66/43.53 % (33058 % 300.66/43.54 Terminated %------------------------------------------------------------------------------