%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWW477_10 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n018.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:35 PM UTC 2026 % Result : Timeout 287.87s 41.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWW477_10 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.18 % Computer : n018.cluster.edu % 0.08/0.18 % Model : x86_64 x86_64 % 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.18 % Memory : 8046.5625MB % 0.08/0.18 % OS : Linux 6.8.0-71-generic % 0.08/0.18 % CPULimit : 300 % 0.08/0.18 % WCLimit : 300 % 0.08/0.18 % DateTime : Mon Sep 28 14:13:40 UTC 2026 % 0.08/0.18 % CPUTime : % 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.08/0.22 Running first-order theorem proving % 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.84/2.14 % (3406420)Detected formulas, will run a generic FOF schedule. % 10.84/2.14 % (3406426)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=672863670:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.84/2.14 % (3406431)dis-21_1_sil=8000:lcm=predicate:random_seed=2704001709: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.84/2.14 % (3406425)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=1078564100:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.84/2.14 % (3406430)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3795416376:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.84/2.14 % (3406428)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3226058085:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.84/2.14 % (3406429)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2168885144:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.84/2.14 % (3406427)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=3055231650:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.84/2.14 % (3406429)Refutation not found, incomplete strategy % 10.84/2.14 % (3406429)------------------------------ % 10.84/2.14 % (3406429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.84/2.14 % (3406429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.84/2.14 % (3406428)Refutation not found, incomplete strategy % 10.84/2.14 % (3406428)------------------------------ % 10.84/2.14 % (3406428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.84/2.14 % (3406428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.84/2.14 % (3406429)CaDiCaL version: 2.1.3 % 10.84/2.14 % (3406429)Termination reason: Refutation not found, incomplete strategy % 10.84/2.14 % (3406429)Time elapsed: 0.001 s % 10.84/2.14 % (3406429)Peak memory usage: 86 MB % 10.84/2.14 % (3406428)CaDiCaL version: 2.1.3 % 10.84/2.14 % (3406428)Termination reason: Refutation not found, incomplete strategy % 10.84/2.14 % (3406428)Time elapsed: 0.001 s % 10.84/2.14 % (3406428)Peak memory usage: 86 MB % 10.84/2.14 % (3406431)Instruction limit reached! % 10.84/2.14 % (3406431)------------------------------ % 10.84/2.14 % (3406431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.84/2.14 % (3406431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.84/2.14 % (3406431)CaDiCaL version: 2.1.3 % 10.84/2.14 % (3406431)Termination reason: Instruction limit % 10.84/2.14 % (3406431)Termination phase: Saturation % 10.84/2.14 % (3406431)Time elapsed: 0.073 s % 10.84/2.14 % (3406431)Peak memory usage: 89 MB % 10.84/2.14 % (3406431)Instructions burned: 129 (million) % 10.84/2.14 % (3406430)Instruction limit reached! % 10.84/2.14 % (3406430)------------------------------ % 10.84/2.14 % (3406430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.84/2.14 % (3406430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.84/2.14 % (3406430)CaDiCaL version: 2.1.3 % 10.84/2.14 % (3406430)Termination reason: Instruction limit % 10.84/2.14 % (3406430)Termination phase: Saturation % 10.84/2.14 % (3406430)Time elapsed: 0.091 s % 10.84/2.14 % (3406430)Peak memory usage: 89 MB % 10.84/2.14 % (3406430)Instructions burned: 140 (million) % 10.84/2.14 % (3406439)lrs+10_1_sil=8000:sp=occurrence:random_seed=543613216:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 10.84/2.14 % (3406439)Refutation not found, incomplete strategy % 10.84/2.14 % (3406439)------------------------------ % 10.84/2.14 % (3406439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.84/2.14 % (3406439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.84/2.14 % (3406439)CaDiCaL version: 2.1.3 % 10.84/2.14 % (3406439)Termination reason: Refutation not found, incomplete strategy % 10.84/2.14 % (3406439)Time elapsed: 0.001 s % 10.84/2.14 % (3406439)Peak memory usage: 86 MB % 10.84/2.14 % (3406429)------------------------------ % 10.84/2.14 % (3406429)------------------------------ % 10.84/2.14 % (3406428)------------------------------ % 10.84/2.14 % (3406428)------------------------------ % 12.09/2.44 % (3406440)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1443139981:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 12.09/2.44 % (3406440)Refutation not found, incomplete strategy % 12.09/2.44 % (3406440)------------------------------ % 12.09/2.44 % (3406440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.44 % (3406440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.44 % (3406440)CaDiCaL version: 2.1.3 % 12.09/2.44 % (3406440)Termination reason: Refutation not found, incomplete strategy % 12.09/2.44 % (3406440)Time elapsed: 0.002 s % 12.09/2.44 % (3406440)Peak memory usage: 87 MB % 12.09/2.44 % (3406440)Instructions burned: 3 (million) % 12.09/2.44 % (3406443)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=4238190666:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 12.09/2.44 % (3406442)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3909679231:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 12.09/2.44 % (3406442)Refutation not found, incomplete strategy % 12.09/2.44 % (3406442)------------------------------ % 12.09/2.44 % (3406442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.44 % (3406442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.44 % (3406442)CaDiCaL version: 2.1.3 % 12.09/2.44 % (3406442)Termination reason: Refutation not found, incomplete strategy % 12.09/2.44 % (3406442)Time elapsed: 0.001 s % 12.09/2.44 % (3406442)Peak memory usage: 87 MB % 12.09/2.44 % (3406439)------------------------------ % 12.09/2.44 % (3406439)------------------------------ % 12.09/2.44 % (3406440)------------------------------ % 12.09/2.44 % (3406440)------------------------------ % 12.09/2.44 % (3406443)Instruction limit reached! % 12.09/2.44 % (3406443)------------------------------ % 12.09/2.44 % (3406443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.44 % (3406443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.44 % (3406443)CaDiCaL version: 2.1.3 % 12.09/2.44 % (3406443)Termination reason: Instruction limit % 12.09/2.44 % (3406443)Termination phase: Saturation % 12.09/2.44 % (3406443)Time elapsed: 0.139 s % 12.09/2.44 % (3406443)Peak memory usage: 91 MB % 12.09/2.44 % (3406443)Instructions burned: 249 (million) % 12.09/2.44 % (3406427)Refutation not found, incomplete strategy % 12.09/2.44 % (3406427)------------------------------ % 12.09/2.44 % (3406427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.44 % (3406427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.44 % (3406427)CaDiCaL version: 2.1.3 % 12.09/2.44 % (3406427)Termination reason: Refutation not found, incomplete strategy % 12.09/2.44 % (3406427)Time elapsed: 0.610 s % 12.09/2.44 % (3406427)Peak memory usage: 132 MB % 12.09/2.44 % (3406427)Instructions burned: 918 (million) % 12.09/2.44 % (3406447)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=211600489:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 12.09/2.44 % (3406447)Refutation not found, incomplete strategy % 12.09/2.44 % (3406447)------------------------------ % 12.09/2.44 % (3406447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.44 % (3406447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.44 % (3406447)CaDiCaL version: 2.1.3 % 12.09/2.44 % (3406447)Termination reason: Refutation not found, incomplete strategy % 12.09/2.44 % (3406447)Time elapsed: 0.001 s % 12.09/2.44 % (3406447)Peak memory usage: 86 MB % 12.09/2.44 % (3406447)Instructions burned: 1 (million) % 12.09/2.44 % (3406442)------------------------------ % 12.09/2.44 % (3406442)------------------------------ % 12.09/2.44 % (3406448)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4043790759:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 12.09/2.44 % (3406449)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3438036957:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 12.09/2.44 % (3406449)Refutation not found, incomplete strategy % 12.09/2.44 % (3406449)------------------------------ % 12.09/2.44 % (3406449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.09/2.44 % (3406449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.09/2.44 % (3406449)CaDiCaL version: 2.1.3 % 13.32/2.68 % (3406449)Termination reason: Refutation not found, incomplete strategy % 13.32/2.68 % (3406449)Time elapsed: 0.017 s % 13.32/2.68 % (3406449)Peak memory usage: 89 MB % 13.32/2.68 % (3406449)Instructions burned: 31 (million) % 13.32/2.68 % (3406452)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2802590007:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 13.32/2.68 % (3406452)Refutation not found, incomplete strategy % 13.32/2.68 % (3406452)------------------------------ % 13.32/2.68 % (3406452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.32/2.68 % (3406452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.32/2.68 % (3406452)CaDiCaL version: 2.1.3 % 13.32/2.68 % (3406452)Termination reason: Refutation not found, incomplete strategy % 13.32/2.68 % (3406452)Time elapsed: 0.011 s % 13.32/2.68 % (3406452)Peak memory usage: 88 MB % 13.32/2.68 % (3406452)Instructions burned: 21 (million) % 13.32/2.68 % (3406427)------------------------------ % 13.32/2.68 % (3406427)------------------------------ % 13.32/2.68 % (3406447)------------------------------ % 13.32/2.68 % (3406447)------------------------------ % 13.32/2.68 % (3406449)------------------------------ % 13.32/2.68 % (3406449)------------------------------ % 13.32/2.68 % (3406455)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3186809899:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi) % 13.32/2.68 % (3406456)lrs+10_1_sil=8000:sp=occurrence:random_seed=1545959559:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 13.32/2.68 % (3406456)Refutation not found, incomplete strategy % 13.32/2.68 % (3406456)------------------------------ % 13.32/2.68 % (3406456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.32/2.68 % (3406456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.32/2.68 % (3406456)CaDiCaL version: 2.1.3 % 13.32/2.68 % (3406456)Termination reason: Refutation not found, incomplete strategy % 13.32/2.68 % (3406456)Time elapsed: 0.001 s % 13.32/2.68 % (3406456)Peak memory usage: 86 MB % 13.32/2.68 % (3406452)------------------------------ % 13.32/2.68 % (3406452)------------------------------ % 13.32/2.68 % (3406455)Instruction limit reached! % 13.32/2.68 % (3406455)------------------------------ % 13.32/2.68 % (3406455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.32/2.68 % (3406455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.32/2.68 % (3406455)CaDiCaL version: 2.1.3 % 13.32/2.68 % (3406455)Termination reason: Instruction limit % 13.32/2.68 % (3406455)Termination phase: Saturation % 13.32/2.68 % (3406455)Time elapsed: 0.063 s % 13.32/2.68 % (3406455)Peak memory usage: 89 MB % 13.32/2.68 % (3406455)Instructions burned: 116 (million) % 13.32/2.68 % (3406457)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1557179093:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi) % 13.32/2.68 % (3406457)Refutation not found, incomplete strategy % 13.32/2.68 % (3406457)------------------------------ % 13.32/2.68 % (3406457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.32/2.68 % (3406457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.32/2.68 % (3406457)CaDiCaL version: 2.1.3 % 13.32/2.68 % (3406457)Termination reason: Refutation not found, incomplete strategy % 13.32/2.68 % (3406457)Time elapsed: 0.015 s % 13.32/2.68 % (3406457)Peak memory usage: 89 MB % 13.32/2.68 % (3406457)Instructions burned: 27 (million) % 13.32/2.68 % (3406461)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2349439165:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 13.32/2.68 % (3406460)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2072175711:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi) % 13.32/2.68 % (3406456)------------------------------ % 13.32/2.68 % (3406456)------------------------------ % 13.32/2.68 % (3406461)Instruction limit reached! % 13.32/2.68 % (3406461)------------------------------ % 13.32/2.68 % (3406461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.32/2.68 % (3406461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.32/2.68 % (3406461)CaDiCaL version: 2.1.3 % 13.32/2.68 % (3406461)Termination reason: Instruction limit % 13.32/2.68 % (3406461)Termination phase: Saturation % 13.32/2.68 % (3406461)Time elapsed: 0.077 s % 13.32/2.68 % (3406461)Peak memory usage: 90 MB % 13.32/2.68 % (3406461)Instructions burned: 135 (million) % 15.15/2.92 % (3406457)------------------------------ % 15.15/2.92 % (3406457)------------------------------ % 15.15/2.92 % (3406466)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3303446167:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi) % 15.15/2.92 % (3406466)Refutation not found, incomplete strategy % 15.15/2.92 % (3406466)------------------------------ % 15.15/2.92 % (3406466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.15/2.92 % (3406466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.92 % (3406466)CaDiCaL version: 2.1.3 % 15.15/2.92 % (3406466)Termination reason: Refutation not found, incomplete strategy % 15.15/2.92 % (3406466)Time elapsed: 0.001 s % 15.15/2.92 % (3406466)Peak memory usage: 86 MB % 15.15/2.92 % (3406466)Instructions burned: 1 (million) % 15.15/2.92 % (3406467)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1384450095:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 15.15/2.92 % (3406468)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=3099005712:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi) % 15.15/2.92 % (3406468)Refutation not found, incomplete strategy % 15.15/2.92 % (3406468)------------------------------ % 15.15/2.92 % (3406468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.15/2.92 % (3406468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.15/2.92 % (3406468)CaDiCaL version: 2.1.3 % 15.15/2.92 % (3406468)Termination reason: Refutation not found, incomplete strategy % 15.15/2.92 % (3406468)Time elapsed: 0.002 s % 15.15/2.92 % (3406468)Peak memory usage: 87 MB % 15.15/2.92 % (3406468)Instructions burned: 3 (million) % 15.15/2.92 [W928 14:13:42.871537175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871570986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871607169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871630836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871656906 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871667920 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871692643 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.15/2.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.15/2.92 [W928 14:13:42.871708703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.871733167 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.871747527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.871771890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.871785507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 % (3406466)------------------------------ % 18.87/3.45 % (3406466)------------------------------ % 18.87/3.45 % (3406460)Refutation not found, incomplete strategy % 18.87/3.45 % (3406460)------------------------------ % 18.87/3.45 % (3406460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.87/3.45 % (3406460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.87/3.45 % (3406460)CaDiCaL version: 2.1.3 % 18.87/3.45 % (3406460)Termination reason: Refutation not found, incomplete strategy % 18.87/3.45 % (3406460)Time elapsed: 0.551 s % 18.87/3.45 % (3406460)Peak memory usage: 125 MB % 18.87/3.45 % (3406460)Instructions burned: 828 (million) % 18.87/3.45 % (3406468)------------------------------ % 18.87/3.45 % (3406468)------------------------------ % 18.87/3.45 [W928 14:13:42.100516447 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.100565950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.100606914 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.100618658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.100644034 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.100655228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.87/3.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.87/3.45 [W928 14:13:42.100680101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.57/5.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.57/5.24 [W928 14:13:42.100691551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.57/5.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.57/5.24 [W928 14:13:42.100715732 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.57/5.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.57/5.24 [W928 14:13:42.100727082 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.57/5.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.57/5.24 [W928 14:13:42.100751902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.57/5.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.57/5.24 [W928 14:13:42.100763179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.57/5.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.57/5.24 % (3406472)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4126066844:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi) % 32.57/5.24 % (3406472)Instruction limit reached! % 32.57/5.24 % (3406472)------------------------------ % 32.57/5.24 % (3406472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.57/5.24 % (3406472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.57/5.24 % (3406472)CaDiCaL version: 2.1.3 % 32.57/5.24 % (3406472)Termination reason: Instruction limit % 32.57/5.24 % (3406472)Termination phase: Saturation % 32.57/5.24 % (3406472)Time elapsed: 0.069 s % 32.57/5.24 % (3406472)Peak memory usage: 90 MB % 32.57/5.24 % (3406472)Instructions burned: 136 (million) % 32.57/5.24 % (3406473)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4229869169:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi) % 32.57/5.24 % (3406473)Refutation not found, incomplete strategy % 32.57/5.24 % (3406473)------------------------------ % 32.57/5.24 % (3406473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.57/5.24 % (3406473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.57/5.24 % (3406473)CaDiCaL version: 2.1.3 % 32.57/5.24 % (3406473)Termination reason: Refutation not found, incomplete strategy % 32.57/5.24 % (3406473)Time elapsed: 0.001 s % 32.57/5.24 % (3406473)Peak memory usage: 86 MB % 32.57/5.24 % (3406467)Refutation not found, incomplete strategy % 32.57/5.24 % (3406467)------------------------------ % 32.57/5.24 % (3406467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.57/5.24 % (3406467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.57/5.24 % (3406467)CaDiCaL version: 2.1.3 % 32.57/5.24 % (3406467)Termination reason: Refutation not found, incomplete strategy % 32.57/5.24 % (3406467)Time elapsed: 0.545 s % 32.57/5.24 % (3406467)Peak memory usage: 125 MB % 32.57/5.24 % (3406467)Instructions burned: 824 (million) % 32.57/5.24 % (3406460)------------------------------ % 32.57/5.24 % (3406460)------------------------------ % 32.57/5.24 % (3406475)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1276180177:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi) % 32.57/5.24 % (3406475)Refutation not found, incomplete strategy % 32.57/5.24 % (3406475)------------------------------ % 32.57/5.24 % (3406475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.57/5.24 % (3406475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.70/5.82 % (3406475)CaDiCaL version: 2.1.3 % 36.70/5.82 % (3406475)Termination reason: Refutation not found, incomplete strategy % 36.70/5.82 % (3406475)Time elapsed: 0.001 s % 36.70/5.82 % (3406475)Peak memory usage: 86 MB % 36.70/5.82 % (3406448)Instruction limit reached! % 36.70/5.82 % (3406448)------------------------------ % 36.70/5.82 % (3406448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.70/5.82 % (3406448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.70/5.82 % (3406448)CaDiCaL version: 2.1.3 % 36.70/5.82 % (3406448)Termination reason: Instruction limit % 36.70/5.82 % (3406448)Termination phase: Saturation % 36.70/5.82 % (3406448)Time elapsed: 1.478 s % 36.70/5.82 % (3406448)Peak memory usage: 139 MB % 36.70/5.82 % (3406448)Instructions burned: 2350 (million) % 36.70/5.82 % (3406477)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=4203513297:i=6060:aac=none:ins=25_2977 on theBenchmark for (2977ds/6060Mi) % 36.70/5.82 % (3406473)------------------------------ % 36.70/5.82 % (3406473)------------------------------ % 36.70/5.82 % (3406467)------------------------------ % 36.70/5.82 % (3406467)------------------------------ % 36.70/5.82 % (3406479)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=3109301208:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi) % 36.70/5.82 % (3406475)------------------------------ % 36.70/5.82 % (3406475)------------------------------ % 36.70/5.82 % (3406481)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=827838843:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi) % 36.70/5.82 % (3406479)Instruction limit reached! % 36.70/5.82 % (3406479)------------------------------ % 36.70/5.82 % (3406479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.70/5.82 % (3406479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.70/5.82 % (3406479)CaDiCaL version: 2.1.3 % 36.70/5.82 % (3406479)Termination reason: Instruction limit % 36.70/5.82 % (3406479)Termination phase: Saturation % 36.70/5.82 % (3406479)Time elapsed: 0.102 s % 36.70/5.82 % (3406479)Peak memory usage: 91 MB % 36.70/5.82 % (3406479)Instructions burned: 150 (million) % 36.70/5.82 % (3406482)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2663673937:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi) % 36.70/5.82 % (3406482)Refutation not found, incomplete strategy % 36.70/5.82 % (3406482)------------------------------ % 36.70/5.82 % (3406482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.70/5.82 % (3406482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.70/5.82 % (3406482)CaDiCaL version: 2.1.3 % 36.70/5.82 % (3406482)Termination reason: Refutation not found, incomplete strategy % 36.70/5.82 % (3406482)Time elapsed: 0.015 s % 36.70/5.82 % (3406482)Peak memory usage: 89 MB % 36.70/5.82 % (3406482)Instructions burned: 28 (million) % 36.70/5.82 % (3406484)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=4228819015:s2a=on:i=185:s2at=1.8:fdi=4_2974 on theBenchmark for (2974ds/185Mi) % 36.70/5.82 % (3406486)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1156684759:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/193Mi) % 36.70/5.82 % (3406486)Refutation not found, incomplete strategy % 36.70/5.82 % (3406486)------------------------------ % 36.70/5.82 % (3406486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.70/5.82 % (3406486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.70/5.82 % (3406486)CaDiCaL version: 2.1.3 % 36.70/5.82 % (3406486)Termination reason: Refutation not found, incomplete strategy % 36.70/5.82 % (3406486)Time elapsed: 0.001 s % 36.70/5.82 % (3406486)Peak memory usage: 86 MB % 36.70/5.82 % (3406486)Instructions burned: 1 (million) % 36.70/5.82 % (3406484)Instruction limit reached! % 36.70/5.82 % (3406484)------------------------------ % 36.70/5.82 % (3406484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 36.70/5.82 % (3406484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 36.70/5.82 % (3406484)CaDiCaL version: 2.1.3 % 42.94/6.84 % (3406484)Termination reason: Instruction limit % 42.94/6.84 % (3406484)Termination phase: Saturation % 42.94/6.84 % (3406484)Time elapsed: 0.120 s % 42.94/6.84 % (3406484)Peak memory usage: 91 MB % 42.94/6.84 % (3406484)Instructions burned: 185 (million) % 42.94/6.84 % (3406482)------------------------------ % 42.94/6.84 % (3406482)------------------------------ % 42.94/6.84 % (3406490)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1883408172:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi) % 42.94/6.84 % (3406490)Refutation not found, incomplete strategy % 42.94/6.84 % (3406490)------------------------------ % 42.94/6.84 % (3406490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.94/6.84 % (3406490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.94/6.84 % (3406490)CaDiCaL version: 2.1.3 % 42.94/6.84 % (3406490)Termination reason: Refutation not found, incomplete strategy % 42.94/6.84 % (3406490)Time elapsed: 0.012 s % 42.94/6.84 % (3406490)Peak memory usage: 88 MB % 42.94/6.84 % (3406490)Instructions burned: 23 (million) % 42.94/6.84 % (3406486)------------------------------ % 42.94/6.84 % (3406486)------------------------------ % 42.94/6.84 % (3406491)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2216677807:i=12111:sd=1:ss=included_2971 on theBenchmark for (2971ds/12111Mi) % 42.94/6.84 % (3406493)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=790627989:i=319:kws=precedence:fsr=off_2970 on theBenchmark for (2970ds/319Mi) % 42.94/6.84 % (3406490)------------------------------ % 42.94/6.84 % (3406490)------------------------------ % 42.94/6.84 % (3406493)Instruction limit reached! % 42.94/6.84 % (3406493)------------------------------ % 42.94/6.84 % (3406493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.94/6.84 % (3406493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.94/6.84 % (3406493)CaDiCaL version: 2.1.3 % 42.94/6.84 % (3406493)Termination reason: Instruction limit % 42.94/6.84 % (3406493)Termination phase: Saturation % 42.94/6.84 % (3406493)Time elapsed: 0.183 s % 42.94/6.84 % (3406493)Peak memory usage: 92 MB % 42.94/6.84 % (3406493)Instructions burned: 321 (million) % 42.94/6.84 % (3406496)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=432409870:i=2064:ep=RST_2967 on theBenchmark for (2967ds/2064Mi) % 42.94/6.84 % (3406496)Refutation not found, incomplete strategy % 42.94/6.84 % (3406496)------------------------------ % 42.94/6.84 % (3406496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.94/6.84 % (3406496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.94/6.84 % (3406496)CaDiCaL version: 2.1.3 % 42.94/6.84 % (3406496)Termination reason: Refutation not found, incomplete strategy % 42.94/6.84 % (3406496)Time elapsed: 0.014 s % 42.94/6.84 % (3406496)Peak memory usage: 88 MB % 42.94/6.84 % (3406496)Instructions burned: 28 (million) % 42.94/6.84 % (3406497)dis-1011_128_sil=32000:random_seed=1197102955:i=3706:ep=RST:av=off_2966 on theBenchmark for (2966ds/3706Mi) % 42.94/6.84 % (3406496)------------------------------ % 42.94/6.84 % (3406496)------------------------------ % 42.94/6.84 % (3406500)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1232806760:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2963 on theBenchmark for (2963ds/757Mi) % 42.94/6.84 % (3406500)Refutation not found, incomplete strategy % 42.94/6.84 % (3406500)------------------------------ % 42.94/6.84 % (3406500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.94/6.84 % (3406500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.94/6.84 % (3406500)CaDiCaL version: 2.1.3 % 42.94/6.84 % (3406500)Termination reason: Refutation not found, incomplete strategy % 42.94/6.84 % (3406500)Time elapsed: 0.001 s % 42.94/6.84 % (3406500)Peak memory usage: 86 MB % 42.94/6.84 % (3406500)------------------------------ % 42.94/6.84 % (3406500)------------------------------ % 42.94/6.84 % (3406502)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=208067254:i=13913:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/13913Mi) % 42.94/6.84 [W928 14:13:45.669022898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.94/6.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669057022 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669104296 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669130836 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669157023 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669167343 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669191720 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669202000 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669225870 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669236340 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669260427 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 [W928 14:13:45.669270970 register_special_ops.cpp:225] Warning: Creating a tensor from 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.54/7.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.54/7.04 % (3406502)Refutation not found, incomplete strategy % 45.54/7.04 % (3406502)------------------------------ % 45.54/7.04 % (3406502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.54/7.04 % (3406502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.54/7.04 % (3406502)CaDiCaL version: 2.1.3 % 45.54/7.04 % (3406502)Termination reason: Refutation not found, incomplete strategy % 45.54/7.04 % (3406502)Time elapsed: 0.545 s % 45.54/7.04 % (3406502)Peak memory usage: 125 MB % 45.54/7.04 % (3406502)Instructions burned: 828 (million) % 45.54/7.04 % (3406502)------------------------------ % 45.54/7.04 % (3406502)------------------------------ % 45.54/7.04 % (3406504)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=444455233:i=9925:aac=none_2949 on theBenchmark for (2949ds/9925Mi) % 76.56/11.43 % (3406477)Instruction limit reached! % 76.56/11.43 % (3406477)------------------------------ % 76.56/11.43 % (3406477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.56/11.43 % (3406477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.56/11.43 % (3406477)CaDiCaL version: 2.1.3 % 76.56/11.43 % (3406477)Termination reason: Instruction limit % 76.56/11.43 % (3406477)Termination phase: Saturation % 76.56/11.43 % (3406477)Time elapsed: 2.894 s % 76.56/11.43 % (3406477)Peak memory usage: 138 MB % 76.56/11.43 % (3406477)Instructions burned: 6062 (million) % 76.56/11.43 % (3406497)Instruction limit reached! % 76.56/11.43 % (3406497)------------------------------ % 76.56/11.43 % (3406497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.56/11.43 % (3406497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.56/11.43 % (3406497)CaDiCaL version: 2.1.3 % 76.56/11.43 % (3406497)Termination reason: Instruction limit % 76.56/11.43 % (3406497)Termination phase: Saturation % 76.56/11.43 % (3406497)Time elapsed: 1.783 s % 76.56/11.43 % (3406497)Peak memory usage: 100 MB % 76.56/11.43 % (3406497)Instructions burned: 3706 (million) % 76.56/11.43 % (3406506)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=37185227:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2947 on theBenchmark for (2947ds/2479Mi) % 76.56/11.43 % (3406507)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3491419591:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2946 on theBenchmark for (2946ds/440Mi) % 76.56/11.43 % (3406506)Refutation not found, incomplete strategy % 76.56/11.43 % (3406506)------------------------------ % 76.56/11.43 % (3406506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.56/11.43 % (3406506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.56/11.43 % (3406506)CaDiCaL version: 2.1.3 % 76.56/11.43 % (3406506)Termination reason: Refutation not found, incomplete strategy % 76.56/11.43 % (3406506)Time elapsed: 0.001 s % 76.56/11.43 % (3406506)Peak memory usage: 86 MB % 76.56/11.43 % (3406506)Instructions burned: 1 (million) % 76.56/11.43 % (3406506)------------------------------ % 76.56/11.43 % (3406506)------------------------------ % 76.56/11.43 % (3406507)Instruction limit reached! % 76.56/11.43 % (3406507)------------------------------ % 76.56/11.43 % (3406507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.56/11.43 % (3406507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.56/11.43 % (3406507)CaDiCaL version: 2.1.3 % 76.56/11.43 % (3406507)Termination reason: Instruction limit % 76.56/11.43 % (3406507)Termination phase: Saturation % 76.56/11.43 % (3406507)Time elapsed: 0.265 s % 76.56/11.43 % (3406507)Peak memory usage: 93 MB % 76.56/11.43 % (3406507)Instructions burned: 440 (million) % 76.56/11.43 % (3406504)Refutation not found, incomplete strategy % 76.56/11.43 % (3406504)------------------------------ % 76.56/11.43 % (3406504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.56/11.43 % (3406504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.56/11.43 % (3406504)CaDiCaL version: 2.1.3 % 76.56/11.43 % (3406504)Termination reason: Refutation not found, incomplete strategy % 76.56/11.43 % (3406504)Time elapsed: 0.600 s % 76.56/11.43 % (3406504)Peak memory usage: 133 MB % 76.56/11.43 % (3406504)Instructions burned: 912 (million) % 76.56/11.43 % (3406510)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4275543027:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2943 on theBenchmark for (2943ds/11145Mi) % 76.56/11.43 % (3406511)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=3420469138:cts=off:i=3034:av=off:er=known:fsd=on_2942 on theBenchmark for (2942ds/3034Mi) % 76.56/11.43 % (3406504)------------------------------ % 76.56/11.43 % (3406504)------------------------------ % 76.56/11.43 % (3406514)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2852567469:st=2:s2a=on:i=524:s2at=2:ss=axioms_2939 on theBenchmark for (2939ds/524Mi) % 76.56/11.43 % (3406514)Refutation not found, incomplete strategy % 76.56/11.43 % (3406514)------------------------------ % 76.56/11.43 % (3406514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.56/11.43 % (3406514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.21/11.54 % (3406514)CaDiCaL version: 2.1.3 % 77.21/11.54 % (3406514)Termination reason: Refutation not found, incomplete strategy % 77.21/11.54 % (3406514)Time elapsed: 0.002 s % 77.21/11.54 % (3406514)Peak memory usage: 87 MB % 77.21/11.54 % (3406514)Instructions burned: 2 (million) % 77.21/11.54 [W928 14:13:46.300457558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300491718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300529788 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300542705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300569872 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300592372 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300619435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300630582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300655052 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300669102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300694023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 [W928 14:13:46.300704309 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.21/11.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.21/11.54 % (3406510)Refutation not found, incomplete strategy % 79.27/11.97 % (3406510)------------------------------ % 79.27/11.97 % (3406510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.27/11.97 % (3406510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.27/11.97 % (3406510)CaDiCaL version: 2.1.3 % 79.27/11.97 % (3406510)Termination reason: Refutation not found, incomplete strategy % 79.27/11.97 % (3406510)Time elapsed: 0.546 s % 79.27/11.97 % (3406510)Peak memory usage: 126 MB % 79.27/11.97 % (3406510)Instructions burned: 825 (million) % 79.27/11.97 % (3406514)------------------------------ % 79.27/11.97 % (3406514)------------------------------ % 79.27/11.97 % (3406516)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=246875656:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2935 on theBenchmark for (2935ds/1016Mi) % 79.27/11.97 % (3406516)Refutation not found, incomplete strategy % 79.27/11.97 % (3406516)------------------------------ % 79.27/11.97 % (3406516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.27/11.97 % (3406516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.27/11.97 % (3406516)CaDiCaL version: 2.1.3 % 79.27/11.97 % (3406516)Termination reason: Refutation not found, incomplete strategy % 79.27/11.97 % (3406516)Time elapsed: 0.001 s % 79.27/11.97 % (3406516)Peak memory usage: 87 MB % 79.27/11.97 % (3406510)------------------------------ % 79.27/11.97 % (3406510)------------------------------ % 79.27/11.97 % (3406518)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1725971725:i=14123:bd=preordered:ins=4_2933 on theBenchmark for (2933ds/14123Mi) % 79.27/11.97 % (3406516)------------------------------ % 79.27/11.97 % (3406516)------------------------------ % 79.27/11.97 % (3406520)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3441344456:i=5781:kws=precedence:bd=all:rawr=on_2931 on theBenchmark for (2931ds/5781Mi) % 79.27/11.97 % (3406511)Instruction limit reached! % 79.27/11.97 % (3406511)------------------------------ % 79.27/11.97 % (3406511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.27/11.97 % (3406511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.27/11.97 % (3406511)CaDiCaL version: 2.1.3 % 79.27/11.97 % (3406511)Termination reason: Instruction limit % 79.27/11.97 % (3406511)Termination phase: Saturation % 79.27/11.97 % (3406511)Time elapsed: 1.743 s % 79.27/11.97 % (3406511)Peak memory usage: 139 MB % 79.27/11.97 % (3406511)Instructions burned: 3035 (million) % 79.27/11.97 % (3406522)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=876641928:i=2448:gtgl=5:bd=preordered:gtg=all_2923 on theBenchmark for (2923ds/2448Mi) % 79.27/11.97 % (3406522)Instruction limit reached! % 79.27/11.97 % (3406522)------------------------------ % 79.27/11.97 % (3406522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.27/11.97 % (3406522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.27/11.97 % (3406522)CaDiCaL version: 2.1.3 % 79.27/11.97 % (3406522)Termination reason: Instruction limit % 79.27/11.97 % (3406522)Termination phase: Saturation % 79.27/11.97 % (3406522)Time elapsed: 1.499 s % 79.27/11.97 % (3406522)Peak memory usage: 144 MB % 79.27/11.97 % (3406522)Instructions burned: 2448 (million) % 79.27/11.97 % (3406524)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=920555349:i=3223:kws=precedence:fgj=on:av=off_2907 on theBenchmark for (2907ds/3223Mi) % 79.27/11.97 % (3406520)Instruction limit reached! % 79.27/11.97 % (3406520)------------------------------ % 79.27/11.97 % (3406520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.27/11.97 % (3406520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.27/11.97 % (3406520)CaDiCaL version: 2.1.3 % 79.27/11.97 % (3406520)Termination reason: Instruction limit % 79.27/11.97 % (3406520)Termination phase: Saturation % 79.27/11.97 % (3406520)Time elapsed: 3.331 s % 79.27/11.97 % (3406520)Peak memory usage: 113 MB % 79.27/11.97 % (3406520)Instructions burned: 5782 (million) % 79.27/11.97 % (3406526)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1278865314:st=5.6:i=2033:sd=3:ss=axioms_2896 on theBenchmark for (2896ds/2033Mi) % 79.27/11.97 % (3406481)Instruction limit reached! % 79.27/11.97 % (3406481)------------------------------ % 79.27/11.97 % (3406481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.27/11.97 % (3406481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.05/12.04 % (3406481)CaDiCaL version: 2.1.3 % 81.05/12.04 % (3406481)Termination reason: Instruction limit % 81.05/12.04 % (3406481)Termination phase: Saturation % 81.05/12.04 % (3406481)Time elapsed: 8.194 s % 81.05/12.04 % (3406481)Peak memory usage: 174 MB % 81.05/12.04 % (3406481)Instructions burned: 14156 (million) % 81.05/12.04 % (3406491)Instruction limit reached! % 81.05/12.04 % (3406491)------------------------------ % 81.05/12.04 % (3406491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.05/12.04 % (3406491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.05/12.04 % (3406491)CaDiCaL version: 2.1.3 % 81.05/12.04 % (3406491)Termination reason: Instruction limit % 81.05/12.04 % (3406491)Termination phase: Saturation % 81.05/12.04 % (3406491)Time elapsed: 7.824 s % 81.05/12.04 % (3406491)Peak memory usage: 216 MB % 81.05/12.04 % (3406491)Instructions burned: 12112 (million) % 81.05/12.04 [W928 14:13:51.964968941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965078745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965124642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965137749 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965165829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965177529 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965204240 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965215823 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965241046 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965252350 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.05/12.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.05/12.04 [W928 14:13:51.965277617 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.965288837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 % (3406528)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=826502920:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2892 on theBenchmark for (2892ds/2055Mi) % 83.89/12.57 % (3406529)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=2111424692:i=21611:sd=3:ss=axioms_2891 on theBenchmark for (2891ds/21611Mi) % 83.89/12.57 % (3406526)Refutation not found, incomplete strategy % 83.89/12.57 % (3406526)------------------------------ % 83.89/12.57 % (3406526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.89/12.57 % (3406526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.89/12.57 % (3406526)CaDiCaL version: 2.1.3 % 83.89/12.57 % (3406526)Termination reason: Refutation not found, incomplete strategy % 83.89/12.57 % (3406526)Time elapsed: 0.571 s % 83.89/12.57 % (3406526)Peak memory usage: 125 MB % 83.89/12.57 % (3406526)Instructions burned: 830 (million) % 83.89/12.57 [W928 14:13:51.394090569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394127306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394167676 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394181073 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394206503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394227113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394253760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394264347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.89/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.89/12.57 [W928 14:13:51.394292790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:51.394303157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:51.394328227 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:51.394338837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 % (3406526)------------------------------ % 93.00/13.85 % (3406526)------------------------------ % 93.00/13.85 [W928 14:13:52.470086401 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470120955 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470158888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470172108 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470200039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470211549 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470238829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470250419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470275996 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.00/13.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.00/13.85 [W928 14:13:52.470287299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 99.50/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.50/14.77 [W928 14:13:52.470312716 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 99.50/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.50/14.77 [W928 14:13:52.470323180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 99.50/14.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 99.50/14.77 % (3406528)Refutation not found, incomplete strategy % 99.50/14.77 % (3406528)------------------------------ % 99.50/14.77 % (3406528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.50/14.77 % (3406528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.50/14.77 % (3406528)CaDiCaL version: 2.1.3 % 99.50/14.77 % (3406528)Termination reason: Refutation not found, incomplete strategy % 99.50/14.77 % (3406528)Time elapsed: 0.550 s % 99.50/14.77 % (3406528)Peak memory usage: 126 MB % 99.50/14.77 % (3406528)Instructions burned: 831 (million) % 99.50/14.77 % (3406532)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3821863723:i=4835:sd=13:ss=axioms:sgt=23_2886 on theBenchmark for (2886ds/4835Mi) % 99.50/14.77 % (3406532)Refutation not found, incomplete strategy % 99.50/14.77 % (3406532)------------------------------ % 99.50/14.77 % (3406532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.50/14.77 % (3406532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.50/14.77 % (3406532)CaDiCaL version: 2.1.3 % 99.50/14.77 % (3406532)Termination reason: Refutation not found, incomplete strategy % 99.50/14.77 % (3406532)Time elapsed: 0.001 s % 99.50/14.77 % (3406532)Peak memory usage: 86 MB % 99.50/14.77 % (3406529)Refutation not found, incomplete strategy % 99.50/14.77 % (3406529)------------------------------ % 99.50/14.77 % (3406529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.50/14.77 % (3406529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.50/14.77 % (3406529)CaDiCaL version: 2.1.3 % 99.50/14.77 % (3406529)Termination reason: Refutation not found, incomplete strategy % 99.50/14.77 % (3406529)Time elapsed: 0.543 s % 99.50/14.77 % (3406529)Peak memory usage: 125 MB % 99.50/14.77 % (3406529)Instructions burned: 829 (million) % 99.50/14.77 % (3406524)Instruction limit reached! % 99.50/14.77 % (3406524)------------------------------ % 99.50/14.77 % (3406524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 99.50/14.77 % (3406524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 99.50/14.77 % (3406524)CaDiCaL version: 2.1.3 % 99.50/14.77 % (3406524)Termination reason: Instruction limit % 99.50/14.77 % (3406524)Termination phase: Saturation % 99.50/14.77 % (3406524)Time elapsed: 2.128 s % 99.50/14.77 % (3406524)Peak memory usage: 146 MB % 99.50/14.77 % (3406524)Instructions burned: 3223 (million) % 99.50/14.77 % (3406528)------------------------------ % 99.50/14.77 % (3406528)------------------------------ % 99.50/14.77 % (3406532)------------------------------ % 99.50/14.77 % (3406532)------------------------------ % 99.50/14.77 % (3406534)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=2759737941:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2884 on theBenchmark for (2884ds/797Mi) % 99.50/14.77 % (3406529)------------------------------ % 99.50/14.77 % (3406529)------------------------------ % 99.50/14.77 % (3406536)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3497105166:i=6038:nm=6_2882 on theBenchmark for (2882ds/6038Mi) % 99.50/14.77 % (3406535)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3463815622:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2882 on theBenchmark for (2882ds/2326Mi) % 99.50/14.77 % (3406535)Refutation not found, incomplete strategy % 99.50/14.77 % (3406535)------------------------------ % 99.50/14.77 % (3406535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.61/16.71 % (3406535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.61/16.71 % (3406535)CaDiCaL version: 2.1.3 % 113.61/16.71 % (3406535)Termination reason: Refutation not found, incomplete strategy % 113.61/16.71 % (3406535)Time elapsed: 0.025 s % 113.61/16.71 % (3406535)Peak memory usage: 89 MB % 113.61/16.71 % (3406535)Instructions burned: 44 (million) % 113.61/16.71 % (3406538)lrs+10_1_sil=32000:sp=occurrence:random_seed=69381225:st=2:i=33334:sd=3:ss=included:sgt=32_2881 on theBenchmark for (2881ds/33334Mi) % 113.61/16.71 % (3406535)------------------------------ % 113.61/16.71 % (3406535)------------------------------ % 113.61/16.71 % (3406534)Instruction limit reached! % 113.61/16.71 % (3406534)------------------------------ % 113.61/16.71 % (3406534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.61/16.71 % (3406534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.61/16.71 % (3406534)CaDiCaL version: 2.1.3 % 113.61/16.71 % (3406534)Termination reason: Instruction limit % 113.61/16.71 % (3406534)Termination phase: Saturation % 113.61/16.71 % (3406534)Time elapsed: 0.522 s % 113.61/16.71 % (3406534)Peak memory usage: 98 MB % 113.61/16.71 % (3406534)Instructions burned: 797 (million) % 113.61/16.71 % (3406542)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3694559105:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2878 on theBenchmark for (2878ds/1008Mi) % 113.61/16.71 % (3406542)Refutation not found, incomplete strategy % 113.61/16.71 % (3406542)------------------------------ % 113.61/16.71 % (3406542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.61/16.71 % (3406542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.61/16.71 % (3406542)CaDiCaL version: 2.1.3 % 113.61/16.71 % (3406542)Termination reason: Refutation not found, incomplete strategy % 113.61/16.71 % (3406542)Time elapsed: 0.001 s % 113.61/16.71 % (3406542)Peak memory usage: 86 MB % 113.61/16.71 % (3406542)Instructions burned: 1 (million) % 113.61/16.71 % (3406543)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=2109376294:i=8327:s2at=5:bd=preordered_2877 on theBenchmark for (2877ds/8327Mi) % 113.61/16.71 % (3406536)Refutation not found, incomplete strategy % 113.61/16.71 % (3406536)------------------------------ % 113.61/16.71 % (3406536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.61/16.71 % (3406536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.61/16.71 % (3406536)CaDiCaL version: 2.1.3 % 113.61/16.71 % (3406536)Termination reason: Refutation not found, incomplete strategy % 113.61/16.71 % (3406536)Time elapsed: 0.603 s % 113.61/16.71 % (3406536)Peak memory usage: 133 MB % 113.61/16.71 % (3406536)Instructions burned: 912 (million) % 113.61/16.71 % (3406542)------------------------------ % 113.61/16.71 % (3406542)------------------------------ % 113.61/16.71 % (3406546)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=3340783850:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2874 on theBenchmark for (2874ds/1083Mi) % 113.61/16.71 % (3406536)------------------------------ % 113.61/16.71 % (3406536)------------------------------ % 113.61/16.71 % (3406548)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2817719785:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2872 on theBenchmark for (2872ds/1084Mi) % 113.61/16.71 % (3406548)Refutation not found, incomplete strategy % 113.61/16.71 % (3406548)------------------------------ % 113.61/16.71 % (3406548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.61/16.71 % (3406548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.61/16.71 % (3406548)CaDiCaL version: 2.1.3 % 113.61/16.71 % (3406548)Termination reason: Refutation not found, incomplete strategy % 113.61/16.71 % (3406548)Time elapsed: 0.001 s % 113.61/16.71 % (3406548)Peak memory usage: 86 MB % 113.61/16.71 % (3406548)------------------------------ % 113.61/16.71 % (3406548)------------------------------ % 113.61/16.71 % (3406546)Instruction limit reached! % 113.61/16.71 % (3406546)------------------------------ % 113.61/16.71 % (3406546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.61/16.71 % (3406546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.61/16.71 % (3406546)CaDiCaL version: 2.1.3 % 113.61/16.71 % (3406546)Termination reason: Instruction limit % 120.05/17.66 % (3406546)Termination phase: Saturation % 120.05/17.66 % (3406546)Time elapsed: 0.473 s % 120.05/17.66 % (3406546)Peak memory usage: 97 MB % 120.05/17.66 % (3406546)Instructions burned: 1084 (million) % 120.05/17.66 % (3406550)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3473034051:i=6995:s2at=5:gtg=all_2868 on theBenchmark for (2868ds/6995Mi) % 120.05/17.66 % (3406551)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2134565730:st=2:i=6225:sd=15:ss=axioms_2867 on theBenchmark for (2867ds/6225Mi) % 120.05/17.66 % (3406551)Refutation not found, incomplete strategy % 120.05/17.66 % (3406551)------------------------------ % 120.05/17.66 % (3406551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.05/17.66 % (3406551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.05/17.66 % (3406551)CaDiCaL version: 2.1.3 % 120.05/17.66 % (3406551)Termination reason: Refutation not found, incomplete strategy % 120.05/17.66 % (3406551)Time elapsed: 0.001 s % 120.05/17.66 % (3406551)Peak memory usage: 86 MB % 120.05/17.66 % (3406551)Instructions burned: 1 (million) % 120.05/17.66 % (3406551)------------------------------ % 120.05/17.66 % (3406551)------------------------------ % 120.05/17.66 % (3406554)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=4137938897:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2864 on theBenchmark for (2864ds/3372Mi) % 120.05/17.66 [W928 14:13:54.195941635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.195975482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196025899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196040249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196069292 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196081576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196107383 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196117933 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.05/17.66 [W928 14:13:54.196143559 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.05/17.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.88/17.93 [W928 14:13:54.196155100 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.88/17.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.88/17.93 [W928 14:13:54.196186890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.88/17.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.88/17.93 [W928 14:13:54.196207430 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.88/17.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.88/17.93 % (3406554)Refutation not found, incomplete strategy % 121.88/17.93 % (3406554)------------------------------ % 121.88/17.93 % (3406554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.88/17.93 % (3406554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.88/17.93 % (3406554)CaDiCaL version: 2.1.3 % 121.88/17.93 % (3406554)Termination reason: Refutation not found, incomplete strategy % 121.88/17.93 % (3406554)Time elapsed: 0.543 s % 121.88/17.93 % (3406554)Peak memory usage: 126 MB % 121.88/17.93 % (3406554)Instructions burned: 830 (million) % 121.88/17.93 % (3406554)------------------------------ % 121.88/17.93 % (3406554)------------------------------ % 121.88/17.93 % (3406556)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2569124142:st=2.3:i=26457:sd=10:ss=included:sgt=8_2854 on theBenchmark for (2854ds/26457Mi) % 121.88/17.93 % (3406518)Instruction limit reached! % 121.88/17.93 % (3406518)------------------------------ % 121.88/17.93 % (3406518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.88/17.93 % (3406518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.88/17.93 % (3406518)CaDiCaL version: 2.1.3 % 121.88/17.93 % (3406518)Termination reason: Instruction limit % 121.88/17.93 % (3406518)Termination phase: Saturation % 121.88/17.93 % (3406518)Time elapsed: 8.090 s % 121.88/17.93 % (3406518)Peak memory usage: 178 MB % 121.88/17.93 % (3406518)Instructions burned: 14123 (million) % 121.88/17.93 % (3406558)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=954262189:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2850 on theBenchmark for (2850ds/13494Mi) % 121.88/17.93 % (3406556)Refutation not found, incomplete strategy % 121.88/17.93 % (3406556)------------------------------ % 121.88/17.93 % (3406556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.88/17.93 % (3406556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.88/17.93 % (3406556)CaDiCaL version: 2.1.3 % 121.88/17.93 % (3406556)Termination reason: Refutation not found, incomplete strategy % 121.88/17.93 % (3406556)Time elapsed: 0.592 s % 121.88/17.93 % (3406556)Peak memory usage: 133 MB % 121.88/17.93 % (3406556)Instructions burned: 912 (million) % 121.88/17.93 % (3406556)------------------------------ % 121.88/17.93 % (3406556)------------------------------ % 121.88/17.93 % (3406560)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=1264329984:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2844 on theBenchmark for (2844ds/2503Mi) % 121.88/17.93 [W928 14:13:56.134513921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.88/17.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.88/17.93 [W928 14:13:56.134547831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.88/17.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.88/17.93 [W928 14:13:56.134586758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134598305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134628622 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134650238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134676969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134687645 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134711992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134722476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134747069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 [W928 14:13:56.134757782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.93/19.73 % (3406560)Refutation not found, incomplete strategy % 134.93/19.73 % (3406560)------------------------------ % 134.93/19.73 % (3406560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.93/19.73 % (3406560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.93/19.73 % (3406560)CaDiCaL version: 2.1.3 % 134.93/19.73 % (3406560)Termination reason: Refutation not found, incomplete strategy % 134.93/19.73 % (3406560)Time elapsed: 0.540 s % 134.93/19.73 % (3406560)Peak memory usage: 126 MB % 134.93/19.73 % (3406560)Instructions burned: 827 (million) % 134.93/19.73 % (3406560)------------------------------ % 134.93/19.73 % (3406560)------------------------------ % 134.93/19.73 % (3406562)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=259188419:i=2559:sd=1:ep=RSTC:ss=axioms_2835 on theBenchmark for (2835ds/2559Mi) % 134.93/19.73 [W928 14:13:57.092057591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 134.93/19.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092093468 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092144615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092156819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092181452 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092192509 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092217159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092228329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092253156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092264156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092288673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 [W928 14:13:57.092299533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 141.35/20.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 141.35/20.67 % (3406562)Refutation not found, incomplete strategy % 141.35/20.67 % (3406562)------------------------------ % 141.35/20.67 % (3406562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 141.35/20.67 % (3406562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 141.35/20.67 % (3406562)CaDiCaL version: 2.1.3 % 141.35/20.67 % (3406562)Termination reason: Refutation not found, incomplete strategy % 141.35/20.67 % (3406562)Time elapsed: 0.545 s % 141.35/20.67 % (3406562)Peak memory usage: 125 MB % 141.35/20.67 % (3406562)Instructions burned: 828 (million) % 141.35/20.67 % (3406543)Instruction limit reached! % 141.35/20.67 % (3406543)------------------------------ % 148.40/21.63 % (3406543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.40/21.63 % (3406543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.40/21.63 % (3406543)CaDiCaL version: 2.1.3 % 148.40/21.63 % (3406543)Termination reason: Instruction limit % 148.40/21.63 % (3406543)Termination phase: Saturation % 148.40/21.63 % (3406543)Time elapsed: 4.815 s % 148.40/21.63 % (3406543)Peak memory usage: 163 MB % 148.40/21.63 % (3406543)Instructions burned: 8327 (million) % 148.40/21.63 % (3406562)------------------------------ % 148.40/21.63 % (3406562)------------------------------ % 148.40/21.63 % (3406564)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3460358478:i=30753:av=off:ss=included_2827 on theBenchmark for (2827ds/30753Mi) % 148.40/21.63 % (3406550)Instruction limit reached! % 148.40/21.63 % (3406550)------------------------------ % 148.40/21.63 % (3406550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.40/21.63 % (3406550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.40/21.63 % (3406550)CaDiCaL version: 2.1.3 % 148.40/21.63 % (3406550)Termination reason: Instruction limit % 148.40/21.63 % (3406550)Termination phase: Saturation % 148.40/21.63 % (3406550)Time elapsed: 4.232 s % 148.40/21.63 % (3406550)Peak memory usage: 155 MB % 148.40/21.63 % (3406550)Instructions burned: 6995 (million) % 148.40/21.63 % (3406565)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=653095955:i=26473:ep=RSTC_2825 on theBenchmark for (2825ds/26473Mi) % 148.40/21.63 % (3406567)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=3695340225:cts=off:i=2759:kws=inv_arity:fgj=on_2824 on theBenchmark for (2824ds/2759Mi) % 148.40/21.63 % (3406567)Refutation not found, incomplete strategy % 148.40/21.63 % (3406567)------------------------------ % 148.40/21.63 % (3406567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.40/21.63 % (3406567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.40/21.63 % (3406567)CaDiCaL version: 2.1.3 % 148.40/21.63 % (3406567)Termination reason: Refutation not found, incomplete strategy % 148.40/21.63 % (3406567)Time elapsed: 0.595 s % 148.40/21.63 % (3406567)Peak memory usage: 133 MB % 148.40/21.63 % (3406567)Instructions burned: 918 (million) % 148.40/21.63 % (3406567)------------------------------ % 148.40/21.63 % (3406567)------------------------------ % 148.40/21.63 % (3406570)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=2288693861:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2814 on theBenchmark for (2814ds/5665Mi) % 148.40/21.63 [W928 14:13:59.158114253 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.40/21.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.40/21.63 [W928 14:13:59.158148787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.40/21.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.40/21.63 [W928 14:13:59.158187614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.40/21.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.40/21.63 [W928 14:13:59.158200401 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.40/21.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.40/21.63 [W928 14:13:59.158229184 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.40/21.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.40/21.63 [W928 14:13:59.158240627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:13:59.158266244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:13:59.158276631 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:13:59.158300625 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:13:59.158310791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:13:59.158335005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:13:59.158344985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 % (3406570)Refutation not found, incomplete strategy % 160.23/23.23 % (3406570)------------------------------ % 160.23/23.23 % (3406570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.23/23.23 % (3406570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.23/23.23 % (3406570)CaDiCaL version: 2.1.3 % 160.23/23.23 % (3406570)Termination reason: Refutation not found, incomplete strategy % 160.23/23.23 % (3406570)Time elapsed: 0.539 s % 160.23/23.23 % (3406570)Peak memory usage: 125 MB % 160.23/23.23 % (3406570)Instructions burned: 828 (million) % 160.23/23.23 % (3406570)------------------------------ % 160.23/23.23 % (3406570)------------------------------ % 160.23/23.23 % (3406572)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=2282703864:i=1532:ep=RS:ss=axioms_2805 on theBenchmark for (2805ds/1532Mi) % 160.23/23.23 [W928 14:14:00.101693921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:14:00.101729205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:14:00.101765865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.23/23.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.23/23.23 [W928 14:14:00.101778245 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101803842 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101826032 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101850659 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101860906 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101884630 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101894670 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101918406 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:00.101928563 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 % (3406572)Refutation not found, incomplete strategy % 163.35/23.77 % (3406572)------------------------------ % 163.35/23.77 % (3406572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.35/23.77 % (3406572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.35/23.77 % (3406572)CaDiCaL version: 2.1.3 % 163.35/23.77 % (3406572)Termination reason: Refutation not found, incomplete strategy % 163.35/23.77 % (3406572)Time elapsed: 0.543 s % 163.35/23.77 % (3406572)Peak memory usage: 126 MB % 163.35/23.77 % (3406572)Instructions burned: 825 (million) % 163.35/23.77 % (3406572)------------------------------ % 163.35/23.77 % (3406572)------------------------------ % 163.35/23.77 % (3406574)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3514611373:i=1565:sd=2:ss=axioms:sgt=32_2795 on theBenchmark for (2795ds/1565Mi) % 163.35/23.77 [W928 14:14:01.058248135 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:01.058282798 register_special_ops.cpp:225] Warning: Creating a tensor from 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.35/23.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.35/23.77 [W928 14:14:01.058321085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058333822 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058359679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058428423 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058464466 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058476033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058500923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058511963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058536890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 [W928 14:14:01.058547950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 169.75/24.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 169.75/24.73 % (3406574)Refutation not found, incomplete strategy % 169.75/24.73 % (3406574)------------------------------ % 169.75/24.73 % (3406574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 169.75/24.73 % (3406574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 169.75/24.73 % (3406574)CaDiCaL version: 2.1.3 % 169.75/24.73 % (3406574)Termination reason: Refutation not found, incomplete strategy % 169.75/24.73 % (3406574)Time elapsed: 0.539 s % 169.75/24.73 % (3406574)Peak memory usage: 125 MB % 169.75/24.73 % (3406574)Instructions burned: 823 (million) % 169.75/24.73 % (3406574)------------------------------ % 169.75/24.73 % (3406574)------------------------------ % 169.75/24.73 % (3406576)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=3134479095:i=1572:fgj=on:gsp=on_2786 on theBenchmark for (2786ds/1572Mi) % 169.75/24.73 % (3406576)Instruction limit reached! % 169.75/24.73 % (3406576)------------------------------ % 169.75/24.73 % (3406576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 176.28/25.68 % (3406576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 176.28/25.68 % (3406576)CaDiCaL version: 2.1.3 % 176.28/25.68 % (3406576)Termination reason: Instruction limit % 176.28/25.68 % (3406576)Termination phase: Saturation % 176.28/25.68 % (3406576)Time elapsed: 1.027 s % 176.28/25.68 % (3406576)Peak memory usage: 135 MB % 176.28/25.68 % (3406576)Instructions burned: 1572 (million) % 176.28/25.68 % (3406578)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3382443309:i=6052:sd=4:ss=axioms:sgt=24_2774 on theBenchmark for (2774ds/6052Mi) % 176.28/25.68 [W928 14:14:03.196452273 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196487557 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196524737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196536970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196563857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196575147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196601351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196612401 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196637974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196649055 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196674505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 176.28/25.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 176.28/25.68 [W928 14:14:03.196685395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 % (3406578)Refutation not found, incomplete strategy % 199.86/28.81 % (3406578)------------------------------ % 199.86/28.81 % (3406578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.81 % (3406578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.81 % (3406578)CaDiCaL version: 2.1.3 % 199.86/28.81 % (3406578)Termination reason: Refutation not found, incomplete strategy % 199.86/28.81 % (3406578)Time elapsed: 0.538 s % 199.86/28.81 % (3406578)Peak memory usage: 126 MB % 199.86/28.81 % (3406578)Instructions burned: 824 (million) % 199.86/28.81 % (3406558)Instruction limit reached! % 199.86/28.81 % (3406558)------------------------------ % 199.86/28.81 % (3406558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 199.86/28.81 % (3406558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 199.86/28.81 % (3406558)CaDiCaL version: 2.1.3 % 199.86/28.81 % (3406558)Termination reason: Instruction limit % 199.86/28.81 % (3406558)Termination phase: Saturation % 199.86/28.81 % (3406558)Time elapsed: 8.308 s % 199.86/28.81 % (3406558)Peak memory usage: 201 MB % 199.86/28.81 % (3406558)Instructions burned: 13495 (million) % 199.86/28.81 % (3406578)------------------------------ % 199.86/28.81 % (3406578)------------------------------ % 199.86/28.81 % (3406580)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=18193532:i=3500:sd=1:bd=preordered:sup=off:ss=included_2766 on theBenchmark for (2766ds/3500Mi) % 199.86/28.81 % (3406581)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=1829943638:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2764 on theBenchmark for (2764ds/1842Mi) % 199.86/28.81 [W928 14:14:04.161170665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161205855 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161243505 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161257502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161283619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161295126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161320056 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 199.86/28.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 199.86/28.81 [W928 14:14:04.161331773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:04.161364383 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:04.161384623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:04.161408103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:04.161419103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 % (3406580)Refutation not found, incomplete strategy % 212.30/30.67 % (3406580)------------------------------ % 212.30/30.67 % (3406580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.67 % (3406580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.67 % (3406580)CaDiCaL version: 2.1.3 % 212.30/30.67 % (3406580)Termination reason: Refutation not found, incomplete strategy % 212.30/30.67 % (3406580)Time elapsed: 0.598 s % 212.30/30.67 % (3406580)Peak memory usage: 133 MB % 212.30/30.67 % (3406580)Instructions burned: 911 (million) % 212.30/30.67 % (3406581)Refutation not found, incomplete strategy % 212.30/30.67 % (3406581)------------------------------ % 212.30/30.67 % (3406581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 212.30/30.67 % (3406581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 212.30/30.67 % (3406581)CaDiCaL version: 2.1.3 % 212.30/30.67 % (3406581)Termination reason: Refutation not found, incomplete strategy % 212.30/30.67 % (3406581)Time elapsed: 0.544 s % 212.30/30.67 % (3406581)Peak memory usage: 126 MB % 212.30/30.67 % (3406581)Instructions burned: 833 (million) % 212.30/30.67 % (3406580)------------------------------ % 212.30/30.67 % (3406580)------------------------------ % 212.30/30.67 % (3406581)------------------------------ % 212.30/30.67 % (3406581)------------------------------ % 212.30/30.67 % (3406584)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2577937547:i=66096:add=on_2755 on theBenchmark for (2755ds/66096Mi) % 212.30/30.67 % (3406585)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=750727284:i=1884:sd=1:nm=60:ss=axioms_2754 on theBenchmark for (2754ds/1884Mi) % 212.30/30.67 [W928 14:14:05.105247550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:05.105292377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:05.105331594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 212.30/30.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 212.30/30.67 [W928 14:14:05.105342648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105367378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105377381 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105402075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105412118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105435588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105445575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105473939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 [W928 14:14:05.105483985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 233.28/33.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 233.28/33.57 % (3406585)Refutation not found, incomplete strategy % 233.28/33.57 % (3406585)------------------------------ % 233.28/33.57 % (3406585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.28/33.57 % (3406585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.57 % (3406585)CaDiCaL version: 2.1.3 % 233.28/33.57 % (3406585)Termination reason: Refutation not found, incomplete strategy % 233.28/33.57 % (3406585)Time elapsed: 0.540 s % 233.28/33.57 % (3406585)Peak memory usage: 125 MB % 233.28/33.57 % (3406585)Instructions burned: 828 (million) % 233.28/33.57 % (3406585)------------------------------ % 233.28/33.57 % (3406585)------------------------------ % 233.28/33.57 % (3406588)lrs-1011_4:1_sil=16000:bsr=on:random_seed=743813292:cts=off:i=5469:bs=on:fsr=off_2745 on theBenchmark for (2745ds/5469Mi) % 233.28/33.57 % (3406588)Instruction limit reached! % 233.28/33.57 % (3406588)------------------------------ % 233.28/33.57 % (3406588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 233.28/33.57 % (3406588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 233.28/33.57 % (3406588)CaDiCaL version: 2.1.3 % 233.28/33.57 % (3406588)Termination reason: Instruction limit % 233.28/33.57 % (3406588)Termination phase: Saturation % 233.28/33.57 % (3406588)Time elapsed: 2.380 s % 233.28/33.57 % (3406588)Peak memory usage: 95 MB % 233.28/33.57 % (3406588)Instructions burned: 5471 (million) % 233.28/33.57 % (3406590)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=742753720:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2720 on theBenchmark for (2720ds/2037Mi) % 238.28/34.27 % (3406590)Instruction limit reached! % 238.28/34.27 % (3406590)------------------------------ % 238.28/34.27 % (3406590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.28/34.27 % (3406590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.28/34.27 % (3406590)CaDiCaL version: 2.1.3 % 238.28/34.27 % (3406590)Termination reason: Instruction limit % 238.28/34.27 % (3406590)Termination phase: Saturation % 238.28/34.27 % (3406590)Time elapsed: 1.308 s % 238.28/34.27 % (3406590)Peak memory usage: 140 MB % 238.28/34.27 % (3406590)Instructions burned: 2038 (million) % 238.28/34.27 % (3406592)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2347116281:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2705 on theBenchmark for (2705ds/2110Mi) % 238.28/34.27 [W928 14:14:10.093524860 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093558890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093596520 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093608440 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093632924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093644037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093669038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093680128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093703921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093714975 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.28/34.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.28/34.27 [W928 14:14:10.093738945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.60/38.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.60/38.21 [W928 14:14:10.093750005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.60/38.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.60/38.21 % (3406592)Refutation not found, incomplete strategy % 266.60/38.21 % (3406592)------------------------------ % 266.60/38.21 % (3406592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.60/38.21 % (3406592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.21 % (3406592)CaDiCaL version: 2.1.3 % 266.60/38.21 % (3406592)Termination reason: Refutation not found, incomplete strategy % 266.60/38.21 % (3406592)Time elapsed: 0.546 s % 266.60/38.21 % (3406592)Peak memory usage: 125 MB % 266.60/38.21 % (3406592)Instructions burned: 828 (million) % 266.60/38.21 % (3406592)------------------------------ % 266.60/38.21 % (3406592)------------------------------ % 266.60/38.21 % (3406594)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=2713739141:i=2430:add=off:aac=none:nm=16_2695 on theBenchmark for (2695ds/2430Mi) % 266.60/38.21 % (3406538)Instruction limit reached! % 266.60/38.21 % (3406538)------------------------------ % 266.60/38.21 % (3406538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.60/38.21 % (3406538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.21 % (3406538)CaDiCaL version: 2.1.3 % 266.60/38.21 % (3406538)Termination reason: Instruction limit % 266.60/38.21 % (3406538)Termination phase: Saturation % 266.60/38.21 % (3406538)Time elapsed: 19.687 s % 266.60/38.21 % (3406538)Peak memory usage: 202 MB % 266.60/38.21 % (3406538)Instructions burned: 33334 (million) % 266.60/38.21 % (3406596)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=282645704:cond=fast:i=4891_2683 on theBenchmark for (2683ds/4891Mi) % 266.60/38.21 % (3406594)Instruction limit reached! % 266.60/38.21 % (3406594)------------------------------ % 266.60/38.21 % (3406594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.60/38.21 % (3406594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.21 % (3406594)CaDiCaL version: 2.1.3 % 266.60/38.21 % (3406594)Termination reason: Instruction limit % 266.60/38.21 % (3406594)Termination phase: Saturation % 266.60/38.21 % (3406594)Time elapsed: 1.471 s % 266.60/38.21 % (3406594)Peak memory usage: 141 MB % 266.60/38.21 % (3406594)Instructions burned: 2430 (million) % 266.60/38.21 % (3406598)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=2851488033:st=2:i=14845:sd=2:ss=included:fsd=on_2679 on theBenchmark for (2679ds/14845Mi) % 266.60/38.21 % (3406565)Instruction limit reached! % 266.60/38.21 % (3406565)------------------------------ % 266.60/38.21 % (3406565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.60/38.21 % (3406565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.21 % (3406565)CaDiCaL version: 2.1.3 % 266.60/38.21 % (3406565)Termination reason: Instruction limit % 266.60/38.21 % (3406565)Termination phase: Saturation % 266.60/38.21 % (3406565)Time elapsed: 15.112 s % 266.60/38.21 % (3406565)Peak memory usage: 495 MB % 266.60/38.21 % (3406565)Instructions burned: 26473 (million) % 266.60/38.21 % (3406598)Refutation not found, incomplete strategy % 266.60/38.21 % (3406598)------------------------------ % 266.60/38.21 % (3406598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 266.60/38.21 % (3406598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 266.60/38.21 % (3406598)CaDiCaL version: 2.1.3 % 266.60/38.21 % (3406598)Termination reason: Refutation not found, incomplete strategy % 266.60/38.21 % (3406598)Time elapsed: 0.587 s % 266.60/38.21 % (3406598)Peak memory usage: 130 MB % 266.60/38.21 % (3406598)Instructions burned: 902 (million) % 266.60/38.21 % (3406600)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2799110924:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2672 on theBenchmark for (2672ds/7534Mi) % 271.15/39.00 % (3406598)------------------------------ % 271.15/39.00 % (3406598)------------------------------ % 271.15/39.00 % (3406602)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=754942741:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2669 on theBenchmark for (2669ds/10353Mi) % 271.15/39.00 [W928 14:14:14.701210337 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701257948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701297345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701308978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701333155 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701343142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701367475 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701377838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701401352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701413779 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701437749 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 271.15/39.00 [W928 14:14:14.701448716 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 271.15/39.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 277.13/39.89 % (3406602)Refutation not found, incomplete strategy % 277.13/39.89 % (3406602)------------------------------ % 277.13/39.89 % (3406602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.13/39.89 % (3406602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.13/39.89 % (3406602)CaDiCaL version: 2.1.3 % 277.13/39.89 % (3406602)Termination reason: Refutation not found, incomplete strategy % 277.13/39.89 % (3406602)Time elapsed: 0.540 s % 277.13/39.89 % (3406602)Peak memory usage: 125 MB % 277.13/39.89 % (3406602)Instructions burned: 824 (million) % 277.13/39.89 % (3406602)------------------------------ % 277.13/39.89 % (3406602)------------------------------ % 277.13/39.89 % (3406604)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3557741545:i=7860_2659 on theBenchmark for (2659ds/7860Mi) % 277.13/39.89 % (3406604)Refutation not found, incomplete strategy % 277.13/39.89 % (3406604)------------------------------ % 277.13/39.89 % (3406604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.13/39.89 % (3406604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.13/39.89 % (3406604)CaDiCaL version: 2.1.3 % 277.13/39.89 % (3406604)Termination reason: Refutation not found, incomplete strategy % 277.13/39.89 % (3406604)Time elapsed: 0.014 s % 277.13/39.89 % (3406604)Peak memory usage: 89 MB % 277.13/39.89 % (3406604)Instructions burned: 27 (million) % 277.13/39.89 % (3406604)------------------------------ % 277.13/39.89 % (3406604)------------------------------ % 277.13/39.89 % (3406606)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=2483956285:i=7896:sd=2:bs=on:ss=included:sgt=20_2654 on theBenchmark for (2654ds/7896Mi) % 277.13/39.89 % (3406596)Instruction limit reached! % 277.13/39.89 % (3406596)------------------------------ % 277.13/39.89 % (3406596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.13/39.89 % (3406596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.13/39.89 % (3406596)CaDiCaL version: 2.1.3 % 277.13/39.89 % (3406596)Termination reason: Instruction limit % 277.13/39.89 % (3406596)Termination phase: Saturation % 277.13/39.89 % (3406596)Time elapsed: 3.165 s % 277.13/39.89 % (3406596)Peak memory usage: 156 MB % 277.13/39.89 % (3406596)Instructions burned: 4892 (million) % 277.13/39.89 % (3406608)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1721875485:i=5812:gtgl=2:gtg=all_2649 on theBenchmark for (2649ds/5812Mi) % 277.13/39.89 % (3406564)Instruction limit reached! % 277.13/39.89 % (3406564)------------------------------ % 277.13/39.89 % (3406564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.13/39.89 % (3406564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.13/39.89 % (3406564)CaDiCaL version: 2.1.3 % 277.13/39.89 % (3406564)Termination reason: Instruction limit % 277.13/39.89 % (3406564)Termination phase: Saturation % 277.13/39.89 % (3406564)Time elapsed: 19.316 s % 277.13/39.89 % (3406564)Peak memory usage: 366 MB % 277.13/39.89 % (3406564)Instructions burned: 30754 (million) % 277.13/39.89 % (3406610)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=3264661904:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2631 on theBenchmark for (2631ds/2965Mi) % 277.13/39.89 % (3406600)Instruction limit reached! % 277.13/39.89 % (3406600)------------------------------ % 277.13/39.89 % (3406600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 277.13/39.89 % (3406600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 277.13/39.89 % (3406600)CaDiCaL version: 2.1.3 % 277.13/39.89 % (3406600)Termination reason: Instruction limit % 277.13/39.89 % (3406600)Termination phase: Saturation % 277.13/39.89 % (3406600)Time elapsed: 4.396 s % 277.13/39.89 % (3406600)Peak memory usage: 172 MB % 277.13/39.89 % (3406600)Instructions burned: 7535 (million) % 277.13/39.89 % (3406612)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=3099038335:i=2967:kws=precedence:bd=preordered:av=off_2626 on theBenchmark for (2626ds/2967Mi) % 277.13/39.89 % (3406610)Refutation not found, incomplete strategy % 277.13/39.89 % (3406610)------------------------------ % 277.13/39.89 % (3406610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.70/40.27 % (3406610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.70/40.27 % (3406610)CaDiCaL version: 2.1.3 % 280.70/40.27 % (3406610)Termination reason: Refutation not found, incomplete strategy % 280.70/40.27 % (3406610)Time elapsed: 0.598 s % 280.70/40.27 % (3406610)Peak memory usage: 133 MB % 280.70/40.27 % (3406610)Instructions burned: 913 (million) % 280.70/40.27 % (3406610)------------------------------ % 280.70/40.27 % (3406610)------------------------------ % 280.70/40.27 % (3406614)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=10457679:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2621 on theBenchmark for (2621ds/3022Mi) % 280.70/40.27 [W928 14:14:18.427346708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427390998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427430965 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427442232 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427468065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427478259 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427503045 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427513342 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427538296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427548306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.70/40.27 [W928 14:14:18.427572673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.70/40.27 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 [W928 14:14:18.427582489 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.83/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 % (3406614)Refutation not found, incomplete strategy % 281.83/40.45 % (3406614)------------------------------ % 281.83/40.45 % (3406614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.83/40.45 % (3406614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.83/40.45 % (3406614)CaDiCaL version: 2.1.3 % 281.83/40.45 % (3406614)Termination reason: Refutation not found, incomplete strategy % 281.83/40.45 % (3406614)Time elapsed: 0.541 s % 281.83/40.45 % (3406614)Peak memory usage: 126 MB % 281.83/40.45 % (3406614)Instructions burned: 824 (million) % 281.83/40.45 % (3406608)Instruction limit reached! % 281.83/40.45 % (3406608)------------------------------ % 281.83/40.45 % (3406608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.83/40.45 % (3406608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.83/40.45 % (3406608)CaDiCaL version: 2.1.3 % 281.83/40.45 % (3406608)Termination reason: Instruction limit % 281.83/40.45 % (3406608)Termination phase: Saturation % 281.83/40.45 % (3406608)Time elapsed: 3.525 s % 281.83/40.45 % (3406608)Peak memory usage: 168 MB % 281.83/40.45 % (3406608)Instructions burned: 5812 (million) % 281.83/40.45 % (3406614)------------------------------ % 281.83/40.45 % (3406614)------------------------------ % 281.83/40.45 % (3406616)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=583597367:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2612 on theBenchmark for (2612ds/3207Mi) % 281.83/40.45 % (3406617)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2273073708:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2612 on theBenchmark for (2612ds/3289Mi) % 281.83/40.45 % (3406606)Instruction limit reached! % 281.83/40.45 % (3406606)------------------------------ % 281.83/40.45 % (3406606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.83/40.45 % (3406606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.83/40.45 % (3406606)CaDiCaL version: 2.1.3 % 281.83/40.45 % (3406606)Termination reason: Instruction limit % 281.83/40.45 % (3406606)Termination phase: Saturation % 281.83/40.45 % (3406606)Time elapsed: 4.406 s % 281.83/40.45 % (3406606)Peak memory usage: 155 MB % 281.83/40.45 % (3406606)Instructions burned: 7899 (million) % 281.83/40.45 [W928 14:14:19.317738483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.83/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 [W928 14:14:19.317773540 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.83/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 [W928 14:14:19.317812190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.83/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 [W928 14:14:19.317823527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.83/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 [W928 14:14:19.317854001 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.83/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.83/40.45 [W928 14:14:19.317865171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 [W928 14:14:19.317890371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 [W928 14:14:19.317901211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 [W928 14:14:19.317925441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 [W928 14:14:19.317936194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 [W928 14:14:19.317960118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 [W928 14:14:19.317970108 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.87/41.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.87/41.25 % (3406620)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1791020510:i=38569:sd=3:ss=axioms:sgt=32_2609 on theBenchmark for (2609ds/38569Mi) % 287.87/41.25 % (3406616)Refutation not found, incomplete strategy % 287.87/41.25 % (3406616)------------------------------ % 287.87/41.25 % (3406616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.87/41.25 % (3406616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.87/41.25 % (3406616)CaDiCaL version: 2.1.3 % 287.87/41.25 % (3406616)Termination reason: Refutation not found, incomplete strategy % 287.87/41.25 % (3406616)Time elapsed: 0.543 s % 287.87/41.25 % (3406616)Peak memory usage: 126 MB % 287.87/41.25 % (3406616)Instructions burned: 823 (million) % 287.87/41.25 % (3406612)Instruction limit reached! % 287.87/41.25 % (3406612)------------------------------ % 287.87/41.25 % (3406612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.87/41.25 % (3406612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.87/41.25 % (3406612)CaDiCaL version: 2.1.3 % 287.87/41.25 % (3406612)Termination reason: Instruction limit % 287.87/41.25 % (3406612)Termination phase: Saturation % 287.87/41.25 % (3406612)Time elapsed: 1.932 s % 287.87/41.25 % (3406612)Peak memory usage: 146 MB % 287.87/41.25 % (3406612)Instructions burned: 2968 (million) % 287.87/41.25 % (3406617)Refutation not found, incomplete strategy % 287.87/41.25 % (3406617)------------------------------ % 287.87/41.25 % (3406617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.87/41.25 % (3406617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.87/41.25 % (3406617)CaDiCaL version: 2.1.3 % 287.87/41.25 % (3406617)Termination reason: Refutation not found, incomplete strategy % 287.87/41.25 % (3406617)Time elapsed: 0.605 s % 287.87/41.25 % (3406617)Peak memory usage: 133 MB % 287.87/41.25 % (3406617)Instructions burned: 919 (million) % 287.87/41.25 % (3406622)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3635696259:cts=off:i=3394_2605 on theBenchmark for (2605ds/3394Mi) % 287.87/41.25 [W928 14:14:20.700562590 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700596653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700634007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700645904 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700671324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700682127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700707658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700718581 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700743238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700754088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700777805 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 [W928 14:14:20.700788602 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 292.84/42.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 292.84/42.22 % (3406616)------------------------------ % 292.84/42.22 % (3406616)------------------------------ % 292.84/42.22 % (3406617)------------------------------ % 292.84/42.22 % (3406617)------------------------------ % 292.84/42.22 % (3406620)Refutation not found, incomplete strategy % 292.84/42.22 % (3406620)------------------------------ % 292.84/42.22 % (3406620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 292.84/42.22 % (3406620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 298.96/42.98 % (3406620)CaDiCaL version: 2.1.3 % 298.96/42.98 % (3406620)Termination reason: Refutation not found, incomplete strategy % 298.96/42.98 % (3406620)Time elapsed: 0.550 s % 298.96/42.98 % (3406620)Peak memory usage: 125 MB % 298.96/42.98 % (3406620)Instructions burned: 828 (million) % 298.96/42.98 % (3406624)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=125257137:i=33824:bd=preordered_2603 on theBenchmark for (2603ds/33824Mi) % 298.96/42.98 % (3406625)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=755160163:i=20684:bd=all:gtg=exists_sym_2602 on theBenchmark for (2602ds/20684Mi) % 298.96/42.98 % (3406620)------------------------------ % 298.96/42.98 % (3406620)------------------------------ % 298.96/42.98 % (3406628)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=45933935: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_2599 on theBenchmark for (2599ds/7222Mi) % 298.96/42.98 [W928 14:14:21.676280975 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676314508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676352142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676364482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676390246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676401426 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676426286 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676437236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676461576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 298.96/42.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 298.96/42.98 [W928 14:14:21.676472563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floatingTerminated % 300.91/43.08 % Vampire exiting % 300.91/43.08 Terminated %------------------------------------------------------------------------------