%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : NUM925_10 : TPTP v9.3.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:17:32 PM UTC 2026 % Result : Timeout 287.34s 42.02s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM925_10 : TPTP v9.3.1. Released v8.2.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.39 % Computer : n007.cluster.edu % 0.10/0.39 % Model : x86_64 x86_64 % 0.10/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.39 % Memory : 8046.5625MB % 0.10/0.39 % OS : Linux 6.8.0-71-generic % 0.10/0.39 % CPULimit : 300 % 0.10/0.39 % WCLimit : 300 % 0.10/0.39 % DateTime : Sun Sep 27 21:39:41 UTC 2026 % 0.10/0.40 % CPUTime : % 0.10/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.43 Running first-order theorem proving % 0.10/0.43 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 % 9.72/2.21 % (1803984)Detected formulas, will run a generic FOF schedule. % 9.72/2.21 % (1803995)dis-21_1_sil=8000:lcm=predicate:random_seed=4089115526:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 9.72/2.21 % (1803995)Instruction limit reached! % 9.72/2.21 % (1803995)------------------------------ % 9.72/2.21 % (1803995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.72/2.21 % (1803995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.72/2.21 % (1803995)CaDiCaL version: 2.1.3 % 9.72/2.21 % (1803995)Termination reason: Instruction limit % 9.72/2.21 % (1803995)Termination phase: Saturation % 9.72/2.21 % (1803995)Time elapsed: 0.041 s % 9.72/2.21 % (1803995)Peak memory usage: 89 MB % 9.72/2.21 % (1803995)Instructions burned: 132 (million) % 9.72/2.21 % (1803992)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3114620225:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 9.72/2.21 % (1803991)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=2351982474:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 9.72/2.21 % (1803989)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=368483686:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 9.72/2.21 % (1803990)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=3332656135:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 9.72/2.21 % (1803993)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3153131138:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 9.72/2.21 % (1803993)Refutation not found, incomplete strategy % 9.72/2.21 % (1803993)------------------------------ % 9.72/2.21 % (1803993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.72/2.21 % (1803993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.72/2.21 % (1803993)CaDiCaL version: 2.1.3 % 9.72/2.21 % (1803993)Termination reason: Refutation not found, incomplete strategy % 9.72/2.21 % (1803993)Time elapsed: 0.0000 s % 9.72/2.21 % (1803993)Peak memory usage: 86 MB % 9.72/2.21 % (1803992)Refutation not found, incomplete strategy % 9.72/2.21 % (1803992)------------------------------ % 9.72/2.21 % (1803992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.72/2.21 % (1803992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.72/2.21 % (1803992)CaDiCaL version: 2.1.3 % 9.72/2.21 % (1803992)Termination reason: Refutation not found, incomplete strategy % 9.72/2.21 % (1803992)Time elapsed: 0.001 s % 9.72/2.21 % (1803992)Peak memory usage: 86 MB % 9.72/2.21 % (1803994)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1217364570:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 9.72/2.21 % (1803994)Instruction limit reached! % 9.72/2.21 % (1803994)------------------------------ % 9.72/2.21 % (1803994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.72/2.21 % (1803994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.72/2.21 % (1803994)CaDiCaL version: 2.1.3 % 9.72/2.21 % (1803994)Termination reason: Instruction limit % 9.72/2.21 % (1803994)Termination phase: Saturation % 9.72/2.21 % (1803994)Time elapsed: 0.048 s % 9.72/2.21 % (1803994)Peak memory usage: 90 MB % 9.72/2.21 % (1803994)Instructions burned: 141 (million) % 9.72/2.21 % (1804002)lrs+10_1_sil=8000:sp=occurrence:random_seed=1730949466:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 9.72/2.21 % (1804002)Refutation not found, incomplete strategy % 9.72/2.21 % (1804002)------------------------------ % 9.72/2.21 % (1804002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.72/2.21 % (1804002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.72/2.21 % (1804002)CaDiCaL version: 2.1.3 % 9.72/2.21 % (1804002)Termination reason: Refutation not found, incomplete strategy % 9.72/2.21 % (1804002)Time elapsed: 0.001 s % 9.72/2.21 % (1804002)Peak memory usage: 87 MB % 9.72/2.21 % (1804004)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2885442487:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 10.62/2.44 % (1804004)Refutation not found, incomplete strategy % 10.62/2.44 % (1804004)------------------------------ % 10.62/2.44 % (1804004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.44 % (1804004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.44 % (1804004)CaDiCaL version: 2.1.3 % 10.62/2.44 % (1804004)Termination reason: Refutation not found, incomplete strategy % 10.62/2.44 % (1804004)Time elapsed: 0.0000 s % 10.62/2.44 % (1804004)Peak memory usage: 87 MB % 10.62/2.44 % (1804004)Instructions burned: 1 (million) % 10.62/2.44 % (1803993)------------------------------ % 10.62/2.44 % (1803993)------------------------------ % 10.62/2.44 % (1803992)------------------------------ % 10.62/2.44 % (1803992)------------------------------ % 10.62/2.44 % (1804004)------------------------------ % 10.62/2.44 % (1804004)------------------------------ % 10.62/2.44 % (1804002)------------------------------ % 10.62/2.44 % (1804002)------------------------------ % 10.62/2.44 % (1804007)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1558247488:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 10.62/2.44 % (1804008)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=2787131667:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.62/2.44 % (1804009)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=554963550:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 10.62/2.44 % (1804009)Refutation not found, incomplete strategy % 10.62/2.44 % (1804009)------------------------------ % 10.62/2.44 % (1804009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.44 % (1804009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.44 % (1804009)CaDiCaL version: 2.1.3 % 10.62/2.44 % (1804009)Termination reason: Refutation not found, incomplete strategy % 10.62/2.44 % (1804009)Time elapsed: 0.0000 s % 10.62/2.44 % (1804009)Peak memory usage: 86 MB % 10.62/2.44 % (1804007)Refutation not found, incomplete strategy % 10.62/2.44 % (1804007)------------------------------ % 10.62/2.44 % (1804007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.44 % (1804007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.44 % (1804007)CaDiCaL version: 2.1.3 % 10.62/2.44 % (1804007)Termination reason: Refutation not found, incomplete strategy % 10.62/2.44 % (1804007)Time elapsed: 0.001 s % 10.62/2.44 % (1804007)Peak memory usage: 86 MB % 10.62/2.44 % (1804010)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=273795660:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 10.62/2.44 % (1804008)Instruction limit reached! % 10.62/2.44 % (1804008)------------------------------ % 10.62/2.44 % (1804008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.44 % (1804008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.44 % (1804008)CaDiCaL version: 2.1.3 % 10.62/2.44 % (1804008)Termination reason: Instruction limit % 10.62/2.44 % (1804008)Termination phase: Saturation % 10.62/2.44 % (1804008)Time elapsed: 0.150 s % 10.62/2.44 % (1804008)Peak memory usage: 91 MB % 10.62/2.44 % (1804008)Instructions burned: 248 (million) % 10.62/2.44 % (1804009)------------------------------ % 10.62/2.44 % (1804009)------------------------------ % 10.62/2.44 % (1803991)Refutation not found, incomplete strategy % 10.62/2.44 % (1803991)------------------------------ % 10.62/2.44 % (1803991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.44 % (1803991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.44 % (1803991)CaDiCaL version: 2.1.3 % 10.62/2.44 % (1803991)Termination reason: Refutation not found, incomplete strategy % 10.62/2.44 % (1803991)Time elapsed: 0.576 s % 10.62/2.44 % (1803991)Peak memory usage: 127 MB % 10.62/2.44 % (1803991)Instructions burned: 846 (million) % 10.62/2.44 % (1804007)------------------------------ % 10.62/2.44 % (1804007)------------------------------ % 10.62/2.44 % (1804015)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4187185734:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 10.62/2.44 % (1804015)Refutation not found, incomplete strategy % 10.62/2.44 % (1804015)------------------------------ % 10.62/2.44 % (1804015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.44 % (1804015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.55/2.72 % (1804015)CaDiCaL version: 2.1.3 % 12.55/2.72 % (1804015)Termination reason: Refutation not found, incomplete strategy % 12.55/2.72 % (1804015)Time elapsed: 0.005 s % 12.55/2.72 % (1804015)Peak memory usage: 88 MB % 12.55/2.72 % (1804015)Instructions burned: 8 (million) % 12.55/2.72 % (1804016)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1627900995:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 12.55/2.72 % (1804016)Refutation not found, incomplete strategy % 12.55/2.72 % (1804016)------------------------------ % 12.55/2.72 % (1804016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.55/2.72 % (1804016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.55/2.72 % (1804016)CaDiCaL version: 2.1.3 % 12.55/2.72 % (1804016)Termination reason: Refutation not found, incomplete strategy % 12.55/2.72 % (1804016)Time elapsed: 0.003 s % 12.55/2.72 % (1804016)Peak memory usage: 87 MB % 12.55/2.72 % (1804016)Instructions burned: 5 (million) % 12.55/2.72 % (1804017)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3526974486:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 12.55/2.72 % (1803991)------------------------------ % 12.55/2.72 % (1803991)------------------------------ % 12.55/2.72 % (1804017)Instruction limit reached! % 12.55/2.72 % (1804017)------------------------------ % 12.55/2.72 % (1804017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.55/2.72 % (1804017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.55/2.72 % (1804017)CaDiCaL version: 2.1.3 % 12.55/2.72 % (1804017)Termination reason: Instruction limit % 12.55/2.72 % (1804017)Termination phase: Saturation % 12.55/2.72 % (1804017)Time elapsed: 0.067 s % 12.55/2.72 % (1804017)Peak memory usage: 89 MB % 12.55/2.72 % (1804017)Instructions burned: 114 (million) % 12.55/2.72 % (1804016)------------------------------ % 12.55/2.72 % (1804016)------------------------------ % 12.55/2.72 % (1804015)------------------------------ % 12.55/2.72 % (1804015)------------------------------ % 12.55/2.72 % (1804022)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3949958878:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 12.55/2.72 % (1804021)lrs+10_1_sil=8000:sp=occurrence:random_seed=1961356243:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 12.55/2.72 % (1804021)Refutation not found, incomplete strategy % 12.55/2.72 % (1804021)------------------------------ % 12.55/2.72 % (1804021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.55/2.72 % (1804021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.55/2.72 % (1804021)CaDiCaL version: 2.1.3 % 12.55/2.72 % (1804021)Termination reason: Refutation not found, incomplete strategy % 12.55/2.72 % (1804021)Time elapsed: 0.001 s % 12.55/2.72 % (1804021)Peak memory usage: 86 MB % 12.55/2.72 % (1804022)Refutation not found, incomplete strategy % 12.55/2.72 % (1804022)------------------------------ % 12.55/2.72 % (1804022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.55/2.72 % (1804022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.55/2.72 % (1804022)CaDiCaL version: 2.1.3 % 12.55/2.72 % (1804022)Termination reason: Refutation not found, incomplete strategy % 12.55/2.72 % (1804022)Time elapsed: 0.004 s % 12.55/2.72 % (1804022)Peak memory usage: 88 MB % 12.55/2.72 % (1804022)Instructions burned: 7 (million) % 12.55/2.72 % (1804023)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2010220039:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 12.55/2.72 % (1804024)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4204996371:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 12.55/2.72 % (1804024)Instruction limit reached! % 12.55/2.72 % (1804024)------------------------------ % 12.55/2.72 % (1804024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.55/2.72 % (1804024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.55/2.72 % (1804024)CaDiCaL version: 2.1.3 % 12.55/2.72 % (1804024)Termination reason: Instruction limit % 12.55/2.72 % (1804024)Termination phase: Saturation % 12.55/2.72 % (1804024)Time elapsed: 0.071 s % 12.55/2.72 % (1804024)Peak memory usage: 90 MB % 12.55/2.72 % (1804024)Instructions burned: 134 (million) % 12.55/2.72 % (1804021)------------------------------ % 12.55/2.72 % (1804021)------------------------------ % 12.55/2.72 % (1804022)------------------------------ % 13.18/2.88 % (1804022)------------------------------ % 13.18/2.88 % (1804029)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3633871887:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi) % 13.18/2.88 % (1804029)Refutation not found, incomplete strategy % 13.18/2.88 % (1804029)------------------------------ % 13.18/2.88 % (1804029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.18/2.88 % (1804029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.18/2.88 % (1804029)CaDiCaL version: 2.1.3 % 13.18/2.88 % (1804029)Termination reason: Refutation not found, incomplete strategy % 13.18/2.88 % (1804029)Time elapsed: 0.001 s % 13.18/2.88 % (1804029)Peak memory usage: 86 MB % 13.18/2.88 % (1804030)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4058476392:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 13.18/2.88 % (1804031)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=933956401:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 13.18/2.88 % (1804031)Refutation not found, incomplete strategy % 13.18/2.88 % (1804031)------------------------------ % 13.18/2.88 % (1804031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.18/2.88 % (1804031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.18/2.88 % (1804031)CaDiCaL version: 2.1.3 % 13.18/2.88 % (1804031)Termination reason: Refutation not found, incomplete strategy % 13.18/2.88 % (1804031)Time elapsed: 0.001 s % 13.18/2.88 % (1804031)Peak memory usage: 88 MB % 13.18/2.88 % (1804031)Instructions burned: 1 (million) % 13.18/2.88 [W927 21:39:43.425257053 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425302676 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425342316 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425353789 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425379016 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425390173 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425414723 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 13.18/2.88 [W927 21:39:43.425427193 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 [W927 21:39:43.425451746 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 [W927 21:39:43.425462333 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 [W927 21:39:43.425542106 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 [W927 21:39:43.425575243 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 % (1804029)------------------------------ % 18.32/3.57 % (1804029)------------------------------ % 18.32/3.57 % (1804031)------------------------------ % 18.32/3.57 % (1804031)------------------------------ % 18.32/3.57 % (1804023)Refutation not found, incomplete strategy % 18.32/3.57 % (1804023)------------------------------ % 18.32/3.57 % (1804023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.57 % (1804023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.57 % (1804023)CaDiCaL version: 2.1.3 % 18.32/3.57 % (1804023)Termination reason: Refutation not found, incomplete strategy % 18.32/3.57 % (1804023)Time elapsed: 0.552 s % 18.32/3.57 % (1804023)Peak memory usage: 125 MB % 18.32/3.57 % (1804023)Instructions burned: 827 (million) % 18.32/3.57 % (1804035)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1457911975:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi) % 18.32/3.57 % (1804036)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1182040261:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/141Mi) % 18.32/3.57 [W927 21:39:43.702157477 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 [W927 21:39:43.702185800 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 % (1804036)Refutation not found, incomplete strategy % 18.32/3.57 % (1804036)------------------------------ % 18.32/3.57 % (1804036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.32/3.57 [W927 21:39:43.702222477 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 % (1804036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.32/3.57 [W927 21:39:43.702234570 register_special_ops.cpp:225] Warning: Creating a tensor from 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.32/3.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.32/3.57 % (1804036)CaDiCaL version: 2.1.3 % 18.32/3.57 % (1804036)Termination reason: Refutation not found, incomplete strategy % 18.32/3.57 % (1804036)Time elapsed: 0.001 s % 18.32/3.57 [W927 21:39:43.702259180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 [W927 21:39:43.702270373 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 % (1804036)Peak memory usage: 86 MB % 29.78/5.10 [W927 21:39:43.702295280 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 [W927 21:39:43.702306217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 [W927 21:39:43.702334323 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 [W927 21:39:43.702345317 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 [W927 21:39:43.702374397 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 [W927 21:39:43.702385307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 29.78/5.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.78/5.10 % (1804035)Instruction limit reached! % 29.78/5.10 % (1804035)------------------------------ % 29.78/5.10 % (1804035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.78/5.10 % (1804035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.78/5.10 % (1804035)CaDiCaL version: 2.1.3 % 29.78/5.10 % (1804035)Termination reason: Instruction limit % 29.78/5.10 % (1804035)Termination phase: Saturation % 29.78/5.10 % (1804035)Time elapsed: 0.081 s % 29.78/5.10 % (1804035)Peak memory usage: 90 MB % 29.78/5.10 % (1804035)Instructions burned: 135 (million) % 29.78/5.10 % (1804023)------------------------------ % 29.78/5.10 % (1804023)------------------------------ % 29.78/5.10 % (1804039)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=869195413:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi) % 29.78/5.10 % (1804039)Refutation not found, incomplete strategy % 29.78/5.10 % (1804039)------------------------------ % 29.78/5.10 % (1804039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.78/5.10 % (1804039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.78/5.10 % (1804039)CaDiCaL version: 2.1.3 % 29.78/5.10 % (1804039)Termination reason: Refutation not found, incomplete strategy % 29.78/5.10 % (1804039)Time elapsed: 0.001 s % 29.78/5.10 % (1804039)Peak memory usage: 86 MB % 29.78/5.10 % (1804030)Refutation not found, incomplete strategy % 29.78/5.10 % (1804030)------------------------------ % 29.78/5.10 % (1804030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.78/5.10 % (1804030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.78/5.10 % (1804030)CaDiCaL version: 2.1.3 % 29.78/5.10 % (1804030)Termination reason: Refutation not found, incomplete strategy % 33.76/5.64 % (1804030)Time elapsed: 0.546 s % 33.76/5.64 % (1804030)Peak memory usage: 125 MB % 33.76/5.64 % (1804030)Instructions burned: 823 (million) % 33.76/5.64 % (1804010)Instruction limit reached! % 33.76/5.64 % (1804010)------------------------------ % 33.76/5.64 % (1804010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.64 % (1804010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.64 % (1804010)CaDiCaL version: 2.1.3 % 33.76/5.64 % (1804010)Termination reason: Instruction limit % 33.76/5.64 % (1804010)Termination phase: Saturation % 33.76/5.64 % (1804010)Time elapsed: 1.414 s % 33.76/5.64 % (1804010)Peak memory usage: 139 MB % 33.76/5.64 % (1804010)Instructions burned: 2352 (million) % 33.76/5.64 % (1804036)------------------------------ % 33.76/5.64 % (1804036)------------------------------ % 33.76/5.64 % (1804041)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=3333714297:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi) % 33.76/5.64 % (1804043)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1636330450:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi) % 33.76/5.64 % (1804042)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=1566334422:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2979 on theBenchmark for (2979ds/150Mi) % 33.76/5.64 % (1804039)------------------------------ % 33.76/5.64 % (1804039)------------------------------ % 33.76/5.64 % (1804030)------------------------------ % 33.76/5.64 % (1804030)------------------------------ % 33.76/5.64 % (1804042)Instruction limit reached! % 33.76/5.64 % (1804042)------------------------------ % 33.76/5.64 % (1804042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.64 % (1804042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.64 % (1804042)CaDiCaL version: 2.1.3 % 33.76/5.64 % (1804042)Termination reason: Instruction limit % 33.76/5.64 % (1804042)Termination phase: Saturation % 33.76/5.64 % (1804042)Time elapsed: 0.096 s % 33.76/5.64 % (1804042)Peak memory usage: 90 MB % 33.76/5.64 % (1804042)Instructions burned: 150 (million) % 33.76/5.64 % (1804047)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3577717789:i=667:av=off:fsr=off_2977 on theBenchmark for (2977ds/667Mi) % 33.76/5.64 % (1804047)Refutation not found, incomplete strategy % 33.76/5.64 % (1804047)------------------------------ % 33.76/5.64 % (1804047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.64 % (1804047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.64 % (1804047)CaDiCaL version: 2.1.3 % 33.76/5.64 % (1804047)Termination reason: Refutation not found, incomplete strategy % 33.76/5.64 % (1804047)Time elapsed: 0.004 s % 33.76/5.64 % (1804047)Peak memory usage: 88 MB % 33.76/5.64 % (1804047)Instructions burned: 7 (million) % 33.76/5.64 % (1804048)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=26650367:s2a=on:i=185:s2at=1.8:fdi=4_2977 on theBenchmark for (2977ds/185Mi) % 33.76/5.64 % (1804049)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1457431619:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2976 on theBenchmark for (2976ds/193Mi) % 33.76/5.64 % (1804049)Refutation not found, incomplete strategy % 33.76/5.64 % (1804049)------------------------------ % 33.76/5.64 % (1804049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.64 % (1804049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.76/5.64 % (1804049)CaDiCaL version: 2.1.3 % 33.76/5.64 % (1804049)Termination reason: Refutation not found, incomplete strategy % 33.76/5.64 % (1804049)Time elapsed: 0.001 s % 33.76/5.64 % (1804049)Peak memory usage: 86 MB % 33.76/5.64 % (1804048)Instruction limit reached! % 33.76/5.64 % (1804048)------------------------------ % 33.76/5.64 % (1804048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.76/5.64 % (1804047)------------------------------ % 33.76/5.64 % (1804047)------------------------------ % 33.76/5.64 % (1804049)------------------------------ % 33.76/5.64 % (1804049)------------------------------ % 33.76/5.64 % (1804048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/6.97 % (1804048)CaDiCaL version: 2.1.3 % 42.71/6.97 % (1804048)Termination reason: Instruction limit % 42.71/6.97 % (1804048)Termination phase: Saturation % 42.71/6.97 % (1804048)Time elapsed: 0.304 s % 42.71/6.97 % (1804048)Peak memory usage: 93 MB % 42.71/6.97 % (1804048)Instructions burned: 546 (million) % 42.71/6.97 % (1804053)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1760689650:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi) % 42.71/6.97 % (1804053)Refutation not found, incomplete strategy % 42.71/6.97 % (1804053)------------------------------ % 42.71/6.97 % (1804053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/6.97 % (1804053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/6.97 % (1804053)CaDiCaL version: 2.1.3 % 42.71/6.97 % (1804053)Termination reason: Refutation not found, incomplete strategy % 42.71/6.97 % (1804053)Time elapsed: 0.004 s % 42.71/6.97 % (1804053)Peak memory usage: 87 MB % 42.71/6.97 % (1804053)Instructions burned: 6 (million) % 42.71/6.97 % (1804054)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1815604334:i=12111:sd=1:ss=included_2973 on theBenchmark for (2973ds/12111Mi) % 42.71/6.97 % (1804055)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=703781919:i=319:kws=precedence:fsr=off_2972 on theBenchmark for (2972ds/319Mi) % 42.71/6.97 % (1804053)------------------------------ % 42.71/6.97 % (1804053)------------------------------ % 42.71/6.97 % (1804055)Instruction limit reached! % 42.71/6.97 % (1804055)------------------------------ % 42.71/6.97 % (1804055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/6.97 % (1804055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/6.97 % (1804055)CaDiCaL version: 2.1.3 % 42.71/6.97 % (1804055)Termination reason: Instruction limit % 42.71/6.97 % (1804055)Termination phase: Saturation % 42.71/6.97 % (1804055)Time elapsed: 0.195 s % 42.71/6.97 % (1804055)Peak memory usage: 93 MB % 42.71/6.97 % (1804055)Instructions burned: 320 (million) % 42.71/6.97 % (1804059)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3377011300:i=2064:ep=RST_2970 on theBenchmark for (2970ds/2064Mi) % 42.71/6.97 % (1804059)Refutation not found, incomplete strategy % 42.71/6.97 % (1804059)------------------------------ % 42.71/6.97 % (1804059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/6.97 % (1804059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/6.97 % (1804059)CaDiCaL version: 2.1.3 % 42.71/6.97 % (1804059)Termination reason: Refutation not found, incomplete strategy % 42.71/6.97 % (1804059)Time elapsed: 0.004 s % 42.71/6.97 % (1804059)Peak memory usage: 88 MB % 42.71/6.97 % (1804059)Instructions burned: 8 (million) % 42.71/6.97 % (1804060)dis-1011_128_sil=32000:random_seed=2894479144:i=3706:ep=RST:av=off_2969 on theBenchmark for (2969ds/3706Mi) % 42.71/6.97 % (1804059)------------------------------ % 42.71/6.97 % (1804059)------------------------------ % 42.71/6.97 % (1804063)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1325713822:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2966 on theBenchmark for (2966ds/757Mi) % 42.71/6.97 % (1804063)Refutation not found, incomplete strategy % 42.71/6.97 % (1804063)------------------------------ % 42.71/6.97 % (1804063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.71/6.97 % (1804063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.71/6.97 % (1804063)CaDiCaL version: 2.1.3 % 42.71/6.97 % (1804063)Termination reason: Refutation not found, incomplete strategy % 42.71/6.97 % (1804063)Time elapsed: 0.001 s % 42.71/6.97 % (1804063)Peak memory usage: 86 MB % 42.71/6.97 % (1804063)------------------------------ % 42.71/6.97 % (1804063)------------------------------ % 42.71/6.97 % (1804065)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=754628000:i=13913:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/13913Mi) % 42.71/6.97 [W927 21:39:45.084968501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 42.71/6.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.71/6.97 [W927 21:39:45.085021701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085060074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085072121 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085096984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085117974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085143917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085155174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085179628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085190744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085215091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 [W927 21:39:45.085226311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 45.81/7.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 45.81/7.34 % (1804065)Refutation not found, incomplete strategy % 45.81/7.34 % (1804065)------------------------------ % 45.81/7.34 % (1804065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 45.81/7.34 % (1804065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 45.81/7.34 % (1804065)CaDiCaL version: 2.1.3 % 45.81/7.34 % (1804065)Termination reason: Refutation not found, incomplete strategy % 45.81/7.34 % (1804065)Time elapsed: 0.540 s % 45.81/7.34 % (1804065)Peak memory usage: 125 MB % 45.81/7.34 % (1804065)Instructions burned: 825 (million) % 45.81/7.34 % (1804065)------------------------------ % 45.81/7.34 % (1804065)------------------------------ % 45.81/7.34 % (1804067)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2607655521:i=9925:aac=none_2953 on theBenchmark for (2953ds/9925Mi) % 69.67/10.85 % (1804067)Refutation not found, incomplete strategy % 69.67/10.85 % (1804067)------------------------------ % 69.67/10.85 % (1804067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.67/10.85 % (1804067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.67/10.85 % (1804067)CaDiCaL version: 2.1.3 % 69.67/10.85 % (1804067)Termination reason: Refutation not found, incomplete strategy % 69.67/10.85 % (1804067)Time elapsed: 0.566 s % 69.67/10.85 % (1804067)Peak memory usage: 128 MB % 69.67/10.85 % (1804067)Instructions burned: 841 (million) % 69.67/10.85 % (1804060)Instruction limit reached! % 69.67/10.85 % (1804060)------------------------------ % 69.67/10.85 % (1804060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.67/10.85 % (1804060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.67/10.85 % (1804060)CaDiCaL version: 2.1.3 % 69.67/10.85 % (1804060)Termination reason: Instruction limit % 69.67/10.85 % (1804060)Termination phase: Saturation % 69.67/10.85 % (1804060)Time elapsed: 2.378 s % 69.67/10.85 % (1804060)Peak memory usage: 114 MB % 69.67/10.85 % (1804060)Instructions burned: 3707 (million) % 69.67/10.85 % (1804067)------------------------------ % 69.67/10.85 % (1804067)------------------------------ % 69.67/10.85 % (1804069)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3910179036:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2944 on theBenchmark for (2944ds/2479Mi) % 69.67/10.85 % (1804069)Refutation not found, incomplete strategy % 69.67/10.85 % (1804069)------------------------------ % 69.67/10.85 % (1804069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.67/10.85 % (1804069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.67/10.85 % (1804069)CaDiCaL version: 2.1.3 % 69.67/10.85 % (1804069)Termination reason: Refutation not found, incomplete strategy % 69.67/10.85 % (1804069)Time elapsed: 0.001 s % 69.67/10.85 % (1804069)Peak memory usage: 86 MB % 69.67/10.85 % (1804070)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2247427064:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2944 on theBenchmark for (2944ds/440Mi) % 69.67/10.85 % (1804041)Instruction limit reached! % 69.67/10.85 % (1804041)------------------------------ % 69.67/10.85 % (1804041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.67/10.85 % (1804041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.67/10.85 % (1804041)CaDiCaL version: 2.1.3 % 69.67/10.85 % (1804041)Termination reason: Instruction limit % 69.67/10.85 % (1804041)Termination phase: Saturation % 69.67/10.85 % (1804041)Time elapsed: 3.692 s % 69.67/10.85 % (1804041)Peak memory usage: 177 MB % 69.67/10.85 % (1804041)Instructions burned: 6060 (million) % 69.67/10.85 % (1804069)------------------------------ % 69.67/10.85 % (1804069)------------------------------ % 69.67/10.85 % (1804070)Instruction limit reached! % 69.67/10.85 % (1804070)------------------------------ % 69.67/10.85 % (1804070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.67/10.85 % (1804070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.67/10.85 % (1804070)CaDiCaL version: 2.1.3 % 69.67/10.85 % (1804070)Termination reason: Instruction limit % 69.67/10.85 % (1804070)Termination phase: Saturation % 69.67/10.85 % (1804070)Time elapsed: 0.242 s % 69.67/10.85 % (1804070)Peak memory usage: 93 MB % 69.67/10.85 % (1804070)Instructions burned: 441 (million) % 69.67/10.85 % (1804073)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1969832052:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2941 on theBenchmark for (2941ds/11145Mi) % 69.67/10.85 % (1804074)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=2801026493:cts=off:i=3034:av=off:er=known:fsd=on_2940 on theBenchmark for (2940ds/3034Mi) % 69.67/10.85 % (1804076)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2023206875:st=2:s2a=on:i=524:s2at=2:ss=axioms_2940 on theBenchmark for (2940ds/524Mi) % 69.67/10.85 % (1804076)Refutation not found, incomplete strategy % 69.67/10.85 % (1804076)------------------------------ % 69.67/10.85 % (1804076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.67/10.85 % (1804076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.67/10.85 % (1804076)CaDiCaL version: 2.1.3 % 69.67/10.85 % (1804076)Termination reason: Refutation not found, incomplete strategy % 70.16/10.95 % (1804076)Time elapsed: 0.001 s % 70.16/10.95 % (1804076)Peak memory usage: 87 MB % 70.16/10.95 % (1804076)Instructions burned: 1 (million) % 70.16/10.95 % (1804076)------------------------------ % 70.16/10.95 % (1804076)------------------------------ % 70.16/10.95 [W927 21:39:47.196569806 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196599753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196636893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196650059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196674543 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196686419 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196710306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196721809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196745803 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196758079 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196782183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 [W927 21:39:47.196794426 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.16/10.95 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.16/10.95 % (1804079)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=717284793:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2936 on theBenchmark for (2936ds/1016Mi) % 74.66/11.45 % (1804079)Refutation not found, incomplete strategy % 74.66/11.45 % (1804079)------------------------------ % 74.66/11.45 % (1804079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.45 % (1804079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.66/11.45 % (1804079)CaDiCaL version: 2.1.3 % 74.66/11.45 % (1804079)Termination reason: Refutation not found, incomplete strategy % 74.66/11.45 % (1804079)Time elapsed: 0.001 s % 74.66/11.45 % (1804079)Peak memory usage: 87 MB % 74.66/11.45 % (1804073)Refutation not found, incomplete strategy % 74.66/11.45 % (1804073)------------------------------ % 74.66/11.45 % (1804073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.45 % (1804073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.66/11.45 % (1804073)CaDiCaL version: 2.1.3 % 74.66/11.45 % (1804073)Termination reason: Refutation not found, incomplete strategy % 74.66/11.45 % (1804073)Time elapsed: 0.545 s % 74.66/11.45 % (1804073)Peak memory usage: 125 MB % 74.66/11.45 % (1804073)Instructions burned: 826 (million) % 74.66/11.45 % (1804079)------------------------------ % 74.66/11.45 % (1804079)------------------------------ % 74.66/11.45 % (1804073)------------------------------ % 74.66/11.45 % (1804073)------------------------------ % 74.66/11.45 % (1804081)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2458598526:i=14123:bd=preordered:ins=4_2932 on theBenchmark for (2932ds/14123Mi) % 74.66/11.45 % (1804082)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3050015004:i=5781:kws=precedence:bd=all:rawr=on_2932 on theBenchmark for (2932ds/5781Mi) % 74.66/11.45 % (1804074)Instruction limit reached! % 74.66/11.45 % (1804074)------------------------------ % 74.66/11.45 % (1804074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.45 % (1804074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.66/11.45 % (1804074)CaDiCaL version: 2.1.3 % 74.66/11.45 % (1804074)Termination reason: Instruction limit % 74.66/11.45 % (1804074)Termination phase: Saturation % 74.66/11.45 % (1804074)Time elapsed: 1.783 s % 74.66/11.45 % (1804074)Peak memory usage: 140 MB % 74.66/11.45 % (1804074)Instructions burned: 3035 (million) % 74.66/11.45 % (1804085)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=2957318678:i=2448:gtgl=5:bd=preordered:gtg=all_2921 on theBenchmark for (2921ds/2448Mi) % 74.66/11.45 % (1804085)Instruction limit reached! % 74.66/11.45 % (1804085)------------------------------ % 74.66/11.45 % (1804085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.45 % (1804085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.66/11.45 % (1804085)CaDiCaL version: 2.1.3 % 74.66/11.45 % (1804085)Termination reason: Instruction limit % 74.66/11.45 % (1804085)Termination phase: Saturation % 74.66/11.45 % (1804085)Time elapsed: 1.334 s % 74.66/11.45 % (1804085)Peak memory usage: 140 MB % 74.66/11.45 % (1804085)Instructions burned: 2449 (million) % 74.66/11.45 % (1804087)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2747118126:i=3223:kws=precedence:fgj=on:av=off_2906 on theBenchmark for (2906ds/3223Mi) % 74.66/11.45 % (1804054)Instruction limit reached! % 74.66/11.45 % (1804054)------------------------------ % 74.66/11.45 % (1804054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.45 % (1804054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.66/11.45 % (1804054)CaDiCaL version: 2.1.3 % 74.66/11.45 % (1804054)Termination reason: Instruction limit % 74.66/11.45 % (1804054)Termination phase: Saturation % 74.66/11.45 % (1804054)Time elapsed: 6.636 s % 74.66/11.45 % (1804054)Peak memory usage: 165 MB % 74.66/11.45 % (1804054)Instructions burned: 12112 (million) % 74.66/11.45 % (1804089)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=20184803:st=5.6:i=2033:sd=3:ss=axioms_2905 on theBenchmark for (2905ds/2033Mi) % 74.66/11.45 [W927 21:39:51.833607028 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.45 [W927 21:39:51.833640581 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833678728 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833690481 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833715915 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833726835 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833751721 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833762651 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833786738 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833797778 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833823471 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 [W927 21:39:51.833834431 register_special_ops.cpp:225] Warning: Creating a tensor from 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.66/11.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.66/11.47 % (1804082)Instruction limit reached! % 74.66/11.47 % (1804082)------------------------------ % 74.66/11.47 % (1804082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.47 % (1804082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.66/11.47 % (1804082)CaDiCaL version: 2.1.3 % 74.66/11.47 % (1804082)Termination reason: Instruction limit % 74.66/11.47 % (1804082)Termination phase: Saturation % 74.66/11.47 % (1804082)Time elapsed: 3.160 s % 74.66/11.47 % (1804082)Peak memory usage: 111 MB % 74.66/11.47 % (1804082)Instructions burned: 5782 (million) % 74.66/11.47 % (1804043)Instruction limit reached! % 74.66/11.47 % (1804043)------------------------------ % 74.66/11.47 % (1804043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.66/11.47 % (1804043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.81/12.91 % (1804043)CaDiCaL version: 2.1.3 % 81.81/12.91 % (1804043)Termination reason: Instruction limit % 81.81/12.91 % (1804043)Termination phase: Saturation % 81.81/12.91 % (1804043)Time elapsed: 7.856 s % 81.81/12.91 % (1804043)Peak memory usage: 187 MB % 81.81/12.91 % (1804043)Instructions burned: 14156 (million) % 81.81/12.91 % (1804089)Refutation not found, incomplete strategy % 81.81/12.91 % (1804089)------------------------------ % 81.81/12.91 % (1804089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 81.81/12.91 % (1804089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 81.81/12.91 % (1804089)CaDiCaL version: 2.1.3 % 81.81/12.91 % (1804089)Termination reason: Refutation not found, incomplete strategy % 81.81/12.91 % (1804089)Time elapsed: 0.547 s % 81.81/12.91 % (1804089)Peak memory usage: 125 MB % 81.81/12.91 % (1804089)Instructions burned: 821 (million) % 81.81/12.91 % (1804091)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3114805584:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2899 on theBenchmark for (2899ds/2055Mi) % 81.81/12.91 % (1804092)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=5477277:i=21611:sd=3:ss=axioms_2899 on theBenchmark for (2899ds/21611Mi) % 81.81/12.91 [W927 21:39:52.436849863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.436891789 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.436929116 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.436940589 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.436964609 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.436975393 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.436999826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.437078733 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.437107633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 81.81/12.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 81.81/12.91 [W927 21:39:52.437119543 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.437145496 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.437155720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453797902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453840672 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453878422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453895219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453919409 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453930809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453956022 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453967139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.453992919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.454014272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.04/14.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.04/14.22 [W927 21:39:52.454041555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.04/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.04/15.05 [W927 21:39:52.454053112 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 97.04/15.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 97.04/15.05 % (1804089)------------------------------ % 97.04/15.05 % (1804089)------------------------------ % 97.04/15.05 % (1804092)Refutation not found, incomplete strategy % 97.04/15.05 % (1804092)------------------------------ % 97.04/15.05 % (1804092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.04/15.05 % (1804092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.04/15.05 % (1804092)CaDiCaL version: 2.1.3 % 97.04/15.05 % (1804092)Termination reason: Refutation not found, incomplete strategy % 97.04/15.05 % (1804092)Time elapsed: 0.635 s % 97.04/15.05 % (1804092)Peak memory usage: 125 MB % 97.04/15.05 % (1804092)Instructions burned: 821 (million) % 97.04/15.05 % (1804091)Refutation not found, incomplete strategy % 97.04/15.05 % (1804091)------------------------------ % 97.04/15.05 % (1804091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.04/15.05 % (1804091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.04/15.05 % (1804091)CaDiCaL version: 2.1.3 % 97.04/15.05 % (1804091)Termination reason: Refutation not found, incomplete strategy % 97.04/15.05 % (1804091)Time elapsed: 0.666 s % 97.04/15.05 % (1804091)Peak memory usage: 126 MB % 97.04/15.05 % (1804091)Instructions burned: 826 (million) % 97.04/15.05 % (1804091)------------------------------ % 97.04/15.05 % (1804091)------------------------------ % 97.04/15.05 % (1804092)------------------------------ % 97.04/15.05 % (1804092)------------------------------ % 97.04/15.05 % (1804087)Instruction limit reached! % 97.04/15.05 % (1804087)------------------------------ % 97.04/15.05 % (1804087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.04/15.05 % (1804087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.04/15.05 % (1804087)CaDiCaL version: 2.1.3 % 97.04/15.05 % (1804087)Termination reason: Instruction limit % 97.04/15.05 % (1804087)Termination phase: Saturation % 97.04/15.05 % (1804087)Time elapsed: 1.930 s % 97.04/15.05 % (1804087)Peak memory usage: 142 MB % 97.04/15.05 % (1804087)Instructions burned: 3224 (million) % 97.04/15.05 % (1804095)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2222204681:i=4835:sd=13:ss=axioms:sgt=23_2892 on theBenchmark for (2892ds/4835Mi) % 97.04/15.05 % (1804095)Refutation not found, incomplete strategy % 97.04/15.05 % (1804095)------------------------------ % 97.04/15.05 % (1804095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.04/15.05 % (1804095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.04/15.05 % (1804095)CaDiCaL version: 2.1.3 % 97.04/15.05 % (1804095)Termination reason: Refutation not found, incomplete strategy % 97.04/15.05 % (1804095)Time elapsed: 0.001 s % 97.04/15.05 % (1804095)Peak memory usage: 86 MB % 97.04/15.05 % (1804096)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=3225940001:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2888 on theBenchmark for (2888ds/797Mi) % 97.04/15.05 % (1804097)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2089716323:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2888 on theBenchmark for (2888ds/2326Mi) % 97.04/15.05 % (1804098)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4136968412:i=6038:nm=6_2886 on theBenchmark for (2886ds/6038Mi) % 97.04/15.05 % (1804097)Refutation not found, incomplete strategy % 97.04/15.05 % (1804097)------------------------------ % 97.04/15.05 % (1804097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 97.04/15.05 % (1804097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 97.04/15.05 % (1804097)CaDiCaL version: 2.1.3 % 97.04/15.05 % (1804097)Termination reason: Refutation not found, incomplete strategy % 97.04/15.05 % (1804097)Time elapsed: 0.006 s % 113.86/17.41 % (1804097)Peak memory usage: 88 MB % 113.86/17.41 % (1804097)Instructions burned: 10 (million) % 113.86/17.41 % (1804095)------------------------------ % 113.86/17.41 % (1804095)------------------------------ % 113.86/17.41 % (1804103)lrs+10_1_sil=32000:sp=occurrence:random_seed=793334676:st=2:i=33334:sd=3:ss=included:sgt=32_2878 on theBenchmark for (2878ds/33334Mi) % 113.86/17.41 % (1804097)------------------------------ % 113.86/17.41 % (1804097)------------------------------ % 113.86/17.41 % (1804105)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=417741005:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2877 on theBenchmark for (2877ds/1008Mi) % 113.86/17.41 % (1804105)Refutation not found, incomplete strategy % 113.86/17.41 % (1804105)------------------------------ % 113.86/17.41 % (1804105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.86/17.41 % (1804105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.86/17.41 % (1804105)CaDiCaL version: 2.1.3 % 113.86/17.41 % (1804105)Termination reason: Refutation not found, incomplete strategy % 113.86/17.41 % (1804105)Time elapsed: 0.001 s % 113.86/17.41 % (1804105)Peak memory usage: 86 MB % 113.86/17.41 % (1804096)Instruction limit reached! % 113.86/17.41 % (1804096)------------------------------ % 113.86/17.41 % (1804096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.86/17.41 % (1804096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.86/17.41 % (1804096)CaDiCaL version: 2.1.3 % 113.86/17.41 % (1804096)Termination reason: Instruction limit % 113.86/17.41 % (1804096)Termination phase: Saturation % 113.86/17.41 % (1804096)Time elapsed: 0.428 s % 113.86/17.41 % (1804096)Peak memory usage: 97 MB % 113.86/17.41 % (1804096)Instructions burned: 797 (million) % 113.86/17.41 % (1804107)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=871396342:i=8327:s2at=5:bd=preordered_2875 on theBenchmark for (2875ds/8327Mi) % 113.86/17.41 % (1804098)Refutation not found, incomplete strategy % 113.86/17.41 % (1804098)------------------------------ % 113.86/17.41 % (1804098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.86/17.41 % (1804098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.86/17.41 % (1804098)CaDiCaL version: 2.1.3 % 113.86/17.41 % (1804098)Termination reason: Refutation not found, incomplete strategy % 113.86/17.41 % (1804098)Time elapsed: 0.559 s % 113.86/17.41 % (1804098)Peak memory usage: 128 MB % 113.86/17.41 % (1804098)Instructions burned: 842 (million) % 113.86/17.41 % (1804105)------------------------------ % 113.86/17.41 % (1804105)------------------------------ % 113.86/17.41 % (1804109)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=765816523:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2873 on theBenchmark for (2873ds/1083Mi) % 113.86/17.41 % (1804098)------------------------------ % 113.86/17.41 % (1804098)------------------------------ % 113.86/17.41 % (1804111)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1034779700:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2871 on theBenchmark for (2871ds/1084Mi) % 113.86/17.41 % (1804111)Refutation not found, incomplete strategy % 113.86/17.41 % (1804111)------------------------------ % 113.86/17.41 % (1804111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.86/17.41 % (1804111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.86/17.41 % (1804111)CaDiCaL version: 2.1.3 % 113.86/17.41 % (1804111)Termination reason: Refutation not found, incomplete strategy % 113.86/17.41 % (1804111)Time elapsed: 0.001 s % 113.86/17.41 % (1804111)Peak memory usage: 86 MB % 113.86/17.41 % (1804111)------------------------------ % 113.86/17.41 % (1804111)------------------------------ % 113.86/17.41 % (1804109)Instruction limit reached! % 113.86/17.41 % (1804109)------------------------------ % 113.86/17.41 % (1804109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.86/17.41 % (1804109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.86/17.41 % (1804109)CaDiCaL version: 2.1.3 % 113.86/17.41 % (1804109)Termination reason: Instruction limit % 113.86/17.41 % (1804109)Termination phase: Saturation % 113.86/17.41 % (1804109)Time elapsed: 0.515 s % 113.86/17.41 % (1804109)Peak memory usage: 99 MB % 113.86/17.41 % (1804109)Instructions burned: 1085 (million) % 113.86/17.41 % (1804113)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=209177606:i=6995:s2at=5:gtg=all_2867 on theBenchmark for (2867ds/6995Mi) % 118.36/18.11 % (1804114)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1964997990:st=2:i=6225:sd=15:ss=axioms_2867 on theBenchmark for (2867ds/6225Mi) % 118.36/18.11 % (1804114)Refutation not found, incomplete strategy % 118.36/18.11 % (1804114)------------------------------ % 118.36/18.11 % (1804114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.36/18.11 % (1804114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.36/18.11 % (1804114)CaDiCaL version: 2.1.3 % 118.36/18.11 % (1804114)Termination reason: Refutation not found, incomplete strategy % 118.36/18.11 % (1804114)Time elapsed: 0.001 s % 118.36/18.11 % (1804114)Peak memory usage: 86 MB % 118.36/18.11 % (1804114)------------------------------ % 118.36/18.11 % (1804114)------------------------------ % 118.36/18.11 % (1804117)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=145254128:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2863 on theBenchmark for (2863ds/3372Mi) % 118.36/18.11 [W927 21:39:55.035934865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.035967669 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036014899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036028635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036056172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036067822 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036093572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036105032 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036130672 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.36/18.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.36/18.11 [W927 21:39:55.036142089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.67/18.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.67/18.50 [W927 21:39:55.036166802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.67/18.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.67/18.50 [W927 21:39:55.036177366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.67/18.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.67/18.50 % (1804117)Refutation not found, incomplete strategy % 120.67/18.50 % (1804117)------------------------------ % 120.67/18.50 % (1804117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.67/18.50 % (1804117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.67/18.50 % (1804117)CaDiCaL version: 2.1.3 % 120.67/18.50 % (1804117)Termination reason: Refutation not found, incomplete strategy % 120.67/18.50 % (1804117)Time elapsed: 0.545 s % 120.67/18.50 % (1804117)Peak memory usage: 126 MB % 120.67/18.50 % (1804117)Instructions burned: 822 (million) % 120.67/18.50 % (1804117)------------------------------ % 120.67/18.50 % (1804117)------------------------------ % 120.67/18.50 % (1804119)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3493962481:st=2.3:i=26457:sd=10:ss=included:sgt=8_2854 on theBenchmark for (2854ds/26457Mi) % 120.67/18.50 % (1804119)Refutation not found, incomplete strategy % 120.67/18.50 % (1804119)------------------------------ % 120.67/18.50 % (1804119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.67/18.50 % (1804119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.67/18.50 % (1804119)CaDiCaL version: 2.1.3 % 120.67/18.50 % (1804119)Termination reason: Refutation not found, incomplete strategy % 120.67/18.50 % (1804119)Time elapsed: 0.560 s % 120.67/18.50 % (1804119)Peak memory usage: 127 MB % 120.67/18.50 % (1804119)Instructions burned: 845 (million) % 120.67/18.50 % (1804119)------------------------------ % 120.67/18.50 % (1804119)------------------------------ % 120.67/18.50 % (1804121)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=482892243:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2844 on theBenchmark for (2844ds/13494Mi) % 120.67/18.50 % (1804081)Instruction limit reached! % 120.67/18.50 % (1804081)------------------------------ % 120.67/18.50 % (1804081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 120.67/18.50 % (1804081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 120.67/18.50 % (1804081)CaDiCaL version: 2.1.3 % 120.67/18.50 % (1804081)Termination reason: Instruction limit % 120.67/18.50 % (1804081)Termination phase: Saturation % 120.67/18.50 % (1804081)Time elapsed: 9.179 s % 120.67/18.50 % (1804081)Peak memory usage: 205 MB % 120.67/18.50 % (1804081)Instructions burned: 14124 (million) % 120.67/18.50 % (1804123)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=3963219518:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2839 on theBenchmark for (2839ds/2503Mi) % 120.67/18.50 [W927 21:39:58.394929640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.67/18.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.67/18.50 [W927 21:39:58.394962657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.67/18.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.67/18.50 [W927 21:39:58.394999297 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 120.67/18.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 120.67/18.50 [W927 21:39:58.395024587 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395051437 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395063060 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395087610 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395098130 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395121484 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395131890 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395155280 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 [W927 21:39:58.395166310 register_special_ops.cpp:225] Warning: Creating a tensor from 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.28/20.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.28/20.19 % (1804123)Refutation not found, incomplete strategy % 133.28/20.19 % (1804123)------------------------------ % 133.28/20.19 % (1804123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.28/20.19 % (1804123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.28/20.19 % (1804123)CaDiCaL version: 2.1.3 % 133.28/20.19 % (1804123)Termination reason: Refutation not found, incomplete strategy % 133.28/20.19 % (1804123)Time elapsed: 0.541 s % 133.28/20.19 % (1804123)Peak memory usage: 125 MB % 133.28/20.19 % (1804123)Instructions burned: 825 (million) % 133.28/20.19 % (1804123)------------------------------ % 133.28/20.19 % (1804123)------------------------------ % 133.28/20.19 % (1804125)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1955857459:i=2559:sd=1:ep=RSTC:ss=axioms_2830 on theBenchmark for (2830ds/2559Mi) % 133.28/20.19 % (1804107)Instruction limit reached! % 133.28/20.19 % (1804107)------------------------------ % 133.28/20.19 % (1804107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 133.28/20.19 % (1804107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 133.28/20.19 % (1804107)CaDiCaL version: 2.1.3 % 133.28/20.19 % (1804107)Termination reason: Instruction limit % 133.28/20.19 % (1804107)Termination phase: Saturation % 133.28/20.19 % (1804107)Time elapsed: 4.656 s % 133.28/20.19 % (1804107)Peak memory usage: 169 MB % 133.28/20.19 % (1804107)Instructions burned: 8327 (million) % 139.63/21.12 % (1804127)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=139269440:i=30753:av=off:ss=included_2827 on theBenchmark for (2827ds/30753Mi) % 139.63/21.12 [W927 21:39:58.320065195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320098922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320137165 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320149702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320175438 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320186668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320212925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320224182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320249748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320261002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320286492 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 [W927 21:39:58.320297605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.63/21.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.63/21.12 % (1804125)Refutation not found, incomplete strategy % 139.63/21.12 % (1804125)------------------------------ % 139.63/21.12 % (1804125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.73/22.04 % (1804125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.73/22.04 % (1804125)CaDiCaL version: 2.1.3 % 146.73/22.04 % (1804125)Termination reason: Refutation not found, incomplete strategy % 146.73/22.04 % (1804125)Time elapsed: 0.540 s % 146.73/22.04 % (1804125)Peak memory usage: 125 MB % 146.73/22.04 % (1804125)Instructions burned: 822 (million) % 146.73/22.04 % (1804113)Instruction limit reached! % 146.73/22.04 % (1804113)------------------------------ % 146.73/22.04 % (1804113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.73/22.04 % (1804113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.73/22.04 % (1804113)CaDiCaL version: 2.1.3 % 146.73/22.04 % (1804113)Termination reason: Instruction limit % 146.73/22.04 % (1804113)Termination phase: Saturation % 146.73/22.04 % (1804113)Time elapsed: 4.289 s % 146.73/22.04 % (1804113)Peak memory usage: 166 MB % 146.73/22.04 % (1804113)Instructions burned: 6996 (million) % 146.73/22.04 % (1804129)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2858232482:i=26473:ep=RSTC_2823 on theBenchmark for (2823ds/26473Mi) % 146.73/22.05 % (1804125)------------------------------ % 146.73/22.05 % (1804125)------------------------------ % 146.73/22.05 % (1804131)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=3818975672:cts=off:i=2759:kws=inv_arity:fgj=on_2821 on theBenchmark for (2821ds/2759Mi) % 146.73/22.05 % (1804131)Refutation not found, incomplete strategy % 146.73/22.05 % (1804131)------------------------------ % 146.73/22.05 % (1804131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.73/22.05 % (1804131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.73/22.05 % (1804131)CaDiCaL version: 2.1.3 % 146.73/22.05 % (1804131)Termination reason: Refutation not found, incomplete strategy % 146.73/22.05 % (1804131)Time elapsed: 0.557 s % 146.73/22.05 % (1804131)Peak memory usage: 128 MB % 146.73/22.05 % (1804131)Instructions burned: 849 (million) % 146.73/22.05 % (1804131)------------------------------ % 146.73/22.05 % (1804131)------------------------------ % 146.73/22.05 % (1804133)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=4099306540:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2811 on theBenchmark for (2811ds/5665Mi) % 146.73/22.05 [W927 21:40:00.175305452 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.73/22.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.73/22.05 [W927 21:40:00.175338722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.73/22.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.73/22.05 [W927 21:40:00.175374089 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.73/22.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.73/22.05 [W927 21:40:00.175387025 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.73/22.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.73/22.05 [W927 21:40:00.175413252 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.73/22.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.73/22.05 [W927 21:40:00.175425662 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.73/22.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:00.175451959 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:00.175462849 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:00.175486616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:00.175497389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:00.175521289 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:00.175532012 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 % (1804133)Refutation not found, incomplete strategy % 157.84/23.64 % (1804133)------------------------------ % 157.84/23.64 % (1804133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 157.84/23.64 % (1804133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.84/23.64 % (1804133)CaDiCaL version: 2.1.3 % 157.84/23.64 % (1804133)Termination reason: Refutation not found, incomplete strategy % 157.84/23.64 % (1804133)Time elapsed: 0.542 s % 157.84/23.64 % (1804133)Peak memory usage: 125 MB % 157.84/23.64 % (1804133)Instructions burned: 825 (million) % 157.84/23.64 % (1804133)------------------------------ % 157.84/23.64 % (1804133)------------------------------ % 157.84/23.64 % (1804135)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=2376790011:i=1532:ep=RS:ss=axioms_2802 on theBenchmark for (2802ds/1532Mi) % 157.84/23.64 [W927 21:40:01.105132388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:01.105165441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:01.105202514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:01.105225261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 157.84/23.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 157.84/23.64 [W927 21:40:01.105256024 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105267221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105291398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105302381 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105336075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105346961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105370365 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:01.105381325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 % (1804135)Refutation not found, incomplete strategy % 162.88/24.31 % (1804135)------------------------------ % 162.88/24.31 % (1804135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 162.88/24.31 % (1804135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 162.88/24.31 % (1804135)CaDiCaL version: 2.1.3 % 162.88/24.31 % (1804135)Termination reason: Refutation not found, incomplete strategy % 162.88/24.31 % (1804135)Time elapsed: 0.547 s % 162.88/24.31 % (1804135)Peak memory usage: 125 MB % 162.88/24.31 % (1804135)Instructions burned: 826 (million) % 162.88/24.31 % (1804135)------------------------------ % 162.88/24.31 % (1804135)------------------------------ % 162.88/24.31 % (1804137)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1588205410:i=1565:sd=2:ss=axioms:sgt=32_2793 on theBenchmark for (2793ds/1565Mi) % 162.88/24.31 [W927 21:40:02.031538107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:02.031582127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 162.88/24.31 [W927 21:40:02.031618214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 162.88/24.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031629394 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031653474 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031675727 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031701234 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031712274 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031735817 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031746064 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031769454 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 [W927 21:40:02.031779620 register_special_ops.cpp:225] Warning: Creating a tensor from 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.01/25.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 168.01/25.08 % (1804137)Refutation not found, incomplete strategy % 168.01/25.08 % (1804137)------------------------------ % 168.01/25.08 % (1804137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.01/25.08 % (1804137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.01/25.08 % (1804137)CaDiCaL version: 2.1.3 % 168.01/25.08 % (1804137)Termination reason: Refutation not found, incomplete strategy % 168.01/25.08 % (1804137)Time elapsed: 0.551 s % 168.01/25.08 % (1804137)Peak memory usage: 125 MB % 168.01/25.08 % (1804137)Instructions burned: 825 (million) % 168.01/25.08 % (1804137)------------------------------ % 168.01/25.08 % (1804137)------------------------------ % 168.01/25.08 % (1804139)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=2599796102:i=1572:fgj=on:gsp=on_2784 on theBenchmark for (2784ds/1572Mi) % 168.01/25.08 % (1804139)Instruction limit reached! % 168.01/25.08 % (1804139)------------------------------ % 168.01/25.08 % (1804139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 168.01/25.08 % (1804139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 168.01/25.08 % (1804139)CaDiCaL version: 2.1.3 % 168.01/25.08 % (1804139)Termination reason: Instruction limit % 168.01/25.08 % (1804139)Termination phase: Saturation % 168.01/25.08 % (1804139)Time elapsed: 1.047 s % 173.27/26.02 % (1804139)Peak memory usage: 134 MB % 173.27/26.02 % (1804139)Instructions burned: 1572 (million) % 173.27/26.02 % (1804141)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1838645758:i=6052:sd=4:ss=axioms:sgt=24_2772 on theBenchmark for (2772ds/6052Mi) % 173.27/26.02 [W927 21:40:04.134195990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134242550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134282117 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134294044 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134319800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134330504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134355037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134368777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134392884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134405324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134430874 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 [W927 21:40:04.134443717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 173.27/26.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 173.27/26.02 % (1804141)Refutation not found, incomplete strategy % 210.63/31.05 % (1804141)------------------------------ % 210.63/31.05 % (1804141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/31.05 % (1804141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/31.05 % (1804141)CaDiCaL version: 2.1.3 % 210.63/31.05 % (1804141)Termination reason: Refutation not found, incomplete strategy % 210.63/31.05 % (1804141)Time elapsed: 0.540 s % 210.63/31.05 % (1804141)Peak memory usage: 125 MB % 210.63/31.05 % (1804141)Instructions burned: 821 (million) % 210.63/31.05 % (1804121)Instruction limit reached! % 210.63/31.05 % (1804121)------------------------------ % 210.63/31.05 % (1804121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 210.63/31.05 % (1804121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 210.63/31.05 % (1804121)CaDiCaL version: 2.1.3 % 210.63/31.05 % (1804121)Termination reason: Instruction limit % 210.63/31.05 % (1804121)Termination phase: Saturation % 210.63/31.05 % (1804121)Time elapsed: 7.850 s % 210.63/31.05 % (1804121)Peak memory usage: 190 MB % 210.63/31.05 % (1804121)Instructions burned: 13495 (million) % 210.63/31.05 % (1804143)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=105675494:i=3500:sd=1:bd=preordered:sup=off:ss=included_2764 on theBenchmark for (2764ds/3500Mi) % 210.63/31.05 % (1804141)------------------------------ % 210.63/31.05 % (1804141)------------------------------ % 210.63/31.05 % (1804145)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=3494193127:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2763 on theBenchmark for (2763ds/1842Mi) % 210.63/31.05 [W927 21:40:05.069150547 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069186288 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069225198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069239284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069265891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069278171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069305278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 210.63/31.05 [W927 21:40:05.069317624 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 210.63/31.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:05.069343454 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:05.069401874 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:05.069437481 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:05.069449258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 % (1804143)Refutation not found, incomplete strategy % 213.52/31.56 % (1804143)------------------------------ % 213.52/31.56 % (1804143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.52/31.56 % (1804143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.52/31.56 % (1804143)CaDiCaL version: 2.1.3 % 213.52/31.56 % (1804143)Termination reason: Refutation not found, incomplete strategy % 213.52/31.56 % (1804143)Time elapsed: 0.563 s % 213.52/31.56 % (1804143)Peak memory usage: 128 MB % 213.52/31.56 % (1804143)Instructions burned: 845 (million) % 213.52/31.56 % (1804145)Refutation not found, incomplete strategy % 213.52/31.56 % (1804145)------------------------------ % 213.52/31.56 % (1804145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 213.52/31.56 % (1804145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 213.52/31.56 % (1804145)CaDiCaL version: 2.1.3 % 213.52/31.56 % (1804145)Termination reason: Refutation not found, incomplete strategy % 213.52/31.56 % (1804145)Time elapsed: 0.551 s % 213.52/31.56 % (1804145)Peak memory usage: 125 MB % 213.52/31.56 % (1804145)Instructions burned: 823 (million) % 213.52/31.56 % (1804143)------------------------------ % 213.52/31.56 % (1804143)------------------------------ % 213.52/31.56 % (1804147)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3995180502:i=66096:add=on_2755 on theBenchmark for (2755ds/66096Mi) % 213.52/31.56 % (1804145)------------------------------ % 213.52/31.56 % (1804145)------------------------------ % 213.52/31.56 % (1804149)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2414583290:i=1884:sd=1:nm=60:ss=axioms_2753 on theBenchmark for (2753ds/1884Mi) % 213.52/31.56 [W927 21:40:06.998689113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:06.998730563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:06.998768466 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:06.998780620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 213.52/31.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 213.52/31.56 [W927 21:40:06.998810023 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998821216 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998846176 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998857303 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998881263 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998892343 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998916383 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 [W927 21:40:06.998927186 register_special_ops.cpp:225] Warning: Creating a tensor from 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.92/34.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.92/34.66 % (1804149)Refutation not found, incomplete strategy % 235.92/34.66 % (1804149)------------------------------ % 235.92/34.66 % (1804149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.92/34.66 % (1804149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.92/34.66 % (1804149)CaDiCaL version: 2.1.3 % 235.92/34.66 % (1804149)Termination reason: Refutation not found, incomplete strategy % 235.92/34.66 % (1804149)Time elapsed: 0.542 s % 235.92/34.66 % (1804149)Peak memory usage: 125 MB % 235.92/34.66 % (1804149)Instructions burned: 826 (million) % 235.92/34.66 % (1804149)------------------------------ % 235.92/34.66 % (1804149)------------------------------ % 235.92/34.66 % (1804151)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3213860785:cts=off:i=5469:bs=on:fsr=off_2744 on theBenchmark for (2744ds/5469Mi) % 235.92/34.66 % (1804151)Instruction limit reached! % 235.92/34.66 % (1804151)------------------------------ % 235.92/34.66 % (1804151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.92/34.66 % (1804151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.92/34.66 % (1804151)CaDiCaL version: 2.1.3 % 235.92/34.66 % (1804151)Termination reason: Instruction limit % 235.92/34.66 % (1804151)Termination phase: Saturation % 235.92/34.66 % (1804151)Time elapsed: 3.097 s % 235.92/34.66 % (1804151)Peak memory usage: 105 MB % 235.92/34.66 % (1804151)Instructions burned: 5470 (million) % 235.92/34.66 % (1804153)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=1355680043:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2712 on theBenchmark for (2712ds/2037Mi) % 235.92/34.66 % (1804153)Instruction limit reached! % 235.92/34.66 % (1804153)------------------------------ % 235.92/34.66 % (1804153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.23/35.21 % (1804153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.23/35.21 % (1804153)CaDiCaL version: 2.1.3 % 240.23/35.21 % (1804153)Termination reason: Instruction limit % 240.23/35.21 % (1804153)Termination phase: Saturation % 240.23/35.21 % (1804153)Time elapsed: 1.256 s % 240.23/35.21 % (1804153)Peak memory usage: 138 MB % 240.23/35.21 % (1804153)Instructions burned: 2038 (million) % 240.23/35.21 % (1804155)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=941423986:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2698 on theBenchmark for (2698ds/2110Mi) % 240.23/35.21 [W927 21:40:12.548607463 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548649190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548686820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548698536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548723023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548733916 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548758383 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548769570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548811623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548823043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548847340 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 240.23/35.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 240.23/35.21 [W927 21:40:12.548858103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 262.89/38.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 262.89/38.48 % (1804155)Refutation not found, incomplete strategy % 262.89/38.48 % (1804155)------------------------------ % 262.89/38.48 % (1804155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.89/38.48 % (1804155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.89/38.48 % (1804155)CaDiCaL version: 2.1.3 % 262.89/38.48 % (1804155)Termination reason: Refutation not found, incomplete strategy % 262.89/38.48 % (1804155)Time elapsed: 0.548 s % 262.89/38.48 % (1804155)Peak memory usage: 125 MB % 262.89/38.48 % (1804155)Instructions burned: 826 (million) % 262.89/38.48 % (1804155)------------------------------ % 262.89/38.48 % (1804155)------------------------------ % 262.89/38.48 % (1804157)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=2706675784:i=2430:add=off:aac=none:nm=16_2688 on theBenchmark for (2688ds/2430Mi) % 262.89/38.48 % (1804103)Instruction limit reached! % 262.89/38.48 % (1804103)------------------------------ % 262.89/38.48 % (1804103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.89/38.48 % (1804103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.89/38.48 % (1804103)CaDiCaL version: 2.1.3 % 262.89/38.48 % (1804103)Termination reason: Instruction limit % 262.89/38.48 % (1804103)Termination phase: Saturation % 262.89/38.48 % (1804103)Time elapsed: 19.681 s % 262.89/38.48 % (1804103)Peak memory usage: 155 MB % 262.89/38.48 % (1804103)Instructions burned: 33335 (million) % 262.89/38.48 % (1804159)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=1298307315:cond=fast:i=4891_2680 on theBenchmark for (2680ds/4891Mi) % 262.89/38.48 % (1804157)Instruction limit reached! % 262.89/38.48 % (1804157)------------------------------ % 262.89/38.48 % (1804157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.89/38.48 % (1804157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.89/38.48 % (1804157)CaDiCaL version: 2.1.3 % 262.89/38.48 % (1804157)Termination reason: Instruction limit % 262.89/38.48 % (1804157)Termination phase: Saturation % 262.89/38.48 % (1804157)Time elapsed: 1.475 s % 262.89/38.48 % (1804157)Peak memory usage: 143 MB % 262.89/38.48 % (1804157)Instructions burned: 2431 (million) % 262.89/38.48 % (1804161)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=3820340709:st=2:i=14845:sd=2:ss=included:fsd=on_2672 on theBenchmark for (2672ds/14845Mi) % 262.89/38.48 % (1804129)Instruction limit reached! % 262.89/38.48 % (1804129)------------------------------ % 262.89/38.48 % (1804129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.89/38.48 % (1804129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.89/38.48 % (1804129)CaDiCaL version: 2.1.3 % 262.89/38.48 % (1804129)Termination reason: Instruction limit % 262.89/38.48 % (1804129)Termination phase: Saturation % 262.89/38.48 % (1804129)Time elapsed: 15.196 s % 262.89/38.48 % (1804129)Peak memory usage: 392 MB % 262.89/38.48 % (1804129)Instructions burned: 26473 (million) % 262.89/38.48 % (1804163)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=790882040:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2669 on theBenchmark for (2669ds/7534Mi) % 262.89/38.48 % (1804161)Refutation not found, incomplete strategy % 262.89/38.48 % (1804161)------------------------------ % 262.89/38.48 % (1804161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 262.89/38.48 % (1804161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 262.89/38.48 % (1804161)CaDiCaL version: 2.1.3 % 262.89/38.48 % (1804161)Termination reason: Refutation not found, incomplete strategy % 262.89/38.48 % (1804161)Time elapsed: 0.557 s % 262.89/38.48 % (1804161)Peak memory usage: 128 MB % 262.89/38.48 % (1804161)Instructions burned: 841 (million) % 262.89/38.48 % (1804161)------------------------------ % 262.89/38.48 % (1804161)------------------------------ % 262.89/38.48 % (1804165)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=3325839866:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2663 on theBenchmark for (2663ds/10353Mi) % 266.03/39.01 [W927 21:40:15.021932451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.021965987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022014984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022029231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022057834 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022069891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022096257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022108041 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022133797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022145391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022171241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 [W927 21:40:15.022183104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 266.03/39.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 266.03/39.01 % (1804165)Refutation not found, incomplete strategy % 266.03/39.01 % (1804165)------------------------------ % 266.03/39.01 % (1804165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.28/39.35 % (1804165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.28/39.35 % (1804165)CaDiCaL version: 2.1.3 % 269.28/39.35 % (1804165)Termination reason: Refutation not found, incomplete strategy % 269.28/39.35 % (1804165)Time elapsed: 0.549 s % 269.28/39.35 % (1804165)Peak memory usage: 125 MB % 269.28/39.35 % (1804165)Instructions burned: 822 (million) % 269.28/39.35 % (1804165)------------------------------ % 269.28/39.35 % (1804165)------------------------------ % 269.28/39.35 % (1804127)Instruction limit reached! % 269.28/39.35 % (1804127)------------------------------ % 269.28/39.35 % (1804127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.28/39.35 % (1804127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.28/39.35 % (1804127)CaDiCaL version: 2.1.3 % 269.28/39.35 % (1804127)Termination reason: Instruction limit % 269.28/39.35 % (1804127)Termination phase: Saturation % 269.28/39.35 % (1804127)Time elapsed: 17.291 s % 269.28/39.35 % (1804127)Peak memory usage: 253 MB % 269.28/39.35 % (1804127)Instructions burned: 30754 (million) % 269.28/39.35 % (1804167)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=137947713:i=7860_2654 on theBenchmark for (2654ds/7860Mi) % 269.28/39.35 % (1804167)Refutation not found, incomplete strategy % 269.28/39.35 % (1804167)------------------------------ % 269.28/39.35 % (1804167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.28/39.35 % (1804167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.28/39.35 % (1804167)CaDiCaL version: 2.1.3 % 269.28/39.35 % (1804167)Termination reason: Refutation not found, incomplete strategy % 269.28/39.35 % (1804167)Time elapsed: 0.005 s % 269.28/39.35 % (1804167)Peak memory usage: 88 MB % 269.28/39.35 % (1804167)Instructions burned: 8 (million) % 269.28/39.35 % (1804168)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=1226189878:i=7896:sd=2:bs=on:ss=included:sgt=20_2653 on theBenchmark for (2653ds/7896Mi) % 269.28/39.35 % (1804167)------------------------------ % 269.28/39.35 % (1804167)------------------------------ % 269.28/39.35 % (1804171)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=838753784:i=5812:gtgl=2:gtg=all_2650 on theBenchmark for (2650ds/5812Mi) % 269.28/39.35 % (1804159)Instruction limit reached! % 269.28/39.35 % (1804159)------------------------------ % 269.28/39.35 % (1804159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.28/39.35 % (1804159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.28/39.35 % (1804159)CaDiCaL version: 2.1.3 % 269.28/39.35 % (1804159)Termination reason: Instruction limit % 269.28/39.35 % (1804159)Termination phase: Saturation % 269.28/39.35 % (1804159)Time elapsed: 3.067 s % 269.28/39.35 % (1804159)Peak memory usage: 157 MB % 269.28/39.35 % (1804159)Instructions burned: 4891 (million) % 269.28/39.35 % (1804173)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=4275029634:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2648 on theBenchmark for (2648ds/2965Mi) % 269.28/39.35 % (1804173)Refutation not found, incomplete strategy % 269.28/39.35 % (1804173)------------------------------ % 269.28/39.35 % (1804173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.28/39.35 % (1804173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.28/39.35 % (1804173)CaDiCaL version: 2.1.3 % 269.28/39.35 % (1804173)Termination reason: Refutation not found, incomplete strategy % 269.28/39.35 % (1804173)Time elapsed: 0.557 s % 269.28/39.35 % (1804173)Peak memory usage: 128 MB % 269.28/39.35 % (1804173)Instructions burned: 844 (million) % 269.28/39.35 % (1804173)------------------------------ % 269.28/39.35 % (1804173)------------------------------ % 269.28/39.35 % (1804175)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=2056592219:i=2967:kws=precedence:bd=preordered:av=off_2639 on theBenchmark for (2639ds/2967Mi) % 269.28/39.35 % (1804163)Instruction limit reached! % 269.28/39.35 % (1804163)------------------------------ % 269.28/39.35 % (1804163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 269.28/39.35 % (1804163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 269.28/39.35 % (1804163)CaDiCaL version: 2.1.3 % 269.28/39.35 % (1804163)Termination reason: Instruction limit % 269.28/39.35 % (1804163)Termination phase: Saturation % 275.26/40.16 % (1804163)Time elapsed: 4.454 s % 275.26/40.16 % (1804163)Peak memory usage: 171 MB % 275.26/40.16 % (1804163)Instructions burned: 7535 (million) % 275.26/40.16 % (1804177)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=15820550:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2623 on theBenchmark for (2623ds/3022Mi) % 275.26/40.16 % (1804175)Instruction limit reached! % 275.26/40.16 % (1804175)------------------------------ % 275.26/40.16 % (1804175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 275.26/40.16 % (1804175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 275.26/40.16 % (1804175)CaDiCaL version: 2.1.3 % 275.26/40.16 % (1804175)Termination reason: Instruction limit % 275.26/40.16 % (1804175)Termination phase: Saturation % 275.26/40.16 % (1804175)Time elapsed: 1.758 s % 275.26/40.16 % (1804175)Peak memory usage: 143 MB % 275.26/40.16 % (1804175)Instructions burned: 2967 (million) % 275.26/40.16 % (1804179)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=157478453:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2620 on theBenchmark for (2620ds/3207Mi) % 275.26/40.16 [W927 21:40:19.989600480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989642320 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989680447 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989691981 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989716227 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989726447 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989751824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989762047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989785817 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 275.26/40.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 275.26/40.16 [W927 21:40:19.989796147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.989820634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.989830724 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 % (1804177)Refutation not found, incomplete strategy % 276.99/40.45 % (1804177)------------------------------ % 276.99/40.45 % (1804177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.99/40.45 % (1804177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.99/40.45 % (1804177)CaDiCaL version: 2.1.3 % 276.99/40.45 % (1804177)Termination reason: Refutation not found, incomplete strategy % 276.99/40.45 % (1804177)Time elapsed: 0.546 s % 276.99/40.45 % (1804177)Peak memory usage: 125 MB % 276.99/40.45 % (1804177)Instructions burned: 826 (million) % 276.99/40.45 [W927 21:40:19.340065077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340098851 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340137244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340158517 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340185351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340201454 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340226737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340236884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 276.99/40.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 276.99/40.45 [W927 21:40:19.340260284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.60/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.60/41.09 [W927 21:40:19.340270334 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.60/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.60/41.09 [W927 21:40:19.340298404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.60/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.60/41.09 [W927 21:40:19.340308527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.60/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.60/41.09 % (1804177)------------------------------ % 281.60/41.09 % (1804177)------------------------------ % 281.60/41.09 % (1804179)Refutation not found, incomplete strategy % 281.60/41.09 % (1804179)------------------------------ % 281.60/41.09 % (1804179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.60/41.09 % (1804179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.60/41.09 % (1804179)CaDiCaL version: 2.1.3 % 281.60/41.09 % (1804179)Termination reason: Refutation not found, incomplete strategy % 281.60/41.09 % (1804179)Time elapsed: 0.550 s % 281.60/41.09 % (1804179)Peak memory usage: 125 MB % 281.60/41.09 % (1804179)Instructions burned: 826 (million) % 281.60/41.09 % (1804182)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2842032948:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2614 on theBenchmark for (2614ds/3289Mi) % 281.60/41.09 % (1804171)Instruction limit reached! % 281.60/41.09 % (1804171)------------------------------ % 281.60/41.09 % (1804171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.60/41.09 % (1804171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.60/41.09 % (1804171)CaDiCaL version: 2.1.3 % 281.60/41.09 % (1804171)Termination reason: Instruction limit % 281.60/41.09 % (1804171)Termination phase: Saturation % 281.60/41.09 % (1804171)Time elapsed: 3.667 s % 281.60/41.09 % (1804171)Peak memory usage: 177 MB % 281.60/41.09 % (1804171)Instructions burned: 5812 (million) % 281.60/41.09 % (1804179)------------------------------ % 281.60/41.09 % (1804179)------------------------------ % 281.60/41.09 % (1804184)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3679037127:i=38569:sd=3:ss=axioms:sgt=32_2612 on theBenchmark for (2612ds/38569Mi) % 281.60/41.09 % (1804185)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2192297174:cts=off:i=3394_2610 on theBenchmark for (2610ds/3394Mi) % 281.60/41.09 % (1804182)Refutation not found, incomplete strategy % 281.60/41.09 % (1804182)------------------------------ % 281.60/41.09 % (1804182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 281.60/41.09 % (1804182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 281.60/41.09 % (1804182)CaDiCaL version: 2.1.3 % 281.60/41.09 % (1804182)Termination reason: Refutation not found, incomplete strategy % 281.60/41.09 % (1804182)Time elapsed: 0.560 s % 281.60/41.09 % (1804182)Peak memory usage: 127 MB % 281.60/41.09 % (1804182)Instructions burned: 847 (million) % 281.60/41.09 [W927 21:40:20.148998762 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.60/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.60/41.09 [W927 21:40:20.149057599 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 281.60/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 281.60/41.09 [W927 21:40:20.149095186 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149108482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149133852 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149145022 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149169936 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149180979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149204802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149269783 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149318929 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 [W927 21:40:20.149349226 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 287.34/42.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 287.34/42.02 % (1804168)Instruction limit reached! % 287.34/42.02 % (1804168)------------------------------ % 287.34/42.02 % (1804168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.34/42.02 % (1804168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/42.02 % (1804168)CaDiCaL version: 2.1.3 % 287.34/42.02 % (1804168)Termination reason: Instruction limit % 287.34/42.02 % (1804168)Termination phase: Saturation % 287.34/42.02 % (1804168)Time elapsed: 4.613 s % 287.34/42.02 % (1804168)Peak memory usage: 192 MB % 287.34/42.02 % (1804168)Instructions burned: 7897 (million) % 287.34/42.02 % (1804184)Refutation not found, incomplete strategy % 287.34/42.02 % (1804184)------------------------------ % 287.34/42.02 % (1804184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 287.34/42.02 % (1804184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 287.34/42.02 % (1804184)CaDiCaL version: 2.1.3 % 287.34/42.02 % (1804184)Termination reason: Refutation not found, incomplete strategy % 287.34/42.02 % (1804184)Time elapsed: 0.547 s % 287.34/42.02 % (1804184)Peak memory usage: 125 MB % 287.34/42.02 % (1804184)Instructions burned: 822 (million) % 287.34/42.02 % (1804182)------------------------------ % 287.34/42.02 % (1804182)------------------------------ % 287.34/42.02 % (1804188)lrsTerminated %------------------------------------------------------------------------------