%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW470_20 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:30:24 PM UTC 2026 % Result : Timeout 289.16s 41.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW470_20 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.19 % Computer : n006.cluster.edu % 0.07/0.19 % Model : x86_64 x86_64 % 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.19 % Memory : 8046.5625MB % 0.07/0.19 % OS : Linux 6.8.0-71-generic % 0.07/0.19 % CPULimit : 300 % 0.07/0.19 % WCLimit : 300 % 0.07/0.19 % DateTime : Mon Sep 28 14:02:15 UTC 2026 % 0.07/0.19 % CPUTime : % 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.07/0.23 Running first-order theorem proving % 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.67/1.96 % (3978876)Detected formulas, will run a generic FOF schedule. % 7.67/1.96 % (3978883)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=2298113638:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 7.67/1.96 % (3978882)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=3586163873:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 7.67/1.96 % (3978886)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1281092500:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 7.67/1.96 % (3978887)dis-21_1_sil=8000:lcm=predicate:random_seed=2278368763: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) % 7.67/1.96 % (3978881)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=3542960784:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 7.67/1.96 % (3978885)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4196339112:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 7.67/1.96 % (3978884)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=812274133:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 7.67/1.96 % (3978885)Refutation not found, incomplete strategy % 7.67/1.96 % (3978885)------------------------------ % 7.67/1.96 % (3978885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.67/1.96 % (3978885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.67/1.96 % (3978885)CaDiCaL version: 2.1.3 % 7.67/1.96 % (3978885)Termination reason: Refutation not found, incomplete strategy % 7.67/1.96 % (3978885)Time elapsed: 0.003 s % 7.67/1.96 % (3978885)Peak memory usage: 87 MB % 7.67/1.96 % (3978885)Instructions burned: 4 (million) % 7.67/1.96 % (3978884)Refutation not found, incomplete strategy % 7.67/1.96 % (3978884)------------------------------ % 7.67/1.96 % (3978884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.67/1.96 % (3978884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.67/1.96 % (3978884)CaDiCaL version: 2.1.3 % 7.67/1.96 % (3978884)Termination reason: Refutation not found, incomplete strategy % 7.67/1.96 % (3978884)Time elapsed: 0.003 s % 7.67/1.96 % (3978884)Peak memory usage: 87 MB % 7.67/1.96 % (3978884)Instructions burned: 4 (million) % 7.67/1.96 % (3978887)Instruction limit reached! % 7.67/1.96 % (3978887)------------------------------ % 7.67/1.96 % (3978887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.67/1.96 % (3978887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.67/1.96 % (3978887)CaDiCaL version: 2.1.3 % 7.67/1.96 % (3978887)Termination reason: Instruction limit % 7.67/1.96 % (3978887)Termination phase: Saturation % 7.67/1.96 % (3978887)Time elapsed: 0.067 s % 7.67/1.96 % (3978887)Peak memory usage: 90 MB % 7.67/1.96 % (3978887)Instructions burned: 129 (million) % 7.67/1.96 % (3978886)Instruction limit reached! % 7.67/1.96 % (3978886)------------------------------ % 7.67/1.96 % (3978886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.67/1.96 % (3978886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.67/1.96 % (3978886)CaDiCaL version: 2.1.3 % 7.67/1.96 % (3978886)Termination reason: Instruction limit % 7.67/1.96 % (3978886)Termination phase: Saturation % 7.67/1.96 % (3978886)Time elapsed: 0.075 s % 7.67/1.96 % (3978886)Peak memory usage: 90 MB % 7.67/1.96 % (3978886)Instructions burned: 139 (million) % 7.67/1.96 % (3978895)lrs+10_1_sil=8000:sp=occurrence:random_seed=2404699593:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 7.67/1.96 % (3978896)lrs+10_1_sil=32000:urr=on:br=off:random_seed=429515415:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 7.67/1.96 % (3978895)Refutation not found, incomplete strategy % 7.67/1.96 % (3978895)------------------------------ % 7.67/1.96 % (3978895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.67/1.96 % (3978895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.67/1.96 % (3978895)CaDiCaL version: 2.1.3 % 7.67/1.96 % (3978895)Termination reason: Refutation not found, incomplete strategy % 10.76/2.24 % (3978895)Time elapsed: 0.003 s % 10.76/2.24 % (3978895)Peak memory usage: 87 MB % 10.76/2.24 % (3978895)Instructions burned: 4 (million) % 10.76/2.24 % (3978896)Refutation not found, incomplete strategy % 10.76/2.24 % (3978896)------------------------------ % 10.76/2.24 % (3978896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.24 % (3978896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.24 % (3978896)CaDiCaL version: 2.1.3 % 10.76/2.24 % (3978896)Termination reason: Refutation not found, incomplete strategy % 10.76/2.24 % (3978896)Time elapsed: 0.009 s % 10.76/2.24 % (3978896)Peak memory usage: 88 MB % 10.76/2.24 % (3978896)Instructions burned: 18 (million) % 10.76/2.24 % (3978884)------------------------------ % 10.76/2.24 % (3978884)------------------------------ % 10.76/2.24 % (3978885)------------------------------ % 10.76/2.24 % (3978885)------------------------------ % 10.76/2.24 % (3978883)Refutation not found, incomplete strategy % 10.76/2.24 % (3978883)------------------------------ % 10.76/2.24 % (3978883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.24 % (3978883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.24 % (3978883)CaDiCaL version: 2.1.3 % 10.76/2.24 % (3978883)Termination reason: Refutation not found, incomplete strategy % 10.76/2.24 % (3978883)Time elapsed: 0.398 s % 10.76/2.24 % (3978883)Peak memory usage: 136 MB % 10.76/2.24 % (3978883)Instructions burned: 1137 (million) % 10.76/2.24 % (3978899)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3524692786:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 10.76/2.24 % (3978900)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=2534705257:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.76/2.24 % (3978899)Refutation not found, incomplete strategy % 10.76/2.24 % (3978899)------------------------------ % 10.76/2.24 % (3978899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.24 % (3978899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.24 % (3978899)CaDiCaL version: 2.1.3 % 10.76/2.24 % (3978899)Termination reason: Refutation not found, incomplete strategy % 10.76/2.24 % (3978899)Time elapsed: 0.003 s % 10.76/2.24 % (3978899)Peak memory usage: 87 MB % 10.76/2.24 % (3978899)Instructions burned: 4 (million) % 10.76/2.24 % (3978896)------------------------------ % 10.76/2.24 % (3978896)------------------------------ % 10.76/2.24 % (3978895)------------------------------ % 10.76/2.24 % (3978895)------------------------------ % 10.76/2.24 % (3978883)------------------------------ % 10.76/2.24 % (3978883)------------------------------ % 10.76/2.24 % (3978900)Instruction limit reached! % 10.76/2.24 % (3978900)------------------------------ % 10.76/2.24 % (3978900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.24 % (3978900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.24 % (3978900)CaDiCaL version: 2.1.3 % 10.76/2.24 % (3978900)Termination reason: Instruction limit % 10.76/2.24 % (3978900)Termination phase: Saturation % 10.76/2.24 % (3978900)Time elapsed: 0.142 s % 10.76/2.24 % (3978900)Peak memory usage: 93 MB % 10.76/2.24 % (3978900)Instructions burned: 249 (million) % 10.76/2.24 % (3978904)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3755277877:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 10.76/2.24 % (3978905)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3341103893:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 10.76/2.24 % (3978903)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1024175555:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 10.76/2.24 % (3978903)Refutation not found, incomplete strategy % 10.76/2.24 % (3978903)------------------------------ % 10.76/2.24 % (3978903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.24 % (3978903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.24 % (3978903)CaDiCaL version: 2.1.3 % 10.76/2.24 % (3978903)Termination reason: Refutation not found, incomplete strategy % 10.76/2.24 % (3978903)Time elapsed: 0.004 s % 10.76/2.24 % (3978903)Peak memory usage: 87 MB % 10.76/2.24 % (3978903)Instructions burned: 6 (million) % 10.76/2.24 % (3978905)Instruction limit reached! % 10.76/2.24 % (3978905)------------------------------ % 10.76/2.24 % (3978905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.44 % (3978905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.44 % (3978905)CaDiCaL version: 2.1.3 % 11.88/2.44 % (3978905)Termination reason: Instruction limit % 11.88/2.44 % (3978905)Termination phase: Saturation % 11.88/2.44 % (3978905)Time elapsed: 0.031 s % 11.88/2.44 % (3978905)Peak memory usage: 90 MB % 11.88/2.44 % (3978905)Instructions burned: 113 (million) % 11.88/2.44 % (3978899)------------------------------ % 11.88/2.44 % (3978899)------------------------------ % 11.88/2.44 % (3978906)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3032563469:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 11.88/2.44 % (3978910)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1561505391:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi) % 11.88/2.44 % (3978906)Refutation not found, incomplete strategy % 11.88/2.44 % (3978906)------------------------------ % 11.88/2.44 % (3978906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.44 % (3978906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.44 % (3978906)CaDiCaL version: 2.1.3 % 11.88/2.44 % (3978906)Termination reason: Refutation not found, incomplete strategy % 11.88/2.44 % (3978906)Time elapsed: 0.045 s % 11.88/2.44 % (3978906)Peak memory usage: 89 MB % 11.88/2.44 % (3978906)Instructions burned: 94 (million) % 11.88/2.44 % (3978910)Instruction limit reached! % 11.88/2.44 % (3978910)------------------------------ % 11.88/2.44 % (3978910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.44 % (3978910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.44 % (3978910)CaDiCaL version: 2.1.3 % 11.88/2.44 % (3978910)Termination reason: Instruction limit % 11.88/2.44 % (3978910)Termination phase: Saturation % 11.88/2.44 % (3978910)Time elapsed: 0.030 s % 11.88/2.44 % (3978910)Peak memory usage: 90 MB % 11.88/2.44 % (3978910)Instructions burned: 115 (million) % 11.88/2.44 % (3978911)lrs+10_1_sil=8000:sp=occurrence:random_seed=4228457433:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 11.88/2.44 % (3978911)Refutation not found, incomplete strategy % 11.88/2.44 % (3978911)------------------------------ % 11.88/2.44 % (3978911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.44 % (3978911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.44 % (3978911)CaDiCaL version: 2.1.3 % 11.88/2.44 % (3978911)Termination reason: Refutation not found, incomplete strategy % 11.88/2.44 % (3978911)Time elapsed: 0.004 s % 11.88/2.44 % (3978911)Peak memory usage: 87 MB % 11.88/2.44 % (3978911)Instructions burned: 5 (million) % 11.88/2.44 % (3978914)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1200548828:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 11.88/2.44 % (3978903)------------------------------ % 11.88/2.44 % (3978903)------------------------------ % 11.88/2.44 % (3978914)Refutation not found, incomplete strategy % 11.88/2.44 % (3978914)------------------------------ % 11.88/2.44 % (3978914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.44 % (3978914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.44 % (3978914)CaDiCaL version: 2.1.3 % 11.88/2.44 % (3978914)Termination reason: Refutation not found, incomplete strategy % 11.88/2.44 % (3978914)Time elapsed: 0.032 s % 11.88/2.44 % (3978914)Peak memory usage: 91 MB % 11.88/2.44 % (3978914)Instructions burned: 113 (million) % 11.88/2.44 % (3978906)------------------------------ % 11.88/2.44 % (3978906)------------------------------ % 11.88/2.44 % (3978917)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3888840187:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 11.88/2.44 % (3978914)------------------------------ % 11.88/2.44 % (3978914)------------------------------ % 11.88/2.44 % (3978911)------------------------------ % 11.88/2.44 % (3978911)------------------------------ % 11.88/2.44 % (3978920)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1776897297:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 11.88/2.44 % (3978920)Refutation not found, incomplete strategy % 11.88/2.44 % (3978920)------------------------------ % 11.88/2.44 % (3978920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.44 % (3978920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.24/2.61 % (3978920)CaDiCaL version: 2.1.3 % 13.24/2.61 % (3978920)Termination reason: Refutation not found, incomplete strategy % 13.24/2.61 % (3978920)Time elapsed: 0.002 s % 13.24/2.61 % (3978920)Peak memory usage: 87 MB % 13.24/2.61 % (3978920)Instructions burned: 6 (million) % 13.24/2.61 % (3978918)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2871421552:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 13.24/2.61 % (3978921)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=664918306:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi) % 13.24/2.61 % (3978918)Instruction limit reached! % 13.24/2.61 % (3978918)------------------------------ % 13.24/2.61 % (3978918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.24/2.61 % (3978918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.24/2.61 % (3978918)CaDiCaL version: 2.1.3 % 13.24/2.61 % (3978918)Termination reason: Instruction limit % 13.24/2.61 % (3978918)Termination phase: Saturation % 13.24/2.61 % (3978918)Time elapsed: 0.074 s % 13.24/2.61 % (3978918)Peak memory usage: 92 MB % 13.24/2.61 % (3978918)Instructions burned: 136 (million) % 13.24/2.61 % (3978920)------------------------------ % 13.24/2.61 % (3978920)------------------------------ % 13.24/2.61 % (3978925)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=3933761922:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 13.24/2.61 % (3978925)Refutation not found, incomplete strategy % 13.24/2.61 % (3978925)------------------------------ % 13.24/2.61 % (3978925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.24/2.61 % (3978925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.24/2.61 % (3978925)CaDiCaL version: 2.1.3 % 13.24/2.61 % (3978925)Termination reason: Refutation not found, incomplete strategy % 13.24/2.61 % (3978925)Time elapsed: 0.012 s % 13.24/2.61 % (3978925)Peak memory usage: 88 MB % 13.24/2.61 % (3978925)Instructions burned: 21 (million) % 13.24/2.61 % (3978926)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4046633646:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi) % 13.24/2.61 % (3978926)Instruction limit reached! % 13.24/2.61 % (3978926)------------------------------ % 13.24/2.61 % (3978926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.24/2.61 % (3978926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.24/2.61 % (3978926)CaDiCaL version: 2.1.3 % 13.24/2.61 % (3978926)Termination reason: Instruction limit % 13.24/2.61 % (3978926)Termination phase: Saturation % 13.24/2.61 % (3978926)Time elapsed: 0.035 s % 13.24/2.61 % (3978926)Peak memory usage: 91 MB % 13.24/2.61 % (3978926)Instructions burned: 138 (million) % 13.24/2.61 [W928 14:02:17.606981026 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. % 13.24/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.24/2.61 [W928 14:02:17.607024513 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. % 13.24/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.24/2.61 [W928 14:02:17.607065543 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. % 13.24/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.24/2.61 [W928 14:02:17.607079046 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. % 13.24/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.24/2.61 [W928 14:02:17.607106849 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607119083 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607145586 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607203193 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607240736 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607252380 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607277120 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.607287836 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 % (3978929)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1997681757:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 16.84/3.10 % (3978929)Refutation not found, incomplete strategy % 16.84/3.10 % (3978929)------------------------------ % 16.84/3.10 % (3978929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.84/3.10 % (3978929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.84/3.10 % (3978929)CaDiCaL version: 2.1.3 % 16.84/3.10 % (3978929)Termination reason: Refutation not found, incomplete strategy % 16.84/3.10 % (3978929)Time elapsed: 0.003 s % 16.84/3.10 % (3978929)Peak memory usage: 87 MB % 16.84/3.10 % (3978929)Instructions burned: 4 (million) % 16.84/3.10 % (3978917)Refutation not found, incomplete strategy % 16.84/3.10 % (3978917)------------------------------ % 16.84/3.10 % (3978917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.84/3.10 % (3978917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.84/3.10 % (3978917)CaDiCaL version: 2.1.3 % 16.84/3.10 % (3978917)Termination reason: Refutation not found, incomplete strategy % 16.84/3.10 % (3978917)Time elapsed: 0.546 s % 16.84/3.10 % (3978917)Peak memory usage: 126 MB % 16.84/3.10 % (3978917)Instructions burned: 844 (million) % 16.84/3.10 % (3978925)------------------------------ % 16.84/3.10 % (3978925)------------------------------ % 16.84/3.10 [W928 14:02:17.806828371 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. % 16.84/3.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.84/3.10 [W928 14:02:17.806866088 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.806905148 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.806916904 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.806943221 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.806953924 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.806978418 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.807055314 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.807094341 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.807105784 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.807130544 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 [W928 14:02:17.807141314 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. % 26.44/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.44/4.45 % (3978917)------------------------------ % 26.44/4.45 % (3978917)------------------------------ % 26.44/4.45 % (3978931)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2446654683:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi) % 26.44/4.45 % (3978931)Refutation not found, incomplete strategy % 26.44/4.45 % (3978931)------------------------------ % 26.44/4.45 % (3978931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.44/4.45 % (3978931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.44/4.45 % (3978931)CaDiCaL version: 2.1.3 % 26.44/4.45 % (3978931)Termination reason: Refutation not found, incomplete strategy % 26.44/4.45 % (3978931)Time elapsed: 0.003 s % 26.44/4.45 % (3978931)Peak memory usage: 87 MB % 26.44/4.45 % (3978931)Instructions burned: 4 (million) % 26.44/4.45 % (3978929)------------------------------ % 26.44/4.45 % (3978929)------------------------------ % 28.54/4.80 % (3978921)Refutation not found, incomplete strategy % 28.54/4.80 % (3978921)------------------------------ % 28.54/4.80 % (3978921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.54/4.80 % (3978921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.54/4.80 % (3978921)CaDiCaL version: 2.1.3 % 28.54/4.80 % (3978921)Termination reason: Refutation not found, incomplete strategy % 28.54/4.80 % (3978921)Time elapsed: 0.570 s % 28.54/4.80 % (3978921)Peak memory usage: 128 MB % 28.54/4.80 % (3978921)Instructions burned: 844 (million) % 28.54/4.80 % (3978932)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=124030108:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi) % 28.54/4.80 % (3978934)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=1477812862:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi) % 28.54/4.80 % (3978931)------------------------------ % 28.54/4.80 % (3978931)------------------------------ % 28.54/4.80 % (3978934)Instruction limit reached! % 28.54/4.80 % (3978934)------------------------------ % 28.54/4.80 % (3978934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.54/4.80 % (3978934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.54/4.80 % (3978934)CaDiCaL version: 2.1.3 % 28.54/4.80 % (3978934)Termination reason: Instruction limit % 28.54/4.80 % (3978934)Termination phase: Saturation % 28.54/4.80 % (3978934)Time elapsed: 0.080 s % 28.54/4.80 % (3978934)Peak memory usage: 91 MB % 28.54/4.80 % (3978934)Instructions burned: 151 (million) % 28.54/4.80 % (3978921)------------------------------ % 28.54/4.80 % (3978921)------------------------------ % 28.54/4.80 % (3978904)Instruction limit reached! % 28.54/4.80 % (3978904)------------------------------ % 28.54/4.80 % (3978904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.54/4.80 % (3978904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.54/4.80 % (3978904)CaDiCaL version: 2.1.3 % 28.54/4.80 % (3978904)Termination reason: Instruction limit % 28.54/4.80 % (3978904)Termination phase: Saturation % 28.54/4.80 % (3978904)Time elapsed: 1.453 s % 28.54/4.80 % (3978904)Peak memory usage: 147 MB % 28.54/4.80 % (3978904)Instructions burned: 2351 (million) % 28.54/4.80 % (3978937)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=960239201:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi) % 28.54/4.80 % (3978938)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3318610579:i=667:av=off:fsr=off_2978 on theBenchmark for (2978ds/667Mi) % 28.54/4.80 % (3978939)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=2732806105:s2a=on:i=185:s2at=1.8:fdi=4_2977 on theBenchmark for (2977ds/185Mi) % 28.54/4.80 % (3978938)Refutation not found, incomplete strategy % 28.54/4.80 % (3978938)------------------------------ % 28.54/4.80 % (3978938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.54/4.80 % (3978938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.54/4.80 % (3978938)CaDiCaL version: 2.1.3 % 28.54/4.80 % (3978938)Termination reason: Refutation not found, incomplete strategy % 28.54/4.80 % (3978938)Time elapsed: 0.061 s % 28.54/4.80 % (3978938)Peak memory usage: 91 MB % 28.54/4.80 % (3978938)Instructions burned: 112 (million) % 28.54/4.80 % (3978940)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=201933515:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2977 on theBenchmark for (2977ds/193Mi) % 28.54/4.80 % (3978940)Refutation not found, incomplete strategy % 28.54/4.80 % (3978940)------------------------------ % 28.54/4.80 % (3978940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.54/4.80 % (3978940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.54/4.80 % (3978940)CaDiCaL version: 2.1.3 % 28.54/4.80 % (3978940)Termination reason: Refutation not found, incomplete strategy % 28.54/4.80 % (3978940)Time elapsed: 0.006 s % 28.54/4.80 % (3978940)Peak memory usage: 87 MB % 28.54/4.80 % (3978940)Instructions burned: 8 (million) % 28.54/4.80 % (3978939)Instruction limit reached! % 28.54/4.80 % (3978939)------------------------------ % 34.45/5.64 % (3978939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.45/5.64 % (3978939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.45/5.64 % (3978939)CaDiCaL version: 2.1.3 % 34.45/5.64 % (3978939)Termination reason: Instruction limit % 34.45/5.64 % (3978939)Termination phase: Saturation % 34.45/5.64 % (3978939)Time elapsed: 0.100 s % 34.45/5.64 % (3978939)Peak memory usage: 92 MB % 34.45/5.64 % (3978939)Instructions burned: 185 (million) % 34.45/5.64 % (3978945)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2937731523:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2975 on theBenchmark for (2975ds/4850Mi) % 34.45/5.64 % (3978938)------------------------------ % 34.45/5.64 % (3978938)------------------------------ % 34.45/5.64 % (3978945)Refutation not found, incomplete strategy % 34.45/5.64 % (3978945)------------------------------ % 34.45/5.64 % (3978945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.45/5.64 % (3978945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.45/5.64 % (3978945)CaDiCaL version: 2.1.3 % 34.45/5.64 % (3978945)Termination reason: Refutation not found, incomplete strategy % 34.45/5.64 % (3978945)Time elapsed: 0.041 s % 34.45/5.64 % (3978945)Peak memory usage: 90 MB % 34.45/5.64 % (3978945)Instructions burned: 86 (million) % 34.45/5.64 % (3978940)------------------------------ % 34.45/5.64 % (3978940)------------------------------ % 34.45/5.64 % (3978948)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3826155730:i=319:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/319Mi) % 34.45/5.64 % (3978947)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=180339335:i=12111:sd=1:ss=included_2973 on theBenchmark for (2973ds/12111Mi) % 34.45/5.64 % (3978945)------------------------------ % 34.45/5.64 % (3978945)------------------------------ % 34.45/5.64 % (3978948)Instruction limit reached! % 34.45/5.64 % (3978948)------------------------------ % 34.45/5.64 % (3978948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.45/5.64 % (3978948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.45/5.64 % (3978948)CaDiCaL version: 2.1.3 % 34.45/5.64 % (3978948)Termination reason: Instruction limit % 34.45/5.64 % (3978948)Termination phase: Saturation % 34.45/5.64 % (3978948)Time elapsed: 0.178 s % 34.45/5.64 % (3978948)Peak memory usage: 94 MB % 34.45/5.64 % (3978948)Instructions burned: 321 (million) % 34.45/5.64 % (3978951)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=989766545:i=2064:ep=RST_2971 on theBenchmark for (2971ds/2064Mi) % 34.45/5.64 % (3978951)Refutation not found, incomplete strategy % 34.45/5.64 % (3978951)------------------------------ % 34.45/5.64 % (3978951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.45/5.64 % (3978951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.45/5.64 % (3978951)CaDiCaL version: 2.1.3 % 34.45/5.64 % (3978951)Termination reason: Refutation not found, incomplete strategy % 34.45/5.64 % (3978951)Time elapsed: 0.048 s % 34.45/5.64 % (3978951)Peak memory usage: 90 MB % 34.45/5.64 % (3978951)Instructions burned: 103 (million) % 34.45/5.64 % (3978952)dis-1011_128_sil=32000:random_seed=1124883989:i=3706:ep=RST:av=off_2970 on theBenchmark for (2970ds/3706Mi) % 34.45/5.64 % (3978951)------------------------------ % 34.45/5.64 % (3978951)------------------------------ % 34.45/5.64 % (3978955)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=103033659:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2967 on theBenchmark for (2967ds/757Mi) % 34.45/5.64 % (3978955)Refutation not found, incomplete strategy % 34.45/5.64 % (3978955)------------------------------ % 34.45/5.64 % (3978955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.45/5.64 % (3978955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.45/5.64 % (3978955)CaDiCaL version: 2.1.3 % 34.45/5.64 % (3978955)Termination reason: Refutation not found, incomplete strategy % 34.45/5.64 % (3978955)Time elapsed: 0.003 s % 34.45/5.64 % (3978955)Peak memory usage: 87 MB % 34.45/5.64 % (3978955)Instructions burned: 4 (million) % 34.45/5.64 % (3978955)------------------------------ % 34.45/5.64 % (3978955)------------------------------ % 34.45/5.64 % (3978957)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2605403388:i=13913:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/13913Mi) % 34.45/5.64 % (3978932)Instruction limit reached! % 36.34/5.94 % (3978932)------------------------------ % 36.34/5.94 % (3978932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.34/5.94 % (3978932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.34/5.94 % (3978932)CaDiCaL version: 2.1.3 % 36.34/5.94 % (3978932)Termination reason: Instruction limit % 36.34/5.94 % (3978932)Termination phase: Saturation % 36.34/5.94 % (3978932)Time elapsed: 1.809 s % 36.34/5.94 % (3978932)Peak memory usage: 150 MB % 36.34/5.94 % (3978932)Instructions burned: 6061 (million) % 36.34/5.94 % (3978959)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2564979197:i=9925:aac=none_2962 on theBenchmark for (2962ds/9925Mi) % 36.34/5.94 [W928 14:02:19.173410183 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173441346 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173482433 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173495706 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173523726 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173535310 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173561650 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173573150 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173598410 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173609660 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 36.34/5.94 [W928 14:02:19.173635436 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. % 36.34/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.72/9.48 [W928 14:02:19.173646720 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. % 61.72/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.72/9.48 % (3978959)Refutation not found, incomplete strategy % 61.72/9.48 % (3978959)------------------------------ % 61.72/9.48 % (3978959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.72/9.48 % (3978959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.72/9.48 % (3978959)CaDiCaL version: 2.1.3 % 61.72/9.48 % (3978959)Termination reason: Refutation not found, incomplete strategy % 61.72/9.48 % (3978959)Time elapsed: 0.417 s % 61.72/9.48 % (3978959)Peak memory usage: 143 MB % 61.72/9.48 % (3978959)Instructions burned: 1112 (million) % 61.72/9.48 % (3978957)Refutation not found, incomplete strategy % 61.72/9.48 % (3978957)------------------------------ % 61.72/9.48 % (3978957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.72/9.48 % (3978957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.72/9.48 % (3978957)CaDiCaL version: 2.1.3 % 61.72/9.48 % (3978957)Termination reason: Refutation not found, incomplete strategy % 61.72/9.48 % (3978957)Time elapsed: 0.556 s % 61.72/9.48 % (3978957)Peak memory usage: 126 MB % 61.72/9.48 % (3978957)Instructions burned: 842 (million) % 61.72/9.48 % (3978959)------------------------------ % 61.72/9.48 % (3978959)------------------------------ % 61.72/9.48 % (3978961)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1618234473:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2955 on theBenchmark for (2955ds/2479Mi) % 61.72/9.48 % (3978961)Refutation not found, incomplete strategy % 61.72/9.48 % (3978961)------------------------------ % 61.72/9.48 % (3978961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.72/9.48 % (3978961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.72/9.48 % (3978961)CaDiCaL version: 2.1.3 % 61.72/9.48 % (3978961)Termination reason: Refutation not found, incomplete strategy % 61.72/9.48 % (3978961)Time elapsed: 0.003 s % 61.72/9.48 % (3978961)Peak memory usage: 87 MB % 61.72/9.48 % (3978961)Instructions burned: 8 (million) % 61.72/9.48 % (3978957)------------------------------ % 61.72/9.48 % (3978957)------------------------------ % 61.72/9.48 % (3978961)------------------------------ % 61.72/9.48 % (3978961)------------------------------ % 61.72/9.48 % (3978963)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2952140957:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2954 on theBenchmark for (2954ds/440Mi) % 61.72/9.48 % (3978964)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4005344978:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2953 on theBenchmark for (2953ds/11145Mi) % 61.72/9.48 % (3978963)Instruction limit reached! % 61.72/9.48 % (3978963)------------------------------ % 61.72/9.48 % (3978963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.72/9.48 % (3978963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.72/9.48 % (3978963)CaDiCaL version: 2.1.3 % 61.72/9.48 % (3978963)Termination reason: Instruction limit % 61.72/9.48 % (3978963)Termination phase: Saturation % 61.72/9.48 % (3978963)Time elapsed: 0.257 s % 61.72/9.48 % (3978963)Peak memory usage: 95 MB % 61.72/9.48 % (3978963)Instructions burned: 440 (million) % 61.72/9.48 [W928 14:02:20.007976911 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. % 61.72/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.72/9.48 [W928 14:02:20.008020514 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. % 61.72/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.72/9.48 [W928 14:02:20.008046875 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008053719 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008066794 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008076995 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008089839 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008095208 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008107534 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008112879 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008125935 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 [W928 14:02:20.008131512 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. % 63.36/9.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.36/9.87 % (3978967)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=2726269273:cts=off:i=3034:av=off:er=known:fsd=on_2950 on theBenchmark for (2950ds/3034Mi) % 63.36/9.87 % (3978964)Refutation not found, incomplete strategy % 63.36/9.87 % (3978964)------------------------------ % 63.36/9.87 % (3978964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.36/9.87 % (3978964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.36/9.87 % (3978964)CaDiCaL version: 2.1.3 % 63.36/9.87 % (3978964)Termination reason: Refutation not found, incomplete strategy % 63.36/9.87 % (3978964)Time elapsed: 0.324 s % 63.36/9.87 % (3978964)Peak memory usage: 128 MB % 63.36/9.87 % (3978964)Instructions burned: 846 (million) % 63.36/9.87 % (3978964)------------------------------ % 63.36/9.87 % (3978964)------------------------------ % 63.36/9.87 % (3978952)Instruction limit reached! % 63.36/9.87 % (3978952)------------------------------ % 63.36/9.87 % (3978952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.36/9.87 % (3978952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.36/9.87 % (3978952)CaDiCaL version: 2.1.3 % 63.36/9.87 % (3978952)Termination reason: Instruction limit % 63.67/9.95 % (3978952)Termination phase: Saturation % 63.67/9.95 % (3978952)Time elapsed: 2.217 s % 63.67/9.95 % (3978952)Peak memory usage: 126 MB % 63.67/9.95 % (3978952)Instructions burned: 3707 (million) % 63.67/9.95 % (3978969)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2521936247:st=2:s2a=on:i=524:s2at=2:ss=axioms_2947 on theBenchmark for (2947ds/524Mi) % 63.67/9.95 % (3978969)Refutation not found, incomplete strategy % 63.67/9.95 % (3978969)------------------------------ % 63.67/9.95 % (3978969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.67/9.95 % (3978969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.67/9.95 % (3978969)CaDiCaL version: 2.1.3 % 63.67/9.95 % (3978969)Termination reason: Refutation not found, incomplete strategy % 63.67/9.95 % (3978969)Time elapsed: 0.004 s % 63.67/9.95 % (3978969)Peak memory usage: 87 MB % 63.67/9.95 % (3978969)Instructions burned: 12 (million) % 63.67/9.95 % (3978970)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2666505958:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2947 on theBenchmark for (2947ds/1016Mi) % 63.67/9.95 % (3978970)Refutation not found, incomplete strategy % 63.67/9.95 % (3978970)------------------------------ % 63.67/9.95 % (3978970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.67/9.95 % (3978970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.67/9.95 % (3978970)CaDiCaL version: 2.1.3 % 63.67/9.95 % (3978970)Termination reason: Refutation not found, incomplete strategy % 63.67/9.95 % (3978970)Time elapsed: 0.004 s % 63.67/9.95 % (3978970)Peak memory usage: 87 MB % 63.67/9.95 % (3978970)Instructions burned: 4 (million) % 63.67/9.95 % (3978969)------------------------------ % 63.67/9.95 % (3978969)------------------------------ % 63.67/9.95 % (3978973)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1021722382:i=14123:bd=preordered:ins=4_2945 on theBenchmark for (2945ds/14123Mi) % 63.67/9.95 % (3978970)------------------------------ % 63.67/9.95 % (3978970)------------------------------ % 63.67/9.95 % (3978975)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3137569696:i=5781:kws=precedence:bd=all:rawr=on_2943 on theBenchmark for (2943ds/5781Mi) % 63.67/9.95 % (3978967)Instruction limit reached! % 63.67/9.95 % (3978967)------------------------------ % 63.67/9.95 % (3978967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.67/9.95 % (3978967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.67/9.95 % (3978967)CaDiCaL version: 2.1.3 % 63.67/9.95 % (3978967)Termination reason: Instruction limit % 63.67/9.95 % (3978967)Termination phase: Saturation % 63.67/9.95 % (3978967)Time elapsed: 1.803 s % 63.67/9.95 % (3978967)Peak memory usage: 146 MB % 63.67/9.95 % (3978967)Instructions burned: 3034 (million) % 63.67/9.95 % (3978977)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=3379977866:i=2448:gtgl=5:bd=preordered:gtg=all_2931 on theBenchmark for (2931ds/2448Mi) % 63.67/9.95 % (3978977)Instruction limit reached! % 63.67/9.95 % (3978977)------------------------------ % 63.67/9.95 % (3978977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.67/9.95 % (3978977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.67/9.96 % (3978977)CaDiCaL version: 2.1.3 % 63.67/9.96 % (3978977)Termination reason: Instruction limit % 63.67/9.96 % (3978977)Termination phase: Saturation % 63.67/9.96 % (3978977)Time elapsed: 1.456 s % 63.67/9.96 % (3978977)Peak memory usage: 147 MB % 63.67/9.96 % (3978977)Instructions burned: 2448 (million) % 63.67/9.96 % (3978979)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2700854121:i=3223:kws=precedence:fgj=on:av=off_2915 on theBenchmark for (2915ds/3223Mi) % 63.67/9.96 % (3978975)Instruction limit reached! % 63.67/9.96 % (3978975)------------------------------ % 63.67/9.96 % (3978975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.67/9.96 % (3978975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.67/9.96 % (3978975)CaDiCaL version: 2.1.3 % 63.67/9.96 % (3978975)Termination reason: Instruction limit % 63.67/9.96 % (3978975)Termination phase: Saturation % 63.67/9.96 % (3978975)Time elapsed: 2.914 s % 63.67/9.96 % (3978975)Peak memory usage: 125 MB % 63.67/9.96 % (3978975)Instructions burned: 5782 (million) % 63.67/9.96 % (3978981)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2655144277:st=5.6:i=2033:sd=3:ss=axioms_2912 on theBenchmark for (2912ds/2033Mi) % 66.47/10.04 % (3978947)Instruction limit reached! % 66.47/10.04 % (3978947)------------------------------ % 66.47/10.04 % (3978947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.47/10.04 % (3978947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.47/10.04 % (3978947)CaDiCaL version: 2.1.3 % 66.47/10.04 % (3978947)Termination reason: Instruction limit % 66.47/10.04 % (3978947)Termination phase: Saturation % 66.47/10.04 % (3978947)Time elapsed: 6.107 s % 66.47/10.04 % (3978947)Peak memory usage: 163 MB % 66.47/10.04 % (3978947)Instructions burned: 12113 (million) % 66.47/10.04 % (3978983)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=4284780067:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2911 on theBenchmark for (2911ds/2055Mi) % 66.47/10.04 % (3978973)Instruction limit reached! % 66.47/10.04 % (3978973)------------------------------ % 66.47/10.04 % (3978973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.47/10.04 % (3978973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.47/10.04 % (3978973)CaDiCaL version: 2.1.3 % 66.47/10.04 % (3978973)Termination reason: Instruction limit % 66.47/10.04 % (3978973)Termination phase: Saturation % 66.47/10.04 % (3978973)Time elapsed: 3.411 s % 66.47/10.04 % (3978973)Peak memory usage: 153 MB % 66.47/10.04 % (3978973)Instructions burned: 14124 (million) % 66.47/10.04 % (3978985)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=2776942663:i=21611:sd=3:ss=axioms_2909 on theBenchmark for (2909ds/21611Mi) % 66.47/10.04 [W928 14:02:24.238710420 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238754650 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238793800 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238805813 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238834367 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238846213 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238873113 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238885273 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. % 66.47/10.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.47/10.04 [W928 14:02:24.238911110 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.238922590 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.238947250 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.238957650 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325200978 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325221795 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325244138 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325253899 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325268398 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325275142 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325288701 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325295299 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325308231 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. % 69.56/10.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 69.56/10.59 [W928 14:02:24.325314701 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.325327948 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.325333938 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411443303 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411475869 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411513673 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411524533 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411551129 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411562729 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411587926 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411599143 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411624726 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411635936 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. % 75.30/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.30/11.35 [W928 14:02:24.411662279 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. % 83.24/12.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.24/12.40 [W928 14:02:24.411673489 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. % 83.24/12.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.24/12.40 % (3978981)Refutation not found, incomplete strategy % 83.24/12.40 % (3978981)------------------------------ % 83.24/12.40 % (3978981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.24/12.40 % (3978981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.40 % (3978981)CaDiCaL version: 2.1.3 % 83.24/12.40 % (3978981)Termination reason: Refutation not found, incomplete strategy % 83.24/12.40 % (3978981)Time elapsed: 0.560 s % 83.24/12.40 % (3978981)Peak memory usage: 128 MB % 83.24/12.40 % (3978981)Instructions burned: 844 (million) % 83.24/12.40 % (3978985)Refutation not found, incomplete strategy % 83.24/12.40 % (3978985)------------------------------ % 83.24/12.40 % (3978985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.24/12.40 % (3978985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.40 % (3978985)CaDiCaL version: 2.1.3 % 83.24/12.40 % (3978985)Termination reason: Refutation not found, incomplete strategy % 83.24/12.40 % (3978985)Time elapsed: 0.305 s % 83.24/12.40 % (3978985)Peak memory usage: 128 MB % 83.24/12.40 % (3978985)Instructions burned: 842 (million) % 83.24/12.40 % (3978985)------------------------------ % 83.24/12.40 % (3978985)------------------------------ % 83.24/12.40 % (3978983)Refutation not found, incomplete strategy % 83.24/12.40 % (3978983)------------------------------ % 83.24/12.40 % (3978983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.24/12.40 % (3978983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.40 % (3978983)CaDiCaL version: 2.1.3 % 83.24/12.40 % (3978983)Termination reason: Refutation not found, incomplete strategy % 83.24/12.40 % (3978983)Time elapsed: 0.564 s % 83.24/12.40 % (3978983)Peak memory usage: 128 MB % 83.24/12.40 % (3978983)Instructions burned: 855 (million) % 83.24/12.40 % (3978981)------------------------------ % 83.24/12.40 % (3978981)------------------------------ % 83.24/12.40 % (3979008)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1409922229:i=4835:sd=13:ss=axioms:sgt=23_2904 on theBenchmark for (2904ds/4835Mi) % 83.24/12.40 % (3979008)Refutation not found, incomplete strategy % 83.24/12.40 % (3979008)------------------------------ % 83.24/12.40 % (3979008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.24/12.40 % (3979008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.40 % (3979008)CaDiCaL version: 2.1.3 % 83.24/12.40 % (3979008)Termination reason: Refutation not found, incomplete strategy % 83.24/12.40 % (3979008)Time elapsed: 0.002 s % 83.24/12.40 % (3979008)Peak memory usage: 87 MB % 83.24/12.40 % (3979008)Instructions burned: 4 (million) % 83.24/12.40 % (3979042)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=3161187393:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2903 on theBenchmark for (2903ds/797Mi) % 83.24/12.40 % (3979008)------------------------------ % 83.24/12.40 % (3979008)------------------------------ % 83.24/12.40 % (3978983)------------------------------ % 83.24/12.40 % (3978983)------------------------------ % 83.24/12.40 % (3979084)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=4253416070:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2902 on theBenchmark for (2902ds/2326Mi) % 83.24/12.40 % (3979084)Refutation not found, incomplete strategy % 83.24/12.40 % (3979084)------------------------------ % 83.24/12.40 % (3979084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.24/12.40 % (3979084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.24/12.40 % (3979084)CaDiCaL version: 2.1.3 % 83.24/12.40 % (3979084)Termination reason: Refutation not found, incomplete strategy % 83.24/12.40 % (3979084)Time elapsed: 0.059 s % 83.24/12.40 % (3979084)Peak memory usage: 92 MB % 83.24/12.40 % (3979084)Instructions burned: 192 (million) % 91.26/13.61 % (3979087)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4138265913:i=6038:nm=6_2901 on theBenchmark for (2901ds/6038Mi) % 91.26/13.61 % (3979084)------------------------------ % 91.26/13.61 % (3979084)------------------------------ % 91.26/13.61 % (3978937)Instruction limit reached! % 91.26/13.61 % (3978937)------------------------------ % 91.26/13.61 % (3978937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.26/13.61 % (3978937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.26/13.61 % (3978937)CaDiCaL version: 2.1.3 % 91.26/13.61 % (3978937)Termination reason: Instruction limit % 91.26/13.61 % (3978937)Termination phase: Saturation % 91.26/13.61 % (3978937)Time elapsed: 7.884 s % 91.26/13.61 % (3978937)Peak memory usage: 167 MB % 91.26/13.61 % (3978937)Instructions burned: 14156 (million) % 91.26/13.61 % (3979147)lrs+10_1_sil=32000:sp=occurrence:random_seed=187329581:st=2:i=33334:sd=3:ss=included:sgt=32_2899 on theBenchmark for (2899ds/33334Mi) % 91.26/13.61 % (3979042)Instruction limit reached! % 91.26/13.61 % (3979042)------------------------------ % 91.26/13.61 % (3979042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.26/13.61 % (3979042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.26/13.61 % (3979042)CaDiCaL version: 2.1.3 % 91.26/13.61 % (3979042)Termination reason: Instruction limit % 91.26/13.61 % (3979042)Termination phase: Saturation % 91.26/13.61 % (3979042)Time elapsed: 0.419 s % 91.26/13.61 % (3979042)Peak memory usage: 93 MB % 91.26/13.61 % (3979042)Instructions burned: 799 (million) % 91.26/13.61 % (3979149)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=251584722:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2898 on theBenchmark for (2898ds/1008Mi) % 91.26/13.61 % (3979149)Refutation not found, incomplete strategy % 91.26/13.61 % (3979149)------------------------------ % 91.26/13.61 % (3979149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.26/13.61 % (3979149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.26/13.61 % (3979149)CaDiCaL version: 2.1.3 % 91.26/13.61 % (3979149)Termination reason: Refutation not found, incomplete strategy % 91.26/13.61 % (3979149)Time elapsed: 0.007 s % 91.26/13.61 % (3979149)Peak memory usage: 87 MB % 91.26/13.61 % (3979149)Instructions burned: 11 (million) % 91.26/13.61 % (3979150)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=1864582021:i=8327:s2at=5:bd=preordered_2898 on theBenchmark for (2898ds/8327Mi) % 91.26/13.61 % (3979149)------------------------------ % 91.26/13.61 % (3979149)------------------------------ % 91.26/13.61 % (3978979)Instruction limit reached! % 91.26/13.61 % (3978979)------------------------------ % 91.26/13.61 % (3978979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.26/13.61 % (3978979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.26/13.61 % (3978979)CaDiCaL version: 2.1.3 % 91.26/13.61 % (3978979)Termination reason: Instruction limit % 91.26/13.61 % (3978979)Termination phase: Saturation % 91.26/13.61 % (3978979)Time elapsed: 1.943 s % 91.26/13.61 % (3978979)Peak memory usage: 147 MB % 91.26/13.61 % (3978979)Instructions burned: 3223 (million) % 91.26/13.61 % (3979087)Refutation not found, incomplete strategy % 91.26/13.61 % (3979087)------------------------------ % 91.26/13.61 % (3979087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.26/13.61 % (3979087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.26/13.61 % (3979087)CaDiCaL version: 2.1.3 % 91.26/13.61 % (3979087)Termination reason: Refutation not found, incomplete strategy % 91.26/13.61 % (3979087)Time elapsed: 0.725 s % 91.26/13.61 % (3979087)Peak memory usage: 144 MB % 91.26/13.61 % (3979087)Instructions burned: 1114 (million) % 91.26/13.61 % (3979153)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=74651725:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2894 on theBenchmark for (2894ds/1083Mi) % 91.26/13.61 % (3979154)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=907539281:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2894 on theBenchmark for (2894ds/1084Mi) % 91.26/13.61 % (3979154)Refutation not found, incomplete strategy % 91.26/13.61 % (3979154)------------------------------ % 93.91/14.03 % (3979154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.91/14.03 % (3979154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.91/14.03 % (3979154)CaDiCaL version: 2.1.3 % 93.91/14.03 % (3979154)Termination reason: Refutation not found, incomplete strategy % 93.91/14.03 % (3979154)Time elapsed: 0.003 s % 93.91/14.03 % (3979154)Peak memory usage: 87 MB % 93.91/14.03 % (3979154)Instructions burned: 4 (million) % 93.91/14.03 % (3979087)------------------------------ % 93.91/14.03 % (3979087)------------------------------ % 93.91/14.03 % (3979154)------------------------------ % 93.91/14.03 % (3979154)------------------------------ % 93.91/14.03 % (3979157)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2164928386:i=6995:s2at=5:gtg=all_2890 on theBenchmark for (2890ds/6995Mi) % 93.91/14.03 % (3979158)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=556449065:st=2:i=6225:sd=15:ss=axioms_2890 on theBenchmark for (2890ds/6225Mi) % 93.91/14.03 % (3979158)Refutation not found, incomplete strategy % 93.91/14.03 % (3979158)------------------------------ % 93.91/14.03 % (3979158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.91/14.03 % (3979158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.91/14.03 % (3979158)CaDiCaL version: 2.1.3 % 93.91/14.03 % (3979158)Termination reason: Refutation not found, incomplete strategy % 93.91/14.03 % (3979158)Time elapsed: 0.004 s % 93.91/14.03 % (3979158)Peak memory usage: 87 MB % 93.91/14.03 % (3979158)Instructions burned: 6 (million) % 93.91/14.03 % (3979153)Instruction limit reached! % 93.91/14.03 % (3979153)------------------------------ % 93.91/14.03 % (3979153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.91/14.03 % (3979153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.91/14.03 % (3979153)CaDiCaL version: 2.1.3 % 93.91/14.03 % (3979153)Termination reason: Instruction limit % 93.91/14.03 % (3979153)Termination phase: Saturation % 93.91/14.03 % (3979153)Time elapsed: 0.555 s % 93.91/14.03 % (3979153)Peak memory usage: 103 MB % 93.91/14.03 % (3979153)Instructions burned: 1083 (million) % 93.91/14.03 % (3979158)------------------------------ % 93.91/14.03 % (3979158)------------------------------ % 93.91/14.03 % (3979161)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1991336618:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2887 on theBenchmark for (2887ds/3372Mi) % 93.91/14.03 % (3979162)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3152011570:st=2.3:i=26457:sd=10:ss=included:sgt=8_2886 on theBenchmark for (2886ds/26457Mi) % 93.91/14.03 [W928 14:02:27.770354464 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. % 93.91/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.91/14.03 [W928 14:02:27.770398521 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. % 93.91/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.91/14.03 [W928 14:02:27.770437884 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. % 93.91/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.91/14.03 [W928 14:02:27.770451221 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. % 93.91/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.91/14.03 [W928 14:02:27.770538098 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. % 93.91/14.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.91/14.03 [W928 14:02:27.770576561 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 [W928 14:02:27.770609438 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 [W928 14:02:27.770620688 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 [W928 14:02:27.770644698 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 [W928 14:02:27.770661431 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 [W928 14:02:27.770686818 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 [W928 14:02:27.770697548 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.90/14.72 % (3979161)Refutation not found, incomplete strategy % 98.90/14.72 % (3979161)------------------------------ % 98.90/14.72 % (3979161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.90/14.72 % (3979161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.90/14.72 % (3979161)CaDiCaL version: 2.1.3 % 98.90/14.72 % (3979161)Termination reason: Refutation not found, incomplete strategy % 98.90/14.72 % (3979161)Time elapsed: 0.562 s % 98.90/14.72 % (3979161)Peak memory usage: 128 MB % 98.90/14.72 % (3979161)Instructions burned: 857 (million) % 98.90/14.72 % (3979161)------------------------------ % 98.90/14.72 % (3979161)------------------------------ % 98.90/14.72 % (3979162)Refutation not found, incomplete strategy % 98.90/14.72 % (3979162)------------------------------ % 98.90/14.72 % (3979162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.90/14.72 % (3979162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.90/14.72 % (3979162)CaDiCaL version: 2.1.3 % 98.90/14.72 % (3979162)Termination reason: Refutation not found, incomplete strategy % 98.90/14.72 % (3979162)Time elapsed: 0.716 s % 98.90/14.72 % (3979162)Peak memory usage: 143 MB % 98.90/14.72 % (3979162)Instructions burned: 1115 (million) % 98.90/14.72 % (3979165)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=2520279267:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2878 on theBenchmark for (2878ds/13494Mi) % 98.90/14.72 % (3979162)------------------------------ % 98.90/14.72 % (3979162)------------------------------ % 98.90/14.72 % (3979167)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=1176041572:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2875 on theBenchmark for (2875ds/2503Mi) % 98.90/14.72 [W928 14:02:28.980862524 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. % 98.90/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.980905894 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.980944041 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.980955534 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.980981037 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981052718 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981092128 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981103594 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981128188 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981139098 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981163798 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 [W928 14:02:28.981174794 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. % 118.70/17.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.70/17.48 % (3979167)Refutation not found, incomplete strategy % 118.70/17.48 % (3979167)------------------------------ % 118.70/17.48 % (3979167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.70/17.48 % (3979167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.70/17.48 % (3979167)CaDiCaL version: 2.1.3 % 118.70/17.48 % (3979167)Termination reason: Refutation not found, incomplete strategy % 118.70/17.48 % (3979167)Time elapsed: 0.557 s % 118.70/17.48 % (3979167)Peak memory usage: 128 MB % 118.70/17.48 % (3979167)Instructions burned: 843 (million) % 118.70/17.48 % (3979167)------------------------------ % 118.70/17.48 % (3979167)------------------------------ % 125.83/18.41 % (3979169)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3117476147:i=2559:sd=1:ep=RSTC:ss=axioms_2866 on theBenchmark for (2866ds/2559Mi) % 125.83/18.41 [W928 14:02:29.919196671 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. % 125.83/18.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.41 [W928 14:02:29.919230554 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. % 125.83/18.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.41 [W928 14:02:29.919268478 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. % 125.83/18.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.41 [W928 14:02:29.919281221 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. % 125.83/18.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.41 [W928 14:02:29.919307341 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. % 125.83/18.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.41 [W928 14:02:29.919318764 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. % 125.83/18.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 [W928 14:02:29.919345188 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. % 125.83/18.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 [W928 14:02:29.919356465 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. % 125.83/18.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 [W928 14:02:29.919381278 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. % 125.83/18.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 [W928 14:02:29.919392655 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. % 125.83/18.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 [W928 14:02:29.919417398 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. % 125.83/18.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 [W928 14:02:29.919428601 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. % 125.83/18.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.83/18.42 % (3979169)Refutation not found, incomplete strategy % 125.83/18.42 % (3979169)------------------------------ % 125.83/18.42 % (3979169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.48/19.23 % (3979169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.48/19.23 % (3979169)CaDiCaL version: 2.1.3 % 131.48/19.23 % (3979169)Termination reason: Refutation not found, incomplete strategy % 131.48/19.23 % (3979169)Time elapsed: 0.554 s % 131.48/19.23 % (3979169)Peak memory usage: 128 MB % 131.48/19.23 % (3979169)Instructions burned: 838 (million) % 131.48/19.23 % (3979169)------------------------------ % 131.48/19.23 % (3979169)------------------------------ % 131.48/19.23 % (3979171)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1770678984:i=30753:av=off:ss=included_2856 on theBenchmark for (2856ds/30753Mi) % 131.48/19.23 % (3979150)Instruction limit reached! % 131.48/19.23 % (3979150)------------------------------ % 131.48/19.23 % (3979150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.48/19.23 % (3979150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.48/19.23 % (3979150)CaDiCaL version: 2.1.3 % 131.48/19.23 % (3979150)Termination reason: Instruction limit % 131.48/19.23 % (3979150)Termination phase: Saturation % 131.48/19.23 % (3979150)Time elapsed: 4.682 s % 131.48/19.23 % (3979150)Peak memory usage: 172 MB % 131.48/19.23 % (3979150)Instructions burned: 8328 (million) % 131.48/19.23 % (3979173)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=552178104:i=26473:ep=RSTC_2849 on theBenchmark for (2849ds/26473Mi) % 131.48/19.23 % (3979157)Instruction limit reached! % 131.48/19.23 % (3979157)------------------------------ % 131.48/19.23 % (3979157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.48/19.23 % (3979157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.48/19.23 % (3979157)CaDiCaL version: 2.1.3 % 131.48/19.23 % (3979157)Termination reason: Instruction limit % 131.48/19.23 % (3979157)Termination phase: Saturation % 131.48/19.23 % (3979157)Time elapsed: 4.131 s % 131.48/19.23 % (3979157)Peak memory usage: 167 MB % 131.48/19.23 % (3979157)Instructions burned: 6995 (million) % 131.48/19.23 % (3979175)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=2429662260:cts=off:i=2759:kws=inv_arity:fgj=on_2848 on theBenchmark for (2848ds/2759Mi) % 131.48/19.23 % (3979175)Refutation not found, incomplete strategy % 131.48/19.23 % (3979175)------------------------------ % 131.48/19.23 % (3979175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 131.48/19.23 % (3979175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 131.48/19.23 % (3979175)CaDiCaL version: 2.1.3 % 131.48/19.23 % (3979175)Termination reason: Refutation not found, incomplete strategy % 131.48/19.23 % (3979175)Time elapsed: 0.740 s % 131.48/19.23 % (3979175)Peak memory usage: 145 MB % 131.48/19.23 % (3979175)Instructions burned: 1162 (million) % 131.48/19.23 % (3979175)------------------------------ % 131.48/19.23 % (3979175)------------------------------ % 131.48/19.23 % (3979177)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=2328066457:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2836 on theBenchmark for (2836ds/5665Mi) % 131.48/19.23 [W928 14:02:32.846178024 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. % 131.48/19.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.48/19.23 [W928 14:02:32.846210018 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. % 131.48/19.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.48/19.23 [W928 14:02:32.846248351 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. % 131.48/19.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 131.48/19.23 [W928 14:02:32.846262248 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846290224 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846301221 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846340128 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846350844 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846375331 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846385261 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846409524 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:32.846419701 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 % (3979177)Refutation not found, incomplete strategy % 132.16/19.36 % (3979177)------------------------------ % 132.16/19.36 % (3979177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.16/19.36 % (3979177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.16/19.36 % (3979177)CaDiCaL version: 2.1.3 % 132.16/19.36 % (3979177)Termination reason: Refutation not found, incomplete strategy % 132.16/19.36 % (3979177)Time elapsed: 0.554 s % 132.16/19.36 % (3979177)Peak memory usage: 128 MB % 132.16/19.36 % (3979177)Instructions burned: 845 (million) % 132.16/19.36 % (3979177)------------------------------ % 132.16/19.36 % (3979177)------------------------------ % 132.16/19.36 % (3979179)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=4291911358:i=1532:ep=RS:ss=axioms_2827 on theBenchmark for (2827ds/1532Mi) % 132.16/19.36 [W928 14:02:33.785429395 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:33.785472322 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. % 132.16/19.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.16/19.36 [W928 14:02:33.785509745 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785521735 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785548972 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785572902 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785600312 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785611442 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785636052 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785646822 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785671246 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 [W928 14:02:33.785682172 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. % 138.57/20.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.57/20.28 % (3979179)Refutation not found, incomplete strategy % 138.57/20.28 % (3979179)------------------------------ % 138.57/20.28 % (3979179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.57/20.28 % (3979179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.57/20.28 % (3979179)CaDiCaL version: 2.1.3 % 138.57/20.28 % (3979179)Termination reason: Refutation not found, incomplete strategy % 138.57/20.28 % (3979179)Time elapsed: 0.555 s % 138.57/20.28 % (3979179)Peak memory usage: 128 MB % 138.57/20.28 % (3979179)Instructions burned: 842 (million) % 138.57/20.28 % (3979179)------------------------------ % 138.57/20.28 % (3979179)------------------------------ % 138.57/20.28 % (3979181)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3269682763:i=1565:sd=2:ss=axioms:sgt=32_2818 on theBenchmark for (2818ds/1565Mi) % 138.57/20.28 % (3979165)Instruction limit reached! % 138.57/20.28 % (3979165)------------------------------ % 138.57/20.28 % (3979165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.57/20.28 % (3979165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.65/21.23 % (3979165)CaDiCaL version: 2.1.3 % 145.65/21.23 % (3979165)Termination reason: Instruction limit % 145.65/21.23 % (3979165)Termination phase: Saturation % 145.65/21.23 % (3979165)Time elapsed: 6.263 s % 145.65/21.23 % (3979165)Peak memory usage: 165 MB % 145.65/21.23 % (3979165)Instructions burned: 13495 (million) % 145.65/21.23 [W928 14:02:34.712613509 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712645925 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712684892 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712697322 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712724099 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712735782 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712761325 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712772585 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712797412 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712808772 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712834649 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 [W928 14:02:34.712846045 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. % 145.65/21.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.65/21.23 % (3979183)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=3052735838:i=1572:fgj=on:gsp=on_2814 on theBenchmark for (2814ds/1572Mi) % 148.87/21.79 % (3979181)Refutation not found, incomplete strategy % 148.87/21.79 % (3979181)------------------------------ % 148.87/21.79 % (3979181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.87/21.79 % (3979181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.87/21.79 % (3979181)CaDiCaL version: 2.1.3 % 148.87/21.79 % (3979181)Termination reason: Refutation not found, incomplete strategy % 148.87/21.79 % (3979181)Time elapsed: 0.565 s % 148.87/21.79 % (3979181)Peak memory usage: 128 MB % 148.87/21.79 % (3979181)Instructions burned: 843 (million) % 148.87/21.79 % (3979181)------------------------------ % 148.87/21.79 % (3979181)------------------------------ % 148.87/21.79 % (3979185)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1089032777:i=6052:sd=4:ss=axioms:sgt=24_2808 on theBenchmark for (2808ds/6052Mi) % 148.87/21.79 [W928 14:02:35.653274238 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653306411 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653344618 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653357848 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653385538 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653396811 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653422515 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653433795 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653458928 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.87/21.80 [W928 14:02:35.653469948 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. % 148.87/21.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.55/22.08 [W928 14:02:35.653495281 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. % 151.55/22.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.55/22.08 [W928 14:02:35.653505395 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. % 151.55/22.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.55/22.08 % (3979183)Instruction limit reached! % 151.55/22.08 % (3979183)------------------------------ % 151.55/22.08 % (3979183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.55/22.08 % (3979183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.55/22.08 % (3979183)CaDiCaL version: 2.1.3 % 151.55/22.08 % (3979183)Termination reason: Instruction limit % 151.55/22.08 % (3979183)Termination phase: Saturation % 151.55/22.08 % (3979183)Time elapsed: 0.940 s % 151.55/22.08 % (3979183)Peak memory usage: 142 MB % 151.55/22.08 % (3979183)Instructions burned: 1573 (million) % 151.55/22.08 % (3979187)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=552299214:i=3500:sd=1:bd=preordered:sup=off:ss=included_2803 on theBenchmark for (2803ds/3500Mi) % 151.55/22.08 % (3979185)Refutation not found, incomplete strategy % 151.55/22.08 % (3979185)------------------------------ % 151.55/22.08 % (3979185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.55/22.08 % (3979185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.55/22.08 % (3979185)CaDiCaL version: 2.1.3 % 151.55/22.08 % (3979185)Termination reason: Refutation not found, incomplete strategy % 151.55/22.08 % (3979185)Time elapsed: 0.560 s % 151.55/22.08 % (3979185)Peak memory usage: 127 MB % 151.55/22.08 % (3979185)Instructions burned: 843 (million) % 151.55/22.08 % (3979185)------------------------------ % 151.55/22.08 % (3979185)------------------------------ % 151.55/22.08 % (3979189)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=3651542290:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2799 on theBenchmark for (2799ds/1842Mi) % 151.55/22.08 % (3979147)Instruction limit reached! % 151.55/22.08 % (3979147)------------------------------ % 151.55/22.08 % (3979147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.55/22.08 % (3979147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.55/22.08 % (3979147)CaDiCaL version: 2.1.3 % 151.55/22.08 % (3979147)Termination reason: Instruction limit % 151.55/22.08 % (3979147)Termination phase: Saturation % 151.55/22.08 % (3979147)Time elapsed: 10.124 s % 151.55/22.08 % (3979147)Peak memory usage: 272 MB % 151.55/22.08 % (3979147)Instructions burned: 33337 (million) % 151.55/22.08 % (3979191)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=278029763:i=66096:add=on_2796 on theBenchmark for (2796ds/66096Mi) % 151.55/22.08 % (3979187)Refutation not found, incomplete strategy % 151.55/22.08 % (3979187)------------------------------ % 151.55/22.08 % (3979187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.55/22.08 % (3979187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.55/22.08 % (3979187)CaDiCaL version: 2.1.3 % 151.55/22.08 % (3979187)Termination reason: Refutation not found, incomplete strategy % 151.55/22.08 % (3979187)Time elapsed: 0.711 s % 151.55/22.08 % (3979187)Peak memory usage: 137 MB % 151.55/22.08 % (3979187)Instructions burned: 1114 (million) % 151.55/22.08 [W928 14:02:36.604517470 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. % 151.55/22.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.55/22.08 [W928 14:02:36.604549370 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. % 151.55/22.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604586374 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604651184 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604690590 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604702304 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604727337 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604738690 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604762784 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604774201 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604798474 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 [W928 14:02:36.604809397 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.47/24.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 166.47/24.17 % (3979187)------------------------------ % 166.47/24.17 % (3979187)------------------------------ % 166.47/24.17 % (3979189)Refutation not found, incomplete strategy % 166.47/24.17 % (3979189)------------------------------ % 166.47/24.17 % (3979189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 166.47/24.17 % (3979189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 166.47/24.17 % (3979189)CaDiCaL version: 2.1.3 % 166.47/24.17 % (3979189)Termination reason: Refutation not found, incomplete strategy % 166.47/24.17 % (3979189)Time elapsed: 0.565 s % 166.47/24.17 % (3979189)Peak memory usage: 128 MB % 166.47/24.17 % (3979189)Instructions burned: 857 (million) % 166.47/24.17 % (3979193)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1045351342:i=1884:sd=1:nm=60:ss=axioms_2792 on theBenchmark for (2792ds/1884Mi) % 166.47/24.17 % (3979189)------------------------------ % 166.47/24.17 % (3979189)------------------------------ % 166.47/24.17 % (3979195)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2398432769:cts=off:i=5469:bs=on:fsr=off_2789 on theBenchmark for (2789ds/5469Mi) % 192.36/27.87 [W928 14:02:36.271168205 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271207571 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271250542 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271261698 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271286842 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271297272 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271321925 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271334082 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271358605 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271369662 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271394178 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 [W928 14:02:36.271405372 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. % 192.36/27.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.36/27.87 % (3979193)Refutation not found, incomplete strategy % 192.36/27.87 % (3979193)------------------------------ % 192.36/27.87 % (3979193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.36/27.87 % (3979193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.38/29.20 % (3979193)CaDiCaL version: 2.1.3 % 202.38/29.20 % (3979193)Termination reason: Refutation not found, incomplete strategy % 202.38/29.20 % (3979193)Time elapsed: 0.556 s % 202.38/29.20 % (3979193)Peak memory usage: 127 MB % 202.38/29.20 % (3979193)Instructions burned: 842 (million) % 202.38/29.20 % (3979193)------------------------------ % 202.38/29.20 % (3979193)------------------------------ % 202.38/29.20 % (3979197)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=2849702416:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2783 on theBenchmark for (2783ds/2037Mi) % 202.38/29.20 % (3979197)Instruction limit reached! % 202.38/29.20 % (3979197)------------------------------ % 202.38/29.20 % (3979197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 202.38/29.20 % (3979197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.38/29.20 % (3979197)CaDiCaL version: 2.1.3 % 202.38/29.20 % (3979197)Termination reason: Instruction limit % 202.38/29.20 % (3979197)Termination phase: Saturation % 202.38/29.20 % (3979197)Time elapsed: 1.206 s % 202.38/29.20 % (3979197)Peak memory usage: 148 MB % 202.38/29.20 % (3979197)Instructions burned: 2039 (million) % 202.38/29.20 % (3979199)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=885088687:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2769 on theBenchmark for (2769ds/2110Mi) % 202.38/29.20 [W928 14:02:39.537182712 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537215599 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537256099 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537270222 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537299199 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537311622 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537337672 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537349349 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 202.38/29.20 [W928 14:02:39.537374956 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. % 202.38/29.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 223.10/32.15 [W928 14:02:39.537386162 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. % 223.10/32.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 223.10/32.15 [W928 14:02:39.537410546 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. % 223.10/32.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 223.10/32.15 [W928 14:02:39.537420899 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. % 223.10/32.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 223.10/32.15 % (3979199)Refutation not found, incomplete strategy % 223.10/32.15 % (3979199)------------------------------ % 223.10/32.15 % (3979199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.10/32.15 % (3979199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.10/32.15 % (3979199)CaDiCaL version: 2.1.3 % 223.10/32.15 % (3979199)Termination reason: Refutation not found, incomplete strategy % 223.10/32.15 % (3979199)Time elapsed: 0.559 s % 223.10/32.15 % (3979199)Peak memory usage: 128 MB % 223.10/32.15 % (3979199)Instructions burned: 846 (million) % 223.10/32.15 % (3979199)------------------------------ % 223.10/32.15 % (3979199)------------------------------ % 223.10/32.15 % (3979249)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=3635141571:i=2430:add=off:aac=none:nm=16_2760 on theBenchmark for (2760ds/2430Mi) % 223.10/32.15 % (3979195)Instruction limit reached! % 223.10/32.15 % (3979195)------------------------------ % 223.10/32.15 % (3979195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.10/32.15 % (3979195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.10/32.15 % (3979195)CaDiCaL version: 2.1.3 % 223.10/32.15 % (3979195)Termination reason: Instruction limit % 223.10/32.15 % (3979195)Termination phase: Saturation % 223.10/32.15 % (3979195)Time elapsed: 3.322 s % 223.10/32.15 % (3979195)Peak memory usage: 121 MB % 223.10/32.15 % (3979195)Instructions burned: 5470 (million) % 223.10/32.15 % (3979319)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=768955187:cond=fast:i=4891_2755 on theBenchmark for (2755ds/4891Mi) % 223.10/32.15 % (3979249)Instruction limit reached! % 223.10/32.15 % (3979249)------------------------------ % 223.10/32.15 % (3979249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.10/32.15 % (3979249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.10/32.15 % (3979249)CaDiCaL version: 2.1.3 % 223.10/32.15 % (3979249)Termination reason: Instruction limit % 223.10/32.15 % (3979249)Termination phase: Saturation % 223.10/32.15 % (3979249)Time elapsed: 1.397 s % 223.10/32.15 % (3979249)Peak memory usage: 141 MB % 223.10/32.15 % (3979249)Instructions burned: 2431 (million) % 223.10/32.15 % (3979452)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=3692909273:st=2:i=14845:sd=2:ss=included:fsd=on_2745 on theBenchmark for (2745ds/14845Mi) % 223.10/32.15 % (3979452)Refutation not found, incomplete strategy % 223.10/32.15 % (3979452)------------------------------ % 223.10/32.15 % (3979452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 223.10/32.15 % (3979452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 223.10/32.15 % (3979452)CaDiCaL version: 2.1.3 % 223.10/32.15 % (3979452)Termination reason: Refutation not found, incomplete strategy % 223.10/32.15 % (3979452)Time elapsed: 0.995 s % 223.10/32.15 % (3979452)Peak memory usage: 145 MB % 223.10/32.15 % (3979452)Instructions burned: 1087 (million) % 223.10/32.15 % (3979452)------------------------------ % 223.10/32.15 % (3979452)------------------------------ % 223.10/32.15 % (3979486)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3247099227:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2729 on theBenchmark for (2729ds/7534Mi) % 230.67/33.23 % (3979319)Instruction limit reached! % 230.67/33.23 % (3979319)------------------------------ % 230.67/33.23 % (3979319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.67/33.23 % (3979319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.67/33.23 % (3979319)CaDiCaL version: 2.1.3 % 230.67/33.23 % (3979319)Termination reason: Instruction limit % 230.67/33.23 % (3979319)Termination phase: Saturation % 230.67/33.23 % (3979319)Time elapsed: 3.450 s % 230.67/33.23 % (3979319)Peak memory usage: 151 MB % 230.67/33.23 % (3979319)Instructions burned: 4893 (million) % 230.67/33.23 % (3979545)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=2403896572:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2719 on theBenchmark for (2719ds/10353Mi) % 230.67/33.23 [W928 14:02:44.574908873 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.574940516 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.574979550 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.574991087 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575029277 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575042420 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575067433 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575078710 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575103690 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575114950 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. % 230.67/33.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.67/33.23 [W928 14:02:44.575139943 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. % 236.51/34.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.51/34.11 [W928 14:02:44.575151020 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. % 236.51/34.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.51/34.11 % (3979545)Refutation not found, incomplete strategy % 236.51/34.11 % (3979545)------------------------------ % 236.51/34.11 % (3979545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.51/34.11 % (3979545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.51/34.11 % (3979545)CaDiCaL version: 2.1.3 % 236.51/34.11 % (3979545)Termination reason: Refutation not found, incomplete strategy % 236.51/34.11 % (3979545)Time elapsed: 0.545 s % 236.51/34.11 % (3979545)Peak memory usage: 127 MB % 236.51/34.11 % (3979545)Instructions burned: 838 (million) % 236.51/34.11 % (3979545)------------------------------ % 236.51/34.11 % (3979545)------------------------------ % 236.51/34.11 % (3979171)Instruction limit reached! % 236.51/34.11 % (3979171)------------------------------ % 236.51/34.11 % (3979171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.51/34.11 % (3979171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.51/34.11 % (3979171)CaDiCaL version: 2.1.3 % 236.51/34.11 % (3979171)Termination reason: Instruction limit % 236.51/34.11 % (3979171)Termination phase: Saturation % 236.51/34.11 % (3979171)Time elapsed: 14.624 s % 236.51/34.11 % (3979171)Peak memory usage: 161 MB % 236.51/34.11 % (3979171)Instructions burned: 30754 (million) % 236.51/34.11 % (3979648)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1489251408:i=7860_2710 on theBenchmark for (2710ds/7860Mi) % 236.51/34.11 % (3979648)Refutation not found, incomplete strategy % 236.51/34.11 % (3979648)------------------------------ % 236.51/34.11 % (3979648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.51/34.11 % (3979648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.51/34.11 % (3979648)CaDiCaL version: 2.1.3 % 236.51/34.11 % (3979648)Termination reason: Refutation not found, incomplete strategy % 236.51/34.11 % (3979648)Time elapsed: 0.056 s % 236.51/34.11 % (3979648)Peak memory usage: 91 MB % 236.51/34.11 % (3979648)Instructions burned: 108 (million) % 236.51/34.11 % (3979649)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=2413718882:i=7896:sd=2:bs=on:ss=included:sgt=20_2709 on theBenchmark for (2709ds/7896Mi) % 236.51/34.11 % (3979648)------------------------------ % 236.51/34.11 % (3979648)------------------------------ % 236.51/34.11 % (3979652)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1905010671:i=5812:gtgl=2:gtg=all_2705 on theBenchmark for (2705ds/5812Mi) % 236.51/34.11 % (3979173)Instruction limit reached! % 236.51/34.11 % (3979173)------------------------------ % 236.51/34.11 % (3979173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.51/34.11 % (3979173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.51/34.11 % (3979173)CaDiCaL version: 2.1.3 % 236.51/34.11 % (3979173)Termination reason: Instruction limit % 236.51/34.11 % (3979173)Termination phase: Saturation % 236.51/34.11 % (3979173)Time elapsed: 15.701 s % 236.51/34.11 % (3979173)Peak memory usage: 506 MB % 236.51/34.11 % (3979173)Instructions burned: 26473 (million) % 236.51/34.11 % (3979654)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=2882151909:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2690 on theBenchmark for (2690ds/2965Mi) % 236.51/34.11 % (3979486)Instruction limit reached! % 236.51/34.11 % (3979486)------------------------------ % 236.51/34.11 % (3979486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.51/34.11 % (3979486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.51/34.11 % (3979486)CaDiCaL version: 2.1.3 % 236.51/34.11 % (3979486)Termination reason: Instruction limit % 236.51/34.11 % (3979486)Termination phase: Saturation % 236.51/34.11 % (3979486)Time elapsed: 4.146 s % 236.51/34.11 % (3979486)Peak memory usage: 154 MB % 236.51/34.11 % (3979486)Instructions burned: 7534 (million) % 236.51/34.11 % (3979656)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=443412650:i=2967:kws=precedence:bd=preordered:av=off_2686 on theBenchmark for (2686ds/2967Mi) % 239.16/34.52 % (3979654)Refutation not found, incomplete strategy % 239.16/34.52 % (3979654)------------------------------ % 239.16/34.52 % (3979654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.16/34.52 % (3979654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.16/34.52 % (3979654)CaDiCaL version: 2.1.3 % 239.16/34.52 % (3979654)Termination reason: Refutation not found, incomplete strategy % 239.16/34.52 % (3979654)Time elapsed: 0.734 s % 239.16/34.52 % (3979654)Peak memory usage: 145 MB % 239.16/34.52 % (3979654)Instructions burned: 1160 (million) % 239.16/34.52 % (3979654)------------------------------ % 239.16/34.52 % (3979654)------------------------------ % 239.16/34.52 % (3979658)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=3448321194:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2679 on theBenchmark for (2679ds/3022Mi) % 239.16/34.52 [W928 14:02:48.602687973 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602719976 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602758753 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602769603 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602794083 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602805560 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602829650 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602840873 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602866063 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602877180 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602903796 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:48.602966540 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 % (3979658)Refutation not found, incomplete strategy % 239.16/34.52 % (3979658)------------------------------ % 239.16/34.52 % (3979658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.16/34.52 % (3979658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.16/34.52 % (3979658)CaDiCaL version: 2.1.3 % 239.16/34.52 % (3979658)Termination reason: Refutation not found, incomplete strategy % 239.16/34.52 % (3979658)Time elapsed: 0.615 s % 239.16/34.52 % (3979658)Peak memory usage: 127 MB % 239.16/34.52 % (3979658)Instructions burned: 842 (million) % 239.16/34.52 % (3979652)Instruction limit reached! % 239.16/34.52 % (3979652)------------------------------ % 239.16/34.52 % (3979652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.16/34.52 % (3979652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.16/34.52 % (3979652)CaDiCaL version: 2.1.3 % 239.16/34.52 % (3979652)Termination reason: Instruction limit % 239.16/34.52 % (3979652)Termination phase: Saturation % 239.16/34.52 % (3979652)Time elapsed: 3.352 s % 239.16/34.52 % (3979652)Peak memory usage: 165 MB % 239.16/34.52 % (3979652)Instructions burned: 5812 (million) % 239.16/34.52 % (3979658)------------------------------ % 239.16/34.52 % (3979658)------------------------------ % 239.16/34.52 % (3979660)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=1694573164:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2671 on theBenchmark for (2671ds/3207Mi) % 239.16/34.52 % (3979661)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1287282357:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2670 on theBenchmark for (2670ds/3289Mi) % 239.16/34.52 % (3979656)Instruction limit reached! % 239.16/34.52 % (3979656)------------------------------ % 239.16/34.52 % (3979656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.16/34.52 % (3979656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.16/34.52 % (3979656)CaDiCaL version: 2.1.3 % 239.16/34.52 % (3979656)Termination reason: Instruction limit % 239.16/34.52 % (3979656)Termination phase: Saturation % 239.16/34.52 % (3979656)Time elapsed: 1.843 s % 239.16/34.52 % (3979656)Peak memory usage: 146 MB % 239.16/34.52 % (3979656)Instructions burned: 2967 (million) % 239.16/34.52 [W928 14:02:49.482746152 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:49.482783852 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:49.482821788 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.16/34.52 [W928 14:02:49.482834215 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. % 239.16/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482860555 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482871332 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482897692 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482923509 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482952275 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482962579 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482987542 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 [W928 14:02:49.482997622 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. % 246.10/35.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.10/35.48 % (3979664)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=4122812938:i=38569:sd=3:ss=axioms:sgt=32_2666 on theBenchmark for (2666ds/38569Mi) % 246.10/35.48 % (3979660)Refutation not found, incomplete strategy % 246.10/35.48 % (3979660)------------------------------ % 246.10/35.48 % (3979660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.10/35.48 % (3979649)Instruction limit reached! % 246.10/35.48 % (3979649)------------------------------ % 246.10/35.48 % (3979649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.10/35.48 % (3979649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.10/35.48 % (3979660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.10/35.48 % (3979649)CaDiCaL version: 2.1.3 % 246.10/35.48 % (3979660)CaDiCaL version: 2.1.3 % 246.10/35.48 % (3979649)Termination reason: Instruction limit % 246.10/35.48 % (3979649)Termination phase: Saturation % 246.10/35.48 % (3979660)Termination reason: Refutation not found, incomplete strategy % 246.10/35.48 % (3979660)Time elapsed: 0.659 s % 246.10/35.48 % (3979649)Time elapsed: 4.483 s % 246.10/35.48 % (3979649)Peak memory usage: 162 MB % 246.10/35.48 % (3979660)Peak memory usage: 128 MB % 246.10/35.48 % (3979660)Instructions burned: 845 (million) % 246.10/35.48 % (3979649)Instructions burned: 8010 (million) % 246.10/35.48 % (3979666)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=1289026723:cts=off:i=3394_2662 on theBenchmark for (2662ds/3394Mi) % 246.10/35.48 % (3979661)Refutation not found, incomplete strategy % 246.10/35.48 % (3979661)------------------------------ % 246.10/35.48 % (3979661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.67/35.82 % (3979661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.67/35.82 % (3979661)CaDiCaL version: 2.1.3 % 248.67/35.82 % (3979661)Termination reason: Refutation not found, incomplete strategy % 248.67/35.82 % (3979661)Time elapsed: 0.732 s % 248.67/35.82 % (3979661)Peak memory usage: 136 MB % 248.67/35.82 % (3979661)Instructions burned: 1170 (million) % 248.67/35.82 [W928 14:02:49.893725872 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893754242 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893796695 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893809529 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893835876 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893847592 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893874079 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893885432 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893910676 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893921936 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893946869 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.67/35.82 [W928 14:02:49.893958152 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. % 248.67/35.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 % (3979660)------------------------------ % 253.14/36.47 % (3979660)------------------------------ % 253.14/36.47 % (3979664)Refutation not found, incomplete strategy % 253.14/36.47 % (3979664)------------------------------ % 253.14/36.47 % (3979664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.14/36.47 % (3979664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.14/36.47 % (3979664)CaDiCaL version: 2.1.3 % 253.14/36.47 % (3979664)Termination reason: Refutation not found, incomplete strategy % 253.14/36.47 % (3979664)Time elapsed: 0.583 s % 253.14/36.47 % (3979664)Peak memory usage: 128 MB % 253.14/36.47 % (3979664)Instructions burned: 842 (million) % 253.14/36.47 % (3979668)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=957668698:i=33824:bd=preordered_2660 on theBenchmark for (2660ds/33824Mi) % 253.14/36.47 % (3979661)------------------------------ % 253.14/36.47 % (3979661)------------------------------ % 253.14/36.47 % (3979670)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=120444772:i=20684:bd=all:gtg=exists_sym_2658 on theBenchmark for (2658ds/20684Mi) % 253.14/36.47 % (3979664)------------------------------ % 253.14/36.47 % (3979664)------------------------------ % 253.14/36.47 % (3979672)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=1842034946:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2657 on theBenchmark for (2657ds/7222Mi) % 253.14/36.47 [W928 14:02:50.849160992 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849197115 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849236952 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849250189 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849280002 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849292212 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849319692 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849331565 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. % 253.14/36.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.14/36.47 [W928 14:02:50.849357402 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.849368899 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.849393569 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.849413469 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 % (3979191)Instruction limit reached! % 289.16/41.57 % (3979191)------------------------------ % 289.16/41.57 % (3979191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.16/41.57 % (3979191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.16/41.57 % (3979191)CaDiCaL version: 2.1.3 % 289.16/41.57 % (3979191)Termination reason: Instruction limit % 289.16/41.57 % (3979191)Termination phase: Saturation % 289.16/41.57 % (3979191)Time elapsed: 14.465 s % 289.16/41.57 % (3979191)Peak memory usage: 166 MB % 289.16/41.57 % (3979191)Instructions burned: 66099 (million) % 289.16/41.57 % (3979674)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=2601551513:st=4:i=7295:sd=4:ep=R:ss=axioms_2651 on theBenchmark for (2651ds/7295Mi) % 289.16/41.57 % (3979672)Refutation not found, incomplete strategy % 289.16/41.57 % (3979672)------------------------------ % 289.16/41.57 % (3979672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.16/41.57 % (3979672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.16/41.57 % (3979672)CaDiCaL version: 2.1.3 % 289.16/41.57 % (3979672)Termination reason: Refutation not found, incomplete strategy % 289.16/41.57 % (3979672)Time elapsed: 0.567 s % 289.16/41.57 % (3979672)Peak memory usage: 127 MB % 289.16/41.57 % (3979672)Instructions burned: 859 (million) % 289.16/41.57 [W928 14:02:50.193111366 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.193132003 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.193153341 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.193159726 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.193174712 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. % 289.16/41.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 289.16/41.57 [W928 14:02:50.193181626 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 [W928 14:02:50.193195908 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 [W928 14:02:50.193201435 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 [W928 14:02:50.193213989 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 [W928 14:02:50.193252426 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 [W928 14:02:50.193273086 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 [W928 14:02:50.193279128 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. % 295.07/42.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.07/42.36 % (3979672)------------------------------ % 295.07/42.36 % (3979672)------------------------------ % 295.07/42.36 % (3979674)Refutation not found, incomplete strategy % 295.07/42.36 % (3979674)------------------------------ % 295.07/42.36 % (3979674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.36 % (3979674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.36 % (3979674)CaDiCaL version: 2.1.3 % 295.07/42.36 % (3979674)Termination reason: Refutation not found, incomplete strategy % 295.07/42.36 % (3979674)Time elapsed: 0.308 s % 295.07/42.36 % (3979674)Peak memory usage: 128 MB % 295.07/42.36 % (3979674)Instructions burned: 844 (million) % 295.07/42.36 % (3979676)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=1935295765:i=4036:ins=10_2647 on theBenchmark for (2647ds/4036Mi) % 295.07/42.36 % (3979674)------------------------------ % 295.07/42.36 % (3979674)------------------------------ % 295.07/42.36 % (3979678)lrs+10_1_sil=128000:lcm=predicate:random_seed=2533163451:st=3:i=43697:sd=5:ss=axioms_2645 on theBenchmark for (2645ds/43697Mi) % 295.07/42.36 % (3979678)Refutation not found, incomplete strategy % 295.07/42.36 % (3979678)------------------------------ % 295.07/42.36 % (3979678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.07/42.36 % (3979678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.07/42.36 % (3979678)CaDiCaL version: 2.1.3 % 295.07/42.36 % (3979678)Termination reason: Refutation not found, incomplete strategy % 295.07/42.36 % (3979678)Time elapsed: 0.002 s % 295.07/42.36 % (3979678)Peak memory usage: 87 MB % 295.07/42.36 % (3979678)Instructions burned: 6 (million) % 295.07/42.36 % (3979678)------------------------------ % 295.07/42.36 % (3979678)------------------------------ % 295.07/42.36 % (3979680)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=3103291377:i=17599:gtg=all:ss=axioms:fsd=on_2643 on theBenchmark for (2643ds/17599Mi) % 295.07/42.36 % (3979666)Instruction limit reached! % 295.07/42.36 % (3979666)------------------------------ % 295.07/42.36 % (3979666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.82/42.80 % (3979666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.82/42.80 % (3979666)CaDiCaL version: 2.1.3 % 297.82/42.80 % (3979666)Termination reason: Instruction limit % 297.82/42.80 % (3979666)Termination phase: Saturation % 297.82/42.80 % (3979666)Time elapsed: 1.962 s % 297.82/42.80 % (3979666)Peak memory usage: 147 MB % 297.82/42.80 % (3979666)Instructions burned: 3396 (million) % 297.82/42.80 % (3979682)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=2026015193:i=4547:bd=preordered_2641 on theBenchmark for (2641ds/4547Mi) % 297.82/42.80 % (3979676)Instruction limit reached! % 297.82/42.80 % (3979676)------------------------------ % 297.82/42.80 % (3979676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.82/42.80 % (3979676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.82/42.80 % (3979676)CaDiCaL version: 2.1.3 % 297.82/42.80 % (3979676)Termination reason: Instruction limit % 297.82/42.80 % (3979676)Termination phase: Saturation % 297.82/42.80 % (3979676)Time elapsed: 2.219 s % 297.82/42.80 % (3979676)Peak memory usage: 145 MB % 297.82/42.80 % (3979676)Instructions burned: 4036 (million) % 297.82/42.80 % (3979684)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=1142350717:i=9294:av=off_2623 on theBenchmark for (2623ds/9294Mi) % 297.82/42.80 % (3979682)Instruction limit reached! % 297.82/42.80 % (3979682)------------------------------ % 297.82/42.80 % (3979682)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.82/42.80 % (3979682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.82/42.80 % (3979682)CaDiCaL version: 2.1.3 % 297.82/42.80 % (3979682)Termination reason: Instruction limit % 297.82/42.80 % (3979682)Termination phase: Saturation % 297.82/42.80 % (3979682)Time elapsed: 2.863 s % 297.82/42.80 % (3979682)Peak memory usage: 168 MB % 297.82/42.80 % (3979682)Instructions burned: 4549 (million) % 297.82/42.80 % (3979732)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1934071931:i=32849:add=on_2611 on theBenchmark for (2611ds/32849Mi) % 297.82/42.80 % (3979680)Instruction limit reached! % 297.82/42.80 % (3979680)------------------------------ % 297.82/42.80 % (3979680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 297.82/42.80 % (3979680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 297.82/42.80 % (3979680)CaDiCaL version: 2.1.3 % 297.82/42.80 % (3979680)Termination reason: Instruction limit % 297.82/42.80 % (3979680)Termination phase: Saturation % 297.82/42.80 % (3979680)Time elapsed: 4.876 s % 297.82/42.80 % (3979680)Peak memory usage: 180 MB % 297.82/42.80 % (3979680)Instructions burned: 17600 (million) % 297.82/42.80 % (3980031)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=277637392:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2593 on theBenchmark for (2593ds/4793Mi) % 297.82/42.80 [W928 14:02:56.941257535 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. % 297.82/42.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 297.82/42.80 [W928 14:02:56.941304558 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. % 297.82/42.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 297.82/42.80 [W928 14:02:56.941325423 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. % 297.82/42.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 297.82/42.80 [W928 14:02:56.941331803 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. % 297.82/42.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 297.82/42.80 [W928 14:02:56.941344894 register_special_ops.cpp:225] WTerminated %------------------------------------------------------------------------------