%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWC423+1 : TPTP v9.3.1. Released v2.5.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 01:03:55 PM UTC 2026 % Result : Timeout 290.94s 41.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC423+1 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.18 % Computer : n007.cluster.edu % 0.09/0.18 % Model : x86_64 x86_64 % 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.18 % Memory : 8046.5625MB % 0.09/0.18 % OS : Linux 6.8.0-71-generic % 0.09/0.18 % CPULimit : 300 % 0.09/0.18 % WCLimit : 300 % 0.09/0.18 % DateTime : Mon Sep 28 09:34:26 UTC 2026 % 0.09/0.18 % CPUTime : % 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.09/0.20 Running first-order theorem proving % 0.09/0.20 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 % 3.75/1.17 % (2268303)Detected formulas, will run a generic FOF schedule. % 3.75/1.17 % (2268311)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1039166684:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 3.75/1.17 % (2268311)Refutation not found, incomplete strategy % 3.75/1.17 % (2268311)------------------------------ % 3.75/1.17 % (2268311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.75/1.17 % (2268311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.75/1.17 % (2268311)CaDiCaL version: 2.1.3 % 3.75/1.17 % (2268311)Termination reason: Refutation not found, incomplete strategy % 3.75/1.17 % (2268311)Time elapsed: 0.0000 s % 3.75/1.17 % (2268311)Peak memory usage: 86 MB % 3.75/1.17 % (2268313)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2076826818:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 3.75/1.17 % (2268308)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=2832379110:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 3.75/1.17 % (2268309)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=3642095306:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 3.75/1.17 % (2268310)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=2367204308:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 3.75/1.17 % (2268312)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3370747363:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 3.75/1.17 % (2268314)dis-21_1_sil=8000:lcm=predicate:random_seed=3576983006: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) % 3.75/1.17 % (2268312)Refutation not found, incomplete strategy % 3.75/1.17 % (2268312)------------------------------ % 3.75/1.17 % (2268312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.75/1.17 % (2268312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.75/1.17 % (2268312)CaDiCaL version: 2.1.3 % 3.75/1.17 % (2268312)Termination reason: Refutation not found, incomplete strategy % 3.75/1.17 % (2268312)Time elapsed: 0.001 s % 3.75/1.17 % (2268312)Peak memory usage: 86 MB % 3.75/1.17 % (2268314)Refutation not found, incomplete strategy % 3.75/1.17 % (2268314)------------------------------ % 3.75/1.17 % (2268314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.75/1.17 % (2268314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.75/1.17 % (2268314)CaDiCaL version: 2.1.3 % 3.75/1.17 % (2268314)Termination reason: Refutation not found, incomplete strategy % 3.75/1.17 % (2268314)Time elapsed: 0.001 s % 3.75/1.17 % (2268314)Peak memory usage: 86 MB % 3.75/1.17 % (2268313)Instruction limit reached! % 3.75/1.17 % (2268313)------------------------------ % 3.75/1.17 % (2268313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.75/1.17 % (2268313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.75/1.17 % (2268313)CaDiCaL version: 2.1.3 % 3.75/1.17 % (2268313)Termination reason: Instruction limit % 3.75/1.17 % (2268313)Termination phase: Saturation % 3.75/1.17 % (2268313)Time elapsed: 0.090 s % 3.75/1.17 % (2268313)Peak memory usage: 90 MB % 3.75/1.17 % (2268313)Instructions burned: 139 (million) % 3.75/1.17 % (2268311)------------------------------ % 3.75/1.17 % (2268311)------------------------------ % 3.75/1.17 % (2268322)lrs+10_1_sil=8000:sp=occurrence:random_seed=3644942664:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 3.75/1.17 % (2268322)Refutation not found, incomplete strategy % 3.75/1.17 % (2268322)------------------------------ % 3.75/1.17 % (2268322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.75/1.17 % (2268322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.75/1.17 % (2268322)CaDiCaL version: 2.1.3 % 3.75/1.17 % (2268322)Termination reason: Refutation not found, incomplete strategy % 3.75/1.17 % (2268322)Time elapsed: 0.002 s % 3.75/1.17 % (2268322)Peak memory usage: 86 MB % 3.75/1.17 % (2268323)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2310496662:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 4.99/1.42 % (2268323)Refutation not found, incomplete strategy % 4.99/1.42 % (2268323)------------------------------ % 4.99/1.42 % (2268323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.99/1.42 % (2268323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.99/1.42 % (2268323)CaDiCaL version: 2.1.3 % 4.99/1.42 % (2268323)Termination reason: Refutation not found, incomplete strategy % 4.99/1.42 % (2268323)Time elapsed: 0.0000 s % 4.99/1.42 % (2268323)Peak memory usage: 87 MB % 4.99/1.42 % (2268323)Instructions burned: 1 (million) % 4.99/1.42 % (2268314)------------------------------ % 4.99/1.42 % (2268314)------------------------------ % 4.99/1.42 % (2268312)------------------------------ % 4.99/1.42 % (2268312)------------------------------ % 4.99/1.42 % (2268323)------------------------------ % 4.99/1.42 % (2268323)------------------------------ % 4.99/1.42 [W928 09:34:27.503182287 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503216104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503253854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503267034 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503293790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503306284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503331994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503344457 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503370050 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503382514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.99/1.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.99/1.42 [W928 09:34:27.503408667 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503421060 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503491200 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503515600 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503566464 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503578191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503604147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503616784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503643217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503654527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503679964 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503691537 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503717094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 [W928 09:34:27.503728427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 7.57/1.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 7.57/1.96 % (2268326)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1300834213:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 7.57/1.96 % (2268327)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=760907692:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 7.57/1.96 % (2268326)Refutation not found, incomplete strategy % 7.57/1.96 % (2268326)------------------------------ % 7.57/1.96 % (2268326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.57/1.96 % (2268326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.96 % (2268326)CaDiCaL version: 2.1.3 % 7.57/1.96 % (2268326)Termination reason: Refutation not found, incomplete strategy % 7.57/1.96 % (2268326)Time elapsed: 0.001 s % 7.57/1.96 % (2268326)Peak memory usage: 86 MB % 7.57/1.96 % (2268322)------------------------------ % 7.57/1.96 % (2268322)------------------------------ % 7.57/1.96 % (2268328)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1506703107:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi) % 7.57/1.96 % (2268328)Refutation not found, incomplete strategy % 7.57/1.96 % (2268328)------------------------------ % 7.57/1.96 % (2268328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.57/1.96 % (2268328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.96 % (2268328)CaDiCaL version: 2.1.3 % 7.57/1.96 % (2268328)Termination reason: Refutation not found, incomplete strategy % 7.57/1.96 % (2268328)Time elapsed: 0.0000 s % 7.57/1.96 % (2268328)Peak memory usage: 86 MB % 7.57/1.96 % (2268327)Instruction limit reached! % 7.57/1.96 % (2268327)------------------------------ % 7.57/1.96 % (2268327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.57/1.96 % (2268327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.96 % (2268327)CaDiCaL version: 2.1.3 % 7.57/1.96 % (2268327)Termination reason: Instruction limit % 7.57/1.96 % (2268327)Termination phase: Saturation % 7.57/1.96 % (2268327)Time elapsed: 0.120 s % 7.57/1.96 % (2268327)Peak memory usage: 91 MB % 7.57/1.96 % (2268327)Instructions burned: 249 (million) % 7.57/1.96 % (2268309)Refutation not found, incomplete strategy % 7.57/1.96 % (2268309)------------------------------ % 7.57/1.96 % (2268309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.57/1.96 % (2268309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.96 % (2268309)CaDiCaL version: 2.1.3 % 7.57/1.96 % (2268309)Termination reason: Refutation not found, incomplete strategy % 7.57/1.96 % (2268309)Time elapsed: 0.555 s % 7.57/1.96 % (2268309)Peak memory usage: 124 MB % 7.57/1.96 % (2268309)Instructions burned: 823 (million) % 7.57/1.96 % (2268310)Refutation not found, incomplete strategy % 7.57/1.96 % (2268310)------------------------------ % 7.57/1.96 % (2268310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.57/1.96 % (2268310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.96 % (2268310)CaDiCaL version: 2.1.3 % 7.57/1.96 % (2268310)Termination reason: Refutation not found, incomplete strategy % 7.57/1.96 % (2268310)Time elapsed: 0.559 s % 7.57/1.96 % (2268310)Peak memory usage: 124 MB % 7.57/1.96 % (2268310)Instructions burned: 826 (million) % 7.57/1.96 % (2268332)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=273882212:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 7.57/1.96 % (2268328)------------------------------ % 7.57/1.96 % (2268328)------------------------------ % 7.57/1.96 % (2268326)------------------------------ % 7.57/1.96 % (2268326)------------------------------ % 7.57/1.96 % (2268333)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4288357259:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 7.57/1.96 % (2268333)Refutation not found, incomplete strategy % 7.57/1.96 % (2268333)------------------------------ % 7.57/1.96 % (2268333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.57/1.96 % (2268333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.57/1.96 % (2268333)CaDiCaL version: 2.1.3 % 7.57/1.96 % (2268333)Termination reason: Refutation not found, incomplete strategy % 7.57/1.96 % (2268333)Time elapsed: 0.001 s % 12.34/2.41 % (2268333)Peak memory usage: 87 MB % 12.34/2.41 % (2268335)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2259894519:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 12.34/2.41 % (2268335)Refutation not found, incomplete strategy % 12.34/2.41 % (2268335)------------------------------ % 12.34/2.41 % (2268335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.41 % (2268335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.41 % (2268335)CaDiCaL version: 2.1.3 % 12.34/2.41 % (2268335)Termination reason: Refutation not found, incomplete strategy % 12.34/2.41 % (2268335)Time elapsed: 0.003 s % 12.34/2.41 % (2268335)Peak memory usage: 88 MB % 12.34/2.41 % (2268335)Instructions burned: 10 (million) % 12.34/2.41 % (2268337)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1699553423:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 12.34/2.41 % (2268337)Refutation not found, incomplete strategy % 12.34/2.41 % (2268337)------------------------------ % 12.34/2.41 % (2268337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.41 % (2268337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.41 % (2268337)CaDiCaL version: 2.1.3 % 12.34/2.41 % (2268337)Termination reason: Refutation not found, incomplete strategy % 12.34/2.41 % (2268337)Time elapsed: 0.001 s % 12.34/2.41 % (2268337)Peak memory usage: 87 MB % 12.34/2.41 % (2268337)Instructions burned: 1 (million) % 12.34/2.41 % (2268309)------------------------------ % 12.34/2.41 % (2268309)------------------------------ % 12.34/2.41 % (2268310)------------------------------ % 12.34/2.41 % (2268310)------------------------------ % 12.34/2.41 % (2268335)------------------------------ % 12.34/2.41 % (2268335)------------------------------ % 12.34/2.41 % (2268333)------------------------------ % 12.34/2.41 % (2268333)------------------------------ % 12.34/2.41 % (2268341)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=741756353:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 12.34/2.41 % (2268340)lrs+10_1_sil=8000:sp=occurrence:random_seed=97528318:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 12.34/2.41 % (2268341)Refutation not found, incomplete strategy % 12.34/2.41 % (2268341)------------------------------ % 12.34/2.41 % (2268341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.41 % (2268341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.41 % (2268341)CaDiCaL version: 2.1.3 % 12.34/2.41 % (2268341)Termination reason: Refutation not found, incomplete strategy % 12.34/2.41 % (2268341)Time elapsed: 0.001 s % 12.34/2.41 % (2268341)Peak memory usage: 86 MB % 12.34/2.41 % (2268340)Refutation not found, incomplete strategy % 12.34/2.41 % (2268340)------------------------------ % 12.34/2.41 % (2268340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.41 % (2268340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.41 % (2268340)CaDiCaL version: 2.1.3 % 12.34/2.41 % (2268340)Termination reason: Refutation not found, incomplete strategy % 12.34/2.41 % (2268340)Time elapsed: 0.001 s % 12.34/2.41 % (2268340)Peak memory usage: 86 MB % 12.34/2.41 % (2268342)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3464288304:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi) % 12.34/2.41 % (2268343)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=698369063:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi) % 12.34/2.41 % (2268337)------------------------------ % 12.34/2.41 % (2268337)------------------------------ % 12.34/2.41 % (2268343)Refutation not found, incomplete strategy % 12.34/2.41 % (2268343)------------------------------ % 12.34/2.41 % (2268343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.41 % (2268343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.41 % (2268343)CaDiCaL version: 2.1.3 % 12.34/2.41 % (2268343)Termination reason: Refutation not found, incomplete strategy % 12.34/2.41 % (2268343)Time elapsed: 0.001 s % 12.34/2.41 % (2268343)Peak memory usage: 86 MB % 12.34/2.41 [W928 09:34:27.293035764 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293064190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293085912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293092067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293107393 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293112956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293125976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293131836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293144642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293150149 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293163279 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 [W928 09:34:27.293168640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.48 % (2268348)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1122209538:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 12.34/2.48 % (2268348)Refutation not found, incomplete strategy % 12.34/2.48 % (2268348)------------------------------ % 12.34/2.48 % (2268348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.48 % (2268348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.48 % (2268348)CaDiCaL version: 2.1.3 % 12.34/2.48 % (2268348)Termination reason: Refutation not found, incomplete strategy % 14.93/2.96 % (2268348)Time elapsed: 0.001 s % 14.93/2.96 % (2268348)Peak memory usage: 86 MB % 14.93/2.96 % (2268341)------------------------------ % 14.93/2.96 % (2268341)------------------------------ % 14.93/2.96 % (2268340)------------------------------ % 14.93/2.96 % (2268340)------------------------------ % 14.93/2.96 % (2268343)------------------------------ % 14.93/2.96 % (2268343)------------------------------ % 14.93/2.96 % (2268342)Refutation not found, incomplete strategy % 14.93/2.96 % (2268342)------------------------------ % 14.93/2.96 % (2268342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.93/2.96 % (2268342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.93/2.96 % (2268342)CaDiCaL version: 2.1.3 % 14.93/2.96 % (2268342)Termination reason: Refutation not found, incomplete strategy % 14.93/2.96 % (2268342)Time elapsed: 0.306 s % 14.93/2.96 % (2268342)Peak memory usage: 125 MB % 14.93/2.96 % (2268342)Instructions burned: 827 (million) % 14.93/2.96 % (2268351)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=2846727087:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 14.93/2.96 % (2268350)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1494397329:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 14.93/2.96 % (2268351)Refutation not found, incomplete strategy % 14.93/2.96 % (2268351)------------------------------ % 14.93/2.96 % (2268351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.93/2.96 % (2268351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.93/2.96 % (2268351)CaDiCaL version: 2.1.3 % 14.93/2.96 % (2268351)Termination reason: Refutation not found, incomplete strategy % 14.93/2.96 % (2268351)Time elapsed: 0.001 s % 14.93/2.96 % (2268351)Peak memory usage: 87 MB % 14.93/2.96 % (2268351)Instructions burned: 1 (million) % 14.93/2.96 % (2268352)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2974896719:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi) % 14.93/2.96 % (2268348)------------------------------ % 14.93/2.96 % (2268348)------------------------------ % 14.93/2.96 % (2268342)------------------------------ % 14.93/2.96 % (2268342)------------------------------ % 14.93/2.96 % (2268352)Instruction limit reached! % 14.93/2.96 % (2268352)------------------------------ % 14.93/2.96 % (2268352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.93/2.96 % (2268352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.93/2.96 % (2268352)CaDiCaL version: 2.1.3 % 14.93/2.96 % (2268352)Termination reason: Instruction limit % 14.93/2.96 % (2268352)Termination phase: Saturation % 14.93/2.96 % (2268352)Time elapsed: 0.076 s % 14.93/2.96 % (2268352)Peak memory usage: 90 MB % 14.93/2.96 % (2268352)Instructions burned: 134 (million) % 14.93/2.96 % (2268357)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=728703114:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/431Mi) % 14.93/2.96 % (2268357)Refutation not found, incomplete strategy % 14.93/2.96 % (2268357)------------------------------ % 14.93/2.96 % (2268357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.93/2.96 % (2268357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.93/2.97 % (2268357)CaDiCaL version: 2.1.3 % 14.93/2.97 % (2268357)Termination reason: Refutation not found, incomplete strategy % 14.93/2.97 % (2268357)Time elapsed: 0.0000 s % 14.93/2.97 % (2268357)Peak memory usage: 86 MB % 14.93/2.97 % (2268351)------------------------------ % 14.93/2.97 % (2268351)------------------------------ % 14.93/2.97 % (2268356)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3498619632:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 14.93/2.97 % (2268356)Refutation not found, incomplete strategy % 14.93/2.97 % (2268356)------------------------------ % 14.93/2.97 % (2268356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.93/2.97 % (2268356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.93/2.97 % (2268356)CaDiCaL version: 2.1.3 % 14.93/2.97 % (2268356)Termination reason: Refutation not found, incomplete strategy % 14.93/2.97 % (2268356)Time elapsed: 0.001 s % 14.93/2.97 % (2268356)Peak memory usage: 86 MB % 14.93/2.97 % (2268358)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=524664412:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi) % 19.41/3.43 % (2268357)------------------------------ % 19.41/3.43 % (2268357)------------------------------ % 19.41/3.43 % (2268361)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=4180327925:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi) % 19.41/3.43 [W928 09:34:28.820563994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820597541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820635034 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820662304 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820690098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820702398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820726974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820790028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820822254 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820834164 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820859881 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.41/3.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.41/3.43 [W928 09:34:28.820871511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 22.20/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 22.20/3.98 % (2268363)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3893627700:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi) % 22.20/3.98 % (2268361)Instruction limit reached! % 22.20/3.98 % (2268361)------------------------------ % 22.20/3.98 % (2268361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.20/3.98 % (2268361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.98 % (2268361)CaDiCaL version: 2.1.3 % 22.20/3.98 % (2268361)Termination reason: Instruction limit % 22.20/3.98 % (2268361)Termination phase: Saturation % 22.20/3.98 % (2268361)Time elapsed: 0.090 s % 22.20/3.98 % (2268361)Peak memory usage: 92 MB % 22.20/3.98 % (2268361)Instructions burned: 152 (million) % 22.20/3.98 % (2268356)------------------------------ % 22.20/3.98 % (2268356)------------------------------ % 22.20/3.98 % (2268350)Refutation not found, incomplete strategy % 22.20/3.98 % (2268350)------------------------------ % 22.20/3.98 % (2268350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.20/3.98 % (2268350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.98 % (2268350)CaDiCaL version: 2.1.3 % 22.20/3.98 % (2268350)Termination reason: Refutation not found, incomplete strategy % 22.20/3.98 % (2268350)Time elapsed: 0.562 s % 22.20/3.98 % (2268350)Peak memory usage: 125 MB % 22.20/3.98 % (2268350)Instructions burned: 821 (million) % 22.20/3.98 % (2268366)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=719605431:i=667:av=off:fsr=off_2980 on theBenchmark for (2980ds/667Mi) % 22.20/3.98 % (2268366)Refutation not found, incomplete strategy % 22.20/3.98 % (2268366)------------------------------ % 22.20/3.98 % (2268366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.20/3.98 % (2268366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.98 % (2268366)CaDiCaL version: 2.1.3 % 22.20/3.98 % (2268366)Termination reason: Refutation not found, incomplete strategy % 22.20/3.98 % (2268366)Time elapsed: 0.006 s % 22.20/3.98 % (2268366)Peak memory usage: 88 MB % 22.20/3.98 % (2268366)Instructions burned: 8 (million) % 22.20/3.98 % (2268367)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=262475288:s2a=on:i=185:s2at=1.8:fdi=4_2980 on theBenchmark for (2980ds/185Mi) % 22.20/3.98 % (2268367)Instruction limit reached! % 22.20/3.98 % (2268367)------------------------------ % 22.20/3.98 % (2268367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.20/3.98 % (2268367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.98 % (2268367)CaDiCaL version: 2.1.3 % 22.20/3.98 % (2268367)Termination reason: Instruction limit % 22.20/3.98 % (2268367)Termination phase: Saturation % 22.20/3.98 % (2268367)Time elapsed: 0.104 s % 22.20/3.98 % (2268367)Peak memory usage: 93 MB % 22.20/3.98 % (2268367)Instructions burned: 185 (million) % 22.20/3.98 % (2268332)Instruction limit reached! % 22.20/3.98 % (2268332)------------------------------ % 22.20/3.98 % (2268332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.20/3.98 % (2268332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.98 % (2268332)CaDiCaL version: 2.1.3 % 22.20/3.98 % (2268332)Termination reason: Instruction limit % 22.20/3.98 % (2268332)Termination phase: Saturation % 22.20/3.98 % (2268332)Time elapsed: 1.479 s % 22.20/3.98 % (2268332)Peak memory usage: 141 MB % 22.20/3.98 % (2268332)Instructions burned: 2350 (million) % 22.20/3.98 % (2268350)------------------------------ % 22.20/3.98 % (2268350)------------------------------ % 22.20/3.98 % (2268366)------------------------------ % 22.20/3.98 % (2268366)------------------------------ % 22.20/3.98 % (2268370)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=71331815:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2978 on theBenchmark for (2978ds/193Mi) % 22.20/3.98 % (2268370)Refutation not found, incomplete strategy % 22.20/3.98 % (2268370)------------------------------ % 22.20/3.98 % (2268370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 22.20/3.98 % (2268370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 22.20/3.98 % (2268370)CaDiCaL version: 2.1.3 % 22.20/3.98 % (2268370)Termination reason: Refutation not found, incomplete strategy % 24.44/4.08 % (2268370)Time elapsed: 0.001 s % 24.44/4.08 % (2268370)Peak memory usage: 86 MB % 24.44/4.08 % (2268371)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=557283382:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2977 on theBenchmark for (2977ds/4850Mi) % 24.44/4.08 % (2268371)Refutation not found, incomplete strategy % 24.44/4.08 % (2268371)------------------------------ % 24.44/4.08 % (2268371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.44/4.08 % (2268371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/4.08 % (2268371)CaDiCaL version: 2.1.3 % 24.44/4.08 % (2268371)Termination reason: Refutation not found, incomplete strategy % 24.44/4.08 % (2268371)Time elapsed: 0.001 s % 24.44/4.08 % (2268371)Peak memory usage: 86 MB % 24.44/4.08 % (2268372)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2890409125:i=12111:sd=1:ss=included_2977 on theBenchmark for (2977ds/12111Mi) % 24.44/4.08 % (2268373)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2423206412:i=319:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/319Mi) % 24.44/4.08 % (2268370)------------------------------ % 24.44/4.08 % (2268370)------------------------------ % 24.44/4.08 % (2268371)------------------------------ % 24.44/4.08 % (2268371)------------------------------ % 24.44/4.08 % (2268373)Instruction limit reached! % 24.44/4.08 % (2268373)------------------------------ % 24.44/4.08 % (2268373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.44/4.08 % (2268373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/4.08 % (2268373)CaDiCaL version: 2.1.3 % 24.44/4.08 % (2268373)Termination reason: Instruction limit % 24.44/4.08 % (2268373)Termination phase: Saturation % 24.44/4.08 % (2268373)Time elapsed: 0.150 s % 24.44/4.08 % (2268373)Peak memory usage: 93 MB % 24.44/4.08 % (2268373)Instructions burned: 321 (million) % 24.44/4.08 % (2268378)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2405901807:i=2064:ep=RST_2974 on theBenchmark for (2974ds/2064Mi) % 24.44/4.08 % (2268378)Refutation not found, incomplete strategy % 24.44/4.08 % (2268378)------------------------------ % 24.44/4.08 % (2268378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.44/4.08 % (2268378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/4.08 % (2268378)CaDiCaL version: 2.1.3 % 24.44/4.08 % (2268378)Termination reason: Refutation not found, incomplete strategy % 24.44/4.08 % (2268378)Time elapsed: 0.007 s % 24.44/4.08 % (2268378)Peak memory usage: 88 MB % 24.44/4.08 % (2268378)Instructions burned: 11 (million) % 24.44/4.08 % (2268379)dis-1011_128_sil=32000:random_seed=3193744421:i=3706:ep=RST:av=off_2974 on theBenchmark for (2974ds/3706Mi) % 24.44/4.08 % (2268380)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1247887630:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2973 on theBenchmark for (2973ds/757Mi) % 24.44/4.08 % (2268380)Refutation not found, incomplete strategy % 24.44/4.08 % (2268380)------------------------------ % 24.44/4.08 % (2268380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 24.44/4.08 % (2268380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 24.44/4.08 % (2268380)CaDiCaL version: 2.1.3 % 24.44/4.08 % (2268380)Termination reason: Refutation not found, incomplete strategy % 24.44/4.08 % (2268380)Time elapsed: 0.001 s % 24.44/4.08 % (2268380)Peak memory usage: 86 MB % 24.44/4.08 [W928 09:34:29.770938716 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.44/4.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.44/4.08 [W928 09:34:29.770971659 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 24.44/4.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 24.44/4.08 [W928 09:34:29.771022839 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771037253 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771072226 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771149419 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771201383 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771216186 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771241569 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771252399 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771277593 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 [W928 09:34:29.771288429 register_special_ops.cpp:225] Warning: Creating a tensor from 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.53/5.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 29.53/5.03 % (2268378)------------------------------ % 29.53/5.03 % (2268378)------------------------------ % 29.53/5.03 % (2268372)Refutation not found, incomplete strategy % 29.53/5.03 % (2268372)------------------------------ % 29.53/5.03 % (2268372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.53/5.03 % (2268372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.53/5.03 % (2268372)CaDiCaL version: 2.1.3 % 29.53/5.03 % (2268372)Termination reason: Refutation not found, incomplete strategy % 29.53/5.03 % (2268372)Time elapsed: 0.544 s % 29.53/5.03 % (2268372)Peak memory usage: 126 MB % 29.53/5.03 % (2268372)Instructions burned: 822 (million) % 29.53/5.03 % (2268380)------------------------------ % 29.53/5.03 % (2268380)------------------------------ % 29.53/5.03 % (2268384)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1892642552:i=13913:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/13913Mi) % 29.53/5.03 % (2268385)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2421185691:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi) % 29.53/5.03 % (2268372)------------------------------ % 29.53/5.03 % (2268372)------------------------------ % 29.53/5.03 % (2268388)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=832506792:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/2479Mi) % 32.22/5.19 % (2268388)Refutation not found, incomplete strategy % 32.22/5.19 % (2268388)------------------------------ % 32.22/5.19 % (2268388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.22/5.19 % (2268388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.22/5.19 % (2268388)CaDiCaL version: 2.1.3 % 32.22/5.19 % (2268388)Termination reason: Refutation not found, incomplete strategy % 32.22/5.19 % (2268388)Time elapsed: 0.001 s % 32.22/5.19 % (2268388)Peak memory usage: 86 MB % 32.22/5.19 [W928 09:34:30.420713184 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420757141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420794128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420806531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420831908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420842311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420867918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420878688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420921681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420932741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420957405 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.22/5.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.22/5.19 [W928 09:34:30.420967951 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/6.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.78/6.86 % (2268388)------------------------------ % 42.78/6.86 % (2268388)------------------------------ % 42.78/6.86 % (2268384)Refutation not found, incomplete strategy % 42.78/6.86 % (2268384)------------------------------ % 42.78/6.86 % (2268384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.78/6.86 % (2268384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.78/6.86 % (2268384)CaDiCaL version: 2.1.3 % 42.78/6.86 % (2268384)Termination reason: Refutation not found, incomplete strategy % 42.78/6.86 % (2268384)Time elapsed: 0.549 s % 42.78/6.86 % (2268384)Peak memory usage: 125 MB % 42.78/6.86 % (2268384)Instructions burned: 825 (million) % 42.78/6.86 % (2268385)Refutation not found, incomplete strategy % 42.78/6.86 % (2268385)------------------------------ % 42.78/6.86 % (2268385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.78/6.86 % (2268385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.78/6.86 % (2268385)CaDiCaL version: 2.1.3 % 42.78/6.86 % (2268385)Termination reason: Refutation not found, incomplete strategy % 42.78/6.86 % (2268385)Time elapsed: 0.570 s % 42.78/6.86 % (2268385)Peak memory usage: 129 MB % 42.78/6.86 % (2268385)Instructions burned: 857 (million) % 42.78/6.86 % (2268390)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4082155654:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2964 on theBenchmark for (2964ds/440Mi) % 42.78/6.86 % (2268384)------------------------------ % 42.78/6.86 % (2268384)------------------------------ % 42.78/6.86 % (2268385)------------------------------ % 42.78/6.86 % (2268385)------------------------------ % 42.78/6.86 % (2268390)Instruction limit reached! % 42.78/6.86 % (2268390)------------------------------ % 42.78/6.86 % (2268390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.78/6.86 % (2268390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.78/6.86 % (2268390)CaDiCaL version: 2.1.3 % 42.78/6.86 % (2268390)Termination reason: Instruction limit % 42.78/6.86 % (2268390)Termination phase: Saturation % 42.78/6.86 % (2268390)Time elapsed: 0.239 s % 42.78/6.86 % (2268390)Peak memory usage: 93 MB % 42.78/6.86 % (2268390)Instructions burned: 441 (million) % 42.78/6.86 % (2268392)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=945335225:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/11145Mi) % 42.78/6.86 % (2268393)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=495109337:cts=off:i=3034:av=off:er=known:fsd=on_2960 on theBenchmark for (2960ds/3034Mi) % 42.78/6.86 % (2268394)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3911225689:st=2:s2a=on:i=524:s2at=2:ss=axioms_2960 on theBenchmark for (2960ds/524Mi) % 42.78/6.86 % (2268394)Refutation not found, incomplete strategy % 42.78/6.86 % (2268394)------------------------------ % 42.78/6.86 % (2268394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 42.78/6.86 % (2268394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 42.78/6.86 % (2268394)CaDiCaL version: 2.1.3 % 42.78/6.86 % (2268394)Termination reason: Refutation not found, incomplete strategy % 42.78/6.86 % (2268394)Time elapsed: 0.001 s % 42.78/6.86 % (2268394)Peak memory usage: 87 MB % 42.78/6.86 % (2268394)Instructions burned: 1 (million) % 42.78/6.86 % (2268394)------------------------------ % 42.78/6.86 % (2268394)------------------------------ % 42.78/6.86 [W928 09:34:30.362258554 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/6.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.78/6.86 [W928 09:34:30.362303541 register_special_ops.cpp:225] Warning: Creating a tensor from 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.78/6.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 42.78/6.86 [W928 09:34:30.362343271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362354845 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362379348 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362390228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362414985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362425928 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362449458 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362460178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362484715 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 [W928 09:34:30.362495461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 43.19/6.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 43.19/6.96 % (2268398)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2918736262:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2956 on theBenchmark for (2956ds/1016Mi) % 43.19/6.96 % (2268398)Refutation not found, incomplete strategy % 43.19/6.96 % (2268398)------------------------------ % 43.19/6.96 % (2268398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.19/6.96 % (2268398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.96 % (2268398)CaDiCaL version: 2.1.3 % 43.19/6.96 % (2268398)Termination reason: Refutation not found, incomplete strategy % 43.19/6.96 % (2268398)Time elapsed: 0.001 s % 43.19/6.96 % (2268398)Peak memory usage: 87 MB % 43.19/6.96 % (2268392)Refutation not found, incomplete strategy % 43.19/6.96 % (2268392)------------------------------ % 43.19/6.96 % (2268392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 43.19/6.96 % (2268392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 43.19/6.96 % (2268392)CaDiCaL version: 2.1.3 % 43.19/6.96 % (2268392)Termination reason: Refutation not found, incomplete strategy % 46.30/7.14 % (2268392)Time elapsed: 0.548 s % 46.30/7.14 % (2268392)Peak memory usage: 125 MB % 46.30/7.14 % (2268392)Instructions burned: 822 (million) % 46.30/7.14 % (2268398)------------------------------ % 46.30/7.14 % (2268398)------------------------------ % 46.30/7.14 % (2268392)------------------------------ % 46.30/7.14 % (2268392)------------------------------ % 46.30/7.14 % (2268400)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2862657520:i=14123:bd=preordered:ins=4_2953 on theBenchmark for (2953ds/14123Mi) % 46.30/7.14 % (2268379)Instruction limit reached! % 46.30/7.14 % (2268379)------------------------------ % 46.30/7.14 % (2268379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.30/7.14 % (2268379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.30/7.14 % (2268379)CaDiCaL version: 2.1.3 % 46.30/7.14 % (2268379)Termination reason: Instruction limit % 46.30/7.14 % (2268379)Termination phase: Saturation % 46.30/7.14 % (2268379)Time elapsed: 2.217 s % 46.30/7.14 % (2268379)Peak memory usage: 111 MB % 46.30/7.14 % (2268379)Instructions burned: 3707 (million) % 46.30/7.14 % (2268401)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2016905687:i=5781:kws=precedence:bd=all:rawr=on_2951 on theBenchmark for (2951ds/5781Mi) % 46.30/7.14 % (2268404)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=2018440703:i=2448:gtgl=5:bd=preordered:gtg=all_2950 on theBenchmark for (2950ds/2448Mi) % 46.30/7.14 % (2268358)Instruction limit reached! % 46.30/7.14 % (2268358)------------------------------ % 46.30/7.14 % (2268358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.30/7.14 % (2268358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.30/7.14 % (2268358)CaDiCaL version: 2.1.3 % 46.30/7.14 % (2268358)Termination reason: Instruction limit % 46.30/7.14 % (2268358)Termination phase: Saturation % 46.30/7.14 % (2268358)Time elapsed: 3.689 s % 46.30/7.14 % (2268358)Peak memory usage: 164 MB % 46.30/7.14 % (2268358)Instructions burned: 6061 (million) % 46.30/7.14 % (2268406)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=72115199:i=3223:kws=precedence:fgj=on:av=off_2945 on theBenchmark for (2945ds/3223Mi) % 46.30/7.14 % (2268393)Instruction limit reached! % 46.30/7.14 % (2268393)------------------------------ % 46.30/7.14 % (2268393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.30/7.14 % (2268393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.30/7.14 % (2268393)CaDiCaL version: 2.1.3 % 46.30/7.14 % (2268393)Termination reason: Instruction limit % 46.30/7.14 % (2268393)Termination phase: Saturation % 46.30/7.14 % (2268393)Time elapsed: 1.776 s % 46.30/7.14 % (2268393)Peak memory usage: 136 MB % 46.30/7.14 % (2268393)Instructions burned: 3034 (million) % 46.30/7.14 % (2268363)Instruction limit reached! % 46.30/7.14 % (2268363)------------------------------ % 46.30/7.14 % (2268363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 46.30/7.14 % (2268363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 46.30/7.14 % (2268363)CaDiCaL version: 2.1.3 % 46.30/7.14 % (2268363)Termination reason: Instruction limit % 46.30/7.14 % (2268363)Termination phase: Saturation % 46.30/7.14 % (2268363)Time elapsed: 4.001 s % 46.30/7.14 % (2268363)Peak memory usage: 262 MB % 46.30/7.14 % (2268363)Instructions burned: 14157 (million) % 46.30/7.14 % (2268408)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3873793162:st=5.6:i=2033:sd=3:ss=axioms_2941 on theBenchmark for (2941ds/2033Mi) % 46.30/7.14 % (2268409)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2343886868:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2940 on theBenchmark for (2940ds/2055Mi) % 46.30/7.14 [W928 09:34:32.194896992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 46.30/7.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 46.30/7.14 [W928 09:34:32.194933897 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.194954397 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.194972835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.194986181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.194991614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.195012527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.195018450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.195032097 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.195037824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.195050682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.195056155 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.294912395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.294949305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 48.01/7.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.01/7.57 [W928 09:34:32.294986881 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295011178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295041628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295096835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295132468 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295144201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295169048 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295180188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295204861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 [W928 09:34:32.295216271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 50.26/7.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 50.26/7.99 % (2268409)Refutation not found, incomplete strategy % 50.26/7.99 % (2268409)------------------------------ % 50.26/7.99 % (2268409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.26/7.99 % (2268409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.26/7.99 % (2268409)CaDiCaL version: 2.1.3 % 50.26/7.99 % (2268409)Termination reason: Refutation not found, incomplete strategy % 50.26/7.99 % (2268409)Time elapsed: 0.311 s % 50.26/7.99 % (2268409)Peak memory usage: 125 MB % 50.26/7.99 % (2268409)Instructions burned: 826 (million) % 50.26/7.99 % (2268404)Instruction limit reached! % 50.26/7.99 % (2268404)------------------------------ % 50.26/7.99 % (2268404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 50.26/7.99 % (2268404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.26/7.99 % (2268404)CaDiCaL version: 2.1.3 % 50.26/7.99 % (2268404)Termination reason: Instruction limit % 50.26/7.99 % (2268404)Termination phase: Saturation % 50.26/7.99 % (2268404)Time elapsed: 1.364 s % 50.26/7.99 % (2268404)Peak memory usage: 141 MB % 50.26/7.99 % (2268404)Instructions burned: 2450 (million) % 50.26/7.99 % (2268409)------------------------------ % 50.26/7.99 % (2268409)------------------------------ % 50.26/7.99 % (2268408)Refutation not found, incomplete strategy % 50.26/7.99 % (2268408)------------------------------ % 55.65/8.65 % (2268408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.65/8.65 % (2268408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.65/8.65 % (2268408)CaDiCaL version: 2.1.3 % 55.65/8.65 % (2268408)Termination reason: Refutation not found, incomplete strategy % 55.65/8.65 % (2268408)Time elapsed: 0.559 s % 55.65/8.65 % (2268408)Peak memory usage: 125 MB % 55.65/8.65 % (2268408)Instructions burned: 822 (million) % 55.65/8.65 % (2268412)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=4273666581:i=21611:sd=3:ss=axioms_2935 on theBenchmark for (2935ds/21611Mi) % 55.65/8.65 % (2268413)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2374691374:i=4835:sd=13:ss=axioms:sgt=23_2934 on theBenchmark for (2934ds/4835Mi) % 55.65/8.65 % (2268413)Refutation not found, incomplete strategy % 55.65/8.65 % (2268413)------------------------------ % 55.65/8.65 % (2268413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.65/8.65 % (2268413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.65/8.65 % (2268413)CaDiCaL version: 2.1.3 % 55.65/8.65 % (2268413)Termination reason: Refutation not found, incomplete strategy % 55.65/8.65 % (2268413)Time elapsed: 0.001 s % 55.65/8.65 % (2268413)Peak memory usage: 86 MB % 55.65/8.65 % (2268408)------------------------------ % 55.65/8.65 % (2268408)------------------------------ % 55.65/8.65 % (2268416)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=1291652151:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2933 on theBenchmark for (2933ds/797Mi) % 55.65/8.65 % (2268416)Refutation not found, incomplete strategy % 55.65/8.65 % (2268416)------------------------------ % 55.65/8.65 % (2268416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.65/8.65 % (2268416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.65/8.65 % (2268416)CaDiCaL version: 2.1.3 % 55.65/8.65 % (2268416)Termination reason: Refutation not found, incomplete strategy % 55.65/8.65 % (2268416)Time elapsed: 0.0000 s % 55.65/8.65 % (2268416)Peak memory usage: 86 MB % 55.65/8.65 % (2268416)Instructions burned: 1 (million) % 55.65/8.65 % (2268413)------------------------------ % 55.65/8.65 % (2268413)------------------------------ % 55.65/8.65 % (2268416)------------------------------ % 55.65/8.65 % (2268416)------------------------------ % 55.65/8.65 [W928 09:34:33.909961894 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.65/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.65/8.65 [W928 09:34:33.910017177 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.65/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.65/8.65 [W928 09:34:33.910056604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.65/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.65/8.65 [W928 09:34:33.910070224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.65/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.65/8.65 [W928 09:34:33.910096041 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.65/8.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.65/8.65 [W928 09:34:33.910108717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 [W928 09:34:33.910135107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 [W928 09:34:33.910146271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 [W928 09:34:33.910170481 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 [W928 09:34:33.910181404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 [W928 09:34:33.910206364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 [W928 09:34:33.910217311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.38/9.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.38/9.32 % (2268419)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1467908733:i=6038:nm=6_2930 on theBenchmark for (2930ds/6038Mi) % 61.38/9.32 % (2268418)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1800670383:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2931 on theBenchmark for (2931ds/2326Mi) % 61.38/9.32 % (2268418)Refutation not found, incomplete strategy % 61.38/9.32 % (2268418)------------------------------ % 61.38/9.32 % (2268418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.38/9.32 % (2268418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.38/9.32 % (2268418)CaDiCaL version: 2.1.3 % 61.38/9.32 % (2268418)Termination reason: Refutation not found, incomplete strategy % 61.38/9.32 % (2268418)Time elapsed: 0.010 s % 61.38/9.32 % (2268418)Peak memory usage: 88 MB % 61.38/9.32 % (2268418)Instructions burned: 16 (million) % 61.38/9.32 % (2268412)Refutation not found, incomplete strategy % 61.38/9.32 % (2268412)------------------------------ % 61.38/9.32 % (2268412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.38/9.32 % (2268412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.38/9.32 % (2268412)CaDiCaL version: 2.1.3 % 61.38/9.32 % (2268412)Termination reason: Refutation not found, incomplete strategy % 61.38/9.32 % (2268412)Time elapsed: 0.555 s % 61.38/9.32 % (2268412)Peak memory usage: 125 MB % 61.38/9.32 % (2268412)Instructions burned: 826 (million) % 61.38/9.32 % (2268418)------------------------------ % 61.38/9.32 % (2268418)------------------------------ % 61.38/9.32 % (2268419)Refutation not found, incomplete strategy % 61.38/9.32 % (2268419)------------------------------ % 61.38/9.32 % (2268419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.38/9.32 % (2268419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.38/9.32 % (2268419)CaDiCaL version: 2.1.3 % 61.38/9.32 % (2268419)Termination reason: Refutation not found, incomplete strategy % 61.38/9.32 % (2268419)Time elapsed: 0.333 s % 61.38/9.32 % (2268419)Peak memory usage: 128 MB % 61.38/9.32 % (2268419)Instructions burned: 858 (million) % 61.38/9.32 % (2268412)------------------------------ % 61.38/9.32 % (2268412)------------------------------ % 62.07/9.48 % (2268422)lrs+10_1_sil=32000:sp=occurrence:random_seed=2911769609:st=2:i=33334:sd=3:ss=included:sgt=32_2927 on theBenchmark for (2927ds/33334Mi) % 62.07/9.48 % (2268422)Refutation not found, incomplete strategy % 62.07/9.48 % (2268422)------------------------------ % 62.07/9.48 % (2268422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.07/9.48 % (2268422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.07/9.48 % (2268422)CaDiCaL version: 2.1.3 % 62.07/9.48 % (2268422)Termination reason: Refutation not found, incomplete strategy % 62.07/9.48 % (2268422)Time elapsed: 0.001 s % 62.07/9.48 % (2268422)Peak memory usage: 86 MB % 62.07/9.48 % (2268423)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=625639168:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2926 on theBenchmark for (2926ds/1008Mi) % 62.07/9.48 % (2268423)Refutation not found, incomplete strategy % 62.07/9.48 % (2268423)------------------------------ % 62.07/9.48 % (2268423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.07/9.48 % (2268423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.07/9.48 % (2268423)CaDiCaL version: 2.1.3 % 62.07/9.48 % (2268423)Termination reason: Refutation not found, incomplete strategy % 62.07/9.48 % (2268423)Time elapsed: 0.001 s % 62.07/9.48 % (2268423)Peak memory usage: 86 MB % 62.07/9.48 % (2268419)------------------------------ % 62.07/9.48 % (2268419)------------------------------ % 62.07/9.48 % (2268426)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=2282357704:i=8327:s2at=5:bd=preordered_2924 on theBenchmark for (2924ds/8327Mi) % 62.07/9.48 % (2268422)------------------------------ % 62.07/9.48 % (2268422)------------------------------ % 62.07/9.48 % (2268423)------------------------------ % 62.07/9.48 % (2268423)------------------------------ % 62.07/9.48 % (2268428)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=62945666:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2923 on theBenchmark for (2923ds/1083Mi) % 62.07/9.48 % (2268406)Instruction limit reached! % 62.07/9.48 % (2268406)------------------------------ % 62.07/9.48 % (2268406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.07/9.48 % (2268406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.07/9.48 % (2268406)CaDiCaL version: 2.1.3 % 62.07/9.48 % (2268406)Termination reason: Instruction limit % 62.07/9.48 % (2268406)Termination phase: Saturation % 62.07/9.48 % (2268406)Time elapsed: 2.244 s % 62.07/9.48 % (2268406)Peak memory usage: 147 MB % 62.07/9.48 % (2268406)Instructions burned: 3224 (million) % 62.07/9.48 % (2268429)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3934142472:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2922 on theBenchmark for (2922ds/1084Mi) % 62.07/9.48 % (2268429)Refutation not found, incomplete strategy % 62.07/9.48 % (2268429)------------------------------ % 62.07/9.48 % (2268429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.07/9.48 % (2268429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.07/9.48 % (2268429)CaDiCaL version: 2.1.3 % 62.07/9.48 % (2268429)Termination reason: Refutation not found, incomplete strategy % 62.07/9.48 % (2268429)Time elapsed: 0.001 s % 62.07/9.48 % (2268429)Peak memory usage: 86 MB % 62.07/9.48 % (2268401)Instruction limit reached! % 62.07/9.48 % (2268401)------------------------------ % 62.07/9.48 % (2268401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.07/9.48 % (2268401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.07/9.48 % (2268401)CaDiCaL version: 2.1.3 % 62.07/9.48 % (2268401)Termination reason: Instruction limit % 62.07/9.48 % (2268401)Termination phase: Saturation % 62.07/9.48 % (2268401)Time elapsed: 2.951 s % 62.07/9.48 % (2268401)Peak memory usage: 148 MB % 62.07/9.48 % (2268401)Instructions burned: 5783 (million) % 62.07/9.48 % (2268432)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2873127014:i=6995:s2at=5:gtg=all_2921 on theBenchmark for (2921ds/6995Mi) % 62.07/9.48 % (2268433)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=840369625:st=2:i=6225:sd=15:ss=axioms_2921 on theBenchmark for (2921ds/6225Mi) % 67.75/10.22 % (2268433)Refutation not found, incomplete strategy % 67.75/10.22 % (2268433)------------------------------ % 67.75/10.22 % (2268433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.75/10.22 % (2268433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.75/10.22 % (2268433)CaDiCaL version: 2.1.3 % 67.75/10.22 % (2268433)Termination reason: Refutation not found, incomplete strategy % 67.75/10.22 % (2268433)Time elapsed: 0.001 s % 67.75/10.22 % (2268433)Peak memory usage: 86 MB % 67.75/10.22 % (2268429)------------------------------ % 67.75/10.22 % (2268429)------------------------------ % 67.75/10.22 % (2268436)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3848356114:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2919 on theBenchmark for (2919ds/3372Mi) % 67.75/10.22 % (2268428)Instruction limit reached! % 67.75/10.22 % (2268428)------------------------------ % 67.75/10.22 % (2268428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.75/10.22 % (2268428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.75/10.22 % (2268428)CaDiCaL version: 2.1.3 % 67.75/10.22 % (2268428)Termination reason: Instruction limit % 67.75/10.22 % (2268428)Termination phase: Saturation % 67.75/10.22 % (2268428)Time elapsed: 0.432 s % 67.75/10.22 % (2268428)Peak memory usage: 96 MB % 67.75/10.22 % (2268428)Instructions burned: 1085 (million) % 67.75/10.22 % (2268433)------------------------------ % 67.75/10.22 % (2268433)------------------------------ % 67.75/10.22 % (2268438)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1810867544:st=2.3:i=26457:sd=10:ss=included:sgt=8_2917 on theBenchmark for (2917ds/26457Mi) % 67.75/10.22 % (2268439)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=666724385:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2917 on theBenchmark for (2917ds/13494Mi) % 67.75/10.22 [W928 09:34:35.652500648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652547298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652583705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652601085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652626032 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652638182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652665615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 67.75/10.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.75/10.22 [W928 09:34:35.652677925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.652703392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.652714428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.652754132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.652765345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816773026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816810500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816847850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816859810 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816884696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816896776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816921306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816932450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.46/10.40 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.46/10.40 [W928 09:34:35.816957153 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:35.816968260 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:35.816999503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:35.817021080 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 % (2268436)Refutation not found, incomplete strategy % 73.67/11.06 % (2268436)------------------------------ % 73.67/11.06 % (2268436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.67/11.06 % (2268436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.67/11.06 % (2268436)CaDiCaL version: 2.1.3 % 73.67/11.06 % (2268436)Termination reason: Refutation not found, incomplete strategy % 73.67/11.06 % (2268436)Time elapsed: 0.622 s % 73.67/11.06 % (2268436)Peak memory usage: 126 MB % 73.67/11.06 % (2268436)Instructions burned: 827 (million) % 73.67/11.06 % (2268438)Refutation not found, incomplete strategy % 73.67/11.06 % (2268438)------------------------------ % 73.67/11.06 % (2268438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 73.67/11.06 % (2268438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 73.67/11.06 % (2268438)CaDiCaL version: 2.1.3 % 73.67/11.06 % (2268438)Termination reason: Refutation not found, incomplete strategy % 73.67/11.06 % (2268438)Time elapsed: 0.638 s % 73.67/11.06 % (2268438)Peak memory usage: 125 MB % 73.67/11.06 % (2268438)Instructions burned: 822 (million) % 73.67/11.06 % (2268436)------------------------------ % 73.67/11.06 % (2268436)------------------------------ % 73.67/11.06 % (2268442)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=3321672897:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2909 on theBenchmark for (2909ds/2503Mi) % 73.67/11.06 % (2268438)------------------------------ % 73.67/11.06 % (2268438)------------------------------ % 73.67/11.06 % (2268444)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=539438316:i=2559:sd=1:ep=RSTC:ss=axioms_2907 on theBenchmark for (2907ds/2559Mi) % 73.67/11.06 [W928 09:34:36.560763747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:36.560798360 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:36.560836147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:36.560848300 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.67/11.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.67/11.06 [W928 09:34:36.560878687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.560890857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.560922110 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.560933000 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.560957024 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.560967857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.560992320 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.561014597 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 % (2268442)Refutation not found, incomplete strategy % 75.24/11.36 % (2268442)------------------------------ % 75.24/11.36 % (2268442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.24/11.36 % (2268442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.24/11.36 % (2268442)CaDiCaL version: 2.1.3 % 75.24/11.36 % (2268442)Termination reason: Refutation not found, incomplete strategy % 75.24/11.36 % (2268442)Time elapsed: 0.542 s % 75.24/11.36 % (2268442)Peak memory usage: 125 MB % 75.24/11.36 % (2268442)Instructions burned: 824 (million) % 75.24/11.36 [W928 09:34:36.732610555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.732642555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.732681339 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.24/11.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.24/11.36 [W928 09:34:36.732694859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732720795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732732175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732757069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732768315 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732792695 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732803786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732829186 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 [W928 09:34:36.732840466 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 79.20/11.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 79.20/11.93 % (2268444)Refutation not found, incomplete strategy % 79.20/11.93 % (2268444)------------------------------ % 79.20/11.93 % (2268444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.20/11.93 % (2268444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.20/11.93 % (2268444)CaDiCaL version: 2.1.3 % 79.20/11.93 % (2268444)Termination reason: Refutation not found, incomplete strategy % 79.20/11.93 % (2268444)Time elapsed: 0.550 s % 79.20/11.93 % (2268444)Peak memory usage: 125 MB % 79.20/11.93 % (2268444)Instructions burned: 825 (million) % 79.20/11.93 % (2268442)------------------------------ % 79.20/11.93 % (2268442)------------------------------ % 79.20/11.93 % (2268446)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3530982159:i=30753:av=off:ss=included_2899 on theBenchmark for (2899ds/30753Mi) % 79.20/11.93 % (2268444)------------------------------ % 79.20/11.93 % (2268444)------------------------------ % 79.20/11.93 % (2268448)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1564296077:i=26473:ep=RSTC_2898 on theBenchmark for (2898ds/26473Mi) % 79.20/11.93 % (2268426)Instruction limit reached! % 79.20/11.93 % (2268426)------------------------------ % 79.20/11.93 % (2268426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 79.20/11.93 % (2268426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 79.20/11.93 % (2268426)CaDiCaL version: 2.1.3 % 79.20/11.93 % (2268426)Termination reason: Instruction limit % 79.20/11.93 % (2268426)Termination phase: Saturation % 79.20/11.93 % (2268426)Time elapsed: 2.810 s % 79.20/11.93 % (2268426)Peak memory usage: 191 MB % 80.66/12.12 % (2268426)Instructions burned: 8329 (million) % 80.66/12.12 % (2268450)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=2402129108:cts=off:i=2759:kws=inv_arity:fgj=on_2895 on theBenchmark for (2895ds/2759Mi) % 80.66/12.12 [W928 09:34:37.523799907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523833510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523871994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523885521 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523914007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523926374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523952767 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523964741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.523990844 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.524013157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.524049467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 [W928 09:34:37.524061974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 80.66/12.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 80.66/12.12 % (2268446)Refutation not found, incomplete strategy % 83.06/12.47 % (2268446)------------------------------ % 83.06/12.47 % (2268446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.47 % (2268446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.47 % (2268446)CaDiCaL version: 2.1.3 % 83.06/12.47 % (2268446)Termination reason: Refutation not found, incomplete strategy % 83.06/12.47 % (2268446)Time elapsed: 0.596 s % 83.06/12.47 % (2268446)Peak memory usage: 125 MB % 83.06/12.47 % (2268446)Instructions burned: 825 (million) % 83.06/12.47 % (2268450)Refutation not found, incomplete strategy % 83.06/12.47 % (2268450)------------------------------ % 83.06/12.47 % (2268450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.06/12.47 % (2268450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.06/12.47 % (2268450)CaDiCaL version: 2.1.3 % 83.06/12.47 % (2268450)Termination reason: Refutation not found, incomplete strategy % 83.06/12.47 % (2268450)Time elapsed: 0.335 s % 83.06/12.47 % (2268450)Peak memory usage: 128 MB % 83.06/12.47 % (2268450)Instructions burned: 854 (million) % 83.06/12.47 % (2268446)------------------------------ % 83.06/12.47 % (2268446)------------------------------ % 83.06/12.47 % (2268450)------------------------------ % 83.06/12.47 % (2268450)------------------------------ % 83.06/12.47 % (2268453)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=2061254619:i=1532:ep=RS:ss=axioms_2889 on theBenchmark for (2889ds/1532Mi) % 83.06/12.47 % (2268452)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=2229526559:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2890 on theBenchmark for (2890ds/5665Mi) % 83.06/12.47 [W928 09:34:37.270309152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270331242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270352063 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270362638 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270376384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270382835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270395896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.06/12.47 [W928 09:34:37.270402151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.06/12.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:37.270414759 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:37.270420308 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:37.270433232 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:37.270445428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 % (2268453)Refutation not found, incomplete strategy % 86.20/13.01 % (2268453)------------------------------ % 86.20/13.01 % (2268453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.20/13.01 % (2268453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.20/13.01 % (2268453)CaDiCaL version: 2.1.3 % 86.20/13.01 % (2268453)Termination reason: Refutation not found, incomplete strategy % 86.20/13.01 % (2268453)Time elapsed: 0.296 s % 86.20/13.01 % (2268453)Peak memory usage: 126 MB % 86.20/13.01 % (2268453)Instructions burned: 825 (million) % 86.20/13.01 [W928 09:34:38.455270158 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455306774 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455345351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455358994 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455385161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455397518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455423161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.20/13.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.20/13.01 [W928 09:34:38.455435294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.455459684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.455483038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.455508718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.455519945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 % (2268453)------------------------------ % 88.53/13.15 % (2268453)------------------------------ % 88.53/13.15 % (2268456)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=963898723:i=1565:sd=2:ss=axioms:sgt=32_2884 on theBenchmark for (2884ds/1565Mi) % 88.53/13.15 % (2268452)Refutation not found, incomplete strategy % 88.53/13.15 % (2268452)------------------------------ % 88.53/13.15 % (2268452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.53/13.15 % (2268452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.53/13.15 % (2268452)CaDiCaL version: 2.1.3 % 88.53/13.15 % (2268452)Termination reason: Refutation not found, incomplete strategy % 88.53/13.15 % (2268452)Time elapsed: 0.544 s % 88.53/13.15 % (2268452)Peak memory usage: 126 MB % 88.53/13.15 % (2268452)Instructions burned: 822 (million) % 88.53/13.15 [W928 09:34:38.806096888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.806121051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.806142332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.806148867 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.806162304 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.53/13.15 [W928 09:34:38.806169005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.53/13.15 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 [W928 09:34:38.806182400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 [W928 09:34:38.806188065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 [W928 09:34:38.806200758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 [W928 09:34:38.806242897 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 [W928 09:34:38.806270681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 [W928 09:34:38.806287248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.94/13.29 % (2268452)------------------------------ % 88.94/13.29 % (2268452)------------------------------ % 88.94/13.29 % (2268456)Refutation not found, incomplete strategy % 88.94/13.29 % (2268456)------------------------------ % 88.94/13.29 % (2268456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.94/13.29 % (2268456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.94/13.29 % (2268456)CaDiCaL version: 2.1.3 % 88.94/13.29 % (2268456)Termination reason: Refutation not found, incomplete strategy % 88.94/13.29 % (2268456)Time elapsed: 0.297 s % 88.94/13.29 % (2268456)Peak memory usage: 125 MB % 88.94/13.29 % (2268456)Instructions burned: 822 (million) % 88.94/13.29 % (2268458)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=125853497:i=1572:fgj=on:gsp=on_2880 on theBenchmark for (2880ds/1572Mi) % 88.94/13.29 % (2268456)------------------------------ % 88.94/13.29 % (2268456)------------------------------ % 88.94/13.29 % (2268432)Instruction limit reached! % 88.94/13.29 % (2268432)------------------------------ % 88.94/13.29 % (2268432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.94/13.29 % (2268432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.94/13.29 % (2268432)CaDiCaL version: 2.1.3 % 88.94/13.29 % (2268432)Termination reason: Instruction limit % 88.94/13.29 % (2268432)Termination phase: Saturation % 88.94/13.29 % (2268432)Time elapsed: 4.153 s % 88.94/13.29 % (2268432)Peak memory usage: 163 MB % 88.94/13.29 % (2268432)Instructions burned: 6995 (million) % 88.94/13.29 % (2268460)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=461716899:i=6052:sd=4:ss=axioms:sgt=24_2879 on theBenchmark for (2879ds/6052Mi) % 88.94/13.29 % (2268461)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=2748566489:i=3500:sd=1:bd=preordered:sup=off:ss=included_2878 on theBenchmark for (2878ds/3500Mi) % 88.94/13.29 [W928 09:34:38.343355748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.94/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343383724 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343405127 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343411433 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343425131 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343430671 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343444397 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343450034 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343463531 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343469170 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343482294 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 [W928 09:34:38.343487834 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/13.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.06/13.69 % (2268460)Refutation not found, incomplete strategy % 91.06/13.69 % (2268460)------------------------------ % 91.06/13.69 % (2268460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.06/13.69 % (2268460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.06/13.69 % (2268460)CaDiCaL version: 2.1.3 % 91.06/13.69 % (2268460)Termination reason: Refutation not found, incomplete strategy % 91.06/13.69 % (2268460)Time elapsed: 0.314 s % 91.06/13.69 % (2268460)Peak memory usage: 125 MB % 91.06/13.69 % (2268460)Instructions burned: 826 (million) % 91.06/13.69 % (2268400)Instruction limit reached! % 91.06/13.69 % (2268400)------------------------------ % 91.06/13.69 % (2268400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.55/14.19 % (2268400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.55/14.19 % (2268400)CaDiCaL version: 2.1.3 % 95.55/14.19 % (2268400)Termination reason: Instruction limit % 95.55/14.19 % (2268400)Termination phase: Saturation % 95.55/14.19 % (2268400)Time elapsed: 7.697 s % 95.55/14.19 % (2268400)Peak memory usage: 240 MB % 95.55/14.19 % (2268400)Instructions burned: 14124 (million) % 95.55/14.19 % (2268460)------------------------------ % 95.55/14.19 % (2268460)------------------------------ % 95.55/14.19 [W928 09:34:39.627574422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627620468 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627659792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627671678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627696218 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627707298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627737092 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627748322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627774182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627785529 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627812375 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.55/14.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.55/14.19 [W928 09:34:39.627825069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 % (2268464)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=2602031030:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2874 on theBenchmark for (2874ds/1842Mi) % 101.95/15.11 % (2268465)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3247538114:i=66096:add=on_2873 on theBenchmark for (2873ds/66096Mi) % 101.95/15.11 % (2268461)Refutation not found, incomplete strategy % 101.95/15.11 % (2268461)------------------------------ % 101.95/15.11 % (2268461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.95/15.11 % (2268461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.95/15.11 % (2268461)CaDiCaL version: 2.1.3 % 101.95/15.11 % (2268461)Termination reason: Refutation not found, incomplete strategy % 101.95/15.11 % (2268461)Time elapsed: 0.550 s % 101.95/15.11 % (2268461)Peak memory usage: 125 MB % 101.95/15.11 % (2268461)Instructions burned: 826 (million) % 101.95/15.11 [W928 09:34:39.026320621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026360061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026397044 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026410367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026436681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026448731 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026474347 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026486144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026511974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.95/15.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.95/15.11 [W928 09:34:39.026523701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:39.026549131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:39.026560111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 % (2268458)Instruction limit reached! % 105.78/15.66 % (2268458)------------------------------ % 105.78/15.66 % (2268458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.78/15.66 % (2268458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.78/15.66 % (2268458)CaDiCaL version: 2.1.3 % 105.78/15.66 % (2268458)Termination reason: Instruction limit % 105.78/15.66 % (2268458)Termination phase: Saturation % 105.78/15.66 % (2268458)Time elapsed: 1.024 s % 105.78/15.66 % (2268458)Peak memory usage: 134 MB % 105.78/15.66 % (2268458)Instructions burned: 1573 (million) % 105.78/15.66 % (2268461)------------------------------ % 105.78/15.66 % (2268461)------------------------------ % 105.78/15.66 % (2268468)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2756908860:i=1884:sd=1:nm=60:ss=axioms_2869 on theBenchmark for (2869ds/1884Mi) % 105.78/15.66 % (2268469)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3462053871:cts=off:i=5469:bs=on:fsr=off_2869 on theBenchmark for (2869ds/5469Mi) % 105.78/15.66 % (2268464)Refutation not found, incomplete strategy % 105.78/15.66 % (2268464)------------------------------ % 105.78/15.66 % (2268464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.78/15.66 % (2268464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.78/15.66 % (2268464)CaDiCaL version: 2.1.3 % 105.78/15.66 % (2268464)Termination reason: Refutation not found, incomplete strategy % 105.78/15.66 % (2268464)Time elapsed: 0.548 s % 105.78/15.66 % (2268464)Peak memory usage: 125 MB % 105.78/15.66 % (2268464)Instructions burned: 828 (million) % 105.78/15.66 % (2268464)------------------------------ % 105.78/15.66 % (2268464)------------------------------ % 105.78/15.66 [W928 09:34:40.529809758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:40.529858331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:40.529896388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:40.529909791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:40.529934531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 105.78/15.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.78/15.66 [W928 09:34:40.529947271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:40.529972498 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:40.529982992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:40.530018175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:40.530030228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:40.530056138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:40.530066448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 % (2268472)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=5979073:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2865 on theBenchmark for (2865ds/2037Mi) % 117.65/17.33 % (2268468)Refutation not found, incomplete strategy % 117.65/17.33 % (2268468)------------------------------ % 117.65/17.33 % (2268468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 117.65/17.33 % (2268468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 117.65/17.33 % (2268468)CaDiCaL version: 2.1.3 % 117.65/17.33 % (2268468)Termination reason: Refutation not found, incomplete strategy % 117.65/17.33 % (2268468)Time elapsed: 0.546 s % 117.65/17.33 % (2268468)Peak memory usage: 125 MB % 117.65/17.33 % (2268468)Instructions burned: 824 (million) % 117.65/17.33 % (2268468)------------------------------ % 117.65/17.33 % (2268468)------------------------------ % 117.65/17.33 % (2268474)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2527932459:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2860 on theBenchmark for (2860ds/2110Mi) % 117.65/17.33 [W928 09:34:41.446174698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:41.446210011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:41.446247878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 117.65/17.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 117.65/17.33 [W928 09:34:41.446261221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446286308 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446297414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446322478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446333538 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446357455 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446368738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446393181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:41.446404271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 % (2268474)Refutation not found, incomplete strategy % 119.14/17.60 % (2268474)------------------------------ % 119.14/17.60 % (2268474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.14/17.60 % (2268474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.14/17.60 % (2268474)CaDiCaL version: 2.1.3 % 119.14/17.60 % (2268474)Termination reason: Refutation not found, incomplete strategy % 119.14/17.60 % (2268474)Time elapsed: 0.543 s % 119.14/17.60 % (2268474)Peak memory usage: 125 MB % 119.14/17.60 % (2268474)Instructions burned: 825 (million) % 119.14/17.60 % (2268472)Instruction limit reached! % 119.14/17.60 % (2268472)------------------------------ % 119.14/17.60 % (2268472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.14/17.60 % (2268472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.14/17.60 % (2268472)CaDiCaL version: 2.1.3 % 119.14/17.60 % (2268472)Termination reason: Instruction limit % 119.14/17.60 % (2268472)Termination phase: Saturation % 119.14/17.60 % (2268472)Time elapsed: 1.239 s % 119.14/17.60 % (2268472)Peak memory usage: 139 MB % 119.14/17.60 % (2268472)Instructions burned: 2039 (million) % 119.14/17.60 % (2268474)------------------------------ % 119.14/17.60 % (2268474)------------------------------ % 119.14/17.60 % (2268476)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=4286825666:i=2430:add=off:aac=none:nm=16_2851 on theBenchmark for (2851ds/2430Mi) % 119.14/17.60 % (2268477)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=3941443715:cond=fast:i=4891_2851 on theBenchmark for (2851ds/4891Mi) % 119.14/17.60 % (2268439)Instruction limit reached! % 119.14/17.60 % (2268439)------------------------------ % 119.14/17.60 % (2268439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.14/17.60 % (2268439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.14/17.60 % (2268439)CaDiCaL version: 2.1.3 % 119.14/17.60 % (2268439)Termination reason: Instruction limit % 119.14/17.60 % (2268439)Termination phase: Saturation % 119.14/17.60 % (2268439)Time elapsed: 7.789 s % 119.14/17.60 % (2268439)Peak memory usage: 251 MB % 119.14/17.60 % (2268439)Instructions burned: 13494 (million) % 119.14/17.60 % (2268480)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=1803127666:st=2:i=14845:sd=2:ss=included:fsd=on_2838 on theBenchmark for (2838ds/14845Mi) % 119.14/17.60 % (2268469)Instruction limit reached! % 119.14/17.60 % (2268469)------------------------------ % 119.14/17.60 % (2268469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.14/17.60 % (2268469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.14/17.60 % (2268469)CaDiCaL version: 2.1.3 % 119.14/17.60 % (2268469)Termination reason: Instruction limit % 119.14/17.60 % (2268469)Termination phase: Saturation % 119.14/17.60 % (2268469)Time elapsed: 3.253 s % 119.14/17.60 % (2268469)Peak memory usage: 116 MB % 119.14/17.60 % (2268469)Instructions burned: 5469 (million) % 119.14/17.60 % (2268476)Instruction limit reached! % 119.14/17.60 % (2268476)------------------------------ % 119.14/17.60 % (2268476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 119.14/17.60 % (2268476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 119.14/17.60 % (2268476)CaDiCaL version: 2.1.3 % 119.14/17.60 % (2268476)Termination reason: Instruction limit % 119.14/17.60 % (2268476)Termination phase: Saturation % 119.14/17.60 % (2268476)Time elapsed: 1.496 s % 119.14/17.60 % (2268476)Peak memory usage: 143 MB % 119.14/17.60 % (2268476)Instructions burned: 2430 (million) % 119.14/17.60 % (2268482)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1751287448:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2835 on theBenchmark for (2835ds/7534Mi) % 119.14/17.60 % (2268483)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=14087610:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2835 on theBenchmark for (2835ds/10353Mi) % 119.14/17.60 [W928 09:34:43.669573642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:43.669606582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:43.669644002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:43.669655718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:43.669686708 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 119.14/17.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 119.14/17.60 [W928 09:34:43.669698765 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.669724282 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.669735238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.669758518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.669769285 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.669793485 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.669804275 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 % (2268480)Refutation not found, incomplete strategy % 123.78/18.16 % (2268480)------------------------------ % 123.78/18.16 % (2268480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.78/18.16 % (2268480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.78/18.16 % (2268480)CaDiCaL version: 2.1.3 % 123.78/18.16 % (2268480)Termination reason: Refutation not found, incomplete strategy % 123.78/18.16 % (2268480)Time elapsed: 0.544 s % 123.78/18.16 % (2268480)Peak memory usage: 125 MB % 123.78/18.16 % (2268480)Instructions burned: 822 (million) % 123.78/18.16 [W928 09:34:43.936597183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.936641613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.936678370 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.936695746 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.78/18.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.78/18.16 [W928 09:34:43.936722893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.53 [W928 09:34:43.936734550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.53 [W928 09:34:43.936759453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.53 [W928 09:34:43.936821817 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.936855653 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.936866993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.936891623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.936902657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.940136066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.940163546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.940200700 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.940214510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.940242096 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.23/18.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.23/18.54 [W928 09:34:43.940253926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 [W928 09:34:43.940280450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 [W928 09:34:43.940337893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 [W928 09:34:43.940372733 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 [W928 09:34:43.940384330 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 [W928 09:34:43.940408857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 [W928 09:34:43.940419170 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 132.56/19.45 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 132.56/19.45 % (2268480)------------------------------ % 132.56/19.45 % (2268480)------------------------------ % 132.56/19.45 % (2268483)Refutation not found, incomplete strategy % 132.56/19.45 % (2268483)------------------------------ % 132.56/19.45 % (2268483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.56/19.45 % (2268483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.56/19.45 % (2268483)CaDiCaL version: 2.1.3 % 132.56/19.45 % (2268483)Termination reason: Refutation not found, incomplete strategy % 132.56/19.45 % (2268483)Time elapsed: 0.535 s % 132.56/19.45 % (2268483)Peak memory usage: 125 MB % 132.56/19.45 % (2268483)Instructions burned: 821 (million) % 132.56/19.45 % (2268482)Refutation not found, incomplete strategy % 132.56/19.45 % (2268482)------------------------------ % 132.56/19.45 % (2268482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.56/19.45 % (2268482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.56/19.45 % (2268482)CaDiCaL version: 2.1.3 % 132.56/19.45 % (2268482)Termination reason: Refutation not found, incomplete strategy % 132.56/19.45 % (2268482)Time elapsed: 0.546 s % 132.56/19.45 % (2268482)Peak memory usage: 125 MB % 132.56/19.45 % (2268482)Instructions burned: 827 (million) % 132.56/19.45 % (2268486)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1829427600:i=7860_2828 on theBenchmark for (2828ds/7860Mi) % 132.56/19.45 % (2268486)Refutation not found, incomplete strategy % 132.56/19.45 % (2268486)------------------------------ % 132.56/19.45 % (2268486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 132.56/19.45 % (2268486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 132.56/19.45 % (2268486)CaDiCaL version: 2.1.3 % 132.56/19.45 % (2268486)Termination reason: Refutation not found, incomplete strategy % 132.56/19.45 % (2268486)Time elapsed: 0.006 s % 132.56/19.45 % (2268486)Peak memory usage: 88 MB % 132.56/19.45 % (2268486)Instructions burned: 10 (million) % 132.56/19.45 % (2268482)------------------------------ % 132.56/19.45 % (2268482)------------------------------ % 132.56/19.45 % (2268483)------------------------------ % 132.56/19.45 % (2268483)------------------------------ % 132.56/19.45 % (2268486)------------------------------ % 132.56/19.45 % (2268486)------------------------------ % 132.56/19.45 % (2268489)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=3132649657:i=5812:gtgl=2:gtg=all_2826 on theBenchmark for (2826ds/5812Mi) % 133.80/19.60 % (2268488)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=1535898909:i=7896:sd=2:bs=on:ss=included:sgt=20_2826 on theBenchmark for (2826ds/7896Mi) % 133.80/19.60 % (2268490)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=2057755493:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2825 on theBenchmark for (2825ds/2965Mi) % 133.80/19.60 [W928 09:34:44.871102023 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871136753 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871176580 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871190137 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871216920 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871229120 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871254640 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871266797 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871291623 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871303727 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871329807 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 133.80/19.60 [W928 09:34:44.871341967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.97/20.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.97/20.39 % (2268477)Instruction limit reached! % 138.97/20.39 % (2268477)------------------------------ % 138.97/20.39 % (2268477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.97/20.39 % (2268477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/20.39 % (2268477)CaDiCaL version: 2.1.3 % 138.97/20.39 % (2268477)Termination reason: Instruction limit % 138.97/20.39 % (2268477)Termination phase: Saturation % 138.97/20.39 % (2268477)Time elapsed: 2.909 s % 138.97/20.39 % (2268477)Peak memory usage: 155 MB % 138.97/20.39 % (2268477)Instructions burned: 4891 (million) % 138.97/20.39 % (2268494)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=1861666015:i=2967:kws=precedence:bd=preordered:av=off_2820 on theBenchmark for (2820ds/2967Mi) % 138.97/20.39 % (2268488)Refutation not found, incomplete strategy % 138.97/20.39 % (2268488)------------------------------ % 138.97/20.39 % (2268488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.97/20.39 % (2268488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/20.39 % (2268488)CaDiCaL version: 2.1.3 % 138.97/20.39 % (2268488)Termination reason: Refutation not found, incomplete strategy % 138.97/20.39 % (2268488)Time elapsed: 0.539 s % 138.97/20.39 % (2268488)Peak memory usage: 125 MB % 138.97/20.39 % (2268488)Instructions burned: 821 (million) % 138.97/20.39 % (2268490)Refutation not found, incomplete strategy % 138.97/20.39 % (2268490)------------------------------ % 138.97/20.39 % (2268490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 138.97/20.39 % (2268490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 138.97/20.39 % (2268490)CaDiCaL version: 2.1.3 % 138.97/20.39 % (2268490)Termination reason: Refutation not found, incomplete strategy % 138.97/20.39 % (2268490)Time elapsed: 0.569 s % 138.97/20.39 % (2268490)Peak memory usage: 128 MB % 138.97/20.39 % (2268490)Instructions burned: 859 (million) % 138.97/20.39 % (2268488)------------------------------ % 138.97/20.39 % (2268488)------------------------------ % 138.97/20.39 % (2268490)------------------------------ % 138.97/20.39 % (2268490)------------------------------ % 138.97/20.39 % (2268496)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=1069874684:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2816 on theBenchmark for (2816ds/3022Mi) % 138.97/20.39 % (2268498)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=967467218:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2815 on theBenchmark for (2815ds/3207Mi) % 138.97/20.39 [W928 09:34:45.790521906 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.97/20.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.97/20.39 [W928 09:34:45.790579672 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.97/20.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.97/20.39 [W928 09:34:45.790617266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.97/20.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.97/20.39 [W928 09:34:45.790629352 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 138.97/20.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 138.97/20.39 [W928 09:34:45.790655896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790668086 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790692366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790714269 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790739903 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790751099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790775446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.790786446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.936789710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.936836230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.936873887 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.936922084 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.936949344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.21/20.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.21/20.53 [W928 09:34:45.936960177 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:45.936985504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:45.936996424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:45.937091880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:45.937128217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:45.937170997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:45.937199017 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 % (2268496)Refutation not found, incomplete strategy % 140.75/20.64 % (2268496)------------------------------ % 140.75/20.64 % (2268496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.75/20.64 % (2268496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.64 % (2268496)CaDiCaL version: 2.1.3 % 140.75/20.64 % (2268496)Termination reason: Refutation not found, incomplete strategy % 140.75/20.64 % (2268496)Time elapsed: 0.545 s % 140.75/20.64 % (2268496)Peak memory usage: 125 MB % 140.75/20.64 % (2268496)Instructions burned: 822 (million) % 140.75/20.64 % (2268498)Refutation not found, incomplete strategy % 140.75/20.64 % (2268498)------------------------------ % 140.75/20.64 % (2268498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.75/20.64 % (2268498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.75/20.64 % (2268498)CaDiCaL version: 2.1.3 % 140.75/20.64 % (2268498)Termination reason: Refutation not found, incomplete strategy % 140.75/20.64 % (2268498)Time elapsed: 0.541 s % 140.75/20.64 % (2268498)Peak memory usage: 125 MB % 140.75/20.64 % (2268498)Instructions burned: 821 (million) % 140.75/20.64 % (2268496)------------------------------ % 140.75/20.64 % (2268496)------------------------------ % 140.75/20.64 % (2268500)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=987041393:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2807 on theBenchmark for (2807ds/3289Mi) % 140.75/20.64 % (2268498)------------------------------ % 140.75/20.64 % (2268498)------------------------------ % 140.75/20.64 % (2268502)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=1114695208:i=38569:sd=3:ss=axioms:sgt=32_2806 on theBenchmark for (2806ds/38569Mi) % 140.75/20.64 [W928 09:34:46.723370901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.75/20.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.75/20.64 [W928 09:34:46.723404691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723441678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723453344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723476628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723498668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723523298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723533238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723556394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723566428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723589648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 [W928 09:34:46.723599701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 159.83/23.20 % (2268494)Instruction limit reached! % 159.83/23.20 % (2268494)------------------------------ % 159.83/23.20 % (2268494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 159.83/23.20 % (2268494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 159.83/23.20 % (2268494)CaDiCaL version: 2.1.3 % 159.83/23.20 % (2268494)Termination reason: Instruction limit % 159.83/23.20 % (2268494)Termination phase: Saturation % 159.83/23.20 % (2268494)Time elapsed: 1.802 s % 159.83/23.20 % (2268494)Peak memory usage: 147 MB % 159.83/23.20 % (2268494)Instructions burned: 2968 (million) % 159.83/23.20 [W928 09:34:46.868059974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 159.83/23.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868175384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868239081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868270091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868312721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868339917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868382701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868411031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868451911 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868478947 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868520681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 [W928 09:34:46.868536258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 177.51/25.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 177.51/25.73 % (2268500)Refutation not found, incomplete strategy % 177.51/25.73 % (2268500)------------------------------ % 177.51/25.73 % (2268500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 177.51/25.73 % (2268500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 177.51/25.73 % (2268500)CaDiCaL version: 2.1.3 % 177.51/25.73 % (2268500)Termination reason: Refutation not found, incomplete strategy % 177.51/25.73 % (2268500)Time elapsed: 0.548 s % 177.51/25.73 % (2268500)Peak memory usage: 125 MB % 177.51/25.73 % (2268500)Instructions burned: 821 (million) % 177.51/25.73 % (2268504)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=3678464040:cts=off:i=3394_2801 on theBenchmark for (2801ds/3394Mi) % 180.64/26.19 % (2268502)Refutation not found, incomplete strategy % 180.64/26.19 % (2268502)------------------------------ % 180.64/26.19 % (2268502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.64/26.19 % (2268502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.64/26.19 % (2268502)CaDiCaL version: 2.1.3 % 180.64/26.19 % (2268502)Termination reason: Refutation not found, incomplete strategy % 180.64/26.19 % (2268502)Time elapsed: 0.547 s % 180.64/26.19 % (2268502)Peak memory usage: 125 MB % 180.64/26.19 % (2268502)Instructions burned: 825 (million) % 180.64/26.19 % (2268500)------------------------------ % 180.64/26.19 % (2268500)------------------------------ % 180.64/26.19 % (2268506)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=2175002782:i=33824:bd=preordered_2798 on theBenchmark for (2798ds/33824Mi) % 180.64/26.19 % (2268502)------------------------------ % 180.64/26.19 % (2268502)------------------------------ % 180.64/26.19 % (2268508)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=172829618:i=20684:bd=all:gtg=exists_sym_2796 on theBenchmark for (2796ds/20684Mi) % 180.64/26.19 % (2268489)Instruction limit reached! % 180.64/26.19 % (2268489)------------------------------ % 180.64/26.19 % (2268489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.64/26.19 % (2268489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.64/26.19 % (2268489)CaDiCaL version: 2.1.3 % 180.64/26.19 % (2268489)Termination reason: Instruction limit % 180.64/26.19 % (2268489)Termination phase: Saturation % 180.64/26.19 % (2268489)Time elapsed: 3.249 s % 180.64/26.19 % (2268489)Peak memory usage: 177 MB % 180.64/26.19 % (2268489)Instructions burned: 5812 (million) % 180.64/26.19 % (2268510)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=2876493474:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2792 on theBenchmark for (2792ds/7222Mi) % 180.64/26.19 % (2268504)Instruction limit reached! % 180.64/26.19 % (2268504)------------------------------ % 180.64/26.19 % (2268504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 180.64/26.19 % (2268504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 180.64/26.19 % (2268504)CaDiCaL version: 2.1.3 % 180.64/26.19 % (2268504)Termination reason: Instruction limit % 180.64/26.19 % (2268504)Termination phase: Saturation % 180.64/26.19 % (2268504)Time elapsed: 2.058 s % 180.64/26.19 % (2268504)Peak memory usage: 148 MB % 180.64/26.19 % (2268504)Instructions burned: 3395 (million) % 180.64/26.19 % (2268514)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=1455893380:st=4:i=7295:sd=4:ep=R:ss=axioms_2779 on theBenchmark for (2779ds/7295Mi) % 180.64/26.19 [W928 09:34:49.536591790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.64/26.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.64/26.19 [W928 09:34:49.536634964 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.64/26.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.64/26.19 [W928 09:34:49.536671967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.64/26.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.64/26.19 [W928 09:34:49.536684120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 180.64/26.19 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 180.64/26.19 [W928 09:34:49.536711897 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536724150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536749630 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536760560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536784520 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536795464 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536819394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 [W928 09:34:49.536830364 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 203.81/29.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 203.81/29.42 % (2268514)Refutation not found, incomplete strategy % 203.81/29.42 % (2268514)------------------------------ % 203.81/29.42 % (2268514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.81/29.42 % (2268514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.81/29.42 % (2268514)CaDiCaL version: 2.1.3 % 203.81/29.42 % (2268514)Termination reason: Refutation not found, incomplete strategy % 203.81/29.42 % (2268514)Time elapsed: 0.543 s % 203.81/29.42 % (2268514)Peak memory usage: 125 MB % 203.81/29.42 % (2268514)Instructions burned: 825 (million) % 203.81/29.42 % (2268514)------------------------------ % 203.81/29.42 % (2268514)------------------------------ % 203.81/29.42 % (2268516)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=111416069:i=4036:ins=10_2770 on theBenchmark for (2770ds/4036Mi) % 203.81/29.42 % (2268448)Instruction limit reached! % 203.81/29.42 % (2268448)------------------------------ % 203.81/29.42 % (2268448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 203.81/29.42 % (2268448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 203.81/29.42 % (2268448)CaDiCaL version: 2.1.3 % 203.81/29.42 % (2268448)Termination reason: Instruction limit % 203.81/29.42 % (2268448)Termination phase: Saturation % 203.81/29.42 % (2268448)Time elapsed: 14.546 s % 203.81/29.42 % (2268448)Peak memory usage: 798 MB % 203.81/29.42 % (2268448)Instructions burned: 26474 (million) % 203.81/29.42 % (2268518)lrs+10_1_sil=128000:lcm=predicate:random_seed=1217974465:st=3:i=43697:sd=5:ss=axioms_2750 on theBenchmark for (2750ds/43697Mi) % 203.81/29.42 % (2268518)Refutation not found, incomplete strategy % 203.81/29.42 % (2268518)------------------------------ % 203.81/29.42 % (2268518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.68/30.54 % (2268518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.68/30.54 % (2268518)CaDiCaL version: 2.1.3 % 211.68/30.54 % (2268518)Termination reason: Refutation not found, incomplete strategy % 211.68/30.54 % (2268518)Time elapsed: 0.001 s % 211.68/30.54 % (2268518)Peak memory usage: 86 MB % 211.68/30.54 % (2268510)Instruction limit reached! % 211.68/30.54 % (2268510)------------------------------ % 211.68/30.54 % (2268510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.68/30.54 % (2268510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.68/30.54 % (2268510)CaDiCaL version: 2.1.3 % 211.68/30.54 % (2268510)Termination reason: Instruction limit % 211.68/30.54 % (2268510)Termination phase: Saturation % 211.68/30.54 % (2268510)Time elapsed: 4.285 s % 211.68/30.54 % (2268510)Peak memory usage: 159 MB % 211.68/30.54 % (2268510)Instructions burned: 7223 (million) % 211.68/30.54 % (2268518)------------------------------ % 211.68/30.54 % (2268518)------------------------------ % 211.68/30.54 % (2268520)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=1792394821:i=17599:gtg=all:ss=axioms:fsd=on_2747 on theBenchmark for (2747ds/17599Mi) % 211.68/30.54 % (2268522)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=45642459:i=4547:bd=preordered_2746 on theBenchmark for (2746ds/4547Mi) % 211.68/30.54 % (2268516)Instruction limit reached! % 211.68/30.54 % (2268516)------------------------------ % 211.68/30.54 % (2268516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 211.68/30.54 % (2268516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 211.68/30.54 % (2268516)CaDiCaL version: 2.1.3 % 211.68/30.54 % (2268516)Termination reason: Instruction limit % 211.68/30.54 % (2268516)Termination phase: Saturation % 211.68/30.54 % (2268516)Time elapsed: 2.392 s % 211.68/30.54 % (2268516)Peak memory usage: 161 MB % 211.68/30.54 % (2268516)Instructions burned: 4041 (million) % 211.68/30.54 [W928 09:34:52.529327668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529350368 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529371762 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529381545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529395831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529402351 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529416589 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 211.68/30.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 211.68/30.54 [W928 09:34:52.529422901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 [W928 09:34:52.529436112 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 [W928 09:34:52.529441696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 [W928 09:34:52.529454931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 [W928 09:34:52.529460568 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 % (2268524)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=197753704:i=9294:av=off_2744 on theBenchmark for (2744ds/9294Mi) % 222.55/32.11 % (2268520)Refutation not found, incomplete strategy % 222.55/32.11 % (2268520)------------------------------ % 222.55/32.11 % (2268520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.55/32.11 % (2268520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.55/32.11 % (2268520)CaDiCaL version: 2.1.3 % 222.55/32.11 % (2268520)Termination reason: Refutation not found, incomplete strategy % 222.55/32.11 % (2268520)Time elapsed: 0.326 s % 222.55/32.11 % (2268520)Peak memory usage: 125 MB % 222.55/32.11 % (2268520)Instructions burned: 823 (million) % 222.55/32.11 % (2268520)------------------------------ % 222.55/32.11 % (2268520)------------------------------ % 222.55/32.11 % (2268526)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=806765070:i=32849:add=on_2741 on theBenchmark for (2741ds/32849Mi) % 222.55/32.11 % (2268522)Instruction limit reached! % 222.55/32.11 % (2268522)------------------------------ % 222.55/32.11 % (2268522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 222.55/32.11 % (2268522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 222.55/32.11 % (2268522)CaDiCaL version: 2.1.3 % 222.55/32.11 % (2268522)Termination reason: Instruction limit % 222.55/32.11 % (2268522)Termination phase: Saturation % 222.55/32.11 % (2268522)Time elapsed: 2.822 s % 222.55/32.11 % (2268522)Peak memory usage: 161 MB % 222.55/32.11 % (2268522)Instructions burned: 4548 (million) % 222.55/32.11 % (2268528)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2356831297:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2717 on theBenchmark for (2717ds/4793Mi) % 222.55/32.11 [W928 09:34:55.760903689 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 [W928 09:34:55.760947142 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 222.55/32.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 222.55/32.11 [W928 09:34:55.760985195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.760998845 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761037285 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761059809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761086742 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761097829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761121702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761132665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761157016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 [W928 09:34:55.761168006 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.02/35.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.02/35.59 % (2268528)Refutation not found, incomplete strategy % 238.02/35.59 % (2268528)------------------------------ % 238.02/35.59 % (2268528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.02/35.59 % (2268528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.02/35.59 % (2268528)CaDiCaL version: 2.1.3 % 238.02/35.59 % (2268528)Termination reason: Refutation not found, incomplete strategy % 238.02/35.59 % (2268528)Time elapsed: 0.543 s % 238.02/35.59 % (2268528)Peak memory usage: 125 MB % 238.02/35.59 % (2268528)Instructions burned: 826 (million) % 238.02/35.59 % (2268528)------------------------------ % 238.02/35.59 % (2268528)------------------------------ % 238.02/35.59 % (2268530)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=1048860844:i=4840:nm=4:av=off_2707 on theBenchmark for (2707ds/4840Mi) % 238.02/35.59 % (2268530)Refutation not found, incomplete strategy % 238.02/35.59 % (2268530)------------------------------ % 238.02/35.59 % (2268530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 238.02/35.59 % (2268530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 238.02/35.59 % (2268530)CaDiCaL version: 2.1.3 % 238.02/35.59 % (2268530)Termination reason: Refutation not found, incomplete strategy % 259.89/37.34 % (2268530)Time elapsed: 0.563 s % 259.89/37.34 % (2268530)Peak memory usage: 128 MB % 259.89/37.34 % (2268530)Instructions burned: 856 (million) % 259.89/37.34 % (2268530)------------------------------ % 259.89/37.34 % (2268530)------------------------------ % 259.89/37.34 % (2268532)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2935487035:cts=off:i=5002_2698 on theBenchmark for (2698ds/5002Mi) % 259.89/37.34 % (2268524)Instruction limit reached! % 259.89/37.34 % (2268524)------------------------------ % 259.89/37.34 % (2268524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 259.89/37.34 % (2268524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 259.89/37.34 % (2268524)CaDiCaL version: 2.1.3 % 259.89/37.34 % (2268524)Termination reason: Instruction limit % 259.89/37.34 % (2268524)Termination phase: Saturation % 259.89/37.34 % (2268524)Time elapsed: 5.329 s % 259.89/37.34 % (2268524)Peak memory usage: 173 MB % 259.89/37.34 % (2268524)Instructions burned: 9296 (million) % 259.89/37.34 % (2268534)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1121384886:i=30479:sd=3:ss=axioms_2690 on theBenchmark for (2690ds/30479Mi) % 259.89/37.34 [W928 09:34:58.442349657 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442382881 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442421004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442433027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442465427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442477701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442503294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442515367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442540861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 259.89/37.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 259.89/37.34 [W928 09:34:58.442552967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.94/41.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.94/41.76 [W928 09:34:58.442578694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.94/41.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.94/41.76 [W928 09:34:58.442589921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.94/41.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.94/41.76 % (2268534)Refutation not found, incomplete strategy % 290.94/41.76 % (2268534)------------------------------ % 290.94/41.76 % (2268534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.94/41.76 % (2268534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.94/41.76 % (2268534)CaDiCaL version: 2.1.3 % 290.94/41.76 % (2268534)Termination reason: Refutation not found, incomplete strategy % 290.94/41.76 % (2268534)Time elapsed: 0.546 s % 290.94/41.76 % (2268534)Peak memory usage: 125 MB % 290.94/41.76 % (2268534)Instructions burned: 825 (million) % 290.94/41.76 % (2268534)------------------------------ % 290.94/41.76 % (2268534)------------------------------ % 290.94/41.76 % (2268508)Instruction limit reached! % 290.94/41.76 % (2268508)------------------------------ % 290.94/41.76 % (2268508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.94/41.76 % (2268508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.94/41.76 % (2268508)CaDiCaL version: 2.1.3 % 290.94/41.76 % (2268508)Termination reason: Instruction limit % 290.94/41.76 % (2268508)Termination phase: Saturation % 290.94/41.76 % (2268508)Time elapsed: 11.468 s % 290.94/41.76 % (2268508)Peak memory usage: 331 MB % 290.94/41.76 % (2268508)Instructions burned: 20685 (million) % 290.94/41.76 % (2268536)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=1036635171:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2681 on theBenchmark for (2681ds/11035Mi) % 290.94/41.76 % (2268537)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=341958672:i=5835_2680 on theBenchmark for (2680ds/5835Mi) % 290.94/41.76 % (2268532)Instruction limit reached! % 290.94/41.76 % (2268532)------------------------------ % 290.94/41.76 % (2268532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.94/41.76 % (2268532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.94/41.76 % (2268532)CaDiCaL version: 2.1.3 % 290.94/41.76 % (2268532)Termination reason: Instruction limit % 290.94/41.76 % (2268532)Termination phase: Saturation % 290.94/41.76 % (2268532)Time elapsed: 2.952 s % 290.94/41.76 % (2268532)Peak memory usage: 159 MB % 290.94/41.76 % (2268532)Instructions burned: 5002 (million) % 290.94/41.76 % (2268540)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=2036978446:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2667 on theBenchmark for (2667ds/5890Mi) % 290.94/41.76 % (2268526)Instruction limit reached! % 290.94/41.76 % (2268526)------------------------------ % 290.94/41.76 % (2268526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.94/41.76 % (2268526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.94/41.76 % (2268526)CaDiCaL version: 2.1.3 % 290.94/41.76 % (2268526)Termination reason: Instruction limit % 290.94/41.76 % (2268526)Termination phase: Saturation % 290.94/41.76 % (2268526)Time elapsed: 8.893 s % 290.94/41.76 % (2268526)Peak memory usage: 412 MB % 290.94/41.76 % (2268526)Instructions burned: 32852 (million) % 290.94/41.76 % (2268542)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=3787711302:cts=off:i=19910:ep=RS_2651 on theBenchmark for (2651ds/19910Mi) % 290.94/41.76 % (2268542)Refutation not found, incomplete strategy % 290.94/41.76 % (2268542)------------------------------ % 290.94/41.76 % (2268542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.94/41.76 % (2268542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.94/41.76 % (2268542)CaDiCaL version: 2.1.3 % 295.94/42.56 % (2268542)Termination reason: Refutation not found, incomplete strategy % 295.94/42.56 % (2268542)Time elapsed: 0.003 s % 295.94/42.56 % (2268542)Peak memory usage: 88 MB % 295.94/42.56 % (2268542)Instructions burned: 9 (million) % 295.94/42.56 % (2268542)------------------------------ % 295.94/42.56 % (2268542)------------------------------ % 295.94/42.56 % (2268544)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=arity:fd=preordered:s2agt=16:sac=on:random_seed=2997705642:i=20312:bd=preordered:fsr=off:er=filter_2649 on theBenchmark for (2649ds/20312Mi) % 295.94/42.56 % (2268537)Instruction limit reached! % 295.94/42.56 % (2268537)------------------------------ % 295.94/42.56 % (2268537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.94/42.56 % (2268537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.94/42.56 % (2268537)CaDiCaL version: 2.1.3 % 295.94/42.56 % (2268537)Termination reason: Instruction limit % 295.94/42.56 % (2268537)Termination phase: Saturation % 295.94/42.56 % (2268537)Time elapsed: 3.458 s % 295.94/42.56 % (2268537)Peak memory usage: 171 MB % 295.94/42.56 % (2268537)Instructions burned: 5835 (million) % 295.94/42.56 % (2268465)Instruction limit reached! % 295.94/42.56 % (2268465)------------------------------ % 295.94/42.56 % (2268465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.94/42.56 % (2268465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.94/42.56 % (2268465)CaDiCaL version: 2.1.3 % 295.94/42.56 % (2268465)Termination reason: Instruction limit % 295.94/42.56 % (2268465)Termination phase: Saturation % 295.94/42.56 % (2268465)Time elapsed: 22.864 s % 295.94/42.56 % (2268465)Peak memory usage: 706 MB % 295.94/42.56 % (2268465)Instructions burned: 66096 (million) % 295.94/42.56 % (2268546)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal_then_units:urr=on:gs=on:sac=on:random_seed=1536786883:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2644 on theBenchmark for (2644ds/13822Mi) % 295.94/42.56 % (2268548)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=984275302:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2643 on theBenchmark for (2643ds/7144Mi) % 295.94/42.56 % (2268548)Refutation not found, incomplete strategy % 295.94/42.56 % (2268548)------------------------------ % 295.94/42.56 % (2268548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.94/42.56 % (2268548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.94/42.56 % (2268548)CaDiCaL version: 2.1.3 % 295.94/42.56 % (2268548)Termination reason: Refutation not found, incomplete strategy % 295.94/42.56 % (2268548)Time elapsed: 0.001 s % 295.94/42.56 % (2268548)Peak memory usage: 87 MB % 295.94/42.56 % (2268548)------------------------------ % 295.94/42.56 % (2268548)------------------------------ % 295.94/42.56 % (2268550)lrs+21_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1427353248:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2639 on theBenchmark for (2639ds/15184Mi) % 295.94/42.56 % (2268506)Instruction limit reached! % 295.94/42.56 % (2268506)------------------------------ % 295.94/42.56 % (2268506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.94/42.56 % (2268506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.94/42.56 % (2268506)CaDiCaL version: 2.1.3 % 295.94/42.56 % (2268506)Termination reason: Instruction limit % 295.94/42.56 % (2268506)Termination phase: Saturation % 295.94/42.56 % (2268506)Time elapsed: 15.901 s % 295.94/42.56 % (2268506)Peak memory usage: 266 MB % 295.94/42.56 % (2268506)Instructions burned: 33827 (million) % 295.94/42.56 % (2268552)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=2628189711:i=107375_2637 on theBenchmark for (2637ds/107375Mi) % 295.94/42.56 % (2268540)Instruction limit reached! % 295.94/42.56 % (2268540)------------------------------ % 295.94/42.56 % (2268540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 295.94/42.56 % (2268540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.94/42.56 % (2268540)CaDiCaL version: 2.1.3 % 295.94/42.56 % (2268540)Termination reason: Instruction limit % 295.94/42.56 % (2268540)Termination phase: Saturation % 295.94/42.56 % (2268540)Time elapsed: 3.344 s % 295.94/42.56 % (2268540)Peak memory usage: 171 MB % 295.94/42.56 % (2268540)Instructions burned: 5890 (million) % 300.62/43.07 % (2268554)dis+11_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=full:npcc=on:sp=const_frequency:spb=units:lcm=predicate:fd=off:sac=on:newcnf=on:random_seed=4236836973:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2632 on theBenchmark for (2632ds/7958Mi) % 300.62/43.07 % (2268536)Instruction limit reached! % 300.62/43.07 % (2268536)------------------------------ % 300.62/43.07 % (2268536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.62/43.07 % (2268536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/43.07 % (2268536)CaDiCaL version: 2.1.3 % 300.62/43.07 % (2268536)Termination reason: Instruction limit % 300.62/43.07 % (2268536)Termination phase: Saturation % 300.62/43.07 % (2268536)Time elapsed: 6.666 s % 300.62/43.07 % (2268536)Peak memory usage: 208 MB % 300.62/43.07 % (2268536)Instructions burned: 11036 (million) % 300.62/43.07 % (2268556)dis+10_128_sil=16000:nwc=0.7:random_seed=544179683:i=15999:nm=2:gsp=on_2613 on theBenchmark for (2613ds/15999Mi) % 300.62/43.07 % (2268544)Instruction limit reached! % 300.62/43.07 % (2268544)------------------------------ % 300.62/43.07 % (2268544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.62/43.07 % (2268544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/43.07 % (2268544)CaDiCaL version: 2.1.3 % 300.62/43.07 % (2268544)Termination reason: Instruction limit % 300.62/43.07 % (2268544)Termination phase: Saturation % 300.62/43.07 % (2268544)Time elapsed: 5.385 s % 300.62/43.07 % (2268544)Peak memory usage: 229 MB % 300.62/43.07 % (2268544)Instructions burned: 20314 (million) % 300.62/43.07 % (2268558)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=2375928114:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2594 on theBenchmark for (2594ds/8139Mi) % 300.62/43.07 % (2268558)Refutation not found, incomplete strategy % 300.62/43.07 % (2268558)------------------------------ % 300.62/43.07 % (2268558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.62/43.07 % (2268558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.62/43.07 % (2268558)CaDiCaL version: 2.1.3 % 300.62/43.07 % (2268558)Termination reason: Refutation not found, incomplete strategy % 300.62/43.07 % (2268558)Time elapsed: 0.0000 s % 300.62/43.07 % (2268558)Peak memory usage: 86 MB % 300.62/43.07 % (2268558)------------------------------ % 300.62/43.07 % (2268558)------------------------------ % 300.62/43.07 % (2268560)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1923774600:st=4:i=8950:sd=5:ss=axioms_2591 on theBenchmark for (2591ds/8950Mi) % 300.62/43.07 [W928 09:35:07.091479566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.62/43.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.62/43.07 [W928 09:35:07.091500606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.62/43.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.62/43.07 [W928 09:35:07.091521191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.62/43.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.62/43.07 [W928 09:35:07.091531498 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.62/43.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.62/43.07 [W928 09:35:07.091544966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 300.62/43.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.62/43.07 [W928 09:35:07.091551903 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating % 300.62/43.07 Terminated %------------------------------------------------------------------------------