%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWB019+3 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n017.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:00:07 PM UTC 2026 % Result : Timeout 300.13s 43.17s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWB019+3 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.13/0.38 % Computer : n017.cluster.edu % 0.13/0.38 % Model : x86_64 x86_64 % 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.38 % Memory : 8046.5625MB % 0.13/0.38 % OS : Linux 6.8.0-71-generic % 0.13/0.38 % CPULimit : 300 % 0.13/0.38 % WCLimit : 300 % 0.13/0.38 % DateTime : Mon Sep 28 06:59:36 UTC 2026 % 0.13/0.38 % CPUTime : % 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.13/0.42 Running first-order theorem proving % 0.13/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 10.28/2.33 % (3362079)Detected formulas, will run a generic FOF schedule. % 10.28/2.33 % (3362084)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=3435319421:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 10.28/2.33 % (3362087)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=542839119:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 10.28/2.33 % (3362090)dis-21_1_sil=8000:lcm=predicate:random_seed=1662366437: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.28/2.33 % (3362085)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=2839783238:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 10.28/2.33 % (3362086)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=490647722:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 10.28/2.33 % (3362088)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=648774892:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 10.28/2.33 % (3362089)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=691685139:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 10.28/2.33 % (3362088)Refutation not found, incomplete strategy % 10.28/2.33 % (3362088)------------------------------ % 10.28/2.33 % (3362088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.33 % (3362088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.33 % (3362088)CaDiCaL version: 2.1.3 % 10.28/2.33 % (3362088)Termination reason: Refutation not found, incomplete strategy % 10.28/2.33 % (3362088)Time elapsed: 0.001 s % 10.28/2.33 % (3362087)Refutation not found, incomplete strategy % 10.28/2.33 % (3362087)------------------------------ % 10.28/2.33 % (3362087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.33 % (3362088)Peak memory usage: 86 MB % 10.28/2.33 % (3362087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.33 % (3362087)CaDiCaL version: 2.1.3 % 10.28/2.33 % (3362087)Termination reason: Refutation not found, incomplete strategy % 10.28/2.33 % (3362087)Time elapsed: 0.001 s % 10.28/2.33 % (3362087)Peak memory usage: 86 MB % 10.28/2.33 % (3362090)Instruction limit reached! % 10.28/2.33 % (3362090)------------------------------ % 10.28/2.33 % (3362090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.33 % (3362090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.33 % (3362090)CaDiCaL version: 2.1.3 % 10.28/2.33 % (3362090)Termination reason: Instruction limit % 10.28/2.33 % (3362090)Termination phase: Saturation % 10.28/2.33 % (3362090)Time elapsed: 0.078 s % 10.28/2.33 % (3362090)Peak memory usage: 89 MB % 10.28/2.33 % (3362090)Instructions burned: 130 (million) % 10.28/2.33 % (3362089)Instruction limit reached! % 10.28/2.33 % (3362089)------------------------------ % 10.28/2.33 % (3362089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.33 % (3362089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.33 % (3362089)CaDiCaL version: 2.1.3 % 10.28/2.33 % (3362089)Termination reason: Instruction limit % 10.28/2.33 % (3362089)Termination phase: Saturation % 10.28/2.33 % (3362089)Time elapsed: 0.085 s % 10.28/2.33 % (3362089)Peak memory usage: 90 MB % 10.28/2.33 % (3362089)Instructions burned: 140 (million) % 10.28/2.33 % (3362098)lrs+10_1_sil=8000:sp=occurrence:random_seed=650196910:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 10.28/2.33 % (3362098)Refutation not found, incomplete strategy % 10.28/2.33 % (3362098)------------------------------ % 10.28/2.33 % (3362098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.28/2.33 % (3362098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.28/2.33 % (3362098)CaDiCaL version: 2.1.3 % 10.28/2.33 % (3362098)Termination reason: Refutation not found, incomplete strategy % 10.28/2.33 % (3362098)Time elapsed: 0.001 s % 10.28/2.33 % (3362098)Peak memory usage: 86 MB % 10.28/2.33 % (3362088)------------------------------ % 10.28/2.33 % (3362088)------------------------------ % 10.28/2.33 % (3362087)------------------------------ % 10.28/2.33 % (3362087)------------------------------ % 11.37/2.53 % (3362099)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2525982140:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 11.37/2.53 % (3362099)Refutation not found, incomplete strategy % 11.37/2.53 % (3362099)------------------------------ % 11.37/2.53 % (3362099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.53 % (3362099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.53 % (3362099)CaDiCaL version: 2.1.3 % 11.37/2.53 % (3362099)Termination reason: Refutation not found, incomplete strategy % 11.37/2.53 % (3362099)Time elapsed: 0.001 s % 11.37/2.53 % (3362099)Peak memory usage: 87 MB % 11.37/2.53 % (3362099)Instructions burned: 1 (million) % 11.37/2.53 % (3362102)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=546534037:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 11.37/2.53 % (3362101)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3826306165:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 11.37/2.53 % (3362101)Refutation not found, incomplete strategy % 11.37/2.53 % (3362101)------------------------------ % 11.37/2.53 % (3362101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.53 % (3362101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.53 % (3362101)CaDiCaL version: 2.1.3 % 11.37/2.53 % (3362101)Termination reason: Refutation not found, incomplete strategy % 11.37/2.53 % (3362101)Time elapsed: 0.001 s % 11.37/2.53 % (3362101)Peak memory usage: 86 MB % 11.37/2.53 % (3362102)Instruction limit reached! % 11.37/2.53 % (3362102)------------------------------ % 11.37/2.53 % (3362102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.53 % (3362102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.53 % (3362102)CaDiCaL version: 2.1.3 % 11.37/2.53 % (3362102)Termination reason: Instruction limit % 11.37/2.53 % (3362102)Termination phase: Saturation % 11.37/2.53 % (3362102)Time elapsed: 0.066 s % 11.37/2.53 % (3362102)Peak memory usage: 92 MB % 11.37/2.53 % (3362102)Instructions burned: 248 (million) % 11.37/2.53 % (3362098)------------------------------ % 11.37/2.53 % (3362098)------------------------------ % 11.37/2.53 % (3362099)------------------------------ % 11.37/2.53 % (3362099)------------------------------ % 11.37/2.53 % (3362086)Refutation not found, incomplete strategy % 11.37/2.53 % (3362086)------------------------------ % 11.37/2.53 % (3362086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.53 % (3362086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.53 % (3362086)CaDiCaL version: 2.1.3 % 11.37/2.53 % (3362086)Termination reason: Refutation not found, incomplete strategy % 11.37/2.53 % (3362086)Time elapsed: 0.563 s % 11.37/2.53 % (3362086)Peak memory usage: 126 MB % 11.37/2.53 % (3362086)Instructions burned: 827 (million) % 11.37/2.53 % (3362106)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=494913726:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi) % 11.37/2.53 % (3362106)Refutation not found, incomplete strategy % 11.37/2.53 % (3362106)------------------------------ % 11.37/2.53 % (3362106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.53 % (3362106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.53 % (3362106)CaDiCaL version: 2.1.3 % 11.37/2.53 % (3362106)Termination reason: Refutation not found, incomplete strategy % 11.37/2.53 % (3362106)Time elapsed: 0.0000 s % 11.37/2.53 % (3362106)Peak memory usage: 86 MB % 11.37/2.53 % (3362107)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=911961482:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 11.37/2.53 % (3362101)------------------------------ % 11.37/2.53 % (3362101)------------------------------ % 11.37/2.53 % (3362108)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=661149307:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 11.37/2.53 % (3362108)Refutation not found, incomplete strategy % 11.37/2.53 % (3362108)------------------------------ % 11.37/2.53 % (3362108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.37/2.53 % (3362108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.37/2.53 % (3362108)CaDiCaL version: 2.1.3 % 11.37/2.53 % (3362108)Termination reason: Refutation not found, incomplete strategy % 13.29/2.82 % (3362108)Time elapsed: 0.002 s % 13.29/2.82 % (3362108)Peak memory usage: 88 MB % 13.29/2.82 % (3362108)Instructions burned: 2 (million) % 13.29/2.82 % (3362106)------------------------------ % 13.29/2.82 % (3362106)------------------------------ % 13.29/2.82 % (3362086)------------------------------ % 13.29/2.82 % (3362086)------------------------------ % 13.29/2.82 % (3362111)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3989147117:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi) % 13.29/2.82 % (3362111)Refutation not found, incomplete strategy % 13.29/2.82 % (3362111)------------------------------ % 13.29/2.82 % (3362111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.29/2.82 % (3362111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.29/2.82 % (3362111)CaDiCaL version: 2.1.3 % 13.29/2.82 % (3362111)Termination reason: Refutation not found, incomplete strategy % 13.29/2.82 % (3362111)Time elapsed: 0.018 s % 13.29/2.82 % (3362111)Peak memory usage: 87 MB % 13.29/2.82 % (3362111)Instructions burned: 36 (million) % 13.29/2.82 % (3362113)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4261048855:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi) % 13.29/2.82 % (3362113)Instruction limit reached! % 13.29/2.82 % (3362113)------------------------------ % 13.29/2.82 % (3362113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.29/2.82 % (3362113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.29/2.82 % (3362113)CaDiCaL version: 2.1.3 % 13.29/2.82 % (3362113)Termination reason: Instruction limit % 13.29/2.82 % (3362113)Termination phase: Saturation % 13.29/2.82 % (3362113)Time elapsed: 0.036 s % 13.29/2.82 % (3362113)Peak memory usage: 89 MB % 13.29/2.82 % (3362113)Instructions burned: 116 (million) % 13.29/2.82 % (3362108)------------------------------ % 13.29/2.82 % (3362108)------------------------------ % 13.29/2.82 % (3362114)lrs+10_1_sil=8000:sp=occurrence:random_seed=1216472087:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi) % 13.29/2.82 % (3362114)Refutation not found, incomplete strategy % 13.29/2.82 % (3362114)------------------------------ % 13.29/2.82 % (3362114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.29/2.82 % (3362114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.29/2.82 % (3362114)CaDiCaL version: 2.1.3 % 13.29/2.82 % (3362114)Termination reason: Refutation not found, incomplete strategy % 13.29/2.82 % (3362114)Time elapsed: 0.001 s % 13.29/2.82 % (3362114)Peak memory usage: 86 MB % 13.29/2.82 % (3362117)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2815517941:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi) % 13.29/2.82 % (3362117)Refutation not found, incomplete strategy % 13.29/2.82 % (3362117)------------------------------ % 13.29/2.82 % (3362117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.29/2.82 % (3362117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.29/2.82 % (3362117)CaDiCaL version: 2.1.3 % 13.29/2.82 % (3362117)Termination reason: Refutation not found, incomplete strategy % 13.29/2.82 % (3362117)Time elapsed: 0.001 s % 13.29/2.82 % (3362117)Peak memory usage: 88 MB % 13.29/2.82 % (3362117)Instructions burned: 1 (million) % 13.29/2.82 % (3362111)------------------------------ % 13.29/2.82 % (3362111)------------------------------ % 13.29/2.82 % (3362118)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3158843138:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi) % 13.29/2.82 % (3362117)------------------------------ % 13.29/2.82 % (3362117)------------------------------ % 13.29/2.82 % (3362114)------------------------------ % 13.29/2.82 % (3362114)------------------------------ % 13.29/2.82 % (3362122)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3338782351:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi) % 13.29/2.82 % (3362122)Refutation not found, incomplete strategy % 13.29/2.82 % (3362122)------------------------------ % 13.29/2.82 % (3362122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.29/2.82 % (3362122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.29/2.82 % (3362122)CaDiCaL version: 2.1.3 % 13.29/2.82 % (3362122)Termination reason: Refutation not found, incomplete strategy % 13.29/2.82 % (3362122)Time elapsed: 0.011 s % 13.29/2.82 % (3362122)Peak memory usage: 89 MB % 13.96/3.01 % (3362122)Instructions burned: 15 (million) % 13.96/3.01 % (3362123)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4274060040:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi) % 13.96/3.01 % (3362123)Refutation not found, incomplete strategy % 13.96/3.01 % (3362123)------------------------------ % 13.96/3.01 % (3362123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.96/3.01 % (3362123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.96/3.01 % (3362123)CaDiCaL version: 2.1.3 % 13.96/3.01 % (3362123)Termination reason: Refutation not found, incomplete strategy % 13.96/3.01 % (3362123)Time elapsed: 0.0000 s % 13.96/3.01 % (3362123)Peak memory usage: 86 MB % 13.96/3.01 % (3362124)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2223993745:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi) % 13.96/3.01 % (3362123)------------------------------ % 13.96/3.01 % (3362123)------------------------------ % 13.96/3.01 [W928 06:59:38.294351284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294409555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294447838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294464975 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294490809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294502419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294528699 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294540196 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294565302 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294576886 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 13.96/3.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.96/3.01 [W928 06:59:38.294602713 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.294614736 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 % (3362122)------------------------------ % 18.23/3.51 % (3362122)------------------------------ % 18.23/3.51 % (3362128)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=4219888049:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi) % 18.23/3.51 % (3362128)Refutation not found, incomplete strategy % 18.23/3.51 % (3362128)------------------------------ % 18.23/3.51 % (3362128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.23/3.51 % (3362128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.23/3.51 % (3362128)CaDiCaL version: 2.1.3 % 18.23/3.51 % (3362128)Termination reason: Refutation not found, incomplete strategy % 18.23/3.51 % (3362128)Time elapsed: 0.001 s % 18.23/3.51 % (3362128)Peak memory usage: 87 MB % 18.23/3.51 % (3362128)Instructions burned: 1 (million) % 18.23/3.51 % (3362118)Refutation not found, incomplete strategy % 18.23/3.51 % (3362118)------------------------------ % 18.23/3.51 % (3362118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.23/3.51 % (3362118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.23/3.51 % (3362118)CaDiCaL version: 2.1.3 % 18.23/3.51 % (3362118)Termination reason: Refutation not found, incomplete strategy % 18.23/3.51 % (3362118)Time elapsed: 0.563 s % 18.23/3.51 % (3362118)Peak memory usage: 125 MB % 18.23/3.51 % (3362118)Instructions burned: 823 (million) % 18.23/3.51 % (3362129)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=87983200:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi) % 18.23/3.51 % (3362128)------------------------------ % 18.23/3.51 % (3362128)------------------------------ % 18.23/3.51 [W928 06:59:38.579086755 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.579122916 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.579161712 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.579174769 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.579202163 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.579213733 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/3.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.23/3.51 [W928 06:59:38.579241060 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.92/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.92/4.45 [W928 06:59:38.579252366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.92/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.92/4.45 [W928 06:59:38.579283977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.92/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.92/4.45 [W928 06:59:38.579294440 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.92/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.92/4.45 [W928 06:59:38.579318077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.92/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.92/4.45 [W928 06:59:38.579328150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.92/4.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.92/4.45 % (3362129)Instruction limit reached! % 24.92/4.45 % (3362129)------------------------------ % 24.92/4.45 % (3362129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.92/4.45 % (3362129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.92/4.45 % (3362129)CaDiCaL version: 2.1.3 % 24.92/4.45 % (3362129)Termination reason: Instruction limit % 24.92/4.45 % (3362129)Termination phase: Saturation % 24.92/4.45 % (3362129)Time elapsed: 0.086 s % 24.92/4.45 % (3362129)Peak memory usage: 90 MB % 24.92/4.45 % (3362129)Instructions burned: 135 (million) % 24.92/4.45 % (3362132)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=108135242:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi) % 24.92/4.45 % (3362132)Refutation not found, incomplete strategy % 24.92/4.45 % (3362132)------------------------------ % 24.92/4.45 % (3362132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.92/4.45 % (3362132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.92/4.45 % (3362132)CaDiCaL version: 2.1.3 % 24.92/4.45 % (3362132)Termination reason: Refutation not found, incomplete strategy % 24.92/4.45 % (3362132)Time elapsed: 0.0000 s % 24.92/4.45 % (3362132)Peak memory usage: 86 MB % 24.92/4.45 % (3362118)------------------------------ % 24.92/4.45 % (3362118)------------------------------ % 24.92/4.45 % (3362124)Refutation not found, incomplete strategy % 24.92/4.45 % (3362124)------------------------------ % 24.92/4.45 % (3362124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.92/4.45 % (3362124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.92/4.45 % (3362124)CaDiCaL version: 2.1.3 % 24.92/4.45 % (3362124)Termination reason: Refutation not found, incomplete strategy % 24.92/4.45 % (3362124)Time elapsed: 0.559 s % 24.92/4.45 % (3362124)Peak memory usage: 125 MB % 24.92/4.45 % (3362124)Instructions burned: 826 (million) % 24.92/4.45 % (3362133)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1973428290:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2980 on theBenchmark for (2980ds/431Mi) % 24.92/4.45 % (3362133)Refutation not found, incomplete strategy % 24.92/4.45 % (3362133)------------------------------ % 24.92/4.45 % (3362133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.92/4.45 % (3362133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.70 % (3362133)CaDiCaL version: 2.1.3 % 25.90/4.70 % (3362133)Termination reason: Refutation not found, incomplete strategy % 25.90/4.70 % (3362133)Time elapsed: 0.001 s % 25.90/4.70 % (3362133)Peak memory usage: 86 MB % 25.90/4.70 % (3362132)------------------------------ % 25.90/4.70 % (3362132)------------------------------ % 25.90/4.70 % (3362135)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=3290947015:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi) % 25.90/4.70 % (3362137)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=608031717:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2978 on theBenchmark for (2978ds/150Mi) % 25.90/4.70 % (3362107)Instruction limit reached! % 25.90/4.70 % (3362107)------------------------------ % 25.90/4.70 % (3362107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.70 % (3362107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.70 % (3362107)CaDiCaL version: 2.1.3 % 25.90/4.70 % (3362107)Termination reason: Instruction limit % 25.90/4.70 % (3362107)Termination phase: Saturation % 25.90/4.70 % (3362107)Time elapsed: 1.508 s % 25.90/4.70 % (3362107)Peak memory usage: 143 MB % 25.90/4.70 % (3362107)Instructions burned: 2350 (million) % 25.90/4.70 % (3362137)Instruction limit reached! % 25.90/4.70 % (3362137)------------------------------ % 25.90/4.70 % (3362137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.70 % (3362137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.70 % (3362137)CaDiCaL version: 2.1.3 % 25.90/4.70 % (3362137)Termination reason: Instruction limit % 25.90/4.70 % (3362137)Termination phase: Saturation % 25.90/4.70 % (3362137)Time elapsed: 0.044 s % 25.90/4.70 % (3362137)Peak memory usage: 91 MB % 25.90/4.70 % (3362137)Instructions burned: 153 (million) % 25.90/4.70 % (3362124)------------------------------ % 25.90/4.70 % (3362124)------------------------------ % 25.90/4.70 % (3362133)------------------------------ % 25.90/4.70 % (3362133)------------------------------ % 25.90/4.70 % (3362140)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1572871380:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi) % 25.90/4.70 % (3362141)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=242256830:i=667:av=off:fsr=off_2976 on theBenchmark for (2976ds/667Mi) % 25.90/4.70 % (3362141)Refutation not found, incomplete strategy % 25.90/4.70 % (3362141)------------------------------ % 25.90/4.70 % (3362141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.70 % (3362141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.70 % (3362141)CaDiCaL version: 2.1.3 % 25.90/4.70 % (3362141)Termination reason: Refutation not found, incomplete strategy % 25.90/4.70 % (3362141)Time elapsed: 0.002 s % 25.90/4.70 % (3362141)Peak memory usage: 87 MB % 25.90/4.70 % (3362141)Instructions burned: 6 (million) % 25.90/4.70 % (3362142)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=1380381576:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi) % 25.90/4.70 % (3362143)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=927077276:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2976 on theBenchmark for (2976ds/193Mi) % 25.90/4.70 % (3362143)Refutation not found, incomplete strategy % 25.90/4.70 % (3362143)------------------------------ % 25.90/4.70 % (3362143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.70 % (3362143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.70 % (3362143)CaDiCaL version: 2.1.3 % 25.90/4.70 % (3362143)Termination reason: Refutation not found, incomplete strategy % 25.90/4.70 % (3362143)Time elapsed: 0.001 s % 25.90/4.70 % (3362143)Peak memory usage: 86 MB % 25.90/4.70 % (3362141)------------------------------ % 25.90/4.70 % (3362141)------------------------------ % 25.90/4.70 % (3362142)Instruction limit reached! % 25.90/4.70 % (3362142)------------------------------ % 25.90/4.70 % (3362142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.70 % (3362142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.70 % (3362142)CaDiCaL version: 2.1.3 % 34.20/5.74 % (3362142)Termination reason: Instruction limit % 34.20/5.74 % (3362142)Termination phase: Saturation % 34.20/5.74 % (3362142)Time elapsed: 0.100 s % 34.20/5.74 % (3362142)Peak memory usage: 91 MB % 34.20/5.74 % (3362142)Instructions burned: 185 (million) % 34.20/5.74 % (3362148)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=151815889:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi) % 34.20/5.74 % (3362148)Refutation not found, incomplete strategy % 34.20/5.74 % (3362148)------------------------------ % 34.20/5.74 % (3362148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.20/5.74 % (3362148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.20/5.74 % (3362148)CaDiCaL version: 2.1.3 % 34.20/5.74 % (3362148)Termination reason: Refutation not found, incomplete strategy % 34.20/5.74 % (3362148)Time elapsed: 0.003 s % 34.20/5.74 % (3362148)Peak memory usage: 88 MB % 34.20/5.74 % (3362148)Instructions burned: 8 (million) % 34.20/5.74 % (3362143)------------------------------ % 34.20/5.74 % (3362143)------------------------------ % 34.20/5.74 % (3362149)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=196669550:i=12111:sd=1:ss=included_2973 on theBenchmark for (2973ds/12111Mi) % 34.20/5.74 % (3362148)------------------------------ % 34.20/5.74 % (3362148)------------------------------ % 34.20/5.74 % (3362152)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1940350530:i=319:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/319Mi) % 34.20/5.74 % (3362153)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3910519645:i=2064:ep=RST_2970 on theBenchmark for (2970ds/2064Mi) % 34.20/5.74 % (3362153)Refutation not found, incomplete strategy % 34.20/5.74 % (3362153)------------------------------ % 34.20/5.74 % (3362153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.20/5.74 % (3362153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.20/5.74 % (3362153)CaDiCaL version: 2.1.3 % 34.20/5.74 % (3362153)Termination reason: Refutation not found, incomplete strategy % 34.20/5.74 % (3362153)Time elapsed: 0.003 s % 34.20/5.74 % (3362153)Peak memory usage: 88 MB % 34.20/5.74 % (3362153)Instructions burned: 8 (million) % 34.20/5.74 % (3362152)Instruction limit reached! % 34.20/5.74 % (3362152)------------------------------ % 34.20/5.74 % (3362152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.20/5.74 % (3362152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.20/5.74 % (3362152)CaDiCaL version: 2.1.3 % 34.20/5.74 % (3362152)Termination reason: Instruction limit % 34.20/5.74 % (3362152)Termination phase: Saturation % 34.20/5.74 % (3362152)Time elapsed: 0.184 s % 34.20/5.74 % (3362152)Peak memory usage: 92 MB % 34.20/5.74 % (3362152)Instructions burned: 319 (million) % 34.20/5.74 % (3362153)------------------------------ % 34.20/5.74 % (3362153)------------------------------ % 34.20/5.74 % (3362158)dis-1011_128_sil=32000:random_seed=1100147026:i=3706:ep=RST:av=off_2968 on theBenchmark for (2968ds/3706Mi) % 34.20/5.74 % (3362159)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2598839437:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2968 on theBenchmark for (2968ds/757Mi) % 34.20/5.74 % (3362159)Refutation not found, incomplete strategy % 34.20/5.74 % (3362159)------------------------------ % 34.20/5.74 % (3362159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.20/5.74 % (3362159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.20/5.74 % (3362159)CaDiCaL version: 2.1.3 % 34.20/5.74 % (3362159)Termination reason: Refutation not found, incomplete strategy % 34.20/5.74 % (3362159)Time elapsed: 0.0000 s % 34.20/5.74 % (3362159)Peak memory usage: 86 MB % 34.20/5.74 % (3362149)Refutation not found, incomplete strategy % 34.20/5.74 % (3362149)------------------------------ % 34.20/5.74 % (3362149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.20/5.74 % (3362149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.20/5.74 % (3362149)CaDiCaL version: 2.1.3 % 34.20/5.74 % (3362149)Termination reason: Refutation not found, incomplete strategy % 34.20/5.74 % (3362149)Time elapsed: 0.613 s % 34.20/5.74 % (3362149)Peak memory usage: 128 MB % 34.20/5.74 % (3362149)Instructions burned: 911 (million) % 34.20/5.74 % (3362159)------------------------------ % 34.20/5.74 % (3362159)------------------------------ % 34.20/5.74 % (3362162)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4004723019:i=13913:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/13913Mi) % 37.58/6.17 % (3362149)------------------------------ % 37.58/6.17 % (3362149)------------------------------ % 37.58/6.17 [W928 06:59:40.420714414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420753291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420775031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420781849 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420795267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420802014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420815896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420830736 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420845120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420851072 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420864298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 [W928 06:59:40.420872525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.58/6.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.58/6.17 % (3362164)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=300326646:i=9925:aac=none_2963 on theBenchmark for (2963ds/9925Mi) % 53.57/8.49 % (3362162)Refutation not found, incomplete strategy % 53.57/8.49 % (3362162)------------------------------ % 53.57/8.49 % (3362162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.57/8.49 % (3362162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.57/8.49 % (3362162)CaDiCaL version: 2.1.3 % 53.57/8.49 % (3362162)Termination reason: Refutation not found, incomplete strategy % 53.57/8.49 % (3362162)Time elapsed: 0.316 s % 53.57/8.49 % (3362162)Peak memory usage: 125 MB % 53.57/8.49 % (3362162)Instructions burned: 827 (million) % 53.57/8.49 % (3362162)------------------------------ % 53.57/8.49 % (3362162)------------------------------ % 53.57/8.49 % (3362166)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1131934677:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/2479Mi) % 53.57/8.49 % (3362166)Refutation not found, incomplete strategy % 53.57/8.49 % (3362166)------------------------------ % 53.57/8.49 % (3362166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.57/8.49 % (3362166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.57/8.49 % (3362166)CaDiCaL version: 2.1.3 % 53.57/8.49 % (3362166)Termination reason: Refutation not found, incomplete strategy % 53.57/8.49 % (3362166)Time elapsed: 0.0000 s % 53.57/8.49 % (3362166)Peak memory usage: 86 MB % 53.57/8.49 % (3362166)------------------------------ % 53.57/8.49 % (3362166)------------------------------ % 53.57/8.49 % (3362164)Refutation not found, incomplete strategy % 53.57/8.49 % (3362164)------------------------------ % 53.57/8.49 % (3362164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.57/8.49 % (3362164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.57/8.49 % (3362164)CaDiCaL version: 2.1.3 % 53.57/8.49 % (3362164)Termination reason: Refutation not found, incomplete strategy % 53.57/8.49 % (3362164)Time elapsed: 0.549 s % 53.57/8.49 % (3362164)Peak memory usage: 129 MB % 53.57/8.49 % (3362164)Instructions burned: 857 (million) % 53.57/8.49 % (3362168)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3673324326:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2956 on theBenchmark for (2956ds/440Mi) % 53.57/8.49 % (3362164)------------------------------ % 53.57/8.49 % (3362164)------------------------------ % 53.57/8.49 % (3362170)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2551190782:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2954 on theBenchmark for (2954ds/11145Mi) % 53.57/8.49 % (3362168)Instruction limit reached! % 53.57/8.49 % (3362168)------------------------------ % 53.57/8.49 % (3362168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 53.57/8.49 % (3362168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 53.57/8.49 % (3362168)CaDiCaL version: 2.1.3 % 53.57/8.49 % (3362168)Termination reason: Instruction limit % 53.57/8.49 % (3362168)Termination phase: Saturation % 53.57/8.49 % (3362168)Time elapsed: 0.212 s % 53.57/8.49 % (3362168)Peak memory usage: 92 MB % 53.57/8.49 % (3362168)Instructions burned: 442 (million) % 53.57/8.49 [W928 06:59:41.496957794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 53.57/8.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 53.57/8.49 [W928 06:59:41.496994416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 53.57/8.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 53.57/8.49 [W928 06:59:41.497024132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 53.57/8.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 53.57/8.49 [W928 06:59:41.497031826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497044933 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497050602 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497071026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497076539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497089051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497094925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497107987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 [W928 06:59:41.497113725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.68/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.68/8.66 % (3362172)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=2660206564:cts=off:i=3034:av=off:er=known:fsd=on_2952 on theBenchmark for (2952ds/3034Mi) % 54.68/8.66 % (3362170)Refutation not found, incomplete strategy % 54.68/8.66 % (3362170)------------------------------ % 54.68/8.66 % (3362170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.68/8.66 % (3362170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.68/8.66 % (3362170)CaDiCaL version: 2.1.3 % 54.68/8.66 % (3362170)Termination reason: Refutation not found, incomplete strategy % 54.68/8.66 % (3362170)Time elapsed: 0.333 s % 54.68/8.66 % (3362170)Peak memory usage: 125 MB % 54.68/8.66 % (3362170)Instructions burned: 827 (million) % 54.68/8.66 % (3362170)------------------------------ % 54.68/8.66 % (3362170)------------------------------ % 54.68/8.66 % (3362174)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1945661163:st=2:s2a=on:i=524:s2at=2:ss=axioms_2948 on theBenchmark for (2948ds/524Mi) % 54.68/8.66 % (3362174)Refutation not found, incomplete strategy % 54.68/8.66 % (3362174)------------------------------ % 54.68/8.66 % (3362174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.68/8.66 % (3362174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.68/8.66 % (3362174)CaDiCaL version: 2.1.3 % 54.68/8.66 % (3362174)Termination reason: Refutation not found, incomplete strategy % 54.68/8.66 % (3362174)Time elapsed: 0.001 s % 54.68/8.66 % (3362174)Peak memory usage: 87 MB % 54.68/8.66 % (3362174)Instructions burned: 1 (million) % 58.23/9.04 % (3362174)------------------------------ % 58.23/9.04 % (3362174)------------------------------ % 58.23/9.04 % (3362158)Instruction limit reached! % 58.23/9.04 % (3362158)------------------------------ % 58.23/9.04 % (3362158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.23/9.04 % (3362158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/9.04 % (3362158)CaDiCaL version: 2.1.3 % 58.23/9.04 % (3362158)Termination reason: Instruction limit % 58.23/9.04 % (3362158)Termination phase: Saturation % 58.23/9.04 % (3362158)Time elapsed: 2.247 s % 58.23/9.04 % (3362158)Peak memory usage: 108 MB % 58.23/9.04 % (3362158)Instructions burned: 3707 (million) % 58.23/9.04 % (3362176)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2090692648:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2945 on theBenchmark for (2945ds/1016Mi) % 58.23/9.04 % (3362176)Refutation not found, incomplete strategy % 58.23/9.04 % (3362176)------------------------------ % 58.23/9.04 % (3362176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.23/9.04 % (3362176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/9.04 % (3362176)CaDiCaL version: 2.1.3 % 58.23/9.04 % (3362176)Termination reason: Refutation not found, incomplete strategy % 58.23/9.04 % (3362176)Time elapsed: 0.001 s % 58.23/9.04 % (3362176)Peak memory usage: 87 MB % 58.23/9.04 % (3362177)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2375201212:i=14123:bd=preordered:ins=4_2944 on theBenchmark for (2944ds/14123Mi) % 58.23/9.04 % (3362176)------------------------------ % 58.23/9.04 % (3362176)------------------------------ % 58.23/9.04 % (3362180)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3452210369:i=5781:kws=precedence:bd=all:rawr=on_2942 on theBenchmark for (2942ds/5781Mi) % 58.23/9.04 % (3362135)Instruction limit reached! % 58.23/9.04 % (3362135)------------------------------ % 58.23/9.04 % (3362135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.23/9.04 % (3362135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/9.04 % (3362135)CaDiCaL version: 2.1.3 % 58.23/9.04 % (3362135)Termination reason: Instruction limit % 58.23/9.04 % (3362135)Termination phase: Saturation % 58.23/9.04 % (3362135)Time elapsed: 3.738 s % 58.23/9.04 % (3362135)Peak memory usage: 157 MB % 58.23/9.04 % (3362135)Instructions burned: 6060 (million) % 58.23/9.04 % (3362182)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=2750244921:i=2448:gtgl=5:bd=preordered:gtg=all_2939 on theBenchmark for (2939ds/2448Mi) % 58.23/9.04 % (3362172)Instruction limit reached! % 58.23/9.04 % (3362172)------------------------------ % 58.23/9.04 % (3362172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.23/9.04 % (3362172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/9.04 % (3362172)CaDiCaL version: 2.1.3 % 58.23/9.04 % (3362172)Termination reason: Instruction limit % 58.23/9.04 % (3362172)Termination phase: Saturation % 58.23/9.04 % (3362172)Time elapsed: 1.852 s % 58.23/9.04 % (3362172)Peak memory usage: 145 MB % 58.23/9.04 % (3362172)Instructions burned: 3035 (million) % 58.23/9.04 % (3362184)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1435234984:i=3223:kws=precedence:fgj=on:av=off_2932 on theBenchmark for (2932ds/3223Mi) % 58.23/9.04 % (3362180)Instruction limit reached! % 58.23/9.04 % (3362180)------------------------------ % 58.23/9.04 % (3362180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.23/9.04 % (3362180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.23/9.04 % (3362180)CaDiCaL version: 2.1.3 % 58.23/9.04 % (3362180)Termination reason: Instruction limit % 58.23/9.04 % (3362180)Termination phase: Saturation % 58.23/9.04 % (3362180)Time elapsed: 1.500 s % 58.23/9.04 % (3362180)Peak memory usage: 129 MB % 58.23/9.04 % (3362180)Instructions burned: 5782 (million) % 58.23/9.04 % (3362186)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2451278229:st=5.6:i=2033:sd=3:ss=axioms_2926 on theBenchmark for (2926ds/2033Mi) % 58.23/9.04 % (3362182)Instruction limit reached! % 58.23/9.04 % (3362182)------------------------------ % 58.23/9.04 % (3362182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 58.23/9.04 % (3362182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 58.95/9.19 % (3362182)CaDiCaL version: 2.1.3 % 58.95/9.19 % (3362182)Termination reason: Instruction limit % 58.95/9.19 % (3362182)Termination phase: Saturation % 58.95/9.19 % (3362182)Time elapsed: 1.438 s % 58.95/9.19 % (3362182)Peak memory usage: 148 MB % 58.95/9.19 % (3362182)Instructions burned: 2449 (million) % 58.95/9.19 [W928 06:59:44.328293436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328317293 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328338087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328344554 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328357553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328364059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328377232 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328383690 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328396661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328403051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328416136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 [W928 06:59:44.328422374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 58.95/9.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 58.95/9.19 % (3362188)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1826637446:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2923 on theBenchmark for (2923ds/2055Mi) % 65.31/10.07 % (3362186)Refutation not found, incomplete strategy % 65.31/10.07 % (3362186)------------------------------ % 65.31/10.07 % (3362186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.31/10.07 % (3362186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.31/10.07 % (3362186)CaDiCaL version: 2.1.3 % 65.31/10.07 % (3362186)Termination reason: Refutation not found, incomplete strategy % 65.31/10.07 % (3362186)Time elapsed: 0.312 s % 65.31/10.07 % (3362186)Peak memory usage: 125 MB % 65.31/10.07 % (3362186)Instructions burned: 823 (million) % 65.31/10.07 % (3362186)------------------------------ % 65.31/10.07 % (3362186)------------------------------ % 65.31/10.07 % (3362190)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=1418626797:i=21611:sd=3:ss=axioms_2920 on theBenchmark for (2920ds/21611Mi) % 65.31/10.07 [W928 06:59:44.797704720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797738717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797777661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797790828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797819534 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797831015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797857898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797869278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797894378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.31/10.07 [W928 06:59:44.797905792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.31/10.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.797930839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.797941299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.948915301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.948954338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.948976014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.948982450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.948995940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949008461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949023146 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949030621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949043469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949048904 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949061953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.92/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.92/11.45 [W928 06:59:44.949074019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.05/12.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.05/12.41 % (3362188)Refutation not found, incomplete strategy % 82.05/12.41 % (3362188)------------------------------ % 82.05/12.41 % (3362188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.05/12.41 % (3362188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.05/12.41 % (3362188)CaDiCaL version: 2.1.3 % 82.05/12.41 % (3362188)Termination reason: Refutation not found, incomplete strategy % 82.05/12.41 % (3362188)Time elapsed: 0.549 s % 82.05/12.41 % (3362188)Peak memory usage: 125 MB % 82.05/12.41 % (3362188)Instructions burned: 823 (million) % 82.05/12.41 % (3362190)Refutation not found, incomplete strategy % 82.05/12.41 % (3362190)------------------------------ % 82.05/12.41 % (3362190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.05/12.41 % (3362190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.05/12.41 % (3362190)CaDiCaL version: 2.1.3 % 82.05/12.41 % (3362190)Termination reason: Refutation not found, incomplete strategy % 82.05/12.41 % (3362190)Time elapsed: 0.317 s % 82.05/12.41 % (3362190)Peak memory usage: 125 MB % 82.05/12.41 % (3362190)Instructions burned: 827 (million) % 82.05/12.41 % (3362190)------------------------------ % 82.05/12.41 % (3362190)------------------------------ % 82.05/12.41 % (3362188)------------------------------ % 82.05/12.41 % (3362188)------------------------------ % 82.05/12.41 % (3362192)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3616291254:i=4835:sd=13:ss=axioms:sgt=23_2914 on theBenchmark for (2914ds/4835Mi) % 82.05/12.41 % (3362192)Refutation not found, incomplete strategy % 82.05/12.41 % (3362192)------------------------------ % 82.05/12.41 % (3362192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.05/12.41 % (3362192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.05/12.41 % (3362192)CaDiCaL version: 2.1.3 % 82.05/12.41 % (3362192)Termination reason: Refutation not found, incomplete strategy % 82.05/12.41 % (3362192)Time elapsed: 0.0000 s % 82.05/12.41 % (3362192)Peak memory usage: 86 MB % 82.05/12.41 % (3362193)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=4275352599:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2914 on theBenchmark for (2914ds/797Mi) % 82.05/12.41 % (3362192)------------------------------ % 82.05/12.41 % (3362192)------------------------------ % 82.05/12.41 % (3362196)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3141483752:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2911 on theBenchmark for (2911ds/2326Mi) % 82.05/12.41 % (3362196)Refutation not found, incomplete strategy % 82.05/12.41 % (3362196)------------------------------ % 82.05/12.41 % (3362196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.05/12.41 % (3362196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.05/12.41 % (3362196)CaDiCaL version: 2.1.3 % 82.05/12.41 % (3362196)Termination reason: Refutation not found, incomplete strategy % 82.05/12.41 % (3362196)Time elapsed: 0.004 s % 82.05/12.41 % (3362196)Peak memory usage: 88 MB % 82.05/12.41 % (3362196)Instructions burned: 13 (million) % 82.05/12.41 % (3362184)Instruction limit reached! % 82.05/12.41 % (3362184)------------------------------ % 82.05/12.41 % (3362184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.05/12.41 % (3362184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.05/12.41 % (3362184)CaDiCaL version: 2.1.3 % 82.05/12.41 % (3362184)Termination reason: Instruction limit % 82.05/12.41 % (3362184)Termination phase: Saturation % 82.05/12.41 % (3362184)Time elapsed: 2.159 s % 82.05/12.41 % (3362184)Peak memory usage: 148 MB % 82.05/12.41 % (3362184)Instructions burned: 3223 (million) % 82.05/12.41 % (3362196)------------------------------ % 82.05/12.41 % (3362196)------------------------------ % 82.05/12.41 % (3362193)Instruction limit reached! % 82.05/12.41 % (3362193)------------------------------ % 82.05/12.41 % (3362193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.05/12.41 % (3362193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.63/15.87 % (3362193)CaDiCaL version: 2.1.3 % 105.63/15.87 % (3362193)Termination reason: Instruction limit % 105.63/15.87 % (3362193)Termination phase: Saturation % 105.63/15.87 % (3362193)Time elapsed: 0.451 s % 105.63/15.87 % (3362193)Peak memory usage: 96 MB % 105.63/15.87 % (3362193)Instructions burned: 799 (million) % 105.63/15.87 % (3362198)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1000096592:i=6038:nm=6_2909 on theBenchmark for (2909ds/6038Mi) % 105.63/15.87 % (3362199)lrs+10_1_sil=32000:sp=occurrence:random_seed=3176674143:st=2:i=33334:sd=3:ss=included:sgt=32_2908 on theBenchmark for (2908ds/33334Mi) % 105.63/15.87 % (3362200)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4121257794:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2907 on theBenchmark for (2907ds/1008Mi) % 105.63/15.87 % (3362200)Refutation not found, incomplete strategy % 105.63/15.87 % (3362200)------------------------------ % 105.63/15.87 % (3362200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.63/15.87 % (3362200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.63/15.87 % (3362200)CaDiCaL version: 2.1.3 % 105.63/15.87 % (3362200)Termination reason: Refutation not found, incomplete strategy % 105.63/15.87 % (3362200)Time elapsed: 0.001 s % 105.63/15.87 % (3362200)Peak memory usage: 86 MB % 105.63/15.87 % (3362200)Instructions burned: 1 (million) % 105.63/15.87 % (3362200)------------------------------ % 105.63/15.87 % (3362200)------------------------------ % 105.63/15.87 % (3362204)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=825564602:i=8327:s2at=5:bd=preordered_2903 on theBenchmark for (2903ds/8327Mi) % 105.63/15.87 % (3362198)Refutation not found, incomplete strategy % 105.63/15.87 % (3362198)------------------------------ % 105.63/15.87 % (3362198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.63/15.87 % (3362198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.63/15.87 % (3362198)CaDiCaL version: 2.1.3 % 105.63/15.87 % (3362198)Termination reason: Refutation not found, incomplete strategy % 105.63/15.87 % (3362198)Time elapsed: 0.577 s % 105.63/15.87 % (3362198)Peak memory usage: 129 MB % 105.63/15.87 % (3362198)Instructions burned: 859 (million) % 105.63/15.87 % (3362140)Instruction limit reached! % 105.63/15.87 % (3362140)------------------------------ % 105.63/15.87 % (3362140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.63/15.87 % (3362140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.63/15.87 % (3362140)CaDiCaL version: 2.1.3 % 105.63/15.87 % (3362140)Termination reason: Instruction limit % 105.63/15.87 % (3362140)Termination phase: Saturation % 105.63/15.87 % (3362140)Time elapsed: 7.418 s % 105.63/15.87 % (3362140)Peak memory usage: 217 MB % 105.63/15.87 % (3362140)Instructions burned: 14155 (million) % 105.63/15.87 % (3362198)------------------------------ % 105.63/15.87 % (3362198)------------------------------ % 105.63/15.87 % (3362206)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=2110852052:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2901 on theBenchmark for (2901ds/1083Mi) % 105.63/15.87 % (3362207)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=487241562:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2899 on theBenchmark for (2899ds/1084Mi) % 105.63/15.87 % (3362207)Refutation not found, incomplete strategy % 105.63/15.87 % (3362207)------------------------------ % 105.63/15.87 % (3362207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.63/15.87 % (3362207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.63/15.87 % (3362207)CaDiCaL version: 2.1.3 % 105.63/15.87 % (3362207)Termination reason: Refutation not found, incomplete strategy % 105.63/15.87 % (3362207)Time elapsed: 0.001 s % 105.63/15.87 % (3362207)Peak memory usage: 86 MB % 105.63/15.87 % (3362207)------------------------------ % 105.63/15.87 % (3362207)------------------------------ % 105.63/15.87 % (3362206)Instruction limit reached! % 105.63/15.87 % (3362206)------------------------------ % 105.63/15.87 % (3362206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.63/15.87 % (3362206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.63/15.87 % (3362206)CaDiCaL version: 2.1.3 % 105.63/15.87 % (3362206)Termination reason: Instruction limit % 106.12/15.94 % (3362206)Termination phase: Saturation % 106.12/15.94 % (3362206)Time elapsed: 0.506 s % 106.12/15.94 % (3362206)Peak memory usage: 100 MB % 106.12/15.94 % (3362206)Instructions burned: 1085 (million) % 106.12/15.94 % (3362210)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=96402760:i=6995:s2at=5:gtg=all_2895 on theBenchmark for (2895ds/6995Mi) % 106.12/15.94 % (3362211)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2139849085:st=2:i=6225:sd=15:ss=axioms_2894 on theBenchmark for (2894ds/6225Mi) % 106.12/15.94 % (3362211)Refutation not found, incomplete strategy % 106.12/15.94 % (3362211)------------------------------ % 106.12/15.94 % (3362211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 106.12/15.94 % (3362211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 106.12/15.94 % (3362211)CaDiCaL version: 2.1.3 % 106.12/15.94 % (3362211)Termination reason: Refutation not found, incomplete strategy % 106.12/15.94 % (3362211)Time elapsed: 0.001 s % 106.12/15.94 % (3362211)Peak memory usage: 86 MB % 106.12/15.94 % (3362211)------------------------------ % 106.12/15.94 % (3362211)------------------------------ % 106.12/15.94 % (3362214)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=624239444:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2890 on theBenchmark for (2890ds/3372Mi) % 106.12/15.94 [W928 06:59:48.168164017 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168201188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168241398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168255758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168281512 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168293528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168332219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168342962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168371976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 106.12/15.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 106.12/15.94 [W928 06:59:48.168382319 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.58/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.58/16.16 [W928 06:59:48.168408429 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.58/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.58/16.16 [W928 06:59:48.168418913 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 108.58/16.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 108.58/16.16 % (3362214)Refutation not found, incomplete strategy % 108.58/16.16 % (3362214)------------------------------ % 108.58/16.16 % (3362214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.58/16.16 % (3362214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.58/16.16 % (3362214)CaDiCaL version: 2.1.3 % 108.58/16.16 % (3362214)Termination reason: Refutation not found, incomplete strategy % 108.58/16.16 % (3362214)Time elapsed: 0.551 s % 108.58/16.16 % (3362214)Peak memory usage: 126 MB % 108.58/16.16 % (3362214)Instructions burned: 828 (million) % 108.58/16.16 % (3362214)------------------------------ % 108.58/16.16 % (3362214)------------------------------ % 108.58/16.16 % (3362216)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=263025848:st=2.3:i=26457:sd=10:ss=included:sgt=8_2880 on theBenchmark for (2880ds/26457Mi) % 108.58/16.16 % (3362216)Refutation not found, incomplete strategy % 108.58/16.16 % (3362216)------------------------------ % 108.58/16.16 % (3362216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.58/16.16 % (3362216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.58/16.16 % (3362216)CaDiCaL version: 2.1.3 % 108.58/16.16 % (3362216)Termination reason: Refutation not found, incomplete strategy % 108.58/16.16 % (3362216)Time elapsed: 0.566 s % 108.58/16.16 % (3362216)Peak memory usage: 128 MB % 108.58/16.16 % (3362216)Instructions burned: 852 (million) % 108.58/16.16 % (3362216)------------------------------ % 108.58/16.16 % (3362216)------------------------------ % 108.58/16.16 % (3362218)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=945867082:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2870 on theBenchmark for (2870ds/13494Mi) % 108.58/16.16 % (3362204)Instruction limit reached! % 108.58/16.16 % (3362204)------------------------------ % 108.58/16.16 % (3362204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.58/16.16 % (3362204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.58/16.16 % (3362204)CaDiCaL version: 2.1.3 % 108.58/16.16 % (3362204)Termination reason: Instruction limit % 108.58/16.16 % (3362204)Termination phase: Saturation % 108.58/16.16 % (3362204)Time elapsed: 4.737 s % 108.58/16.16 % (3362204)Peak memory usage: 191 MB % 108.58/16.16 % (3362204)Instructions burned: 8327 (million) % 108.58/16.16 % (3362220)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=1563301392:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2854 on theBenchmark for (2854ds/2503Mi) % 108.58/16.16 % (3362177)Instruction limit reached! % 108.58/16.16 % (3362177)------------------------------ % 108.58/16.16 % (3362177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 108.58/16.16 % (3362177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 108.58/16.16 % (3362177)CaDiCaL version: 2.1.3 % 108.58/16.16 % (3362177)Termination reason: Instruction limit % 108.58/16.16 % (3362177)Termination phase: Saturation % 108.58/16.16 % (3362177)Time elapsed: 8.995 s % 108.58/16.16 % (3362177)Peak memory usage: 256 MB % 108.58/16.16 % (3362177)Instructions burned: 14123 (million) % 108.58/16.16 % (3362222)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3561553932:i=2559:sd=1:ep=RSTC:ss=axioms_2852 on theBenchmark for (2852ds/2559Mi) % 108.58/16.16 % (3362210)Instruction limit reached! % 108.58/16.16 % (3362210)------------------------------ % 122.07/18.13 % (3362210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 122.07/18.13 % (3362210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 122.07/18.13 % (3362210)CaDiCaL version: 2.1.3 % 122.07/18.13 % (3362210)Termination reason: Instruction limit % 122.07/18.13 % (3362210)Termination phase: Saturation % 122.07/18.13 % (3362210)Time elapsed: 4.364 s % 122.07/18.13 % (3362210)Peak memory usage: 167 MB % 122.07/18.13 % (3362210)Instructions burned: 6996 (million) % 122.07/18.13 [W928 06:59:51.704556553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704599960 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704638500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704662367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704692687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704703594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704727724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704738901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704762321 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704773151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704799075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 122.07/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 122.07/18.13 [W928 06:59:51.704811181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 % (3362224)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1846744982:i=30753:av=off:ss=included_2849 on theBenchmark for (2849ds/30753Mi) % 129.16/19.10 % (3362220)Refutation not found, incomplete strategy % 129.16/19.10 % (3362220)------------------------------ % 129.16/19.10 % (3362220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 129.16/19.10 % (3362220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 129.16/19.10 % (3362220)CaDiCaL version: 2.1.3 % 129.16/19.10 % (3362220)Termination reason: Refutation not found, incomplete strategy % 129.16/19.10 % (3362220)Time elapsed: 0.553 s % 129.16/19.10 % (3362220)Peak memory usage: 125 MB % 129.16/19.10 % (3362220)Instructions burned: 827 (million) % 129.16/19.10 [W928 06:59:51.916895266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.916940076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.916980206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.916992293 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917031356 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917044273 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917070990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917082673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917107900 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917119894 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 129.16/19.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 129.16/19.10 [W928 06:59:51.917147504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 [W928 06:59:51.917159227 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 % (3362222)Refutation not found, incomplete strategy % 133.02/19.68 % (3362222)------------------------------ % 133.02/19.68 % (3362222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.02/19.68 % (3362222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.68 % (3362222)CaDiCaL version: 2.1.3 % 133.02/19.68 % (3362222)Termination reason: Refutation not found, incomplete strategy % 133.02/19.68 % (3362222)Time elapsed: 0.554 s % 133.02/19.68 % (3362222)Peak memory usage: 125 MB % 133.02/19.68 % (3362222)Instructions burned: 823 (million) % 133.02/19.68 % (3362220)------------------------------ % 133.02/19.68 % (3362220)------------------------------ % 133.02/19.68 % (3362226)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3151739473:i=26473:ep=RSTC_2844 on theBenchmark for (2844ds/26473Mi) % 133.02/19.68 % (3362222)------------------------------ % 133.02/19.68 % (3362222)------------------------------ % 133.02/19.68 % (3362228)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=1224567917:cts=off:i=2759:kws=inv_arity:fgj=on_2842 on theBenchmark for (2842ds/2759Mi) % 133.02/19.68 % (3362228)Refutation not found, incomplete strategy % 133.02/19.68 % (3362228)------------------------------ % 133.02/19.68 % (3362228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.02/19.68 % (3362228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.02/19.68 % (3362228)CaDiCaL version: 2.1.3 % 133.02/19.68 % (3362228)Termination reason: Refutation not found, incomplete strategy % 133.02/19.68 % (3362228)Time elapsed: 0.572 s % 133.02/19.68 % (3362228)Peak memory usage: 129 MB % 133.02/19.68 % (3362228)Instructions burned: 858 (million) % 133.02/19.68 % (3362228)------------------------------ % 133.02/19.68 % (3362228)------------------------------ % 133.02/19.68 % (3362230)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=166401129:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2832 on theBenchmark for (2832ds/5665Mi) % 133.02/19.68 [W928 06:59:53.887597568 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 [W928 06:59:53.887631932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 [W928 06:59:53.887668762 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 [W928 06:59:53.887681039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 [W928 06:59:53.887707836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 133.02/19.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.02/19.68 [W928 06:59:53.887719209 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:53.887744333 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:53.887754676 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:53.887778503 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:53.887788740 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:53.887811923 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:53.887822060 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 % (3362230)Refutation not found, incomplete strategy % 134.53/19.94 % (3362230)------------------------------ % 134.53/19.94 % (3362230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 134.53/19.94 % (3362230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 134.53/19.94 % (3362230)CaDiCaL version: 2.1.3 % 134.53/19.94 % (3362230)Termination reason: Refutation not found, incomplete strategy % 134.53/19.94 % (3362230)Time elapsed: 0.549 s % 134.53/19.94 % (3362230)Peak memory usage: 125 MB % 134.53/19.94 % (3362230)Instructions burned: 826 (million) % 134.53/19.94 % (3362230)------------------------------ % 134.53/19.94 % (3362230)------------------------------ % 134.53/19.94 % (3362232)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=1701265384:i=1532:ep=RS:ss=axioms_2823 on theBenchmark for (2823ds/1532Mi) % 134.53/19.94 [W928 06:59:54.863332829 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:54.863367932 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:54.863406986 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 134.53/19.94 [W928 06:59:54.863420462 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/19.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863447223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863458059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863483163 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863493686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863517146 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863527627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863551930 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 [W928 06:59:54.863562410 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.56/20.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.56/20.46 % (3362232)Refutation not found, incomplete strategy % 138.56/20.46 % (3362232)------------------------------ % 138.56/20.46 % (3362232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.46 % (3362232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.46 % (3362232)CaDiCaL version: 2.1.3 % 138.56/20.46 % (3362232)Termination reason: Refutation not found, incomplete strategy % 138.56/20.46 % (3362232)Time elapsed: 0.548 s % 138.56/20.46 % (3362232)Peak memory usage: 125 MB % 138.56/20.46 % (3362232)Instructions burned: 827 (million) % 138.56/20.46 % (3362199)Instruction limit reached! % 138.56/20.46 % (3362199)------------------------------ % 138.56/20.46 % (3362199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.56/20.46 % (3362199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.56/20.46 % (3362199)CaDiCaL version: 2.1.3 % 138.56/20.46 % (3362199)Termination reason: Instruction limit % 138.56/20.46 % (3362199)Termination phase: Saturation % 138.56/20.46 % (3362199)Time elapsed: 9.353 s % 138.56/20.46 % (3362199)Peak memory usage: 372 MB % 138.56/20.46 % (3362199)Instructions burned: 33338 (million) % 138.56/20.46 % (3362232)------------------------------ % 138.56/20.46 % (3362232)------------------------------ % 138.56/20.46 % (3362234)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1925537041:i=1565:sd=2:ss=axioms:sgt=32_2813 on theBenchmark for (2813ds/1565Mi) % 138.56/20.46 % (3362235)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=3640460709:i=1572:fgj=on:gsp=on_2813 on theBenchmark for (2813ds/1572Mi) % 143.33/21.06 [W928 06:59:55.596589736 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596610461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596630871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596637004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596649702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596656114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596669073 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596675237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596687554 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596693946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596707127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 [W928 06:59:55.596713664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 143.33/21.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 143.33/21.06 % (3362234)Refutation not found, incomplete strategy % 143.33/21.06 % (3362234)------------------------------ % 143.33/21.06 % (3362234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 143.33/21.06 % (3362234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 143.33/21.06 % (3362234)CaDiCaL version: 2.1.3 % 151.60/22.23 % (3362234)Termination reason: Refutation not found, incomplete strategy % 151.60/22.23 % (3362234)Time elapsed: 0.312 s % 151.60/22.23 % (3362234)Peak memory usage: 125 MB % 151.60/22.23 % (3362234)Instructions burned: 827 (million) % 151.60/22.23 % (3362234)------------------------------ % 151.60/22.23 % (3362234)------------------------------ % 151.60/22.23 % (3362238)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=215493884:i=6052:sd=4:ss=axioms:sgt=24_2807 on theBenchmark for (2807ds/6052Mi) % 151.60/22.23 [W928 06:59:56.219937687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.219960675 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.219982234 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.219988636 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220008331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220014526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220028302 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220033616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220046160 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220061493 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220075526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 151.60/22.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 151.60/22.23 [W928 06:59:56.220080842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 % (3362238)Refutation not found, incomplete strategy % 155.12/22.82 % (3362238)------------------------------ % 155.12/22.82 % (3362238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.12/22.82 % (3362238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/22.82 % (3362238)CaDiCaL version: 2.1.3 % 155.12/22.82 % (3362238)Termination reason: Refutation not found, incomplete strategy % 155.12/22.82 % (3362238)Time elapsed: 0.311 s % 155.12/22.82 % (3362238)Peak memory usage: 125 MB % 155.12/22.82 % (3362238)Instructions burned: 824 (million) % 155.12/22.82 % (3362235)Instruction limit reached! % 155.12/22.82 % (3362235)------------------------------ % 155.12/22.82 % (3362235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.12/22.82 % (3362235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.12/22.82 % (3362235)CaDiCaL version: 2.1.3 % 155.12/22.82 % (3362235)Termination reason: Instruction limit % 155.12/22.82 % (3362235)Termination phase: Saturation % 155.12/22.82 % (3362235)Time elapsed: 1.046 s % 155.12/22.82 % (3362235)Peak memory usage: 135 MB % 155.12/22.82 % (3362235)Instructions burned: 1572 (million) % 155.12/22.82 % (3362238)------------------------------ % 155.12/22.82 % (3362238)------------------------------ % 155.12/22.82 % (3362241)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=614817008:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2801 on theBenchmark for (2801ds/1842Mi) % 155.12/22.82 % (3362240)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=373568587:i=3500:sd=1:bd=preordered:sup=off:ss=included_2801 on theBenchmark for (2801ds/3500Mi) % 155.12/22.82 [W928 06:59:56.824732311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824770817 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824791825 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824797968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824810942 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824816389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824829551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.12/22.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.12/22.82 [W928 06:59:56.824836326 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.10/24.62 [W928 06:59:56.824849089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.10/24.62 [W928 06:59:56.824854615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.10/24.62 [W928 06:59:56.824867195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.10/24.62 [W928 06:59:56.824881551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.10/24.62 % (3362241)Refutation not found, incomplete strategy % 168.10/24.62 % (3362241)------------------------------ % 168.10/24.62 % (3362241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.10/24.62 % (3362241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.62 % (3362241)CaDiCaL version: 2.1.3 % 168.10/24.62 % (3362241)Termination reason: Refutation not found, incomplete strategy % 168.10/24.62 % (3362241)Time elapsed: 0.294 s % 168.10/24.62 % (3362241)Peak memory usage: 126 MB % 168.10/24.62 % (3362241)Instructions burned: 825 (million) % 168.10/24.62 % (3362241)------------------------------ % 168.10/24.62 % (3362241)------------------------------ % 168.10/24.62 % (3362244)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3816072929:i=66096:add=on_2795 on theBenchmark for (2795ds/66096Mi) % 168.10/24.62 % (3362240)Refutation not found, incomplete strategy % 168.10/24.62 % (3362240)------------------------------ % 168.10/24.62 % (3362240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.10/24.62 % (3362240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.62 % (3362240)CaDiCaL version: 2.1.3 % 168.10/24.62 % (3362240)Termination reason: Refutation not found, incomplete strategy % 168.10/24.62 % (3362240)Time elapsed: 0.558 s % 168.10/24.62 % (3362240)Peak memory usage: 127 MB % 168.10/24.62 % (3362240)Instructions burned: 831 (million) % 168.10/24.62 % (3362240)------------------------------ % 168.10/24.62 % (3362240)------------------------------ % 168.10/24.62 % (3362246)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=97878588:i=1884:sd=1:nm=60:ss=axioms_2791 on theBenchmark for (2791ds/1884Mi) % 168.10/24.62 % (3362218)Instruction limit reached! % 168.10/24.62 % (3362218)------------------------------ % 168.10/24.62 % (3362218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.10/24.62 % (3362218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.10/24.62 % (3362218)CaDiCaL version: 2.1.3 % 168.10/24.62 % (3362218)Termination reason: Instruction limit % 168.10/24.62 % (3362218)Termination phase: Saturation % 168.10/24.62 % (3362218)Time elapsed: 8.178 s % 168.10/24.62 % (3362218)Peak memory usage: 235 MB % 168.10/24.62 % (3362218)Instructions burned: 13494 (million) % 168.10/24.62 [W928 06:59:57.996079753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.10/24.62 [W928 06:59:57.996115053 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 168.10/24.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996154437 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996165604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996190784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996200991 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996226381 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996236511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996260614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996270591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996294561 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 [W928 06:59:57.996304531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.30/28.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.30/28.50 % (3362248)lrs-1011_4:1_sil=16000:bsr=on:random_seed=225722693:cts=off:i=5469:bs=on:fsr=off_2786 on theBenchmark for (2786ds/5469Mi) % 196.30/28.50 % (3362246)Refutation not found, incomplete strategy % 196.30/28.50 % (3362246)------------------------------ % 196.30/28.50 % (3362246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.30/28.50 % (3362246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.30/28.50 % (3362246)CaDiCaL version: 2.1.3 % 196.30/28.50 % (3362246)Termination reason: Refutation not found, incomplete strategy % 196.30/28.50 % (3362246)Time elapsed: 0.545 s % 196.30/28.50 % (3362246)Peak memory usage: 125 MB % 196.30/28.50 % (3362246)Instructions burned: 823 (million) % 196.30/28.50 % (3362246)------------------------------ % 196.30/28.50 % (3362246)------------------------------ % 196.30/28.50 % (3362250)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=2143594262:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2782 on theBenchmark for (2782ds/2037Mi) % 200.81/29.15 % (3362250)Instruction limit reached! % 200.81/29.15 % (3362250)------------------------------ % 200.81/29.15 % (3362250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.81/29.15 % (3362250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.81/29.15 % (3362250)CaDiCaL version: 2.1.3 % 200.81/29.15 % (3362250)Termination reason: Instruction limit % 200.81/29.15 % (3362250)Termination phase: Saturation % 200.81/29.15 % (3362250)Time elapsed: 1.254 s % 200.81/29.15 % (3362250)Peak memory usage: 139 MB % 200.81/29.15 % (3362250)Instructions burned: 2039 (million) % 200.81/29.15 % (3362252)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1244191620:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2767 on theBenchmark for (2767ds/2110Mi) % 200.81/29.15 [W928 07:00:00.385169106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385203386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385242136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385265913 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385293586 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385305120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385331187 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385342670 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385372800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385385830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.81/29.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.81/29.15 [W928 07:00:00.385410774 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.08 [W928 07:00:00.385423607 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 228.48/33.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 228.48/33.08 % (3362252)Refutation not found, incomplete strategy % 228.48/33.08 % (3362252)------------------------------ % 228.48/33.08 % (3362252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.48/33.08 % (3362252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.48/33.08 % (3362252)CaDiCaL version: 2.1.3 % 228.48/33.08 % (3362252)Termination reason: Refutation not found, incomplete strategy % 228.48/33.08 % (3362252)Time elapsed: 0.548 s % 228.48/33.08 % (3362252)Peak memory usage: 125 MB % 228.48/33.08 % (3362252)Instructions burned: 827 (million) % 228.48/33.08 % (3362252)------------------------------ % 228.48/33.08 % (3362252)------------------------------ % 228.48/33.08 % (3362248)Instruction limit reached! % 228.48/33.08 % (3362248)------------------------------ % 228.48/33.08 % (3362248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.48/33.08 % (3362248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.48/33.08 % (3362248)CaDiCaL version: 2.1.3 % 228.48/33.08 % (3362248)Termination reason: Instruction limit % 228.48/33.08 % (3362248)Termination phase: Saturation % 228.48/33.08 % (3362248)Time elapsed: 2.776 s % 228.48/33.08 % (3362248)Peak memory usage: 109 MB % 228.48/33.08 % (3362248)Instructions burned: 5470 (million) % 228.48/33.08 % (3362254)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=2933238998:i=2430:add=off:aac=none:nm=16_2758 on theBenchmark for (2758ds/2430Mi) % 228.48/33.08 % (3362255)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=2887316607:cond=fast:i=4891_2757 on theBenchmark for (2757ds/4891Mi) % 228.48/33.08 % (3362254)Instruction limit reached! % 228.48/33.08 % (3362254)------------------------------ % 228.48/33.08 % (3362254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.48/33.08 % (3362254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.48/33.08 % (3362254)CaDiCaL version: 2.1.3 % 228.48/33.08 % (3362254)Termination reason: Instruction limit % 228.48/33.08 % (3362254)Termination phase: Saturation % 228.48/33.08 % (3362254)Time elapsed: 1.540 s % 228.48/33.08 % (3362254)Peak memory usage: 140 MB % 228.48/33.08 % (3362254)Instructions burned: 2431 (million) % 228.48/33.08 % (3362258)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=3711364807:st=2:i=14845:sd=2:ss=included:fsd=on_2741 on theBenchmark for (2741ds/14845Mi) % 228.48/33.08 % (3362258)Refutation not found, incomplete strategy % 228.48/33.08 % (3362258)------------------------------ % 228.48/33.08 % (3362258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.48/33.08 % (3362258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.48/33.08 % (3362258)CaDiCaL version: 2.1.3 % 228.48/33.08 % (3362258)Termination reason: Refutation not found, incomplete strategy % 228.48/33.08 % (3362258)Time elapsed: 0.552 s % 228.48/33.08 % (3362258)Peak memory usage: 127 MB % 228.48/33.08 % (3362258)Instructions burned: 831 (million) % 228.48/33.08 % (3362258)------------------------------ % 228.48/33.08 % (3362258)------------------------------ % 228.48/33.08 % (3362260)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1329533929:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2731 on theBenchmark for (2731ds/7534Mi) % 228.48/33.08 % (3362260)Refutation not found, incomplete strategy % 228.48/33.08 % (3362260)------------------------------ % 228.48/33.08 % (3362260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 228.48/33.08 % (3362260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 228.48/33.08 % (3362260)CaDiCaL version: 2.1.3 % 228.48/33.08 % (3362260)Termination reason: Refutation not found, incomplete strategy % 228.48/33.08 % (3362260)Time elapsed: 0.606 s % 231.96/33.67 % (3362260)Peak memory usage: 128 MB % 231.96/33.67 % (3362260)Instructions burned: 919 (million) % 231.96/33.67 % (3362255)Instruction limit reached! % 231.96/33.67 % (3362255)------------------------------ % 231.96/33.67 % (3362255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.96/33.67 % (3362255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.96/33.67 % (3362255)CaDiCaL version: 2.1.3 % 231.96/33.67 % (3362255)Termination reason: Instruction limit % 231.96/33.67 % (3362255)Termination phase: Saturation % 231.96/33.67 % (3362255)Time elapsed: 3.275 s % 231.96/33.67 % (3362255)Peak memory usage: 165 MB % 231.96/33.67 % (3362255)Instructions burned: 4891 (million) % 231.96/33.67 % (3362260)------------------------------ % 231.96/33.67 % (3362260)------------------------------ % 231.96/33.67 % (3362262)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=271406474:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2722 on theBenchmark for (2722ds/10353Mi) % 231.96/33.67 % (3362263)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3020925759:i=7860_2721 on theBenchmark for (2721ds/7860Mi) % 231.96/33.67 % (3362263)Refutation not found, incomplete strategy % 231.96/33.67 % (3362263)------------------------------ % 231.96/33.67 % (3362263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 231.96/33.67 % (3362263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 231.96/33.67 % (3362263)CaDiCaL version: 2.1.3 % 231.96/33.67 % (3362263)Termination reason: Refutation not found, incomplete strategy % 231.96/33.67 % (3362263)Time elapsed: 0.005 s % 231.96/33.67 % (3362263)Peak memory usage: 88 MB % 231.96/33.67 % (3362263)Instructions burned: 8 (million) % 231.96/33.67 [W928 07:00:04.915657924 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915692311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915732165 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915743742 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915771508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915783325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915809389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 231.96/33.67 [W928 07:00:04.915821129 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 231.96/33.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.54/34.08 [W928 07:00:04.915846866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.54/34.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.54/34.08 [W928 07:00:04.915870786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.54/34.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.54/34.08 [W928 07:00:04.915896839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.54/34.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.54/34.08 [W928 07:00:04.915907073 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.54/34.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.54/34.08 % (3362263)------------------------------ % 235.54/34.08 % (3362263)------------------------------ % 235.54/34.08 % (3362262)Refutation not found, incomplete strategy % 235.54/34.08 % (3362262)------------------------------ % 235.54/34.08 % (3362262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.54/34.08 % (3362262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.54/34.08 % (3362262)CaDiCaL version: 2.1.3 % 235.54/34.08 % (3362262)Termination reason: Refutation not found, incomplete strategy % 235.54/34.08 % (3362262)Time elapsed: 0.554 s % 235.54/34.08 % (3362262)Peak memory usage: 125 MB % 235.54/34.08 % (3362262)Instructions burned: 827 (million) % 235.54/34.08 % (3362266)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=2355925119:i=7896:sd=2:bs=on:ss=included:sgt=20_2716 on theBenchmark for (2716ds/7896Mi) % 235.54/34.08 % (3362262)------------------------------ % 235.54/34.08 % (3362262)------------------------------ % 235.54/34.08 % (3362268)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1993997209:i=5812:gtgl=2:gtg=all_2712 on theBenchmark for (2712ds/5812Mi) % 235.54/34.08 % (3362226)Instruction limit reached! % 235.54/34.08 % (3362226)------------------------------ % 235.54/34.08 % (3362226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.54/34.08 % (3362226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.54/34.08 % (3362226)CaDiCaL version: 2.1.3 % 235.54/34.08 % (3362226)Termination reason: Instruction limit % 235.54/34.08 % (3362226)Termination phase: Saturation % 235.54/34.08 % (3362226)Time elapsed: 14.723 s % 235.54/34.08 % (3362226)Peak memory usage: 1106 MB % 235.54/34.08 % (3362226)Instructions burned: 26473 (million) % 235.54/34.08 % (3362270)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=3169863960:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2694 on theBenchmark for (2694ds/2965Mi) % 235.54/34.08 % (3362270)Refutation not found, incomplete strategy % 235.54/34.08 % (3362270)------------------------------ % 235.54/34.08 % (3362270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.54/34.08 % (3362270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.54/34.08 % (3362270)CaDiCaL version: 2.1.3 % 235.54/34.08 % (3362270)Termination reason: Refutation not found, incomplete strategy % 235.54/34.08 % (3362270)Time elapsed: 0.573 s % 235.54/34.08 % (3362270)Peak memory usage: 129 MB % 235.54/34.08 % (3362270)Instructions burned: 858 (million) % 235.54/34.08 % (3362270)------------------------------ % 235.54/34.08 % (3362270)------------------------------ % 235.54/34.08 % (3362272)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=2051653472:i=2967:kws=precedence:bd=preordered:av=off_2684 on theBenchmark for (2684ds/2967Mi) % 235.54/34.08 % (3362224)Instruction limit reached! % 235.54/34.08 % (3362224)------------------------------ % 235.54/34.08 % (3362224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.79/34.67 % (3362224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.79/34.67 % (3362224)CaDiCaL version: 2.1.3 % 238.79/34.67 % (3362224)Termination reason: Instruction limit % 238.79/34.67 % (3362224)Termination phase: Saturation % 238.79/34.67 % (3362224)Time elapsed: 17.035 s % 238.79/34.67 % (3362224)Peak memory usage: 419 MB % 238.79/34.67 % (3362224)Instructions burned: 30754 (million) % 238.79/34.67 % (3362274)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=3631801012:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2677 on theBenchmark for (2677ds/3022Mi) % 238.79/34.67 % (3362268)Instruction limit reached! % 238.79/34.67 % (3362268)------------------------------ % 238.79/34.67 % (3362268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.79/34.67 % (3362268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.79/34.67 % (3362268)CaDiCaL version: 2.1.3 % 238.79/34.67 % (3362268)Termination reason: Instruction limit % 238.79/34.67 % (3362268)Termination phase: Saturation % 238.79/34.67 % (3362268)Time elapsed: 3.788 s % 238.79/34.67 % (3362268)Peak memory usage: 170 MB % 238.79/34.67 % (3362268)Instructions burned: 5813 (million) % 238.79/34.67 [W928 07:00:09.432376424 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432411701 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432451458 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432463691 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432495212 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432506922 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432534162 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432545932 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432571415 register_special_ops.cpp:225] Warning: Creating a tensor from 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.79/34.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.79/34.67 [W928 07:00:09.432583142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.432608819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.432634496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 % (3362276)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=3593990762:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2673 on theBenchmark for (2673ds/3207Mi) % 239.61/34.86 % (3362274)Refutation not found, incomplete strategy % 239.61/34.86 % (3362274)------------------------------ % 239.61/34.86 % (3362274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.61/34.86 % (3362274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.61/34.86 % (3362274)CaDiCaL version: 2.1.3 % 239.61/34.86 % (3362274)Termination reason: Refutation not found, incomplete strategy % 239.61/34.86 % (3362274)Time elapsed: 0.559 s % 239.61/34.86 % (3362274)Peak memory usage: 125 MB % 239.61/34.86 % (3362274)Instructions burned: 823 (million) % 239.61/34.86 % (3362266)Instruction limit reached! % 239.61/34.86 % (3362266)------------------------------ % 239.61/34.86 % (3362266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.61/34.86 % (3362266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.61/34.86 % (3362266)CaDiCaL version: 2.1.3 % 239.61/34.86 % (3362266)Termination reason: Instruction limit % 239.61/34.86 % (3362266)Termination phase: Saturation % 239.61/34.86 % (3362266)Time elapsed: 4.577 s % 239.61/34.86 % (3362266)Peak memory usage: 149 MB % 239.61/34.86 % (3362266)Instructions burned: 7897 (million) % 239.61/34.86 [W928 07:00:09.841070159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.841105809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.841143219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.841155366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.841180583 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.841192333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.61/34.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.61/34.86 [W928 07:00:09.841217816 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.26/36.70 [W928 07:00:09.841239927 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.26/36.70 [W928 07:00:09.841269427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.26/36.70 [W928 07:00:09.841280487 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.26/36.70 [W928 07:00:09.841304577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.26/36.70 [W928 07:00:09.841314820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 253.26/36.70 % (3362278)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2104044947:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2669 on theBenchmark for (2669ds/3289Mi) % 253.26/36.70 % (3362274)------------------------------ % 253.26/36.70 % (3362274)------------------------------ % 253.26/36.70 % (3362276)Refutation not found, incomplete strategy % 253.26/36.70 % (3362276)------------------------------ % 253.26/36.70 % (3362276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.26/36.70 % (3362276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.26/36.70 % (3362276)CaDiCaL version: 2.1.3 % 253.26/36.70 % (3362276)Termination reason: Refutation not found, incomplete strategy % 253.26/36.70 % (3362276)Time elapsed: 0.549 s % 253.26/36.70 % (3362276)Peak memory usage: 125 MB % 253.26/36.70 % (3362276)Instructions burned: 827 (million) % 253.26/36.70 % (3362280)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2743615426:i=38569:sd=3:ss=axioms:sgt=32_2667 on theBenchmark for (2667ds/38569Mi) % 253.26/36.70 % (3362272)Instruction limit reached! % 253.26/36.70 % (3362272)------------------------------ % 253.26/36.70 % (3362272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 253.26/36.70 % (3362272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 253.26/36.70 % (3362272)CaDiCaL version: 2.1.3 % 253.26/36.70 % (3362272)Termination reason: Instruction limit % 253.26/36.70 % (3362272)Termination phase: Saturation % 253.26/36.70 % (3362272)Time elapsed: 1.828 s % 253.26/36.70 % (3362272)Peak memory usage: 147 MB % 253.26/36.70 % (3362272)Instructions burned: 2969 (million) % 253.26/36.70 % (3362276)------------------------------ % 253.26/36.70 % (3362276)------------------------------ % 253.26/36.70 % (3362282)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=4088723516:cts=off:i=3394_2664 on theBenchmark for (2664ds/3394Mi) % 253.26/36.70 % (3362283)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=2998703745:i=33824:bd=preordered_2663 on theBenchmark for (2663ds/33824Mi) % 253.26/36.70 [W928 07:00:10.435231076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 253.26/36.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435265100 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435303047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435326583 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435353367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435363544 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435388190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435398331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435422144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435432484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435456284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 [W928 07:00:10.435466448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.17/39.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.17/39.26 % (3362278)Refutation not found, incomplete strategy % 272.17/39.26 % (3362278)------------------------------ % 272.17/39.26 % (3362278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.17/39.26 % (3362278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.17/39.26 % (3362278)CaDiCaL version: 2.1.3 % 272.17/39.26 % (3362278)Termination reason: Refutation not found, incomplete strategy % 272.17/39.26 % (3362278)Time elapsed: 0.575 s % 272.17/39.26 % (3362278)Peak memory usage: 129 MB % 272.17/39.26 % (3362278)Instructions burned: 852 (million) % 272.17/39.26 % (3362280)Refutation not found, incomplete strategy % 272.17/39.26 % (3362280)------------------------------ % 300.13/43.17 % (3362280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.17 % (3362280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.17 % (3362280)CaDiCaL version: 2.1.3 % 300.13/43.17 % (3362280)Termination reason: Refutation not found, incomplete strategy % 300.13/43.17 % (3362280)Time elapsed: 0.567 s % 300.13/43.17 % (3362280)Peak memory usage: 125 MB % 300.13/43.17 % (3362280)Instructions burned: 826 (million) % 300.13/43.17 % (3362278)------------------------------ % 300.13/43.17 % (3362278)------------------------------ % 300.13/43.17 % (3362280)------------------------------ % 300.13/43.17 % (3362280)------------------------------ % 300.13/43.17 % (3362286)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=832153119:i=20684:bd=all:gtg=exists_sym_2659 on theBenchmark for (2659ds/20684Mi) % 300.13/43.17 % (3362288)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=658921010:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2657 on theBenchmark for (2657ds/7222Mi) % 300.13/43.17 % (3362288)Refutation not found, incomplete strategy % 300.13/43.17 % (3362288)------------------------------ % 300.13/43.17 % (3362288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.17 % (3362288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.17 % (3362288)CaDiCaL version: 2.1.3 % 300.13/43.17 % (3362288)Termination reason: Refutation not found, incomplete strategy % 300.13/43.17 % (3362288)Time elapsed: 0.592 s % 300.13/43.17 % (3362288)Peak memory usage: 129 MB % 300.13/43.17 % (3362288)Instructions burned: 859 (million) % 300.13/43.17 % (3362288)------------------------------ % 300.13/43.17 % (3362288)------------------------------ % 300.13/43.17 % (3362290)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3916179277:st=4:i=7295:sd=4:ep=R:ss=axioms_2647 on theBenchmark for (2647ds/7295Mi) % 300.13/43.17 % (3362282)Instruction limit reached! % 300.13/43.17 % (3362282)------------------------------ % 300.13/43.17 % (3362282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.17 % (3362282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.17 % (3362282)CaDiCaL version: 2.1.3 % 300.13/43.17 % (3362282)Termination reason: Instruction limit % 300.13/43.17 % (3362282)Termination phase: Saturation % 300.13/43.17 % (3362282)Time elapsed: 2.151 s % 300.13/43.17 % (3362282)Peak memory usage: 146 MB % 300.13/43.17 % (3362282)Instructions burned: 3394 (million) % 300.13/43.17 [W928 07:00:12.458241019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458271069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458310813 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458323986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458351523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458363070 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458389560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458411074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458439131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458449937 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458475424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 [W928 07:00:12.458485951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.13/43.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.13/43.17 % (3362292)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3004613647:i=4036:ins=10_2641 on theBenchmark for (2641ds/4036Mi) % 300.13/43.17 % (3362290)Refutation not found, incomplete strategy % 300.13/43.17 % (3362290)------------------------------ % 300.13/43.17 % (3362290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.17 % (3362290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.17 % (3362290)CaDiCaL version: 2.1.3 % 300.13/43.17 % (3362290)Termination reason: Refutation not found, incomplete strategy % 300.13/43.17 % (3362290)Time elapsed: 0.575 s % 300.13/43.17 % (3362290)Peak memory usage: 125 MB % 300.13/43.17 % (3362290)Instructions burned: 827 (million) % 300.13/43.17 % (3362290)------------------------------ % 300.13/43.17 % (3362290)------------------------------ % 300.13/43.17 % (3362294)lrs+10_1_sil=128000:lcm=predicate:random_seed=2635220229:st=3:i=43697:sd=5:ss=axioms_2637 on theBenchmark for (2637ds/43697Mi) % 300.13/43.17 % (3362294)Refutation not found, incomplete strategy % 300.13/43.17 % (3362294)------------------------------ % 300.13/43.17 % (3362294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.17 % (3362294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.13/43.17 % (3362294)CaDiCaL version: 2.1.3 % 300.13/43.17 % (3362294)Termination reason: Refutation not found, incomplete strategy % 300.13/43.17 % (3362294)Time elapsed: 0.001 s % 300.13/43.17 % (3362294)Peak memory usage: 86 MB % 300.13/43.17 % (3362294)------------------------------ % 300.13/43.17 % (3362294)------------------------------ % 300.13/43.17 % (3362296)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=77402003:i=17599:gtg=all:ss=axioms:fsd=on_2632 on theBenchmark for (2632ds/17599Mi) % 300.13/43.17 % (3362292)Instruction limit reached! % 300.13/43.17 % (3362292)------------------------------ % 300.13/43.17 % (3362292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.13/43.17 % (3362292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c8 % 300.13/43.18 Terminated %------------------------------------------------------------------------------