%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW478_20 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n010.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:37 PM UTC 2026 % Result : Timeout 291.91s 42.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW478_20 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.17 % Computer : n010.cluster.edu % 0.07/0.17 % Model : x86_64 x86_64 % 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.17 % Memory : 8046.5625MB % 0.07/0.17 % OS : Linux 6.8.0-71-generic % 0.07/0.17 % CPULimit : 300 % 0.07/0.17 % WCLimit : 300 % 0.07/0.17 % DateTime : Mon Sep 28 14:14:17 UTC 2026 % 0.07/0.18 % CPUTime : % 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.21 Running first-order theorem proving % 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 10.76/2.27 % (1943707)Detected formulas, will run a generic FOF schedule. % 10.76/2.27 % (1943712)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=2402107087:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.76/2.27 % (1943717)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3270224635:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.76/2.27 % (1943716)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2585167881:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.76/2.27 % (1943715)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4223157979:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.76/2.27 % (1943714)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=1744926742:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.76/2.27 % (1943718)dis-21_1_sil=8000:lcm=predicate:random_seed=1096226774:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 10.76/2.27 % (1943713)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=3411017983:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.76/2.27 % (1943716)Refutation not found, incomplete strategy % 10.76/2.27 % (1943716)------------------------------ % 10.76/2.27 % (1943716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.27 % (1943716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.27 % (1943715)Refutation not found, incomplete strategy % 10.76/2.27 % (1943715)------------------------------ % 10.76/2.27 % (1943715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.27 % (1943716)CaDiCaL version: 2.1.3 % 10.76/2.27 % (1943716)Termination reason: Refutation not found, incomplete strategy % 10.76/2.27 % (1943716)Time elapsed: 0.004 s % 10.76/2.27 % (1943716)Peak memory usage: 87 MB % 10.76/2.27 % (1943715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.27 % (1943716)Instructions burned: 5 (million) % 10.76/2.27 % (1943715)CaDiCaL version: 2.1.3 % 10.76/2.27 % (1943715)Termination reason: Refutation not found, incomplete strategy % 10.76/2.27 % (1943715)Time elapsed: 0.004 s % 10.76/2.27 % (1943715)Peak memory usage: 88 MB % 10.76/2.27 % (1943715)Instructions burned: 5 (million) % 10.76/2.27 % (1943718)Instruction limit reached! % 10.76/2.27 % (1943718)------------------------------ % 10.76/2.27 % (1943718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.27 % (1943718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.27 % (1943718)CaDiCaL version: 2.1.3 % 10.76/2.27 % (1943718)Termination reason: Instruction limit % 10.76/2.27 % (1943718)Termination phase: Saturation % 10.76/2.27 % (1943718)Time elapsed: 0.068 s % 10.76/2.27 % (1943718)Peak memory usage: 91 MB % 10.76/2.27 % (1943718)Instructions burned: 130 (million) % 10.76/2.27 % (1943717)Instruction limit reached! % 10.76/2.27 % (1943717)------------------------------ % 10.76/2.27 % (1943717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.27 % (1943717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.76/2.27 % (1943717)CaDiCaL version: 2.1.3 % 10.76/2.27 % (1943717)Termination reason: Instruction limit % 10.76/2.27 % (1943717)Termination phase: Saturation % 10.76/2.27 % (1943717)Time elapsed: 0.073 s % 10.76/2.27 % (1943717)Peak memory usage: 91 MB % 10.76/2.27 % (1943717)Instructions burned: 140 (million) % 10.76/2.27 % (1943727)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4173951705:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi) % 10.76/2.27 % (1943726)lrs+10_1_sil=8000:sp=occurrence:random_seed=2568022390:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi) % 10.76/2.27 % (1943715)------------------------------ % 10.76/2.27 % (1943715)------------------------------ % 10.76/2.27 % (1943716)------------------------------ % 10.76/2.27 % (1943716)------------------------------ % 10.76/2.27 % (1943726)Refutation not found, incomplete strategy % 10.76/2.27 % (1943726)------------------------------ % 10.76/2.27 % (1943726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.76/2.27 % (1943726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.49 % (1943726)CaDiCaL version: 2.1.3 % 12.09/2.49 % (1943726)Termination reason: Refutation not found, incomplete strategy % 12.09/2.49 % (1943726)Time elapsed: 0.004 s % 12.09/2.49 % (1943726)Peak memory usage: 88 MB % 12.09/2.49 % (1943726)Instructions burned: 4 (million) % 12.09/2.49 % (1943727)Refutation not found, incomplete strategy % 12.09/2.49 % (1943727)------------------------------ % 12.09/2.49 % (1943727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.49 % (1943727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.49 % (1943727)CaDiCaL version: 2.1.3 % 12.09/2.49 % (1943727)Termination reason: Refutation not found, incomplete strategy % 12.09/2.49 % (1943727)Time elapsed: 0.010 s % 12.09/2.49 % (1943727)Peak memory usage: 88 MB % 12.09/2.49 % (1943727)Instructions burned: 19 (million) % 12.09/2.49 % (1943731)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=944309747:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 12.09/2.49 % (1943730)lrs+1011_1_sil=32000:sp=occurrence:random_seed=588498955:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 12.09/2.49 % (1943730)Refutation not found, incomplete strategy % 12.09/2.49 % (1943730)------------------------------ % 12.09/2.49 % (1943730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.49 % (1943730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.49 % (1943730)CaDiCaL version: 2.1.3 % 12.09/2.49 % (1943730)Termination reason: Refutation not found, incomplete strategy % 12.09/2.49 % (1943730)Time elapsed: 0.004 s % 12.09/2.49 % (1943730)Peak memory usage: 88 MB % 12.09/2.49 % (1943730)Instructions burned: 4 (million) % 12.09/2.49 % (1943726)------------------------------ % 12.09/2.49 % (1943726)------------------------------ % 12.09/2.49 % (1943727)------------------------------ % 12.09/2.49 % (1943727)------------------------------ % 12.09/2.49 % (1943731)Instruction limit reached! % 12.09/2.49 % (1943731)------------------------------ % 12.09/2.49 % (1943731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.49 % (1943731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.49 % (1943731)CaDiCaL version: 2.1.3 % 12.09/2.49 % (1943731)Termination reason: Instruction limit % 12.09/2.49 % (1943731)Termination phase: Saturation % 12.09/2.49 % (1943731)Time elapsed: 0.145 s % 12.09/2.49 % (1943731)Peak memory usage: 93 MB % 12.09/2.49 % (1943731)Instructions burned: 248 (million) % 12.09/2.49 % (1943735)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3708648251:i=2350_2992 on theBenchmark for (2992ds/2350Mi) % 12.09/2.49 % (1943734)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=114814238:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi) % 12.09/2.49 % (1943730)------------------------------ % 12.09/2.49 % (1943730)------------------------------ % 12.09/2.49 % (1943734)Refutation not found, incomplete strategy % 12.09/2.49 % (1943734)------------------------------ % 12.09/2.49 % (1943734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.49 % (1943734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.49 % (1943734)CaDiCaL version: 2.1.3 % 12.09/2.49 % (1943734)Termination reason: Refutation not found, incomplete strategy % 12.09/2.49 % (1943734)Time elapsed: 0.005 s % 12.09/2.49 % (1943734)Peak memory usage: 87 MB % 12.09/2.49 % (1943734)Instructions burned: 6 (million) % 12.09/2.49 % (1943736)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=597194678:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 12.09/2.49 % (1943714)Refutation not found, incomplete strategy % 12.09/2.49 % (1943714)------------------------------ % 12.09/2.49 % (1943714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.49 % (1943714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.49 % (1943714)CaDiCaL version: 2.1.3 % 12.09/2.49 % (1943714)Termination reason: Refutation not found, incomplete strategy % 12.09/2.49 % (1943714)Time elapsed: 0.783 s % 12.09/2.49 % (1943714)Peak memory usage: 150 MB % 12.09/2.49 % (1943714)Instructions burned: 1209 (million) % 12.09/2.49 % (1943736)Instruction limit reached! % 12.09/2.49 % (1943736)------------------------------ % 12.09/2.49 % (1943736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.09/2.83 % (1943736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.09/2.83 % (1943736)CaDiCaL version: 2.1.3 % 14.09/2.83 % (1943736)Termination reason: Instruction limit % 14.09/2.83 % (1943736)Termination phase: Saturation % 14.09/2.83 % (1943736)Time elapsed: 0.059 s % 14.09/2.83 % (1943736)Peak memory usage: 91 MB % 14.09/2.83 % (1943736)Instructions burned: 114 (million) % 14.09/2.83 % (1943739)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2509794937:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi) % 14.09/2.83 % (1943739)Refutation not found, incomplete strategy % 14.09/2.83 % (1943739)------------------------------ % 14.09/2.83 % (1943739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.09/2.83 % (1943739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.09/2.83 % (1943739)CaDiCaL version: 2.1.3 % 14.09/2.83 % (1943739)Termination reason: Refutation not found, incomplete strategy % 14.09/2.83 % (1943739)Time elapsed: 0.039 s % 14.09/2.83 % (1943739)Peak memory usage: 90 MB % 14.09/2.83 % (1943739)Instructions burned: 77 (million) % 14.09/2.83 % (1943734)------------------------------ % 14.09/2.83 % (1943734)------------------------------ % 14.09/2.83 % (1943741)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1568709528:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi) % 14.09/2.83 % (1943741)Instruction limit reached! % 14.09/2.83 % (1943741)------------------------------ % 14.09/2.83 % (1943741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.09/2.83 % (1943741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.09/2.83 % (1943741)CaDiCaL version: 2.1.3 % 14.09/2.83 % (1943741)Termination reason: Instruction limit % 14.09/2.83 % (1943741)Termination phase: Saturation % 14.09/2.83 % (1943741)Time elapsed: 0.058 s % 14.09/2.83 % (1943741)Peak memory usage: 91 MB % 14.09/2.83 % (1943741)Instructions burned: 114 (million) % 14.09/2.83 % (1943714)------------------------------ % 14.09/2.83 % (1943714)------------------------------ % 14.09/2.83 % (1943743)lrs+10_1_sil=8000:sp=occurrence:random_seed=1398268444:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi) % 14.09/2.83 % (1943743)Refutation not found, incomplete strategy % 14.09/2.83 % (1943743)------------------------------ % 14.09/2.83 % (1943743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.09/2.83 % (1943743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.09/2.83 % (1943743)CaDiCaL version: 2.1.3 % 14.09/2.83 % (1943743)Termination reason: Refutation not found, incomplete strategy % 14.09/2.83 % (1943743)Time elapsed: 0.004 s % 14.09/2.83 % (1943743)Peak memory usage: 88 MB % 14.09/2.83 % (1943743)Instructions burned: 5 (million) % 14.09/2.83 % (1943739)------------------------------ % 14.09/2.83 % (1943739)------------------------------ % 14.09/2.83 % (1943745)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=770581969:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi) % 14.09/2.83 % (1943746)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3995336659:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi) % 14.09/2.83 % (1943745)Refutation not found, incomplete strategy % 14.09/2.83 % (1943745)------------------------------ % 14.09/2.83 % (1943745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.09/2.83 % (1943745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.09/2.83 % (1943745)CaDiCaL version: 2.1.3 % 14.09/2.83 % (1943745)Termination reason: Refutation not found, incomplete strategy % 14.09/2.83 % (1943745)Time elapsed: 0.059 s % 14.09/2.83 % (1943745)Peak memory usage: 92 MB % 14.09/2.83 % (1943745)Instructions burned: 109 (million) % 14.09/2.83 % (1943748)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=541375563:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi) % 14.09/2.83 % (1943743)------------------------------ % 14.09/2.83 % (1943743)------------------------------ % 14.09/2.83 % (1943748)Instruction limit reached! % 14.09/2.83 % (1943748)------------------------------ % 14.09/2.83 % (1943748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.09/2.83 % (1943748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.09/2.83 % (1943748)CaDiCaL version: 2.1.3 % 14.09/2.83 % (1943748)Termination reason: Instruction limit % 13.67/3.00 % (1943748)Termination phase: Saturation % 13.67/3.00 % (1943748)Time elapsed: 0.071 s % 13.67/3.00 % (1943748)Peak memory usage: 91 MB % 13.67/3.00 % (1943748)Instructions burned: 134 (million) % 13.67/3.00 % (1943752)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=418312494:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi) % 13.67/3.00 % (1943752)Refutation not found, incomplete strategy % 13.67/3.00 % (1943752)------------------------------ % 13.67/3.00 % (1943752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.67/3.00 % (1943752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.67/3.00 % (1943752)CaDiCaL version: 2.1.3 % 13.67/3.00 % (1943752)Termination reason: Refutation not found, incomplete strategy % 13.67/3.00 % (1943752)Time elapsed: 0.005 s % 13.67/3.00 % (1943752)Peak memory usage: 88 MB % 13.67/3.00 % (1943752)Instructions burned: 6 (million) % 13.67/3.00 % (1943745)------------------------------ % 13.67/3.00 % (1943745)------------------------------ % 13.67/3.00 % (1943753)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=710507687:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi) % 13.67/3.00 [W928 14:14:20.699263013 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699309156 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699349320 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699361753 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699387017 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699404390 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699430677 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699445350 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699469787 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/3.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.67/3.00 [W928 14:14:20.699482807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.699508374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.699519600 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 % (1943755)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=1869479806:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi) % 19.10/3.50 % (1943755)Refutation not found, incomplete strategy % 19.10/3.50 % (1943755)------------------------------ % 19.10/3.50 % (1943755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.10/3.50 % (1943755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.10/3.50 % (1943755)CaDiCaL version: 2.1.3 % 19.10/3.50 % (1943755)Termination reason: Refutation not found, incomplete strategy % 19.10/3.50 % (1943755)Time elapsed: 0.012 s % 19.10/3.50 % (1943755)Peak memory usage: 89 MB % 19.10/3.50 % (1943755)Instructions burned: 23 (million) % 19.10/3.50 % (1943752)------------------------------ % 19.10/3.50 % (1943752)------------------------------ % 19.10/3.50 % (1943746)Refutation not found, incomplete strategy % 19.10/3.50 % (1943746)------------------------------ % 19.10/3.50 % (1943746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.10/3.50 % (1943746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.10/3.50 % (1943746)CaDiCaL version: 2.1.3 % 19.10/3.50 % (1943746)Termination reason: Refutation not found, incomplete strategy % 19.10/3.50 % (1943746)Time elapsed: 0.578 s % 19.10/3.50 % (1943746)Peak memory usage: 130 MB % 19.10/3.50 % (1943746)Instructions burned: 855 (million) % 19.10/3.50 % (1943758)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1594883613:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi) % 19.10/3.50 % (1943755)------------------------------ % 19.10/3.50 % (1943755)------------------------------ % 19.10/3.50 [W928 14:14:20.039070654 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.039104128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.039144578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.039158575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.039186565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.10/3.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.10/3.50 [W928 14:14:20.039198891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 [W928 14:14:20.039225845 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 [W928 14:14:20.039239598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 [W928 14:14:20.039263772 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 [W928 14:14:20.039274528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 [W928 14:14:20.039298272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 [W928 14:14:20.039309292 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.56/5.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.56/5.41 % (1943758)Instruction limit reached! % 33.56/5.41 % (1943758)------------------------------ % 33.56/5.41 % (1943758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.56/5.41 % (1943758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.56/5.41 % (1943758)CaDiCaL version: 2.1.3 % 33.56/5.41 % (1943758)Termination reason: Instruction limit % 33.56/5.41 % (1943758)Termination phase: Saturation % 33.56/5.41 % (1943758)Time elapsed: 0.063 s % 33.56/5.41 % (1943758)Peak memory usage: 91 MB % 33.56/5.41 % (1943758)Instructions burned: 135 (million) % 33.56/5.41 % (1943735)Instruction limit reached! % 33.56/5.41 % (1943735)------------------------------ % 33.56/5.41 % (1943735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.56/5.41 % (1943735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.56/5.41 % (1943735)CaDiCaL version: 2.1.3 % 33.56/5.41 % (1943735)Termination reason: Instruction limit % 33.56/5.41 % (1943735)Termination phase: Saturation % 33.56/5.41 % (1943735)Time elapsed: 1.330 s % 33.56/5.41 % (1943735)Peak memory usage: 152 MB % 33.56/5.41 % (1943735)Instructions burned: 2352 (million) % 33.56/5.41 % (1943746)------------------------------ % 33.56/5.41 % (1943746)------------------------------ % 33.56/5.41 % (1943760)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4071712225:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi) % 33.56/5.41 % (1943760)Refutation not found, incomplete strategy % 33.56/5.41 % (1943760)------------------------------ % 33.56/5.41 % (1943760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.56/5.41 % (1943760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.56/5.41 % (1943760)CaDiCaL version: 2.1.3 % 33.56/5.41 % (1943760)Termination reason: Refutation not found, incomplete strategy % 33.56/5.41 % (1943760)Time elapsed: 0.004 s % 33.56/5.41 % (1943760)Peak memory usage: 88 MB % 33.56/5.41 % (1943760)Instructions burned: 5 (million) % 33.56/5.41 % (1943761)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3425971279:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 33.56/5.41 % (1943761)Refutation not found, incomplete strategy % 33.56/5.41 % (1943761)------------------------------ % 34.24/5.59 % (1943761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.24/5.59 % (1943761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.24/5.59 % (1943761)CaDiCaL version: 2.1.3 % 34.24/5.59 % (1943761)Termination reason: Refutation not found, incomplete strategy % 34.24/5.59 % (1943761)Time elapsed: 0.004 s % 34.24/5.59 % (1943761)Peak memory usage: 88 MB % 34.24/5.59 % (1943761)Instructions burned: 4 (million) % 34.24/5.59 % (1943753)Refutation not found, incomplete strategy % 34.24/5.59 % (1943753)------------------------------ % 34.24/5.59 % (1943753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.24/5.59 % (1943753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.24/5.59 % (1943753)CaDiCaL version: 2.1.3 % 34.24/5.59 % (1943753)Termination reason: Refutation not found, incomplete strategy % 34.24/5.59 % (1943753)Time elapsed: 0.584 s % 34.24/5.59 % (1943753)Peak memory usage: 130 MB % 34.24/5.59 % (1943753)Instructions burned: 855 (million) % 34.24/5.59 % (1943762)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=550435857:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi) % 34.24/5.59 % (1943763)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=3526821047:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi) % 34.24/5.59 % (1943763)Instruction limit reached! % 34.24/5.59 % (1943763)------------------------------ % 34.24/5.59 % (1943763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.24/5.59 % (1943763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.24/5.59 % (1943763)CaDiCaL version: 2.1.3 % 34.24/5.59 % (1943763)Termination reason: Instruction limit % 34.24/5.59 % (1943763)Termination phase: Saturation % 34.24/5.59 % (1943763)Time elapsed: 0.083 s % 34.24/5.59 % (1943763)Peak memory usage: 92 MB % 34.24/5.59 % (1943763)Instructions burned: 151 (million) % 34.24/5.59 % (1943760)------------------------------ % 34.24/5.59 % (1943760)------------------------------ % 34.24/5.59 % (1943761)------------------------------ % 34.24/5.59 % (1943761)------------------------------ % 34.24/5.59 % (1943753)------------------------------ % 34.24/5.59 % (1943753)------------------------------ % 34.24/5.59 % (1943768)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=4207311371:i=14155:bd=all_2974 on theBenchmark for (2974ds/14155Mi) % 34.24/5.59 % (1943769)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3214402195:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi) % 34.24/5.59 % (1943770)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=695891444:s2a=on:i=185:s2at=1.8:fdi=4_2974 on theBenchmark for (2974ds/185Mi) % 34.24/5.59 % (1943769)Refutation not found, incomplete strategy % 34.24/5.59 % (1943769)------------------------------ % 34.24/5.59 % (1943769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.24/5.59 % (1943769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.24/5.59 % (1943769)CaDiCaL version: 2.1.3 % 34.24/5.59 % (1943769)Termination reason: Refutation not found, incomplete strategy % 34.24/5.59 % (1943769)Time elapsed: 0.063 s % 34.24/5.59 % (1943769)Peak memory usage: 92 MB % 34.24/5.59 % (1943769)Instructions burned: 119 (million) % 34.24/5.59 % (1943771)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2236457594:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2973 on theBenchmark for (2973ds/193Mi) % 34.24/5.59 % (1943771)Refutation not found, incomplete strategy % 34.24/5.59 % (1943771)------------------------------ % 34.24/5.59 % (1943771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.24/5.59 % (1943771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.24/5.59 % (1943771)CaDiCaL version: 2.1.3 % 34.24/5.59 % (1943771)Termination reason: Refutation not found, incomplete strategy % 34.24/5.59 % (1943771)Time elapsed: 0.007 s % 34.24/5.59 % (1943771)Peak memory usage: 88 MB % 34.24/5.59 % (1943771)Instructions burned: 8 (million) % 34.24/5.59 % (1943770)Instruction limit reached! % 34.24/5.59 % (1943770)------------------------------ % 34.24/5.59 % (1943770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.10/7.11 % (1943770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.10/7.11 % (1943770)CaDiCaL version: 2.1.3 % 45.10/7.11 % (1943770)Termination reason: Instruction limit % 45.10/7.11 % (1943770)Termination phase: Saturation % 45.10/7.11 % (1943770)Time elapsed: 0.097 s % 45.10/7.11 % (1943770)Peak memory usage: 93 MB % 45.10/7.11 % (1943770)Instructions burned: 185 (million) % 45.10/7.11 % (1943769)------------------------------ % 45.10/7.11 % (1943769)------------------------------ % 45.10/7.11 % (1943776)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2319784480:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi) % 45.10/7.11 % (1943771)------------------------------ % 45.10/7.11 % (1943771)------------------------------ % 45.10/7.11 % (1943776)Refutation not found, incomplete strategy % 45.10/7.11 % (1943776)------------------------------ % 45.10/7.11 % (1943776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.10/7.11 % (1943776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.10/7.11 % (1943776)CaDiCaL version: 2.1.3 % 45.10/7.11 % (1943776)Termination reason: Refutation not found, incomplete strategy % 45.10/7.11 % (1943776)Time elapsed: 0.046 s % 45.10/7.11 % (1943776)Peak memory usage: 90 MB % 45.10/7.11 % (1943776)Instructions burned: 87 (million) % 45.10/7.11 % (1943778)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3770747379:i=12111:sd=1:ss=included_2969 on theBenchmark for (2969ds/12111Mi) % 45.10/7.11 % (1943779)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=245760064:i=319:kws=precedence:fsr=off_2969 on theBenchmark for (2969ds/319Mi) % 45.10/7.11 % (1943776)------------------------------ % 45.10/7.11 % (1943776)------------------------------ % 45.10/7.11 % (1943779)Instruction limit reached! % 45.10/7.11 % (1943779)------------------------------ % 45.10/7.11 % (1943779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.10/7.11 % (1943779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.10/7.11 % (1943779)CaDiCaL version: 2.1.3 % 45.10/7.11 % (1943779)Termination reason: Instruction limit % 45.10/7.11 % (1943779)Termination phase: Saturation % 45.10/7.11 % (1943779)Time elapsed: 0.168 s % 45.10/7.11 % (1943779)Peak memory usage: 94 MB % 45.10/7.11 % (1943779)Instructions burned: 319 (million) % 45.10/7.11 % (1943782)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=740815421:i=2064:ep=RST_2966 on theBenchmark for (2966ds/2064Mi) % 45.10/7.11 % (1943783)dis-1011_128_sil=32000:random_seed=3426046213:i=3706:ep=RST:av=off_2966 on theBenchmark for (2966ds/3706Mi) % 45.10/7.11 % (1943782)Refutation not found, incomplete strategy % 45.10/7.11 % (1943782)------------------------------ % 45.10/7.11 % (1943782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.10/7.11 % (1943782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.10/7.11 % (1943782)CaDiCaL version: 2.1.3 % 45.10/7.11 % (1943782)Termination reason: Refutation not found, incomplete strategy % 45.10/7.11 % (1943782)Time elapsed: 0.052 s % 45.10/7.11 % (1943782)Peak memory usage: 91 MB % 45.10/7.11 % (1943782)Instructions burned: 107 (million) % 45.10/7.11 % (1943782)------------------------------ % 45.10/7.11 % (1943782)------------------------------ % 45.10/7.11 % (1943786)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2982307815:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2962 on theBenchmark for (2962ds/757Mi) % 45.10/7.11 % (1943786)Refutation not found, incomplete strategy % 45.10/7.11 % (1943786)------------------------------ % 45.10/7.11 % (1943786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.10/7.11 % (1943786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.10/7.11 % (1943786)CaDiCaL version: 2.1.3 % 45.10/7.11 % (1943786)Termination reason: Refutation not found, incomplete strategy % 45.10/7.11 % (1943786)Time elapsed: 0.017 s % 45.10/7.11 % (1943786)Peak memory usage: 88 MB % 45.10/7.11 % (1943786)Instructions burned: 4 (million) % 45.10/7.11 % (1943786)------------------------------ % 45.10/7.11 % (1943786)------------------------------ % 45.10/7.11 % (1943788)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1312576765:i=13913:ss=axioms:sgt=8_2957 on theBenchmark for (2957ds/13913Mi) % 45.10/7.11 [W928 14:14:23.624654904 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.624771721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.624837594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.624872681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.624919371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.624951048 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.624997198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.625040945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.625094858 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.625127385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.625171845 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 [W928 14:14:23.625202939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.74/7.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.74/7.17 % (1943788)Refutation not found, incomplete strategy % 45.74/7.17 % (1943788)------------------------------ % 45.74/7.17 % (1943788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.74/7.17 % (1943788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.74/7.17 % (1943788)CaDiCaL version: 2.1.3 % 45.74/7.17 % (1943788)Termination reason: Refutation not found, incomplete strategy % 62.52/9.54 % (1943788)Time elapsed: 0.559 s % 62.52/9.54 % (1943788)Peak memory usage: 130 MB % 62.52/9.54 % (1943788)Instructions burned: 854 (million) % 62.52/9.54 % (1943788)------------------------------ % 62.52/9.54 % (1943788)------------------------------ % 62.52/9.54 % (1943790)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4278432497:i=9925:aac=none_2948 on theBenchmark for (2948ds/9925Mi) % 62.52/9.54 % (1943783)Instruction limit reached! % 62.52/9.54 % (1943783)------------------------------ % 62.52/9.54 % (1943783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.52/9.54 % (1943783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.52/9.54 % (1943783)CaDiCaL version: 2.1.3 % 62.52/9.54 % (1943783)Termination reason: Instruction limit % 62.52/9.54 % (1943783)Termination phase: Saturation % 62.52/9.54 % (1943783)Time elapsed: 1.957 s % 62.52/9.54 % (1943783)Peak memory usage: 105 MB % 62.52/9.54 % (1943783)Instructions burned: 3707 (million) % 62.52/9.54 % (1943792)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=865013646:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2945 on theBenchmark for (2945ds/2479Mi) % 62.52/9.54 % (1943792)Refutation not found, incomplete strategy % 62.52/9.54 % (1943792)------------------------------ % 62.52/9.54 % (1943792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.52/9.54 % (1943792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.52/9.54 % (1943792)CaDiCaL version: 2.1.3 % 62.52/9.54 % (1943792)Termination reason: Refutation not found, incomplete strategy % 62.52/9.54 % (1943792)Time elapsed: 0.006 s % 62.52/9.54 % (1943792)Peak memory usage: 88 MB % 62.52/9.54 % (1943792)Instructions burned: 8 (million) % 62.52/9.54 % (1943762)Instruction limit reached! % 62.52/9.54 % (1943762)------------------------------ % 62.52/9.54 % (1943762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.52/9.54 % (1943762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.52/9.54 % (1943762)CaDiCaL version: 2.1.3 % 62.52/9.54 % (1943762)Termination reason: Instruction limit % 62.52/9.54 % (1943762)Termination phase: Saturation % 62.52/9.54 % (1943762)Time elapsed: 3.364 s % 62.52/9.54 % (1943762)Peak memory usage: 155 MB % 62.52/9.54 % (1943762)Instructions burned: 6062 (million) % 62.52/9.54 % (1943792)------------------------------ % 62.52/9.54 % (1943792)------------------------------ % 62.52/9.54 % (1943794)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=244967927:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2942 on theBenchmark for (2942ds/440Mi) % 62.52/9.54 % (1943795)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1356902854:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2941 on theBenchmark for (2941ds/11145Mi) % 62.52/9.54 % (1943790)Refutation not found, incomplete strategy % 62.52/9.54 % (1943790)------------------------------ % 62.52/9.54 % (1943790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.52/9.54 % (1943790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.52/9.54 % (1943790)CaDiCaL version: 2.1.3 % 62.52/9.54 % (1943790)Termination reason: Refutation not found, incomplete strategy % 62.52/9.54 % (1943790)Time elapsed: 0.751 s % 62.52/9.54 % (1943790)Peak memory usage: 154 MB % 62.52/9.54 % (1943790)Instructions burned: 1162 (million) % 62.52/9.54 % (1943794)Instruction limit reached! % 62.52/9.54 % (1943794)------------------------------ % 62.52/9.54 % (1943794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.52/9.54 % (1943794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.52/9.54 % (1943794)CaDiCaL version: 2.1.3 % 62.52/9.54 % (1943794)Termination reason: Instruction limit % 62.52/9.54 % (1943794)Termination phase: Saturation % 62.52/9.54 % (1943794)Time elapsed: 0.244 s % 62.52/9.54 % (1943794)Peak memory usage: 96 MB % 62.52/9.54 % (1943794)Instructions burned: 441 (million) % 62.52/9.54 % (1943790)------------------------------ % 62.52/9.54 % (1943790)------------------------------ % 62.52/9.54 % (1943798)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=379736450:cts=off:i=3034:av=off:er=known:fsd=on_2938 on theBenchmark for (2938ds/3034Mi) % 62.52/9.54 [W928 14:14:24.325331885 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325369842 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325410505 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325423055 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325448696 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325459009 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325483312 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325493462 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325517209 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325527366 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325552209 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 [W928 14:14:24.325562323 register_special_ops.cpp:225] Warning: Creating a tensor from 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.39/10.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.39/10.09 % (1943800)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1499850773:st=2:s2a=on:i=524:s2at=2:ss=axioms_2936 on theBenchmark for (2936ds/524Mi) % 66.39/10.09 % (1943800)Refutation not found, incomplete strategy % 66.39/10.09 % (1943800)------------------------------ % 66.39/10.09 % (1943800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.39/10.09 % (1943800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.83/10.84 % (1943800)CaDiCaL version: 2.1.3 % 70.83/10.84 % (1943800)Termination reason: Refutation not found, incomplete strategy % 70.83/10.84 % (1943800)Time elapsed: 0.008 s % 70.83/10.84 % (1943800)Peak memory usage: 88 MB % 70.83/10.84 % (1943800)Instructions burned: 12 (million) % 70.83/10.84 % (1943795)Refutation not found, incomplete strategy % 70.83/10.84 % (1943795)------------------------------ % 70.83/10.84 % (1943795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.83/10.84 % (1943795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.83/10.84 % (1943795)CaDiCaL version: 2.1.3 % 70.83/10.84 % (1943795)Termination reason: Refutation not found, incomplete strategy % 70.83/10.84 % (1943795)Time elapsed: 0.580 s % 70.83/10.84 % (1943795)Peak memory usage: 130 MB % 70.83/10.84 % (1943795)Instructions burned: 858 (million) % 70.83/10.84 % (1943800)------------------------------ % 70.83/10.84 % (1943800)------------------------------ % 70.83/10.84 % (1943795)------------------------------ % 70.83/10.84 % (1943795)------------------------------ % 70.83/10.84 % (1943802)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1411905690:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2932 on theBenchmark for (2932ds/1016Mi) % 70.83/10.84 % (1943802)Refutation not found, incomplete strategy % 70.83/10.84 % (1943802)------------------------------ % 70.83/10.84 % (1943802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.83/10.84 % (1943802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.83/10.84 % (1943802)CaDiCaL version: 2.1.3 % 70.83/10.84 % (1943802)Termination reason: Refutation not found, incomplete strategy % 70.83/10.84 % (1943802)Time elapsed: 0.004 s % 70.83/10.84 % (1943802)Peak memory usage: 88 MB % 70.83/10.84 % (1943802)Instructions burned: 5 (million) % 70.83/10.84 % (1943803)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2725197777:i=14123:bd=preordered:ins=4_2931 on theBenchmark for (2931ds/14123Mi) % 70.83/10.84 % (1943802)------------------------------ % 70.83/10.84 % (1943802)------------------------------ % 70.83/10.84 % (1943806)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3447021055:i=5781:kws=precedence:bd=all:rawr=on_2928 on theBenchmark for (2928ds/5781Mi) % 70.83/10.84 % (1943778)Instruction limit reached! % 70.83/10.84 % (1943778)------------------------------ % 70.83/10.84 % (1943778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.83/10.84 % (1943778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.83/10.84 % (1943778)CaDiCaL version: 2.1.3 % 70.83/10.84 % (1943778)Termination reason: Instruction limit % 70.83/10.84 % (1943778)Termination phase: Saturation % 70.83/10.84 % (1943778)Time elapsed: 4.811 s % 70.83/10.84 % (1943778)Peak memory usage: 143 MB % 70.83/10.84 % (1943778)Instructions burned: 12114 (million) % 70.83/10.84 % (1943798)Instruction limit reached! % 70.83/10.84 % (1943798)------------------------------ % 70.83/10.84 % (1943798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.83/10.84 % (1943798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.83/10.84 % (1943798)CaDiCaL version: 2.1.3 % 70.83/10.84 % (1943798)Termination reason: Instruction limit % 70.83/10.84 % (1943798)Termination phase: Saturation % 70.83/10.84 % (1943798)Time elapsed: 1.733 s % 70.83/10.84 % (1943798)Peak memory usage: 155 MB % 70.83/10.84 % (1943798)Instructions burned: 3034 (million) % 70.83/10.84 % (1943808)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=1482480511:i=2448:gtgl=5:bd=preordered:gtg=all_2920 on theBenchmark for (2920ds/2448Mi) % 70.83/10.84 % (1943809)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1634898818:i=3223:kws=precedence:fgj=on:av=off_2919 on theBenchmark for (2919ds/3223Mi) % 70.83/10.84 % (1943768)Instruction limit reached! % 70.83/10.84 % (1943768)------------------------------ % 70.83/10.84 % (1943768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.83/10.84 % (1943768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.83/10.84 % (1943768)CaDiCaL version: 2.1.3 % 70.83/10.84 % (1943768)Termination reason: Instruction limit % 70.83/10.84 % (1943768)Termination phase: Saturation % 70.83/10.84 % (1943768)Time elapsed: 6.020 s % 70.83/10.84 % (1943768)Peak memory usage: 152 MB % 70.83/10.84 % (1943768)Instructions burned: 14158 (million) % 70.83/10.84 % (1943812)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3345328402:st=5.6:i=2033:sd=3:ss=axioms_2912 on theBenchmark for (2912ds/2033Mi) % 71.22/10.91 [W928 14:14:27.128144037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.91 [W928 14:14:27.128178781 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.91 [W928 14:14:27.128218274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128232241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128260221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128272014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128298641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128310091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128335471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128346738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128371901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 [W928 14:14:27.128383128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.22/10.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.22/10.92 % (1943812)Refutation not found, incomplete strategy % 71.22/10.92 % (1943812)------------------------------ % 71.22/10.92 % (1943812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.22/10.92 % (1943812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.22/11.35 % (1943812)CaDiCaL version: 2.1.3 % 75.22/11.35 % (1943812)Termination reason: Refutation not found, incomplete strategy % 75.22/11.35 % (1943812)Time elapsed: 0.553 s % 75.22/11.35 % (1943812)Peak memory usage: 128 MB % 75.22/11.35 % (1943812)Instructions burned: 854 (million) % 75.22/11.35 % (1943808)Instruction limit reached! % 75.22/11.35 % (1943808)------------------------------ % 75.22/11.35 % (1943808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.22/11.35 % (1943808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.22/11.35 % (1943808)CaDiCaL version: 2.1.3 % 75.22/11.35 % (1943808)Termination reason: Instruction limit % 75.22/11.35 % (1943808)Termination phase: Saturation % 75.22/11.35 % (1943808)Time elapsed: 1.449 s % 75.22/11.35 % (1943808)Peak memory usage: 146 MB % 75.22/11.35 % (1943808)Instructions burned: 2448 (million) % 75.22/11.35 % (1943812)------------------------------ % 75.22/11.35 % (1943812)------------------------------ % 75.22/11.35 % (1943814)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1459510722:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2903 on theBenchmark for (2903ds/2055Mi) % 75.22/11.35 % (1943815)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=3909645077:i=21611:sd=3:ss=axioms_2903 on theBenchmark for (2903ds/21611Mi) % 75.22/11.35 % (1943809)Instruction limit reached! % 75.22/11.35 % (1943809)------------------------------ % 75.22/11.35 % (1943809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.22/11.35 % (1943809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.22/11.35 % (1943809)CaDiCaL version: 2.1.3 % 75.22/11.35 % (1943809)Termination reason: Instruction limit % 75.22/11.35 % (1943809)Termination phase: Saturation % 75.22/11.35 % (1943809)Time elapsed: 1.840 s % 75.22/11.35 % (1943809)Peak memory usage: 149 MB % 75.22/11.35 % (1943809)Instructions burned: 3224 (million) % 75.22/11.35 [W928 14:14:28.051057192 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051093733 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051133199 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051146463 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051175033 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051186800 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051216163 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.22/11.35 [W928 14:14:28.051227660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.051254086 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.051264366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.051289106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.051300066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 % (1943806)Instruction limit reached! % 84.30/12.61 % (1943806)------------------------------ % 84.30/12.61 % (1943806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 84.30/12.61 % (1943806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 84.30/12.61 % (1943806)CaDiCaL version: 2.1.3 % 84.30/12.61 % (1943806)Termination reason: Instruction limit % 84.30/12.61 % (1943806)Termination phase: Saturation % 84.30/12.61 % (1943806)Time elapsed: 2.863 s % 84.30/12.61 % (1943806)Peak memory usage: 118 MB % 84.30/12.61 % (1943806)Instructions burned: 5782 (million) % 84.30/12.61 [W928 14:14:28.125936410 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.125981964 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.126031557 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.126044674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.126071734 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.126094167 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 84.30/12.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 84.30/12.61 [W928 14:14:28.126124211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.22/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.22/13.84 [W928 14:14:28.126134724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.22/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.22/13.84 [W928 14:14:28.126159551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.22/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.22/13.84 [W928 14:14:28.126169761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.22/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.22/13.84 [W928 14:14:28.126204931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.22/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.22/13.84 [W928 14:14:28.126222554 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 92.22/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 92.22/13.84 % (1943818)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3724006256:i=4835:sd=13:ss=axioms:sgt=23_2899 on theBenchmark for (2899ds/4835Mi) % 92.22/13.84 % (1943818)Refutation not found, incomplete strategy % 92.22/13.84 % (1943818)------------------------------ % 92.22/13.84 % (1943818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.22/13.84 % (1943818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.22/13.84 % (1943818)CaDiCaL version: 2.1.3 % 92.22/13.84 % (1943818)Termination reason: Refutation not found, incomplete strategy % 92.22/13.84 % (1943818)Time elapsed: 0.004 s % 92.22/13.84 % (1943818)Peak memory usage: 88 MB % 92.22/13.84 % (1943818)Instructions burned: 4 (million) % 92.22/13.84 % (1943814)Refutation not found, incomplete strategy % 92.22/13.84 % (1943814)------------------------------ % 92.22/13.84 % (1943814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.22/13.84 % (1943814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.22/13.84 % (1943814)CaDiCaL version: 2.1.3 % 92.22/13.84 % (1943814)Termination reason: Refutation not found, incomplete strategy % 92.22/13.84 % (1943814)Time elapsed: 0.585 s % 92.22/13.84 % (1943814)Peak memory usage: 128 MB % 92.22/13.84 % (1943814)Instructions burned: 868 (million) % 92.22/13.84 % (1943819)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=3913584878:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2898 on theBenchmark for (2898ds/797Mi) % 92.22/13.84 % (1943815)Refutation not found, incomplete strategy % 92.22/13.84 % (1943815)------------------------------ % 92.22/13.84 % (1943815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 92.22/13.84 % (1943815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 92.22/13.84 % (1943815)CaDiCaL version: 2.1.3 % 92.22/13.84 % (1943815)Termination reason: Refutation not found, incomplete strategy % 92.22/13.84 % (1943815)Time elapsed: 0.588 s % 92.22/13.84 % (1943815)Peak memory usage: 127 MB % 92.22/13.84 % (1943815)Instructions burned: 853 (million) % 92.22/13.84 % (1943818)------------------------------ % 92.22/13.84 % (1943818)------------------------------ % 92.22/13.84 % (1943814)------------------------------ % 92.22/13.84 % (1943814)------------------------------ % 92.22/13.84 % (1943815)------------------------------ % 92.22/13.84 % (1943815)------------------------------ % 92.22/13.84 % (1943822)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1124586294:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2894 on theBenchmark for (2894ds/2326Mi) % 103.56/15.31 % (1943823)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1652518258:i=6038:nm=6_2893 on theBenchmark for (2893ds/6038Mi) % 103.56/15.31 % (1943819)Instruction limit reached! % 103.56/15.31 % (1943819)------------------------------ % 103.56/15.31 % (1943819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.56/15.31 % (1943819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.56/15.31 % (1943819)CaDiCaL version: 2.1.3 % 103.56/15.31 % (1943819)Termination reason: Instruction limit % 103.56/15.31 % (1943819)Termination phase: Saturation % 103.56/15.31 % (1943819)Time elapsed: 0.413 s % 103.56/15.31 % (1943819)Peak memory usage: 92 MB % 103.56/15.31 % (1943819)Instructions burned: 798 (million) % 103.56/15.31 % (1943822)Refutation not found, incomplete strategy % 103.56/15.31 % (1943822)------------------------------ % 103.56/15.31 % (1943822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.56/15.31 % (1943822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.56/15.31 % (1943822)CaDiCaL version: 2.1.3 % 103.56/15.31 % (1943822)Termination reason: Refutation not found, incomplete strategy % 103.56/15.31 % (1943822)Time elapsed: 0.107 s % 103.56/15.31 % (1943822)Peak memory usage: 92 MB % 103.56/15.31 % (1943822)Instructions burned: 189 (million) % 103.56/15.31 % (1943825)lrs+10_1_sil=32000:sp=occurrence:random_seed=1397349484:st=2:i=33334:sd=3:ss=included:sgt=32_2893 on theBenchmark for (2893ds/33334Mi) % 103.56/15.31 % (1943827)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=768947648:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2892 on theBenchmark for (2892ds/1008Mi) % 103.56/15.31 % (1943827)Refutation not found, incomplete strategy % 103.56/15.31 % (1943827)------------------------------ % 103.56/15.31 % (1943827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.56/15.31 % (1943827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.56/15.31 % (1943827)CaDiCaL version: 2.1.3 % 103.56/15.31 % (1943827)Termination reason: Refutation not found, incomplete strategy % 103.56/15.31 % (1943827)Time elapsed: 0.008 s % 103.56/15.31 % (1943827)Peak memory usage: 88 MB % 103.56/15.31 % (1943827)Instructions burned: 11 (million) % 103.56/15.31 % (1943822)------------------------------ % 103.56/15.31 % (1943822)------------------------------ % 103.56/15.31 % (1943827)------------------------------ % 103.56/15.31 % (1943827)------------------------------ % 103.56/15.31 % (1943830)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=303485606:i=8327:s2at=5:bd=preordered_2889 on theBenchmark for (2889ds/8327Mi) % 103.56/15.31 % (1943831)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=935731087:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2887 on theBenchmark for (2887ds/1083Mi) % 103.56/15.31 % (1943823)Refutation not found, incomplete strategy % 103.56/15.31 % (1943823)------------------------------ % 103.56/15.31 % (1943823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.56/15.31 % (1943823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.56/15.31 % (1943823)CaDiCaL version: 2.1.3 % 103.56/15.31 % (1943823)Termination reason: Refutation not found, incomplete strategy % 103.56/15.31 % (1943823)Time elapsed: 0.735 s % 103.56/15.31 % (1943823)Peak memory usage: 139 MB % 103.56/15.31 % (1943823)Instructions burned: 1163 (million) % 103.56/15.31 % (1943823)------------------------------ % 103.56/15.31 % (1943823)------------------------------ % 103.56/15.31 % (1943831)Instruction limit reached! % 103.56/15.31 % (1943831)------------------------------ % 103.56/15.31 % (1943831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.56/15.31 % (1943831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.56/15.31 % (1943831)CaDiCaL version: 2.1.3 % 103.56/15.31 % (1943831)Termination reason: Instruction limit % 103.56/15.31 % (1943831)Termination phase: Saturation % 103.56/15.31 % (1943831)Time elapsed: 0.529 s % 103.56/15.31 % (1943831)Peak memory usage: 102 MB % 103.56/15.31 % (1943831)Instructions burned: 1085 (million) % 103.56/15.31 % (1943834)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3526547955:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2882 on theBenchmark for (2882ds/1084Mi) % 107.66/15.91 % (1943834)Refutation not found, incomplete strategy % 107.66/15.91 % (1943834)------------------------------ % 107.66/15.91 % (1943834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.66/15.91 % (1943834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.66/15.91 % (1943834)CaDiCaL version: 2.1.3 % 107.66/15.91 % (1943834)Termination reason: Refutation not found, incomplete strategy % 107.66/15.91 % (1943834)Time elapsed: 0.004 s % 107.66/15.91 % (1943834)Peak memory usage: 87 MB % 107.66/15.91 % (1943834)Instructions burned: 5 (million) % 107.66/15.91 % (1943835)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2972952998:i=6995:s2at=5:gtg=all_2880 on theBenchmark for (2880ds/6995Mi) % 107.66/15.91 % (1943834)------------------------------ % 107.66/15.91 % (1943834)------------------------------ % 107.66/15.91 % (1943838)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=359534331:st=2:i=6225:sd=15:ss=axioms_2878 on theBenchmark for (2878ds/6225Mi) % 107.66/15.91 % (1943838)Refutation not found, incomplete strategy % 107.66/15.91 % (1943838)------------------------------ % 107.66/15.91 % (1943838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.66/15.91 % (1943838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.66/15.91 % (1943838)CaDiCaL version: 2.1.3 % 107.66/15.91 % (1943838)Termination reason: Refutation not found, incomplete strategy % 107.66/15.91 % (1943838)Time elapsed: 0.005 s % 107.66/15.91 % (1943838)Peak memory usage: 88 MB % 107.66/15.91 % (1943838)Instructions burned: 6 (million) % 107.66/15.91 % (1943838)------------------------------ % 107.66/15.91 % (1943838)------------------------------ % 107.66/15.91 % (1943840)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2190126838:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2873 on theBenchmark for (2873ds/3372Mi) % 107.66/15.91 % (1943803)Instruction limit reached! % 107.66/15.91 % (1943803)------------------------------ % 107.66/15.91 % (1943803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 107.66/15.91 % (1943803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 107.66/15.91 % (1943803)CaDiCaL version: 2.1.3 % 107.66/15.91 % (1943803)Termination reason: Instruction limit % 107.66/15.91 % (1943803)Termination phase: Saturation % 107.66/15.91 % (1943803)Time elapsed: 5.840 s % 107.66/15.91 % (1943803)Peak memory usage: 151 MB % 107.66/15.91 % (1943803)Instructions burned: 14125 (million) % 107.66/15.91 % (1943842)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=103360858:st=2.3:i=26457:sd=10:ss=included:sgt=8_2870 on theBenchmark for (2870ds/26457Mi) % 107.66/15.91 [W928 14:14:31.051957663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 107.66/15.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.66/15.91 [W928 14:14:31.052009636 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 107.66/15.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.66/15.91 [W928 14:14:31.052050180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 107.66/15.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.66/15.91 [W928 14:14:31.052067047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 107.66/15.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.66/15.91 [W928 14:14:31.052092677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 107.66/15.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 107.66/15.91 [W928 14:14:31.052104863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 [W928 14:14:31.052130763 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 [W928 14:14:31.052141037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 [W928 14:14:31.052165020 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 [W928 14:14:31.052175484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 [W928 14:14:31.052201120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 [W928 14:14:31.052211604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 111.37/16.41 % (1943840)Refutation not found, incomplete strategy % 111.37/16.41 % (1943840)------------------------------ % 111.37/16.41 % (1943840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.37/16.41 % (1943840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.37/16.41 % (1943840)CaDiCaL version: 2.1.3 % 111.37/16.41 % (1943840)Termination reason: Refutation not found, incomplete strategy % 111.37/16.41 % (1943840)Time elapsed: 0.569 s % 111.37/16.41 % (1943840)Peak memory usage: 131 MB % 111.37/16.41 % (1943840)Instructions burned: 869 (million) % 111.37/16.41 % (1943840)------------------------------ % 111.37/16.41 % (1943840)------------------------------ % 111.37/16.41 % (1943844)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=2527414214:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2863 on theBenchmark for (2863ds/13494Mi) % 111.37/16.41 % (1943842)Refutation not found, incomplete strategy % 111.37/16.41 % (1943842)------------------------------ % 111.37/16.41 % (1943842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.37/16.41 % (1943842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.37/16.41 % (1943842)CaDiCaL version: 2.1.3 % 111.37/16.41 % (1943842)Termination reason: Refutation not found, incomplete strategy % 111.37/16.41 % (1943842)Time elapsed: 0.758 s % 111.37/16.41 % (1943842)Peak memory usage: 153 MB % 111.37/16.41 % (1943842)Instructions burned: 1166 (million) % 111.37/16.41 % (1943842)------------------------------ % 111.37/16.41 % (1943842)------------------------------ % 111.37/16.41 % (1943846)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=3897588683:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2858 on theBenchmark for (2858ds/2503Mi) % 111.37/16.41 [W928 14:14:32.517809646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 111.37/16.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517844002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517892419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517904409 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517947406 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517958219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517983169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.517993389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.518028796 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.518040306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.518065116 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 [W928 14:14:32.518075346 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 126.43/18.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 126.43/18.62 % (1943846)Refutation not found, incomplete strategy % 126.43/18.62 % (1943846)------------------------------ % 126.43/18.62 % (1943846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 126.43/18.62 % (1943846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 126.43/18.62 % (1943846)CaDiCaL version: 2.1.3 % 126.43/18.62 % (1943846)Termination reason: Refutation not found, incomplete strategy % 126.43/18.62 % (1943846)Time elapsed: 0.564 s % 126.43/18.62 % (1943846)Peak memory usage: 130 MB % 126.43/18.62 % (1943846)Instructions burned: 854 (million) % 126.43/18.62 % (1943846)------------------------------ % 126.43/18.62 % (1943846)------------------------------ % 126.43/18.62 % (1943848)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2440507232:i=2559:sd=1:ep=RSTC:ss=axioms_2849 on theBenchmark for (2849ds/2559Mi) % 133.52/19.61 [W928 14:14:33.499865841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.499899064 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.499938711 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.499951498 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.499978471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.499990201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.500028138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.500040998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.500066081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.500077652 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.500101758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 [W928 14:14:33.500123055 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.52/19.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.52/19.61 % (1943830)Instruction limit reached! % 133.52/19.61 % (1943830)------------------------------ % 133.52/19.61 % (1943830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.99/20.59 % (1943830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.99/20.59 % (1943830)CaDiCaL version: 2.1.3 % 139.99/20.59 % (1943830)Termination reason: Instruction limit % 139.99/20.59 % (1943830)Termination phase: Saturation % 139.99/20.59 % (1943830)Time elapsed: 4.529 s % 139.99/20.59 % (1943830)Peak memory usage: 162 MB % 139.99/20.59 % (1943830)Instructions burned: 8329 (million) % 139.99/20.59 % (1943848)Refutation not found, incomplete strategy % 139.99/20.59 % (1943848)------------------------------ % 139.99/20.59 % (1943848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.99/20.59 % (1943848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.99/20.59 % (1943848)CaDiCaL version: 2.1.3 % 139.99/20.59 % (1943848)Termination reason: Refutation not found, incomplete strategy % 139.99/20.59 % (1943848)Time elapsed: 0.565 s % 139.99/20.59 % (1943848)Peak memory usage: 130 MB % 139.99/20.59 % (1943848)Instructions burned: 853 (million) % 139.99/20.59 % (1943850)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1608359758:i=30753:av=off:ss=included_2842 on theBenchmark for (2842ds/30753Mi) % 139.99/20.59 % (1943848)------------------------------ % 139.99/20.59 % (1943848)------------------------------ % 139.99/20.59 % (1943852)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=709679298:i=26473:ep=RSTC_2839 on theBenchmark for (2839ds/26473Mi) % 139.99/20.59 % (1943835)Instruction limit reached! % 139.99/20.59 % (1943835)------------------------------ % 139.99/20.59 % (1943835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.99/20.59 % (1943835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.99/20.59 % (1943835)CaDiCaL version: 2.1.3 % 139.99/20.59 % (1943835)Termination reason: Instruction limit % 139.99/20.59 % (1943835)Termination phase: Saturation % 139.99/20.59 % (1943835)Time elapsed: 4.161 s % 139.99/20.59 % (1943835)Peak memory usage: 169 MB % 139.99/20.59 % (1943835)Instructions burned: 6997 (million) % 139.99/20.59 % (1943854)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=1153777942:cts=off:i=2759:kws=inv_arity:fgj=on_2837 on theBenchmark for (2837ds/2759Mi) % 139.99/20.59 % (1943854)Refutation not found, incomplete strategy % 139.99/20.59 % (1943854)------------------------------ % 139.99/20.59 % (1943854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.99/20.59 % (1943854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.99/20.59 % (1943854)CaDiCaL version: 2.1.3 % 139.99/20.59 % (1943854)Termination reason: Refutation not found, incomplete strategy % 139.99/20.59 % (1943854)Time elapsed: 0.752 s % 139.99/20.59 % (1943854)Peak memory usage: 139 MB % 139.99/20.59 % (1943854)Instructions burned: 1209 (million) % 139.99/20.59 % (1943854)------------------------------ % 139.99/20.59 % (1943854)------------------------------ % 139.99/20.59 % (1943856)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=3982948986:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2825 on theBenchmark for (2825ds/5665Mi) % 139.99/20.59 [W928 14:14:36.833455183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.99/20.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.99/20.59 [W928 14:14:36.833489580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.99/20.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.99/20.59 [W928 14:14:36.833528214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.99/20.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.99/20.59 [W928 14:14:36.833540370 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833567454 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833578010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833602584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833613707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833637907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833648847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833673281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:36.833684194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 % (1943856)Refutation not found, incomplete strategy % 142.42/21.01 % (1943856)------------------------------ % 142.42/21.01 % (1943856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 142.42/21.01 % (1943856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 142.42/21.01 % (1943856)CaDiCaL version: 2.1.3 % 142.42/21.01 % (1943856)Termination reason: Refutation not found, incomplete strategy % 142.42/21.01 % (1943856)Time elapsed: 0.561 s % 142.42/21.01 % (1943856)Peak memory usage: 131 MB % 142.42/21.01 % (1943856)Instructions burned: 855 (million) % 142.42/21.01 % (1943856)------------------------------ % 142.42/21.01 % (1943856)------------------------------ % 142.42/21.01 % (1943858)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=2205864133:i=1532:ep=RS:ss=axioms_2816 on theBenchmark for (2816ds/1532Mi) % 142.42/21.01 [W928 14:14:37.817581648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:37.817618328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 142.42/21.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 142.42/21.01 [W928 14:14:37.817657368 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817671181 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817702698 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817714465 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817739905 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817750832 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817775105 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817785958 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817810109 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 [W928 14:14:37.817820929 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.32/22.04 % (1943858)Refutation not found, incomplete strategy % 151.32/22.04 % (1943858)------------------------------ % 151.32/22.04 % (1943858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 151.32/22.04 % (1943858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 151.32/22.04 % (1943858)CaDiCaL version: 2.1.3 % 151.32/22.04 % (1943858)Termination reason: Refutation not found, incomplete strategy % 151.32/22.04 % (1943858)Time elapsed: 0.563 s % 151.32/22.04 % (1943858)Peak memory usage: 130 MB % 151.32/22.04 % (1943858)Instructions burned: 854 (million) % 151.32/22.04 % (1943858)------------------------------ % 151.32/22.04 % (1943858)------------------------------ % 151.32/22.04 % (1943860)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2309531476:i=1565:sd=2:ss=axioms:sgt=32_2806 on theBenchmark for (2806ds/1565Mi) % 151.32/22.04 [W928 14:14:38.800614016 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/22.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800656773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800695613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800707096 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800732846 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800742813 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800766670 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800776580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800800067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800810083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800833820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 [W928 14:14:38.800847810 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 156.32/23.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 156.32/23.03 % (1943860)Refutation not found, incomplete strategy % 156.32/23.03 % (1943860)------------------------------ % 156.32/23.03 % (1943860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 156.32/23.03 % (1943860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 156.32/23.03 % (1943860)CaDiCaL version: 2.1.3 % 156.32/23.03 % (1943860)Termination reason: Refutation not found, incomplete strategy % 156.32/23.03 % (1943860)Time elapsed: 0.560 s % 156.32/23.03 % (1943860)Peak memory usage: 129 MB % 156.32/23.03 % (1943860)Instructions burned: 854 (million) % 156.32/23.03 % (1943860)------------------------------ % 156.32/23.03 % (1943860)------------------------------ % 163.53/24.01 % (1943862)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=3602056628:i=1572:fgj=on:gsp=on_2796 on theBenchmark for (2796ds/1572Mi) % 163.53/24.01 % (1943844)Instruction limit reached! % 163.53/24.01 % (1943844)------------------------------ % 163.53/24.01 % (1943844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.53/24.01 % (1943844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.53/24.01 % (1943844)CaDiCaL version: 2.1.3 % 163.53/24.01 % (1943844)Termination reason: Instruction limit % 163.53/24.01 % (1943844)Termination phase: Saturation % 163.53/24.01 % (1943844)Time elapsed: 7.027 s % 163.53/24.01 % (1943844)Peak memory usage: 249 MB % 163.53/24.01 % (1943844)Instructions burned: 13496 (million) % 163.53/24.01 % (1943864)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3453218365:i=6052:sd=4:ss=axioms:sgt=24_2791 on theBenchmark for (2791ds/6052Mi) % 163.53/24.01 [W928 14:14:39.253037514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253073518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253111254 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253124004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253151528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253163314 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253190321 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253201855 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253227195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.53/24.01 [W928 14:14:39.253238598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.53/24.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:39.253264428 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:39.253320952 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 % (1943862)Instruction limit reached! % 192.25/27.81 % (1943862)------------------------------ % 192.25/27.81 % (1943862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.25/27.81 % (1943862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.25/27.81 % (1943862)CaDiCaL version: 2.1.3 % 192.25/27.81 % (1943862)Termination reason: Instruction limit % 192.25/27.81 % (1943862)Termination phase: Saturation % 192.25/27.81 % (1943862)Time elapsed: 0.936 s % 192.25/27.81 % (1943862)Peak memory usage: 154 MB % 192.25/27.81 % (1943862)Instructions burned: 1573 (million) % 192.25/27.81 % (1943864)Refutation not found, incomplete strategy % 192.25/27.81 % (1943864)------------------------------ % 192.25/27.81 % (1943864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 192.25/27.81 % (1943864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 192.25/27.81 % (1943864)CaDiCaL version: 2.1.3 % 192.25/27.81 % (1943864)Termination reason: Refutation not found, incomplete strategy % 192.25/27.81 % (1943864)Time elapsed: 0.561 s % 192.25/27.81 % (1943864)Peak memory usage: 130 MB % 192.25/27.81 % (1943864)Instructions burned: 852 (million) % 192.25/27.81 % (1943866)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=2569284947:i=3500:sd=1:bd=preordered:sup=off:ss=included_2785 on theBenchmark for (2785ds/3500Mi) % 192.25/27.81 % (1943864)------------------------------ % 192.25/27.81 % (1943864)------------------------------ % 192.25/27.81 % (1943868)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=680392123:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2781 on theBenchmark for (2781ds/1842Mi) % 192.25/27.81 [W928 14:14:40.239463145 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:40.239508242 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:40.239548305 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:40.239559329 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:40.239585212 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 192.25/27.81 [W928 14:14:40.239595459 register_special_ops.cpp:225] Warning: Creating a tensor from 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.25/27.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:40.239620282 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:40.239630799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:40.239654556 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:40.239664752 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:40.239688086 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:40.239698066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 % (1943866)Refutation not found, incomplete strategy % 201.01/29.13 % (1943866)------------------------------ % 201.01/29.13 % (1943866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.01/29.13 % (1943866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.01/29.13 % (1943866)CaDiCaL version: 2.1.3 % 201.01/29.13 % (1943866)Termination reason: Refutation not found, incomplete strategy % 201.01/29.13 % (1943866)Time elapsed: 0.742 s % 201.01/29.13 % (1943866)Peak memory usage: 151 MB % 201.01/29.13 % (1943866)Instructions burned: 1167 (million) % 201.01/29.13 % (1943868)Refutation not found, incomplete strategy % 201.01/29.13 % (1943868)------------------------------ % 201.01/29.13 % (1943868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 201.01/29.13 % (1943868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 201.01/29.13 % (1943868)CaDiCaL version: 2.1.3 % 201.01/29.13 % (1943868)Termination reason: Refutation not found, incomplete strategy % 201.01/29.13 % (1943868)Time elapsed: 0.574 s % 201.01/29.13 % (1943868)Peak memory usage: 130 MB % 201.01/29.13 % (1943868)Instructions burned: 870 (million) % 201.01/29.13 % (1943866)------------------------------ % 201.01/29.13 % (1943866)------------------------------ % 201.01/29.13 % (1943868)------------------------------ % 201.01/29.13 % (1943868)------------------------------ % 201.01/29.13 % (1943870)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3463135768:i=66096:add=on_2773 on theBenchmark for (2773ds/66096Mi) % 201.01/29.13 % (1943871)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=421298849:i=1884:sd=1:nm=60:ss=axioms_2771 on theBenchmark for (2771ds/1884Mi) % 201.01/29.13 [W928 14:14:41.216021902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 201.01/29.13 [W928 14:14:41.216067435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 201.01/29.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216108262 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216120385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216146172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216156355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216181889 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216192896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216217139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216228136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216252016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 [W928 14:14:41.216262822 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.66/30.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.66/30.46 % (1943871)Refutation not found, incomplete strategy % 210.66/30.46 % (1943871)------------------------------ % 210.66/30.46 % (1943871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.66/30.46 % (1943871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.66/30.46 % (1943871)CaDiCaL version: 2.1.3 % 210.66/30.46 % (1943871)Termination reason: Refutation not found, incomplete strategy % 210.66/30.46 % (1943871)Time elapsed: 0.561 s % 210.66/30.46 % (1943871)Peak memory usage: 130 MB % 210.66/30.46 % (1943871)Instructions burned: 856 (million) % 210.66/30.46 % (1943871)------------------------------ % 210.66/30.46 % (1943871)------------------------------ % 210.66/30.46 % (1943874)lrs-1011_4:1_sil=16000:bsr=on:random_seed=267253715:cts=off:i=5469:bs=on:fsr=off_2762 on theBenchmark for (2762ds/5469Mi) % 210.66/30.46 % (1943874)Instruction limit reached! % 210.66/30.46 % (1943874)------------------------------ % 210.66/30.46 % (1943874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.66/30.46 % (1943874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.33/31.25 % (1943874)CaDiCaL version: 2.1.3 % 216.33/31.25 % (1943874)Termination reason: Instruction limit % 216.33/31.25 % (1943874)Termination phase: Saturation % 216.33/31.25 % (1943874)Time elapsed: 3.225 s % 216.33/31.25 % (1943874)Peak memory usage: 111 MB % 216.33/31.25 % (1943874)Instructions burned: 5469 (million) % 216.33/31.25 % (1943876)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=3050848417:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2728 on theBenchmark for (2728ds/2037Mi) % 216.33/31.25 % (1943850)Instruction limit reached! % 216.33/31.25 % (1943850)------------------------------ % 216.33/31.25 % (1943850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 216.33/31.25 % (1943850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 216.33/31.25 % (1943850)CaDiCaL version: 2.1.3 % 216.33/31.25 % (1943850)Termination reason: Instruction limit % 216.33/31.25 % (1943850)Termination phase: Saturation % 216.33/31.25 % (1943850)Time elapsed: 11.998 s % 216.33/31.25 % (1943850)Peak memory usage: 152 MB % 216.33/31.25 % (1943850)Instructions burned: 30754 (million) % 216.33/31.25 % (1943878)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1766594371:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2720 on theBenchmark for (2720ds/2110Mi) % 216.33/31.25 [W928 14:14:46.338273486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338318780 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338363996 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338376183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338409153 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338421003 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338447223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338458820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 216.33/31.25 [W928 14:14:46.338484493 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 216.33/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 219.70/31.83 [W928 14:14:46.338495863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 219.70/31.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 219.70/31.83 [W928 14:14:46.338520194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 219.70/31.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 219.70/31.83 [W928 14:14:46.338530130 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 219.70/31.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 219.70/31.83 % (1943876)Instruction limit reached! % 219.70/31.83 % (1943876)------------------------------ % 219.70/31.83 % (1943876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.70/31.83 % (1943876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.70/31.83 % (1943876)CaDiCaL version: 2.1.3 % 219.70/31.83 % (1943876)Termination reason: Instruction limit % 219.70/31.83 % (1943876)Termination phase: Saturation % 219.70/31.83 % (1943876)Time elapsed: 1.175 s % 219.70/31.83 % (1943876)Peak memory usage: 144 MB % 219.70/31.83 % (1943876)Instructions burned: 2038 (million) % 219.70/31.83 % (1943878)Refutation not found, incomplete strategy % 219.70/31.83 % (1943878)------------------------------ % 219.70/31.83 % (1943878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.70/31.83 % (1943878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.70/31.83 % (1943878)CaDiCaL version: 2.1.3 % 219.70/31.83 % (1943878)Termination reason: Refutation not found, incomplete strategy % 219.70/31.83 % (1943878)Time elapsed: 0.576 s % 219.70/31.83 % (1943878)Peak memory usage: 130 MB % 219.70/31.83 % (1943878)Instructions burned: 856 (million) % 219.70/31.83 % (1943880)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=2512621389:i=2430:add=off:aac=none:nm=16_2715 on theBenchmark for (2715ds/2430Mi) % 219.70/31.83 % (1943712)Instruction limit reached! % 219.70/31.83 % (1943712)------------------------------ % 219.70/31.83 % (1943712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.70/31.83 % (1943712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.70/31.83 % (1943712)CaDiCaL version: 2.1.3 % 219.70/31.83 % (1943712)Termination reason: Instruction limit % 219.70/31.83 % (1943712)Termination phase: Saturation % 219.70/31.83 % (1943712)Time elapsed: 28.508 s % 219.70/31.83 % (1943712)Peak memory usage: 165 MB % 219.70/31.83 % (1943712)Instructions burned: 141193 (million) % 219.70/31.83 % (1943882)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=31795317:cond=fast:i=4891_2712 on theBenchmark for (2712ds/4891Mi) % 219.70/31.83 % (1943878)------------------------------ % 219.70/31.83 % (1943878)------------------------------ % 219.70/31.83 % (1943884)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=3058411318:st=2:i=14845:sd=2:ss=included:fsd=on_2710 on theBenchmark for (2710ds/14845Mi) % 219.70/31.83 % (1943825)Instruction limit reached! % 219.70/31.83 % (1943825)------------------------------ % 219.70/31.83 % (1943825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 219.70/31.83 % (1943825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 219.70/31.83 % (1943825)CaDiCaL version: 2.1.3 % 219.70/31.83 % (1943825)Termination reason: Instruction limit % 219.70/31.83 % (1943825)Termination phase: Saturation % 219.70/31.83 % (1943825)Time elapsed: 18.262 s % 219.70/31.83 % (1943825)Peak memory usage: 218 MB % 219.70/31.83 % (1943825)Instructions burned: 33335 (million) % 219.70/31.83 % (1943886)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=220586599:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2708 on theBenchmark for (2708ds/7534Mi) % 219.70/31.83 % (1943884)Refutation not found, incomplete strategy % 230.98/33.34 % (1943884)------------------------------ % 230.98/33.34 % (1943884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.98/33.34 % (1943884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.98/33.34 % (1943884)CaDiCaL version: 2.1.3 % 230.98/33.34 % (1943884)Termination reason: Refutation not found, incomplete strategy % 230.98/33.34 % (1943884)Time elapsed: 0.731 s % 230.98/33.34 % (1943884)Peak memory usage: 141 MB % 230.98/33.34 % (1943884)Instructions burned: 1142 (million) % 230.98/33.34 % (1943884)------------------------------ % 230.98/33.34 % (1943884)------------------------------ % 230.98/33.34 % (1943852)Instruction limit reached! % 230.98/33.34 % (1943852)------------------------------ % 230.98/33.34 % (1943852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.98/33.34 % (1943852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.98/33.34 % (1943852)CaDiCaL version: 2.1.3 % 230.98/33.34 % (1943852)Termination reason: Instruction limit % 230.98/33.34 % (1943852)Termination phase: Saturation % 230.98/33.34 % (1943852)Time elapsed: 13.903 s % 230.98/33.34 % (1943852)Peak memory usage: 502 MB % 230.98/33.34 % (1943852)Instructions burned: 26476 (million) % 230.98/33.34 % (1943880)Instruction limit reached! % 230.98/33.34 % (1943880)------------------------------ % 230.98/33.34 % (1943880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.98/33.34 % (1943880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.98/33.34 % (1943880)CaDiCaL version: 2.1.3 % 230.98/33.34 % (1943880)Termination reason: Instruction limit % 230.98/33.34 % (1943880)Termination phase: Saturation % 230.98/33.34 % (1943880)Time elapsed: 1.459 s % 230.98/33.34 % (1943880)Peak memory usage: 152 MB % 230.98/33.34 % (1943880)Instructions burned: 2431 (million) % 230.98/33.34 % (1943888)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=3259321598:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2699 on theBenchmark for (2699ds/10353Mi) % 230.98/33.34 % (1943889)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=542617819:i=7860_2698 on theBenchmark for (2698ds/7860Mi) % 230.98/33.34 % (1943890)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=4092773892:i=7896:sd=2:bs=on:ss=included:sgt=20_2698 on theBenchmark for (2698ds/7896Mi) % 230.98/33.34 % (1943889)Refutation not found, incomplete strategy % 230.98/33.34 % (1943889)------------------------------ % 230.98/33.34 % (1943889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 230.98/33.34 % (1943889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 230.98/33.34 % (1943889)CaDiCaL version: 2.1.3 % 230.98/33.34 % (1943889)Termination reason: Refutation not found, incomplete strategy % 230.98/33.34 % (1943889)Time elapsed: 0.056 s % 230.98/33.34 % (1943889)Peak memory usage: 92 MB % 230.98/33.34 % (1943889)Instructions burned: 110 (million) % 230.98/33.34 % (1943889)------------------------------ % 230.98/33.34 % (1943889)------------------------------ % 230.98/33.34 [W928 14:14:48.459024945 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.98/33.34 [W928 14:14:48.459062629 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.98/33.34 [W928 14:14:48.459103345 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 230.98/33.34 [W928 14:14:48.459124152 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/33.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459151572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459166756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459192896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459203019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459226949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459236909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459261596 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 [W928 14:14:48.459271723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.61/33.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.61/33.40 % (1943894)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1595554540:i=5812:gtgl=2:gtg=all_2694 on theBenchmark for (2694ds/5812Mi) % 231.61/33.40 % (1943888)Refutation not found, incomplete strategy % 231.61/33.40 % (1943888)------------------------------ % 231.61/33.40 % (1943888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.61/33.40 % (1943888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.61/33.40 % (1943888)CaDiCaL version: 2.1.3 % 231.61/33.40 % (1943888)Termination reason: Refutation not found, incomplete strategy % 231.61/33.40 % (1943888)Time elapsed: 0.565 s % 231.61/33.40 % (1943888)Peak memory usage: 131 MB % 231.61/33.40 % (1943888)Instructions burned: 854 (million) % 231.61/33.40 % (1943882)Instruction limit reached! % 231.61/33.40 % (1943882)------------------------------ % 231.61/33.40 % (1943882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.61/33.40 % (1943882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.61/33.40 % (1943882)CaDiCaL version: 2.1.3 % 231.61/33.40 % (1943882)Termination reason: Instruction limit % 231.61/33.40 % (1943882)Termination phase: Saturation % 231.61/33.40 % (1943882)Time elapsed: 2.083 s % 231.61/33.40 % (1943882)Peak memory usage: 151 MB % 231.61/33.40 % (1943882)Instructions burned: 4891 (million) % 231.61/33.40 % (1943888)------------------------------ % 231.61/33.40 % (1943888)------------------------------ % 231.61/33.40 % (1943896)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=3180875659:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2690 on theBenchmark for (2690ds/2965Mi) % 231.61/33.40 % (1943897)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=927209392:i=2967:kws=precedence:bd=preordered:av=off_2689 on theBenchmark for (2689ds/2967Mi) % 234.24/33.94 % (1943896)Refutation not found, incomplete strategy % 234.24/33.94 % (1943896)------------------------------ % 234.24/33.94 % (1943896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.24/33.94 % (1943896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.24/33.94 % (1943896)CaDiCaL version: 2.1.3 % 234.24/33.94 % (1943896)Termination reason: Refutation not found, incomplete strategy % 234.24/33.94 % (1943896)Time elapsed: 0.779 s % 234.24/33.94 % (1943896)Peak memory usage: 152 MB % 234.24/33.94 % (1943896)Instructions burned: 1203 (million) % 234.24/33.94 % (1943896)------------------------------ % 234.24/33.94 % (1943896)------------------------------ % 234.24/33.94 % (1943900)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=3963416398:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2678 on theBenchmark for (2678ds/3022Mi) % 234.24/33.94 % (1943890)Instruction limit reached! % 234.24/33.94 % (1943890)------------------------------ % 234.24/33.94 % (1943890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 234.24/33.94 % (1943890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 234.24/33.94 % (1943890)CaDiCaL version: 2.1.3 % 234.24/33.94 % (1943890)Termination reason: Instruction limit % 234.24/33.94 % (1943890)Termination phase: Saturation % 234.24/33.94 % (1943890)Time elapsed: 2.132 s % 234.24/33.94 % (1943890)Peak memory usage: 151 MB % 234.24/33.94 % (1943890)Instructions burned: 7901 (million) % 234.24/33.94 % (1943902)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=3352261870:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2675 on theBenchmark for (2675ds/3207Mi) % 234.24/33.94 [W928 14:14:50.547793684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.24/33.94 [W928 14:14:50.547828354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.24/33.94 [W928 14:14:50.547866461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.24/33.94 [W928 14:14:50.547878641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.24/33.94 [W928 14:14:50.547905414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.24/33.94 [W928 14:14:50.547917614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 234.24/33.94 [W928 14:14:50.547944338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 234.24/33.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:50.547956501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:50.547982248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:50.547993245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:50.548029435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:50.548041448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 % (1943886)Instruction limit reached! % 237.56/34.24 % (1943886)------------------------------ % 237.56/34.24 % (1943886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 237.56/34.24 % (1943886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 237.56/34.24 % (1943886)CaDiCaL version: 2.1.3 % 237.56/34.24 % (1943886)Termination reason: Instruction limit % 237.56/34.24 % (1943886)Termination phase: Saturation % 237.56/34.24 % (1943886)Time elapsed: 3.427 s % 237.56/34.24 % (1943886)Peak memory usage: 144 MB % 237.56/34.24 % (1943886)Instructions burned: 7536 (million) % 237.56/34.24 [W928 14:14:51.615226852 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:51.615255392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:51.615278066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:51.615285773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:51.615300086 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:51.615306465 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 237.56/34.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 237.56/34.24 [W928 14:14:51.615319949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.46/35.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.46/35.05 [W928 14:14:51.615326976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.46/35.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.46/35.05 [W928 14:14:51.615340623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.46/35.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.46/35.05 [W928 14:14:51.615346066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.46/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.46/35.06 [W928 14:14:51.615360369 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.46/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.46/35.06 [W928 14:14:51.615398307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 243.46/35.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 243.46/35.06 % (1943897)Instruction limit reached! % 243.46/35.06 % (1943897)------------------------------ % 243.46/35.06 % (1943897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.46/35.06 % (1943897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.46/35.06 % (1943897)CaDiCaL version: 2.1.3 % 243.46/35.06 % (1943897)Termination reason: Instruction limit % 243.46/35.06 % (1943897)Termination phase: Saturation % 243.46/35.06 % (1943897)Time elapsed: 1.671 s % 243.46/35.06 % (1943897)Peak memory usage: 151 MB % 243.46/35.06 % (1943897)Instructions burned: 2969 (million) % 243.46/35.06 % (1943902)Refutation not found, incomplete strategy % 243.46/35.06 % (1943902)------------------------------ % 243.46/35.06 % (1943902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.46/35.06 % (1943902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.46/35.06 % (1943902)CaDiCaL version: 2.1.3 % 243.46/35.06 % (1943902)Termination reason: Refutation not found, incomplete strategy % 243.46/35.06 % (1943902)Time elapsed: 0.307 s % 243.46/35.06 % (1943902)Peak memory usage: 128 MB % 243.46/35.06 % (1943902)Instructions burned: 854 (million) % 243.46/35.06 % (1943900)Refutation not found, incomplete strategy % 243.46/35.06 % (1943900)------------------------------ % 243.46/35.06 % (1943900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 243.46/35.06 % (1943900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 243.46/35.06 % (1943900)CaDiCaL version: 2.1.3 % 243.46/35.06 % (1943900)Termination reason: Refutation not found, incomplete strategy % 243.46/35.06 % (1943900)Time elapsed: 0.564 s % 243.46/35.06 % (1943900)Peak memory usage: 128 MB % 243.46/35.06 % (1943900)Instructions burned: 853 (million) % 243.46/35.06 % (1943904)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3744166706:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2672 on theBenchmark for (2672ds/3289Mi) % 243.46/35.06 % (1943902)------------------------------ % 243.46/35.06 % (1943902)------------------------------ % 243.46/35.06 % (1943905)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1140329208:i=38569:sd=3:ss=axioms:sgt=32_2671 on theBenchmark for (2671ds/38569Mi) % 243.46/35.06 % (1943900)------------------------------ % 243.46/35.06 % (1943900)------------------------------ % 243.46/35.06 % (1943907)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2440579814:cts=off:i=3394_2669 on theBenchmark for (2669ds/3394Mi) % 243.46/35.06 % (1943909)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=2016735738:i=33824:bd=preordered_2668 on theBenchmark for (2668ds/33824Mi) % 246.07/35.47 [W928 14:14:51.277398878 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277431778 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277471648 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277484165 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277518028 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277530075 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277556625 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277568308 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277594722 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277606338 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277633018 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 [W928 14:14:51.277644622 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07/35.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.07/35.47 % (1943904)Refutation not found, incomplete strategy % 246.07/35.47 % (1943904)------------------------------ % 246.07/35.47 % (1943904)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.07/35.47 % (1943904)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.24/35.89 % (1943904)CaDiCaL version: 2.1.3 % 248.24/35.89 % (1943904)Termination reason: Refutation not found, incomplete strategy % 248.24/35.89 % (1943904)Time elapsed: 0.682 s % 248.24/35.89 % (1943904)Peak memory usage: 148 MB % 248.24/35.89 % (1943904)Instructions burned: 1218 (million) % 248.24/35.89 % (1943905)Refutation not found, incomplete strategy % 248.24/35.89 % (1943905)------------------------------ % 248.24/35.89 % (1943905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.24/35.89 % (1943905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.24/35.89 % (1943905)CaDiCaL version: 2.1.3 % 248.24/35.89 % (1943905)Termination reason: Refutation not found, incomplete strategy % 248.24/35.89 % (1943905)Time elapsed: 0.568 s % 248.24/35.89 % (1943905)Peak memory usage: 130 MB % 248.24/35.89 % (1943905)Instructions burned: 854 (million) % 248.24/35.89 % (1943904)------------------------------ % 248.24/35.89 % (1943904)------------------------------ % 248.24/35.89 % (1943905)------------------------------ % 248.24/35.89 % (1943905)------------------------------ % 248.24/35.89 % (1943912)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1010350199:i=20684:bd=all:gtg=exists_sym_2662 on theBenchmark for (2662ds/20684Mi) % 248.24/35.89 % (1943913)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=2687378741: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_2661 on theBenchmark for (2661ds/7222Mi) % 248.24/35.89 % (1943894)Instruction limit reached! % 248.24/35.89 % (1943894)------------------------------ % 248.24/35.89 % (1943894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 248.24/35.89 % (1943894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 248.24/35.89 % (1943894)CaDiCaL version: 2.1.3 % 248.24/35.89 % (1943894)Termination reason: Instruction limit % 248.24/35.89 % (1943894)Termination phase: Saturation % 248.24/35.89 % (1943894)Time elapsed: 3.504 s % 248.24/35.89 % (1943894)Peak memory usage: 169 MB % 248.24/35.89 % (1943894)Instructions burned: 5812 (million) % 248.24/35.89 [W928 14:14:52.264892582 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/35.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.24/35.89 [W928 14:14:52.264941478 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/35.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.24/35.89 [W928 14:14:52.264982289 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/35.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.24/35.89 [W928 14:14:52.264995235 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/35.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.24/35.89 [W928 14:14:52.265033452 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/35.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.24/35.89 [W928 14:14:52.265058849 register_special_ops.cpp:225] Warning: Creating a tensor from 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.24/35.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 248.24/35.89 [W928 14:14:52.265086159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:52.265096986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:52.265122502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:52.265136429 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:52.265160856 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:52.265171319 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 % (1943916)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1087462429:st=4:i=7295:sd=4:ep=R:ss=axioms_2657 on theBenchmark for (2657ds/7295Mi) % 282.67/40.65 % (1943913)Refutation not found, incomplete strategy % 282.67/40.65 % (1943913)------------------------------ % 282.67/40.65 % (1943913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.67/40.65 % (1943913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.67/40.65 % (1943913)CaDiCaL version: 2.1.3 % 282.67/40.65 % (1943913)Termination reason: Refutation not found, incomplete strategy % 282.67/40.65 % (1943913)Time elapsed: 0.569 s % 282.67/40.65 % (1943913)Peak memory usage: 130 MB % 282.67/40.65 % (1943913)Instructions burned: 871 (million) % 282.67/40.65 % (1943907)Instruction limit reached! % 282.67/40.65 % (1943907)------------------------------ % 282.67/40.65 % (1943907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.67/40.65 % (1943907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.67/40.65 % (1943907)CaDiCaL version: 2.1.3 % 282.67/40.65 % (1943907)Termination reason: Instruction limit % 282.67/40.65 % (1943907)Termination phase: Saturation % 282.67/40.65 % (1943907)Time elapsed: 1.644 s % 282.67/40.65 % (1943907)Peak memory usage: 153 MB % 282.67/40.65 % (1943907)Instructions burned: 3395 (million) % 282.67/40.65 [W928 14:14:53.676241448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:53.676275551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:53.676316422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.67/40.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.67/40.65 [W928 14:14:53.676329702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676356748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676424209 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676461535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676472479 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676497779 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676508005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676532189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 [W928 14:14:53.676542602 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 291.91/42.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 291.91/42.03 % (1943913)------------------------------ % 291.91/42.03 % (1943913)------------------------------ % 291.91/42.03 % (1943918)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=1256682923:i=4036:ins=10_2652 on theBenchmark for (2652ds/4036Mi) % 291.91/42.03 % (1943919)lrs+10_1_sil=128000:lcm=predicate:random_seed=2893217766:st=3:i=43697:sd=5:ss=axioms_2651 on theBenchmark for (2651ds/43697Mi) % 291.91/42.03 % (1943919)Refutation not found, incomplete strategy % 291.91/42.03 % (1943919)------------------------------ % 291.91/42.03 % (1943919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.91/42.03 % (1943919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.91/42.03 % (1943919)CaDiCaL version: 2.1.3 % 291.91/42.03 % (1943919)Termination reason: Refutation not found, incomplete strategy % 291.91/42.03 % (1943919)Time elapsed: 0.005 s % 291.91/42.03 % (1943919)Peak memory usage: 88 MB % 291.91/42.03 % (1943919)Instructions burned: 7 (million) % 291.91/42.03 % (1943916)Refutation not found, incomplete strategy % 291.91/42.03 % (1943916)------------------------------ % 291.91/42.03 % (1943916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 291.91/42.03 % (1943916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 291.91/42.03 % (1943916)CaDiCaL version: 2.1.3 % 291.91/42.03 % (1943916)Termination reason: Refutation not found, incomplete strategy % 291.91/42.03 % (1943916)Time elapsed: 0.568 s % 291.91/42.03 % (1943916)Peak memory usage: 130 MB % 291.91/42.03 % (1943916)Instructions burned: 856 (million) % 291.91/42.03 % (1943919)------------------------------ % 295.96/42.58 % (1943919)------------------------------ % 295.96/42.58 % (1943916)------------------------------ % 295.96/42.58 % (1943916)------------------------------ % 295.96/42.58 % (1943923)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=2168836761:i=4547:bd=preordered_2647 on theBenchmark for (2647ds/4547Mi) % 295.96/42.58 % (1943922)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=892879398:i=17599:gtg=all:ss=axioms:fsd=on_2647 on theBenchmark for (2647ds/17599Mi) % 295.96/42.58 % (1943918)Instruction limit reached! % 295.96/42.58 % (1943918)------------------------------ % 295.96/42.58 % (1943918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.96/42.58 % (1943918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.96/42.58 % (1943918)CaDiCaL version: 2.1.3 % 295.96/42.58 % (1943918)Termination reason: Instruction limit % 295.96/42.58 % (1943918)Termination phase: Saturation % 295.96/42.58 % (1943918)Time elapsed: 2.258 s % 295.96/42.58 % (1943918)Peak memory usage: 148 MB % 295.96/42.58 % (1943918)Instructions burned: 4037 (million) % 295.96/42.58 % (1943926)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=1431937864:i=9294:av=off_2627 on theBenchmark for (2627ds/9294Mi) % 295.96/42.58 % (1943923)Instruction limit reached! % 295.96/42.58 % (1943923)------------------------------ % 295.96/42.58 % (1943923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.96/42.58 % (1943923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.96/42.58 % (1943923)CaDiCaL version: 2.1.3 % 295.96/42.58 % (1943923)Termination reason: Instruction limit % 295.96/42.58 % (1943923)Termination phase: Saturation % 295.96/42.58 % (1943923)Time elapsed: 2.814 s % 295.96/42.58 % (1943923)Peak memory usage: 165 MB % 295.96/42.58 % (1943923)Instructions burned: 4548 (million) % 295.96/42.58 % (1943928)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3534929965:i=32849:add=on_2617 on theBenchmark for (2617ds/32849Mi) % 295.96/42.58 % (1943912)Instruction limit reached! % 295.96/42.58 % (1943912)------------------------------ % 295.96/42.58 % (1943912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.96/42.58 % (1943912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.96/42.58 % (1943912)CaDiCaL version: 2.1.3 % 295.96/42.58 % (1943912)Termination reason: Instruction limit % 295.96/42.58 % (1943912)Termination phase: Saturation % 295.96/42.58 % (1943912)Time elapsed: 5.800 s % 295.96/42.58 % (1943912)Peak memory usage: 181 MB % 295.96/42.58 % (1943912)Instructions burned: 20688 (million) % 295.96/42.58 % (1943930)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1842337896:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2603 on theBenchmark for (2603ds/4793Mi) % 295.96/42.58 [W928 14:14:58.862234532 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/42.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.96/42.58 [W928 14:14:58.862257983 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/42.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.96/42.58 [W928 14:14:58.862279528 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/42.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.96/42.58 [W928 14:14:58.862290348 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/42.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 295.96/42.58 [W928 14:14:58.862304428 register_special_ops.cpp:225] WarninTerminated %------------------------------------------------------------------------------