%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWB006+3 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 12:59:59 PM UTC 2026 % Result : Timeout 300.67s 43.33s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWB006+3 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.35 % Computer : n015.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 28 06:59:32 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.39 Running first-order theorem proving % 0.12/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.03/1.91 % (2440175)Detected formulas, will run a generic FOF schedule. % 6.03/1.91 % (2440199)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=439793357:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 6.03/1.91 % (2440199)Refutation not found, incomplete strategy % 6.03/1.91 % (2440199)------------------------------ % 6.03/1.91 % (2440199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.03/1.91 % (2440199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.91 % (2440199)CaDiCaL version: 2.1.3 % 6.03/1.91 % (2440199)Termination reason: Refutation not found, incomplete strategy % 6.03/1.91 % (2440199)Time elapsed: 0.001 s % 6.03/1.91 % (2440199)Peak memory usage: 87 MB % 6.03/1.91 % (2440195)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=272614225:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 6.03/1.91 % (2440196)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=31868763:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 6.03/1.92 % (2440197)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=2215632511:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 6.03/1.92 % (2440201)dis-21_1_sil=8000:lcm=predicate:random_seed=2564963820: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) % 6.03/1.92 % (2440198)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2483872984:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 6.03/1.92 % (2440200)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4179097463:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 6.03/1.92 % (2440198)Refutation not found, incomplete strategy % 6.03/1.92 % (2440198)------------------------------ % 6.03/1.92 % (2440198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.03/1.92 % (2440198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.92 % (2440198)CaDiCaL version: 2.1.3 % 6.03/1.92 % (2440198)Termination reason: Refutation not found, incomplete strategy % 6.03/1.92 % (2440198)Time elapsed: 0.001 s % 6.03/1.92 % (2440198)Peak memory usage: 87 MB % 6.03/1.92 % (2440199)------------------------------ % 6.03/1.92 % (2440199)------------------------------ % 6.03/1.92 % (2440201)Instruction limit reached! % 6.03/1.92 % (2440201)------------------------------ % 6.03/1.92 % (2440201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.03/1.92 % (2440201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.92 % (2440201)CaDiCaL version: 2.1.3 % 6.03/1.92 % (2440201)Termination reason: Instruction limit % 6.03/1.92 % (2440201)Termination phase: Saturation % 6.03/1.92 % (2440201)Time elapsed: 0.132 s % 6.03/1.92 % (2440201)Peak memory usage: 89 MB % 6.03/1.92 % (2440201)Instructions burned: 129 (million) % 6.03/1.92 % (2440200)Instruction limit reached! % 6.03/1.92 % (2440200)------------------------------ % 6.03/1.92 % (2440200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.03/1.92 % (2440200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.92 % (2440200)CaDiCaL version: 2.1.3 % 6.03/1.92 % (2440200)Termination reason: Instruction limit % 6.03/1.92 % (2440200)Termination phase: Saturation % 6.03/1.92 % (2440200)Time elapsed: 0.138 s % 6.03/1.92 % (2440200)Peak memory usage: 90 MB % 6.03/1.92 % (2440200)Instructions burned: 139 (million) % 6.03/1.92 % (2440217)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1963182848:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi) % 6.03/1.92 % (2440217)Refutation not found, incomplete strategy % 6.03/1.92 % (2440217)------------------------------ % 6.03/1.92 % (2440217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.03/1.92 % (2440217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.03/1.92 % (2440217)CaDiCaL version: 2.1.3 % 6.03/1.92 % (2440217)Termination reason: Refutation not found, incomplete strategy % 6.03/1.92 % (2440217)Time elapsed: 0.001 s % 6.03/1.92 % (2440217)Peak memory usage: 88 MB % 6.03/1.92 % (2440217)Instructions burned: 1 (million) % 6.03/1.92 % (2440198)------------------------------ % 10.23/2.32 % (2440198)------------------------------ % 10.23/2.32 % (2440216)lrs+10_1_sil=8000:sp=occurrence:random_seed=1054982928:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi) % 10.23/2.32 % (2440216)Refutation not found, incomplete strategy % 10.23/2.32 % (2440216)------------------------------ % 10.23/2.32 % (2440216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.23/2.32 % (2440216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.23/2.32 % (2440216)CaDiCaL version: 2.1.3 % 10.23/2.32 % (2440216)Termination reason: Refutation not found, incomplete strategy % 10.23/2.32 % (2440216)Time elapsed: 0.002 s % 10.23/2.32 % (2440216)Peak memory usage: 88 MB % 10.23/2.32 % (2440218)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1994828098:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi) % 10.23/2.32 % (2440218)Refutation not found, incomplete strategy % 10.23/2.32 % (2440218)------------------------------ % 10.23/2.32 % (2440218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.23/2.32 % (2440218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.23/2.32 % (2440218)CaDiCaL version: 2.1.3 % 10.23/2.32 % (2440218)Termination reason: Refutation not found, incomplete strategy % 10.23/2.32 % (2440218)Time elapsed: 0.002 s % 10.23/2.32 % (2440218)Peak memory usage: 88 MB % 10.23/2.32 [W928 06:59:33.445908350 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.445955073 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446035067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446057541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446102941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446121568 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446166455 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446185382 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.23/2.32 [W928 06:59:33.446228989 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.23/2.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.446247515 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.446291382 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.446370233 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.496088659 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.496216037 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.496299574 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.496319397 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.496363308 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 [W928 06:59:33.496383018 register_special_ops.cpp:225] Warning: Creating a tensor from 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.30/2.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.30/2.77 % (2440217)------------------------------ % 12.30/2.77 % (2440217)------------------------------ % 12.30/2.77 % (2440225)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=2255031533:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi) % 12.30/2.77 % (2440196)Refutation not found, incomplete strategy % 12.30/2.77 % (2440196)------------------------------ % 12.30/2.77 % (2440196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.30/2.77 % (2440196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.30/2.77 % (2440196)CaDiCaL version: 2.1.3 % 12.30/2.77 % (2440196)Termination reason: Refutation not found, incomplete strategy % 12.30/2.77 % (2440196)Time elapsed: 0.796 s % 12.30/2.77 % (2440196)Peak memory usage: 126 MB % 12.30/2.77 % (2440196)Instructions burned: 822 (million) % 12.30/2.77 % (2440228)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1778032572:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi) % 12.30/2.77 % (2440228)Refutation not found, incomplete strategy % 12.30/2.77 % (2440228)------------------------------ % 12.30/2.77 % (2440228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.30/2.77 % (2440228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.30/2.77 % (2440228)CaDiCaL version: 2.1.3 % 12.70/2.96 % (2440228)Termination reason: Refutation not found, incomplete strategy % 12.70/2.96 % (2440228)Time elapsed: 0.001 s % 12.70/2.96 % (2440228)Peak memory usage: 87 MB % 12.70/2.96 % (2440228)Instructions burned: 1 (million) % 12.70/2.96 % (2440216)------------------------------ % 12.70/2.96 % (2440216)------------------------------ % 12.70/2.96 % (2440218)------------------------------ % 12.70/2.96 % (2440218)------------------------------ % 12.70/2.96 % (2440197)Refutation not found, incomplete strategy % 12.70/2.96 % (2440197)------------------------------ % 12.70/2.96 % (2440197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.70/2.96 % (2440197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.70/2.96 % (2440197)CaDiCaL version: 2.1.3 % 12.70/2.96 % (2440197)Termination reason: Refutation not found, incomplete strategy % 12.70/2.96 % (2440197)Time elapsed: 0.875 s % 12.70/2.96 % (2440197)Peak memory usage: 127 MB % 12.70/2.96 % (2440197)Instructions burned: 888 (million) % 12.70/2.96 % (2440225)Instruction limit reached! % 12.70/2.96 % (2440225)------------------------------ % 12.70/2.96 % (2440225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.70/2.96 % (2440225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.70/2.96 % (2440225)CaDiCaL version: 2.1.3 % 12.70/2.96 % (2440225)Termination reason: Instruction limit % 12.70/2.96 % (2440225)Termination phase: Saturation % 12.70/2.96 % (2440225)Time elapsed: 0.152 s % 12.70/2.96 % (2440225)Peak memory usage: 92 MB % 12.70/2.96 % (2440225)Instructions burned: 250 (million) % 12.70/2.96 % (2440228)------------------------------ % 12.70/2.96 % (2440228)------------------------------ % 12.70/2.96 % (2440234)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3591466306:i=2350_2989 on theBenchmark for (2989ds/2350Mi) % 12.70/2.96 % (2440196)------------------------------ % 12.70/2.96 % (2440196)------------------------------ % 12.70/2.96 % (2440236)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=170650516:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi) % 12.70/2.96 % (2440235)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2583039805:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi) % 12.70/2.96 % (2440235)Refutation not found, incomplete strategy % 12.70/2.96 % (2440235)------------------------------ % 12.70/2.96 % (2440235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.70/2.96 % (2440235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.70/2.96 % (2440235)CaDiCaL version: 2.1.3 % 12.70/2.96 % (2440235)Termination reason: Refutation not found, incomplete strategy % 12.70/2.96 % (2440235)Time elapsed: 0.002 s % 12.70/2.96 % (2440235)Peak memory usage: 88 MB % 12.70/2.96 % (2440237)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1438442978:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi) % 12.70/2.96 % (2440197)------------------------------ % 12.70/2.96 % (2440197)------------------------------ % 12.70/2.96 % (2440236)Instruction limit reached! % 12.70/2.96 % (2440236)------------------------------ % 12.70/2.96 % (2440236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.70/2.96 % (2440236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.70/2.96 % (2440236)CaDiCaL version: 2.1.3 % 12.70/2.96 % (2440236)Termination reason: Instruction limit % 12.70/2.96 % (2440236)Termination phase: Saturation % 12.70/2.96 % (2440236)Time elapsed: 0.063 s % 12.70/2.96 % (2440236)Peak memory usage: 89 MB % 12.70/2.96 % (2440236)Instructions burned: 129 (million) % 12.70/2.96 % (2440237)Instruction limit reached! % 12.70/2.96 % (2440237)------------------------------ % 12.70/2.96 % (2440237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.70/2.96 % (2440237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.70/2.96 % (2440237)CaDiCaL version: 2.1.3 % 12.70/2.96 % (2440237)Termination reason: Instruction limit % 12.70/2.96 % (2440237)Termination phase: Saturation % 12.70/2.96 % (2440237)Time elapsed: 0.033 s % 12.70/2.96 % (2440237)Peak memory usage: 89 MB % 12.70/2.96 % (2440237)Instructions burned: 118 (million) % 12.70/2.96 % (2440239)lrs+10_1_sil=8000:sp=occurrence:random_seed=4131350821:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi) % 12.70/2.96 % (2440239)Refutation not found, incomplete strategy % 12.70/2.96 % (2440239)------------------------------ % 12.70/2.96 % (2440239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.00/3.44 % (2440239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.00/3.44 % (2440239)CaDiCaL version: 2.1.3 % 18.00/3.44 % (2440239)Termination reason: Refutation not found, incomplete strategy % 18.00/3.44 % (2440239)Time elapsed: 0.001 s % 18.00/3.44 % (2440239)Peak memory usage: 88 MB % 18.00/3.44 % (2440244)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2601514466:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi) % 18.00/3.44 % (2440244)Refutation not found, incomplete strategy % 18.00/3.44 % (2440244)------------------------------ % 18.00/3.44 % (2440244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.00/3.44 % (2440244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.00/3.44 % (2440244)CaDiCaL version: 2.1.3 % 18.00/3.44 % (2440244)Termination reason: Refutation not found, incomplete strategy % 18.00/3.44 % (2440244)Time elapsed: 0.001 s % 18.00/3.44 % (2440244)Peak memory usage: 88 MB % 18.00/3.44 % (2440245)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1216380150:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi) % 18.00/3.44 % (2440246)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=49456325:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi) % 18.00/3.44 % (2440246)Refutation not found, incomplete strategy % 18.00/3.44 % (2440246)------------------------------ % 18.00/3.44 % (2440246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.00/3.44 % (2440246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.00/3.44 % (2440246)CaDiCaL version: 2.1.3 % 18.00/3.44 % (2440246)Termination reason: Refutation not found, incomplete strategy % 18.00/3.44 % (2440246)Time elapsed: 0.002 s % 18.00/3.44 % (2440246)Peak memory usage: 88 MB % 18.00/3.44 % (2440235)------------------------------ % 18.00/3.44 % (2440235)------------------------------ % 18.00/3.44 % (2440244)------------------------------ % 18.00/3.44 % (2440244)------------------------------ % 18.00/3.44 % (2440239)------------------------------ % 18.00/3.44 % (2440239)------------------------------ % 18.00/3.44 % (2440283)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3023824978:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi) % 18.00/3.44 % (2440295)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=467450483:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi) % 18.00/3.44 % (2440246)------------------------------ % 18.00/3.44 % (2440246)------------------------------ % 18.00/3.44 % (2440308)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=3392797738:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi) % 18.00/3.44 % (2440308)Refutation not found, incomplete strategy % 18.00/3.44 % (2440308)------------------------------ % 18.00/3.44 % (2440308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.00/3.44 % (2440308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.00/3.44 % (2440308)CaDiCaL version: 2.1.3 % 18.00/3.44 % (2440308)Termination reason: Refutation not found, incomplete strategy % 18.00/3.44 % (2440308)Time elapsed: 0.002 s % 18.00/3.44 % (2440308)Peak memory usage: 88 MB % 18.00/3.44 % (2440308)Instructions burned: 1 (million) % 18.00/3.44 [W928 06:59:34.584403414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.00/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.00/3.44 [W928 06:59:34.584438097 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.00/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.00/3.44 [W928 06:59:34.584473068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.00/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.584486734 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.584519831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.584541111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 % (2440328)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3860069301:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi) % 23.44/4.18 [W928 06:59:34.648585882 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.648623723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.648644310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.648650857 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.648663740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 [W928 06:59:34.648669230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 23.44/4.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.44/4.18 % (2440328)Instruction limit reached! % 23.44/4.18 % (2440328)------------------------------ % 23.44/4.18 % (2440328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.44/4.18 % (2440328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.44/4.18 % (2440328)CaDiCaL version: 2.1.3 % 23.44/4.18 % (2440328)Termination reason: Instruction limit % 23.44/4.18 % (2440328)Termination phase: Saturation % 23.44/4.18 % (2440328)Time elapsed: 0.085 s % 23.44/4.18 % (2440328)Peak memory usage: 90 MB % 23.44/4.18 % (2440328)Instructions burned: 134 (million) % 23.44/4.18 % (2440283)Instruction limit reached! % 23.44/4.18 % (2440283)------------------------------ % 23.44/4.18 % (2440283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.44/4.18 % (2440283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.44/4.18 % (2440283)CaDiCaL version: 2.1.3 % 23.44/4.18 % (2440283)Termination reason: Instruction limit % 23.44/4.18 % (2440283)Termination phase: Saturation % 23.44/4.18 % (2440283)Time elapsed: 0.350 s % 23.44/4.18 % (2440283)Peak memory usage: 91 MB % 23.44/4.18 % (2440283)Instructions burned: 592 (million) % 23.44/4.18 % (2440245)Refutation not found, incomplete strategy % 29.83/5.08 % (2440245)------------------------------ % 29.83/5.08 % (2440245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.83/5.08 % (2440245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.83/5.08 % (2440245)CaDiCaL version: 2.1.3 % 29.83/5.08 % (2440245)Termination reason: Refutation not found, incomplete strategy % 29.83/5.08 % (2440245)Time elapsed: 0.578 s % 29.83/5.08 % (2440245)Peak memory usage: 127 MB % 29.83/5.08 % (2440245)Instructions burned: 857 (million) % 29.83/5.08 % (2440295)Refutation not found, incomplete strategy % 29.83/5.08 % (2440295)------------------------------ % 29.83/5.08 % (2440295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.83/5.08 % (2440295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.83/5.08 % (2440295)CaDiCaL version: 2.1.3 % 29.83/5.08 % (2440295)Termination reason: Refutation not found, incomplete strategy % 29.83/5.08 % (2440295)Time elapsed: 0.338 s % 29.83/5.08 % (2440295)Peak memory usage: 127 MB % 29.83/5.08 % (2440295)Instructions burned: 856 (million) % 29.83/5.08 % (2440308)------------------------------ % 29.83/5.08 % (2440308)------------------------------ % 29.83/5.08 % (2440364)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4052194699:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi) % 29.83/5.08 % (2440364)Refutation not found, incomplete strategy % 29.83/5.08 % (2440364)------------------------------ % 29.83/5.08 % (2440364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.83/5.08 % (2440364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.83/5.08 % (2440364)CaDiCaL version: 2.1.3 % 29.83/5.08 % (2440364)Termination reason: Refutation not found, incomplete strategy % 29.83/5.08 % (2440364)Time elapsed: 0.001 s % 29.83/5.08 % (2440364)Peak memory usage: 88 MB % 29.83/5.08 % (2440365)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=322579733:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi) % 29.83/5.08 % (2440365)Refutation not found, incomplete strategy % 29.83/5.08 % (2440365)------------------------------ % 29.83/5.08 % (2440365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.83/5.08 % (2440365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.83/5.08 % (2440365)CaDiCaL version: 2.1.3 % 29.83/5.08 % (2440365)Termination reason: Refutation not found, incomplete strategy % 29.83/5.08 % (2440365)Time elapsed: 0.001 s % 29.83/5.08 % (2440365)Peak memory usage: 88 MB % 29.83/5.08 % (2440245)------------------------------ % 29.83/5.08 % (2440245)------------------------------ % 29.83/5.08 % (2440366)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=2391281085:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi) % 29.83/5.08 % (2440295)------------------------------ % 29.83/5.08 % (2440295)------------------------------ % 29.83/5.08 % (2440375)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=2097795167:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi) % 29.83/5.08 % (2440364)------------------------------ % 29.83/5.08 % (2440364)------------------------------ % 29.83/5.08 % (2440375)Instruction limit reached! % 29.83/5.08 % (2440375)------------------------------ % 29.83/5.08 % (2440375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 29.83/5.08 % (2440375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.83/5.08 % (2440375)CaDiCaL version: 2.1.3 % 29.83/5.08 % (2440375)Termination reason: Instruction limit % 29.83/5.08 % (2440375)Termination phase: Saturation % 29.83/5.08 % (2440375)Time elapsed: 0.045 s % 29.83/5.08 % (2440375)Peak memory usage: 91 MB % 29.83/5.08 % (2440375)Instructions burned: 154 (million) % 29.83/5.08 % (2440365)------------------------------ % 29.83/5.08 % (2440365)------------------------------ % 29.83/5.08 % (2440386)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1782970602:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi) % 29.83/5.08 % (2440418)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=499273305:s2a=on:i=185:s2at=1.8:fdi=4_2975 on theBenchmark for (2975ds/185Mi) % 33.83/5.72 % (2440417)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=34762300:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi) % 33.83/5.72 % (2440418)Instruction limit reached! % 33.83/5.72 % (2440418)------------------------------ % 33.83/5.72 % (2440418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.72 % (2440418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.72 % (2440418)CaDiCaL version: 2.1.3 % 33.83/5.72 % (2440418)Termination reason: Instruction limit % 33.83/5.72 % (2440418)Termination phase: Saturation % 33.83/5.72 % (2440418)Time elapsed: 0.053 s % 33.83/5.72 % (2440418)Peak memory usage: 91 MB % 33.83/5.72 % (2440418)Instructions burned: 186 (million) % 33.83/5.72 % (2440423)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=137267544:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2974 on theBenchmark for (2974ds/193Mi) % 33.83/5.72 % (2440423)Refutation not found, incomplete strategy % 33.83/5.72 % (2440423)------------------------------ % 33.83/5.72 % (2440423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.72 % (2440423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.72 % (2440423)CaDiCaL version: 2.1.3 % 33.83/5.72 % (2440423)Termination reason: Refutation not found, incomplete strategy % 33.83/5.72 % (2440423)Time elapsed: 0.001 s % 33.83/5.72 % (2440423)Peak memory usage: 86 MB % 33.83/5.72 % (2440426)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=235989494:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2973 on theBenchmark for (2973ds/4850Mi) % 33.83/5.72 % (2440234)Instruction limit reached! % 33.83/5.72 % (2440234)------------------------------ % 33.83/5.72 % (2440234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.72 % (2440234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.72 % (2440234)CaDiCaL version: 2.1.3 % 33.83/5.72 % (2440234)Termination reason: Instruction limit % 33.83/5.72 % (2440234)Termination phase: Saturation % 33.83/5.72 % (2440234)Time elapsed: 1.514 s % 33.83/5.72 % (2440234)Peak memory usage: 141 MB % 33.83/5.72 % (2440234)Instructions burned: 2351 (million) % 33.83/5.72 % (2440423)------------------------------ % 33.83/5.72 % (2440423)------------------------------ % 33.83/5.72 % (2440417)Instruction limit reached! % 33.83/5.72 % (2440417)------------------------------ % 33.83/5.72 % (2440417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.72 % (2440417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.72 % (2440417)CaDiCaL version: 2.1.3 % 33.83/5.72 % (2440417)Termination reason: Instruction limit % 33.83/5.72 % (2440417)Termination phase: Saturation % 33.83/5.72 % (2440417)Time elapsed: 0.312 s % 33.83/5.72 % (2440417)Peak memory usage: 112 MB % 33.83/5.72 % (2440417)Instructions burned: 669 (million) % 33.83/5.72 % (2440429)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3398237294:i=12111:sd=1:ss=included_2972 on theBenchmark for (2972ds/12111Mi) % 33.83/5.72 % (2440430)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=490494772:i=319:kws=precedence:fsr=off_2970 on theBenchmark for (2970ds/319Mi) % 33.83/5.72 % (2440431)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4146623978:i=2064:ep=RST_2970 on theBenchmark for (2970ds/2064Mi) % 33.83/5.72 % (2440430)Instruction limit reached! % 33.83/5.72 % (2440430)------------------------------ % 33.83/5.72 % (2440430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 33.83/5.72 % (2440430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 33.83/5.72 % (2440430)CaDiCaL version: 2.1.3 % 33.83/5.72 % (2440430)Termination reason: Instruction limit % 33.83/5.72 % (2440430)Termination phase: Saturation % 33.83/5.72 % (2440430)Time elapsed: 0.182 s % 33.83/5.72 % (2440430)Peak memory usage: 92 MB % 33.83/5.72 % (2440430)Instructions burned: 319 (million) % 33.83/5.72 [W928 06:59:35.996875217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 33.83/5.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 33.83/5.72 [W928 06:59:35.996919367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.74/5.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.74/5.93 [W928 06:59:35.996956127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.74/5.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.74/5.93 [W928 06:59:35.996967757 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.74/5.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.74/5.93 [W928 06:59:35.996991797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.74/5.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.74/5.93 [W928 06:59:35.997088118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.74/5.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.74/5.93 % (2440435)dis-1011_128_sil=32000:random_seed=3252700644:i=3706:ep=RST:av=off_2967 on theBenchmark for (2967ds/3706Mi) % 34.74/5.93 % (2440429)Refutation not found, incomplete strategy % 34.74/5.93 % (2440429)------------------------------ % 34.74/5.93 % (2440429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.74/5.93 % (2440429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.93 % (2440429)CaDiCaL version: 2.1.3 % 34.74/5.93 % (2440429)Termination reason: Refutation not found, incomplete strategy % 34.74/5.93 % (2440429)Time elapsed: 0.576 s % 34.74/5.93 % (2440429)Peak memory usage: 128 MB % 34.74/5.93 % (2440429)Instructions burned: 861 (million) % 34.74/5.93 % (2440429)------------------------------ % 34.74/5.93 % (2440429)------------------------------ % 34.74/5.93 % (2440431)Instruction limit reached! % 34.74/5.93 % (2440431)------------------------------ % 34.74/5.93 % (2440431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.74/5.93 % (2440431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.93 % (2440431)CaDiCaL version: 2.1.3 % 34.74/5.93 % (2440431)Termination reason: Instruction limit % 34.74/5.93 % (2440431)Termination phase: Saturation % 34.74/5.93 % (2440431)Time elapsed: 0.812 s % 34.74/5.93 % (2440431)Peak memory usage: 90 MB % 34.74/5.93 % (2440431)Instructions burned: 2065 (million) % 34.74/5.93 % (2440437)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=282892027:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2962 on theBenchmark for (2962ds/757Mi) % 34.74/5.93 % (2440437)Refutation not found, incomplete strategy % 34.74/5.93 % (2440437)------------------------------ % 34.74/5.93 % (2440437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.74/5.93 % (2440437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.93 % (2440437)CaDiCaL version: 2.1.3 % 34.74/5.93 % (2440437)Termination reason: Refutation not found, incomplete strategy % 34.74/5.93 % (2440437)Time elapsed: 0.001 s % 34.74/5.93 % (2440437)Peak memory usage: 88 MB % 34.74/5.93 % (2440438)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=672845460:i=13913:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/13913Mi) % 34.74/5.93 % (2440437)------------------------------ % 34.74/5.93 % (2440437)------------------------------ % 34.74/5.93 % (2440426)Instruction limit reached! % 34.74/5.93 % (2440426)------------------------------ % 34.74/5.93 % (2440426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.74/5.93 % (2440426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.74/5.93 % (2440426)CaDiCaL version: 2.1.3 % 34.74/5.93 % (2440426)Termination reason: Instruction limit % 34.74/5.93 % (2440426)Termination phase: Saturation % 34.74/5.93 % (2440426)Time elapsed: 1.459 s % 34.74/5.93 % (2440426)Peak memory usage: 109 MB % 48.73/7.72 % (2440426)Instructions burned: 4852 (million) % 48.73/7.72 % (2440441)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3937747975:i=9925:aac=none_2958 on theBenchmark for (2958ds/9925Mi) % 48.73/7.72 % (2440442)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1602856680:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/2479Mi) % 48.73/7.72 % (2440442)Refutation not found, incomplete strategy % 48.73/7.72 % (2440442)------------------------------ % 48.73/7.72 % (2440442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.73/7.72 % (2440442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.72 % (2440442)CaDiCaL version: 2.1.3 % 48.73/7.72 % (2440442)Termination reason: Refutation not found, incomplete strategy % 48.73/7.72 % (2440442)Time elapsed: 0.001 s % 48.73/7.72 % (2440442)Peak memory usage: 87 MB % 48.73/7.72 [W928 06:59:37.130743900 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/7.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.73/7.72 [W928 06:59:37.130789540 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/7.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.73/7.72 [W928 06:59:37.130823157 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/7.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.73/7.72 [W928 06:59:37.130835017 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/7.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.73/7.72 [W928 06:59:37.130862504 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/7.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.73/7.72 [W928 06:59:37.130874897 register_special_ops.cpp:225] Warning: Creating a tensor from 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.73/7.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.73/7.72 % (2440442)------------------------------ % 48.73/7.72 % (2440442)------------------------------ % 48.73/7.72 % (2440445)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=309035280:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2955 on theBenchmark for (2955ds/440Mi) % 48.73/7.72 % (2440438)Refutation not found, incomplete strategy % 48.73/7.72 % (2440438)------------------------------ % 48.73/7.72 % (2440438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.73/7.72 % (2440438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.72 % (2440438)CaDiCaL version: 2.1.3 % 48.73/7.72 % (2440438)Termination reason: Refutation not found, incomplete strategy % 48.73/7.72 % (2440438)Time elapsed: 0.571 s % 48.73/7.72 % (2440438)Peak memory usage: 127 MB % 48.73/7.72 % (2440438)Instructions burned: 852 (million) % 48.73/7.72 % (2440445)Instruction limit reached! % 48.73/7.72 % (2440445)------------------------------ % 48.73/7.72 % (2440445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.73/7.72 % (2440445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.73/7.72 % (2440445)CaDiCaL version: 2.1.3 % 48.73/7.72 % (2440445)Termination reason: Instruction limit % 48.73/7.72 % (2440445)Termination phase: Saturation % 48.73/7.72 % (2440445)Time elapsed: 0.112 s % 48.73/7.72 % (2440445)Peak memory usage: 92 MB % 48.73/7.72 % (2440445)Instructions burned: 441 (million) % 48.73/7.72 % (2440447)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=68045647:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2952 on theBenchmark for (2952ds/11145Mi) % 59.39/9.22 % (2440438)------------------------------ % 59.39/9.22 % (2440438)------------------------------ % 59.39/9.22 % (2440449)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=2219345178:cts=off:i=3034:av=off:er=known:fsd=on_2950 on theBenchmark for (2950ds/3034Mi) % 59.39/9.22 [W928 06:59:37.742149412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742166341 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742187464 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742194548 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742208077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742214311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742227480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742233635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742246623 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742252820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742265613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.39/9.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.39/9.22 [W928 06:59:37.742271809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.32/9.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.32/9.80 % (2440447)Refutation not found, incomplete strategy % 63.32/9.80 % (2440447)------------------------------ % 63.32/9.80 % (2440447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.32/9.80 % (2440447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.32/9.80 % (2440447)CaDiCaL version: 2.1.3 % 63.32/9.80 % (2440447)Termination reason: Refutation not found, incomplete strategy % 63.32/9.80 % (2440447)Time elapsed: 0.303 s % 63.32/9.80 % (2440447)Peak memory usage: 126 MB % 63.32/9.80 % (2440447)Instructions burned: 827 (million) % 63.32/9.80 % (2440447)------------------------------ % 63.32/9.80 % (2440447)------------------------------ % 63.32/9.80 % (2440451)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1439253695:st=2:s2a=on:i=524:s2at=2:ss=axioms_2946 on theBenchmark for (2946ds/524Mi) % 63.32/9.80 % (2440451)Refutation not found, incomplete strategy % 63.32/9.80 % (2440451)------------------------------ % 63.32/9.80 % (2440451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.32/9.80 % (2440451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.32/9.80 % (2440451)CaDiCaL version: 2.1.3 % 63.32/9.80 % (2440451)Termination reason: Refutation not found, incomplete strategy % 63.32/9.80 % (2440451)Time elapsed: 0.002 s % 63.32/9.80 % (2440451)Peak memory usage: 88 MB % 63.32/9.80 % (2440451)Instructions burned: 1 (million) % 63.32/9.80 % (2440435)Instruction limit reached! % 63.32/9.80 % (2440435)------------------------------ % 63.32/9.80 % (2440435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.32/9.80 % (2440435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.32/9.80 % (2440435)CaDiCaL version: 2.1.3 % 63.32/9.80 % (2440435)Termination reason: Instruction limit % 63.32/9.80 % (2440435)Termination phase: Saturation % 63.32/9.80 % (2440435)Time elapsed: 2.178 s % 63.32/9.80 % (2440435)Peak memory usage: 105 MB % 63.32/9.80 % (2440435)Instructions burned: 3706 (million) % 63.32/9.80 % (2440451)------------------------------ % 63.32/9.80 % (2440451)------------------------------ % 63.32/9.80 % (2440453)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3504958790:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2943 on theBenchmark for (2943ds/1016Mi) % 63.32/9.80 % (2440453)Refutation not found, incomplete strategy % 63.32/9.80 % (2440453)------------------------------ % 63.32/9.80 % (2440453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.32/9.80 % (2440453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.32/9.80 % (2440453)CaDiCaL version: 2.1.3 % 63.32/9.80 % (2440453)Termination reason: Refutation not found, incomplete strategy % 63.32/9.80 % (2440453)Time elapsed: 0.001 s % 63.32/9.80 % (2440453)Peak memory usage: 87 MB % 63.32/9.80 % (2440366)Instruction limit reached! % 63.32/9.80 % (2440366)------------------------------ % 63.32/9.80 % (2440366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.32/9.80 % (2440366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.32/9.80 % (2440366)CaDiCaL version: 2.1.3 % 63.32/9.80 % (2440366)Termination reason: Instruction limit % 63.32/9.80 % (2440366)Termination phase: Saturation % 63.32/9.80 % (2440366)Time elapsed: 3.547 s % 63.32/9.80 % (2440366)Peak memory usage: 159 MB % 63.32/9.80 % (2440366)Instructions burned: 6061 (million) % 63.32/9.80 % (2440454)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1396636283:i=14123:bd=preordered:ins=4_2942 on theBenchmark for (2942ds/14123Mi) % 63.32/9.80 % (2440453)------------------------------ % 63.32/9.80 % (2440453)------------------------------ % 63.32/9.80 % (2440456)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2108286075:i=5781:kws=precedence:bd=all:rawr=on_2941 on theBenchmark for (2941ds/5781Mi) % 63.32/9.80 % (2440459)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=3111219081:i=2448:gtgl=5:bd=preordered:gtg=all_2939 on theBenchmark for (2939ds/2448Mi) % 63.32/9.80 % (2440449)Instruction limit reached! % 63.32/9.80 % (2440449)------------------------------ % 63.32/9.80 % (2440449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.32/9.80 % (2440449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.85/9.99 % (2440449)CaDiCaL version: 2.1.3 % 63.85/9.99 % (2440449)Termination reason: Instruction limit % 63.85/9.99 % (2440449)Termination phase: Saturation % 63.85/9.99 % (2440449)Time elapsed: 1.798 s % 63.85/9.99 % (2440449)Peak memory usage: 145 MB % 63.85/9.99 % (2440449)Instructions burned: 3035 (million) % 63.85/9.99 % (2440461)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=94764637:i=3223:kws=precedence:fgj=on:av=off_2931 on theBenchmark for (2931ds/3223Mi) % 63.85/9.99 % (2440459)Instruction limit reached! % 63.85/9.99 % (2440459)------------------------------ % 63.85/9.99 % (2440459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.85/9.99 % (2440459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.85/9.99 % (2440459)CaDiCaL version: 2.1.3 % 63.85/9.99 % (2440459)Termination reason: Instruction limit % 63.85/9.99 % (2440459)Termination phase: Saturation % 63.85/9.99 % (2440459)Time elapsed: 1.464 s % 63.85/9.99 % (2440459)Peak memory usage: 144 MB % 63.85/9.99 % (2440459)Instructions burned: 2449 (million) % 63.85/9.99 % (2440463)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2184228576:st=5.6:i=2033:sd=3:ss=axioms_2923 on theBenchmark for (2923ds/2033Mi) % 63.85/9.99 % (2440441)Instruction limit reached! % 63.85/9.99 % (2440441)------------------------------ % 63.85/9.99 % (2440441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.85/9.99 % (2440441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.85/9.99 % (2440441)CaDiCaL version: 2.1.3 % 63.85/9.99 % (2440441)Termination reason: Instruction limit % 63.85/9.99 % (2440441)Termination phase: Saturation % 63.85/9.99 % (2440441)Time elapsed: 3.689 s % 63.85/9.99 % (2440441)Peak memory usage: 191 MB % 63.85/9.99 % (2440441)Instructions burned: 9926 (million) % 63.85/9.99 % (2440465)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3619580340:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2919 on theBenchmark for (2919ds/2055Mi) % 63.85/9.99 [W928 06:59:41.036582906 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.85/9.99 [W928 06:59:41.036620572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.85/9.99 [W928 06:59:41.036641893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.85/9.99 [W928 06:59:41.036648179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.85/9.99 [W928 06:59:41.036661705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.85/9.99 [W928 06:59:41.036667248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.85/9.99 [W928 06:59:41.036680894 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.85/9.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.036687961 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.036701094 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.036706862 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.036719538 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.036725264 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 % (2440465)Refutation not found, incomplete strategy % 67.58/10.62 % (2440465)------------------------------ % 67.58/10.62 % (2440465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.58/10.62 % (2440465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.58/10.62 % (2440465)CaDiCaL version: 2.1.3 % 67.58/10.62 % (2440465)Termination reason: Refutation not found, incomplete strategy % 67.58/10.62 % (2440465)Time elapsed: 0.301 s % 67.58/10.62 % (2440465)Peak memory usage: 126 MB % 67.58/10.62 % (2440465)Instructions burned: 823 (million) % 67.58/10.62 % (2440465)------------------------------ % 67.58/10.62 % (2440465)------------------------------ % 67.58/10.62 % (2440467)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=2226021005:i=21611:sd=3:ss=axioms_2913 on theBenchmark for (2913ds/21611Mi) % 67.58/10.62 % (2440456)Instruction limit reached! % 67.58/10.62 % (2440456)------------------------------ % 67.58/10.62 % (2440456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.58/10.62 % (2440456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.58/10.62 % (2440456)CaDiCaL version: 2.1.3 % 67.58/10.62 % (2440456)Termination reason: Instruction limit % 67.58/10.62 % (2440456)Termination phase: Saturation % 67.58/10.62 % (2440456)Time elapsed: 2.917 s % 67.58/10.62 % (2440456)Peak memory usage: 127 MB % 67.58/10.62 % (2440456)Instructions burned: 5782 (million) % 67.58/10.62 [W928 06:59:41.619472810 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.619494478 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.619515096 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 67.58/10.62 [W928 06:59:41.619522196 register_special_ops.cpp:225] Warning: Creating a tensor from 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.58/10.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619535986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619541839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619554483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619560166 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619572403 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619578125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619591068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 [W928 06:59:41.619596873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 74.19/11.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.19/11.44 % (2440467)Refutation not found, incomplete strategy % 74.19/11.44 % (2440467)------------------------------ % 74.19/11.44 % (2440467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.19/11.44 % (2440467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.19/11.44 % (2440467)CaDiCaL version: 2.1.3 % 74.19/11.44 % (2440467)Termination reason: Refutation not found, incomplete strategy % 74.19/11.44 % (2440467)Time elapsed: 0.310 s % 74.19/11.44 % (2440467)Peak memory usage: 126 MB % 74.19/11.44 % (2440467)Instructions burned: 826 (million) % 74.19/11.44 % (2440469)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3077105996:i=4835:sd=13:ss=axioms:sgt=23_2910 on theBenchmark for (2910ds/4835Mi) % 74.19/11.44 % (2440469)Refutation not found, incomplete strategy % 74.19/11.44 % (2440469)------------------------------ % 74.19/11.44 % (2440469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.19/11.44 % (2440469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.19/11.44 % (2440469)CaDiCaL version: 2.1.3 % 74.19/11.44 % (2440469)Termination reason: Refutation not found, incomplete strategy % 74.19/11.44 % (2440469)Time elapsed: 0.001 s % 74.19/11.44 % (2440469)Peak memory usage: 88 MB % 74.19/11.44 % (2440463)Instruction limit reached! % 74.19/11.44 % (2440463)------------------------------ % 74.19/11.44 % (2440463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.19/11.44 % (2440463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.19/11.44 % (2440463)CaDiCaL version: 2.1.3 % 74.19/11.44 % (2440463)Termination reason: Instruction limit % 74.19/11.44 % (2440463)Termination phase: Saturation % 75.42/11.66 % (2440463)Time elapsed: 1.323 s % 75.42/11.66 % (2440463)Peak memory usage: 133 MB % 75.42/11.66 % (2440463)Instructions burned: 2034 (million) % 75.42/11.66 % (2440467)------------------------------ % 75.42/11.66 % (2440467)------------------------------ % 75.42/11.66 % (2440461)Instruction limit reached! % 75.42/11.66 % (2440461)------------------------------ % 75.42/11.66 % (2440461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.42/11.66 % (2440461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.42/11.66 % (2440461)CaDiCaL version: 2.1.3 % 75.42/11.66 % (2440461)Termination reason: Instruction limit % 75.42/11.66 % (2440461)Termination phase: Saturation % 75.42/11.66 % (2440461)Time elapsed: 2.166 s % 75.42/11.66 % (2440461)Peak memory usage: 148 MB % 75.42/11.66 % (2440461)Instructions burned: 3225 (million) % 75.42/11.66 % (2440471)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=1544369261:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2908 on theBenchmark for (2908ds/797Mi) % 75.42/11.66 % (2440472)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=447615238:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2907 on theBenchmark for (2907ds/2326Mi) % 75.42/11.66 % (2440472)Refutation not found, incomplete strategy % 75.42/11.66 % (2440472)------------------------------ % 75.42/11.66 % (2440472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.42/11.66 % (2440472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.42/11.66 % (2440472)CaDiCaL version: 2.1.3 % 75.42/11.66 % (2440472)Termination reason: Refutation not found, incomplete strategy % 75.42/11.66 % (2440472)Time elapsed: 0.004 s % 75.42/11.66 % (2440472)Peak memory usage: 88 MB % 75.42/11.66 % (2440472)Instructions burned: 13 (million) % 75.42/11.66 % (2440469)------------------------------ % 75.42/11.66 % (2440469)------------------------------ % 75.42/11.66 % (2440473)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1826621188:i=6038:nm=6_2907 on theBenchmark for (2907ds/6038Mi) % 75.42/11.66 % (2440472)------------------------------ % 75.42/11.66 % (2440472)------------------------------ % 75.42/11.66 % (2440476)lrs+10_1_sil=32000:sp=occurrence:random_seed=1402730591:st=2:i=33334:sd=3:ss=included:sgt=32_2906 on theBenchmark for (2906ds/33334Mi) % 75.42/11.66 % (2440476)Refutation not found, incomplete strategy % 75.42/11.66 % (2440476)------------------------------ % 75.42/11.66 % (2440476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.42/11.66 % (2440476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.42/11.66 % (2440476)CaDiCaL version: 2.1.3 % 75.42/11.66 % (2440476)Termination reason: Refutation not found, incomplete strategy % 75.42/11.66 % (2440476)Time elapsed: 0.001 s % 75.42/11.66 % (2440476)Peak memory usage: 88 MB % 75.42/11.66 % (2440478)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1535938893:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2905 on theBenchmark for (2905ds/1008Mi) % 75.42/11.66 % (2440478)Refutation not found, incomplete strategy % 75.42/11.66 % (2440478)------------------------------ % 75.42/11.66 % (2440478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.42/11.66 % (2440478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.42/11.66 % (2440478)CaDiCaL version: 2.1.3 % 75.42/11.66 % (2440478)Termination reason: Refutation not found, incomplete strategy % 75.42/11.66 % (2440478)Time elapsed: 0.001 s % 75.42/11.66 % (2440478)Peak memory usage: 88 MB % 75.42/11.66 % (2440478)Instructions burned: 1 (million) % 75.42/11.66 % (2440478)------------------------------ % 75.42/11.66 % (2440478)------------------------------ % 75.42/11.66 % (2440471)Instruction limit reached! % 75.42/11.66 % (2440471)------------------------------ % 75.42/11.66 % (2440471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.42/11.66 % (2440471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.42/11.66 % (2440471)CaDiCaL version: 2.1.3 % 75.42/11.66 % (2440471)Termination reason: Instruction limit % 75.42/11.66 % (2440471)Termination phase: Saturation % 75.42/11.66 % (2440471)Time elapsed: 0.460 s % 75.42/11.66 % (2440471)Peak memory usage: 95 MB % 75.42/11.66 % (2440471)Instructions burned: 799 (million) % 75.42/11.66 % (2440476)------------------------------ % 75.42/11.66 % (2440476)------------------------------ % 82.62/12.63 % (2440386)Instruction limit reached! % 82.62/12.63 % (2440386)------------------------------ % 82.62/12.63 % (2440386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.62/12.63 % (2440386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.62/12.63 % (2440386)CaDiCaL version: 2.1.3 % 82.62/12.63 % (2440386)Termination reason: Instruction limit % 82.62/12.63 % (2440386)Termination phase: Saturation % 82.62/12.63 % (2440386)Time elapsed: 7.315 s % 82.62/12.63 % (2440386)Peak memory usage: 232 MB % 82.62/12.63 % (2440386)Instructions burned: 14157 (million) % 82.62/12.63 % (2440481)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=3561162347:i=8327:s2at=5:bd=preordered_2902 on theBenchmark for (2902ds/8327Mi) % 82.62/12.63 % (2440483)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1982627888:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2902 on theBenchmark for (2902ds/1084Mi) % 82.62/12.63 % (2440482)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=3858361966:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2902 on theBenchmark for (2902ds/1083Mi) % 82.62/12.63 % (2440483)Refutation not found, incomplete strategy % 82.62/12.63 % (2440483)------------------------------ % 82.62/12.63 % (2440483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.62/12.63 % (2440483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.62/12.63 % (2440483)CaDiCaL version: 2.1.3 % 82.62/12.63 % (2440483)Termination reason: Refutation not found, incomplete strategy % 82.62/12.63 % (2440483)Time elapsed: 0.001 s % 82.62/12.63 % (2440483)Peak memory usage: 87 MB % 82.62/12.63 % (2440473)Refutation not found, incomplete strategy % 82.62/12.63 % (2440473)------------------------------ % 82.62/12.63 % (2440473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.62/12.63 % (2440473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.62/12.63 % (2440473)CaDiCaL version: 2.1.3 % 82.62/12.63 % (2440473)Termination reason: Refutation not found, incomplete strategy % 82.62/12.63 % (2440473)Time elapsed: 0.604 s % 82.62/12.63 % (2440473)Peak memory usage: 130 MB % 82.62/12.63 % (2440473)Instructions burned: 885 (million) % 82.62/12.63 % (2440484)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=64951747:i=6995:s2at=5:gtg=all_2901 on theBenchmark for (2901ds/6995Mi) % 82.62/12.63 % (2440483)------------------------------ % 82.62/12.63 % (2440483)------------------------------ % 82.62/12.63 % (2440473)------------------------------ % 82.62/12.63 % (2440473)------------------------------ % 82.62/12.63 % (2440489)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=889463939:st=2:i=6225:sd=15:ss=axioms_2898 on theBenchmark for (2898ds/6225Mi) % 82.62/12.63 % (2440489)Refutation not found, incomplete strategy % 82.62/12.63 % (2440489)------------------------------ % 82.62/12.63 % (2440489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.62/12.63 % (2440489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.62/12.63 % (2440489)CaDiCaL version: 2.1.3 % 82.62/12.63 % (2440489)Termination reason: Refutation not found, incomplete strategy % 82.62/12.63 % (2440489)Time elapsed: 0.001 s % 82.62/12.63 % (2440489)Peak memory usage: 88 MB % 82.62/12.63 % (2440482)Instruction limit reached! % 82.62/12.63 % (2440482)------------------------------ % 82.62/12.63 % (2440482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.62/12.63 % (2440482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.62/12.63 % (2440482)CaDiCaL version: 2.1.3 % 82.62/12.63 % (2440482)Termination reason: Instruction limit % 82.62/12.63 % (2440482)Termination phase: Saturation % 82.62/12.63 % (2440482)Time elapsed: 0.498 s % 82.62/12.63 % (2440482)Peak memory usage: 98 MB % 82.62/12.63 % (2440482)Instructions burned: 1084 (million) % 82.62/12.63 % (2440490)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2055742160:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2897 on theBenchmark for (2897ds/3372Mi) % 82.62/12.63 % (2440489)------------------------------ % 82.62/12.63 % (2440489)------------------------------ % 82.62/12.63 % (2440493)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=605525312:st=2.3:i=26457:sd=10:ss=included:sgt=8_2895 on theBenchmark for (2895ds/26457Mi) % 83.12/12.80 % (2440494)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=1812239735:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2894 on theBenchmark for (2894ds/13494Mi) % 83.12/12.80 [W928 06:59:43.472204328 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472247951 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472286962 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472305608 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472336335 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472347752 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472373499 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472384369 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472408909 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472421502 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472446303 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.12/12.80 [W928 06:59:43.472458353 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/12.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:43.634824001 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:43.634856991 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:43.634893074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:43.634905214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:43.634929545 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:43.634942105 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 % (2440490)Refutation not found, incomplete strategy % 89.43/13.61 % (2440490)------------------------------ % 89.43/13.61 % (2440490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.43/13.61 % (2440490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.43/13.61 % (2440490)CaDiCaL version: 2.1.3 % 89.43/13.61 % (2440490)Termination reason: Refutation not found, incomplete strategy % 89.43/13.61 % (2440490)Time elapsed: 0.548 s % 89.43/13.61 % (2440490)Peak memory usage: 126 MB % 89.43/13.61 % (2440490)Instructions burned: 825 (million) % 89.43/13.61 % (2440493)Refutation not found, incomplete strategy % 89.43/13.61 % (2440493)------------------------------ % 89.43/13.61 % (2440493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.43/13.61 % (2440493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.43/13.61 % (2440493)CaDiCaL version: 2.1.3 % 89.43/13.61 % (2440493)Termination reason: Refutation not found, incomplete strategy % 89.43/13.61 % (2440493)Time elapsed: 0.571 s % 89.43/13.61 % (2440493)Peak memory usage: 128 MB % 89.43/13.61 % (2440493)Instructions burned: 858 (million) % 89.43/13.61 % (2440490)------------------------------ % 89.43/13.61 % (2440490)------------------------------ % 89.43/13.61 % (2440497)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=1860324965:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2887 on theBenchmark for (2887ds/2503Mi) % 89.43/13.61 % (2440493)------------------------------ % 89.43/13.61 % (2440493)------------------------------ % 89.43/13.61 % (2440499)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=4111777037:i=2559:sd=1:ep=RSTC:ss=axioms_2885 on theBenchmark for (2885ds/2559Mi) % 89.43/13.61 [W928 06:59:44.446522525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.43/13.61 [W928 06:59:44.446556125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.43/13.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.446591156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.446602782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.446627073 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.446637583 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613737442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613772372 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613809233 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613820326 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613845913 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613858223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613885043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613896820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 94.96/14.34 [W928 06:59:44.613922497 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 94.96/14.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.50/14.65 [W928 06:59:44.613933890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.50/14.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.50/14.65 [W928 06:59:44.613964620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.50/14.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.50/14.65 [W928 06:59:44.614043391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.50/14.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.50/14.65 % (2440497)Refutation not found, incomplete strategy % 96.50/14.65 % (2440497)------------------------------ % 96.50/14.65 % (2440497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.50/14.65 % (2440497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.50/14.65 % (2440497)CaDiCaL version: 2.1.3 % 96.50/14.65 % (2440497)Termination reason: Refutation not found, incomplete strategy % 96.50/14.65 % (2440497)Time elapsed: 0.568 s % 96.50/14.65 % (2440497)Peak memory usage: 128 MB % 96.50/14.65 % (2440497)Instructions burned: 856 (million) % 96.50/14.65 % (2440499)Refutation not found, incomplete strategy % 96.50/14.65 % (2440499)------------------------------ % 96.50/14.65 % (2440499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.50/14.65 % (2440499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.50/14.65 % (2440499)CaDiCaL version: 2.1.3 % 96.50/14.65 % (2440499)Termination reason: Refutation not found, incomplete strategy % 96.50/14.65 % (2440499)Time elapsed: 0.546 s % 96.50/14.65 % (2440499)Peak memory usage: 126 MB % 96.50/14.65 % (2440499)Instructions burned: 826 (million) % 96.50/14.65 % (2440497)------------------------------ % 96.50/14.65 % (2440497)------------------------------ % 96.50/14.65 % (2440499)------------------------------ % 96.50/14.65 % (2440499)------------------------------ % 96.50/14.65 % (2440502)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4232812543:i=30753:av=off:ss=included_2877 on theBenchmark for (2877ds/30753Mi) % 96.50/14.65 % (2440481)Instruction limit reached! % 96.50/14.65 % (2440481)------------------------------ % 96.50/14.65 % (2440481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 96.50/14.65 % (2440481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 96.50/14.65 % (2440481)CaDiCaL version: 2.1.3 % 96.50/14.65 % (2440481)Termination reason: Instruction limit % 96.50/14.65 % (2440481)Termination phase: Saturation % 96.50/14.65 % (2440481)Time elapsed: 2.649 s % 96.50/14.65 % (2440481)Peak memory usage: 186 MB % 96.50/14.65 % (2440481)Instructions burned: 8327 (million) % 96.50/14.65 % (2440512)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3684400628:i=26473:ep=RSTC_2876 on theBenchmark for (2876ds/26473Mi) % 96.50/14.65 % (2440545)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=388550564:cts=off:i=2759:kws=inv_arity:fgj=on_2874 on theBenchmark for (2874ds/2759Mi) % 96.50/14.65 [W928 06:59:45.427693189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.50/14.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.50/14.65 [W928 06:59:45.427726572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 96.50/14.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 96.50/14.65 [W928 06:59:45.427762896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:45.427775966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:45.427807873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:45.427871256 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 % (2440502)Refutation not found, incomplete strategy % 102.51/15.35 % (2440502)------------------------------ % 102.51/15.35 % (2440502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.51/15.35 % (2440502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.51/15.35 % (2440502)CaDiCaL version: 2.1.3 % 102.51/15.35 % (2440502)Termination reason: Refutation not found, incomplete strategy % 102.51/15.35 % (2440502)Time elapsed: 0.571 s % 102.51/15.35 % (2440502)Peak memory usage: 127 MB % 102.51/15.35 % (2440502)Instructions burned: 856 (million) % 102.51/15.35 % (2440545)Refutation not found, incomplete strategy % 102.51/15.35 % (2440545)------------------------------ % 102.51/15.35 % (2440545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 102.51/15.35 % (2440545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 102.51/15.35 % (2440545)CaDiCaL version: 2.1.3 % 102.51/15.35 % (2440545)Termination reason: Refutation not found, incomplete strategy % 102.51/15.35 % (2440545)Time elapsed: 0.325 s % 102.51/15.35 % (2440545)Peak memory usage: 130 MB % 102.51/15.35 % (2440545)Instructions burned: 886 (million) % 102.51/15.35 % (2440545)------------------------------ % 102.51/15.35 % (2440545)------------------------------ % 102.51/15.35 % (2440502)------------------------------ % 102.51/15.35 % (2440502)------------------------------ % 102.51/15.35 % (2440663)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=3205081581:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2868 on theBenchmark for (2868ds/5665Mi) % 102.51/15.35 % (2440679)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=1842544631:i=1532:ep=RS:ss=axioms_2867 on theBenchmark for (2867ds/1532Mi) % 102.51/15.35 [W928 06:59:46.151771768 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:46.151807855 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:46.151828356 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:46.151835174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 102.51/15.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 102.51/15.35 [W928 06:59:46.151848196 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151853683 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151876847 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151882113 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151894332 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151906518 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151919978 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.151925485 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 % (2440663)Refutation not found, incomplete strategy % 105.90/16.04 % (2440663)------------------------------ % 105.90/16.04 % (2440663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 105.90/16.04 % (2440663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 105.90/16.04 % (2440663)CaDiCaL version: 2.1.3 % 105.90/16.04 % (2440663)Termination reason: Refutation not found, incomplete strategy % 105.90/16.04 % (2440663)Time elapsed: 0.322 s % 105.90/16.04 % (2440663)Peak memory usage: 126 MB % 105.90/16.04 % (2440663)Instructions burned: 828 (million) % 105.90/16.04 [W928 06:59:46.469326160 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.469390094 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.469452151 register_special_ops.cpp:225] Warning: Creating a tensor from 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.90/16.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 105.90/16.04 [W928 06:59:46.469470968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469525712 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469544078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469586859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469604092 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469645582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469662406 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469703676 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:46.469720600 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 % (2440663)------------------------------ % 110.48/16.53 % (2440663)------------------------------ % 110.48/16.53 % (2440679)Refutation not found, incomplete strategy % 110.48/16.53 % (2440679)------------------------------ % 110.48/16.53 % (2440679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.48/16.53 % (2440679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.48/16.53 % (2440679)CaDiCaL version: 2.1.3 % 110.48/16.53 % (2440679)Termination reason: Refutation not found, incomplete strategy % 110.48/16.53 % (2440679)Time elapsed: 0.699 s % 110.48/16.53 % (2440679)Peak memory usage: 126 MB % 110.48/16.53 % (2440679)Instructions burned: 826 (million) % 110.48/16.53 % (2440760)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2329556595:i=1565:sd=2:ss=axioms:sgt=32_2861 on theBenchmark for (2861ds/1565Mi) % 110.48/16.53 [W928 06:59:47.165893392 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:47.165922767 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.48/16.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.48/16.53 [W928 06:59:47.165950321 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.165959920 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.165979803 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.165988287 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 % (2440679)------------------------------ % 112.26/16.96 % (2440679)------------------------------ % 112.26/16.96 % (2440484)Instruction limit reached! % 112.26/16.96 % (2440484)------------------------------ % 112.26/16.96 % (2440484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.26/16.96 % (2440484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/16.96 % (2440484)CaDiCaL version: 2.1.3 % 112.26/16.96 % (2440484)Termination reason: Instruction limit % 112.26/16.96 % (2440484)Termination phase: Saturation % 112.26/16.96 % (2440484)Time elapsed: 4.631 s % 112.26/16.96 % (2440484)Peak memory usage: 166 MB % 112.26/16.96 % (2440484)Instructions burned: 6996 (million) % 112.26/16.96 % (2440760)Refutation not found, incomplete strategy % 112.26/16.96 % (2440760)------------------------------ % 112.26/16.96 % (2440760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 112.26/16.96 % (2440760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 112.26/16.96 % (2440760)CaDiCaL version: 2.1.3 % 112.26/16.96 % (2440760)Termination reason: Refutation not found, incomplete strategy % 112.26/16.96 % (2440760)Time elapsed: 0.601 s % 112.26/16.96 % (2440760)Peak memory usage: 127 MB % 112.26/16.96 % (2440760)Instructions burned: 852 (million) % 112.26/16.96 % (2440762)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=734815534:i=1572:fgj=on:gsp=on_2854 on theBenchmark for (2854ds/1572Mi) % 112.26/16.96 % (2440763)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=39381011:i=6052:sd=4:ss=axioms:sgt=24_2853 on theBenchmark for (2853ds/6052Mi) % 112.26/16.96 % (2440760)------------------------------ % 112.26/16.96 % (2440760)------------------------------ % 112.26/16.96 [W928 06:59:47.849479856 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.849538391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.849563138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.849569525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 112.26/16.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 112.26/16.96 [W928 06:59:47.849583578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 [W928 06:59:47.849589586 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 % (2440454)Instruction limit reached! % 114.71/17.13 % (2440454)------------------------------ % 114.71/17.13 % (2440454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.71/17.13 % (2440454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.71/17.13 % (2440454)CaDiCaL version: 2.1.3 % 114.71/17.13 % (2440454)Termination reason: Instruction limit % 114.71/17.13 % (2440454)Termination phase: Saturation % 114.71/17.13 % (2440454)Time elapsed: 9.362 s % 114.71/17.13 % (2440454)Peak memory usage: 251 MB % 114.71/17.13 % (2440454)Instructions burned: 14124 (million) % 114.71/17.13 % (2440766)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=3319264059:i=3500:sd=1:bd=preordered:sup=off:ss=included_2848 on theBenchmark for (2848ds/3500Mi) % 114.71/17.13 % (2440763)Refutation not found, incomplete strategy % 114.71/17.13 % (2440763)------------------------------ % 114.71/17.13 % (2440763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 114.71/17.13 % (2440763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 114.71/17.13 % (2440763)CaDiCaL version: 2.1.3 % 114.71/17.13 % (2440763)Termination reason: Refutation not found, incomplete strategy % 114.71/17.13 % (2440763)Time elapsed: 0.390 s % 114.71/17.13 % (2440763)Peak memory usage: 127 MB % 114.71/17.13 % (2440763)Instructions burned: 855 (million) % 114.71/17.13 % (2440773)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=1773370545:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2847 on theBenchmark for (2847ds/1842Mi) % 114.71/17.13 % (2440763)------------------------------ % 114.71/17.13 % (2440763)------------------------------ % 114.71/17.13 % (2440817)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2035591068:i=66096:add=on_2845 on theBenchmark for (2845ds/66096Mi) % 114.71/17.13 [W928 06:59:48.342088747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 [W928 06:59:48.342129874 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 [W928 06:59:48.342168151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 [W928 06:59:48.342181628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 [W928 06:59:48.342207931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 114.71/17.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 114.71/17.13 [W928 06:59:48.342219234 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 % (2440762)Instruction limit reached! % 136.02/20.11 % (2440762)------------------------------ % 136.02/20.11 % (2440762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.02/20.11 % (2440762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.02/20.11 % (2440762)CaDiCaL version: 2.1.3 % 136.02/20.11 % (2440762)Termination reason: Instruction limit % 136.02/20.11 % (2440762)Termination phase: Saturation % 136.02/20.11 % (2440762)Time elapsed: 0.943 s % 136.02/20.11 % (2440762)Peak memory usage: 135 MB % 136.02/20.11 % (2440762)Instructions burned: 1574 (million) % 136.02/20.11 [W928 06:59:48.512889568 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 [W928 06:59:48.512937815 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 [W928 06:59:48.512972565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 [W928 06:59:48.512983578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 [W928 06:59:48.513022255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 [W928 06:59:48.513034836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 136.02/20.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 136.02/20.11 % (2440766)Refutation not found, incomplete strategy % 136.02/20.11 % (2440766)------------------------------ % 136.02/20.11 % (2440766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.02/20.11 % (2440766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.02/20.11 % (2440766)CaDiCaL version: 2.1.3 % 136.02/20.11 % (2440766)Termination reason: Refutation not found, incomplete strategy % 136.02/20.11 % (2440766)Time elapsed: 0.572 s % 136.02/20.11 % (2440766)Peak memory usage: 127 MB % 136.02/20.11 % (2440766)Instructions burned: 857 (million) % 136.02/20.11 % (2440863)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3351278774:i=1884:sd=1:nm=60:ss=axioms_2842 on theBenchmark for (2842ds/1884Mi) % 136.02/20.11 % (2440773)Refutation not found, incomplete strategy % 136.02/20.11 % (2440773)------------------------------ % 136.02/20.11 % (2440773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 136.02/20.11 % (2440773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 136.02/20.11 % (2440773)CaDiCaL version: 2.1.3 % 136.02/20.11 % (2440773)Termination reason: Refutation not found, incomplete strategy % 136.02/20.11 % (2440773)Time elapsed: 0.573 s % 136.02/20.11 % (2440773)Peak memory usage: 127 MB % 136.02/20.11 % (2440773)Instructions burned: 858 (million) % 136.02/20.11 % (2440766)------------------------------ % 136.02/20.11 % (2440766)------------------------------ % 136.02/20.11 [W928 06:59:48.775917139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.775950617 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.775971850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.775977913 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.775991758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.775997223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.776024519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.776045229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.776063660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.776069000 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.776081877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 [W928 06:59:48.776087068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.32/20.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.32/20.52 % (2440863)Refutation not found, incomplete strategy % 139.32/20.52 % (2440863)------------------------------ % 139.32/20.52 % (2440863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.32/20.52 % (2440863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.32/20.52 % (2440863)CaDiCaL version: 2.1.3 % 139.32/20.52 % (2440863)Termination reason: Refutation not found, incomplete strategy % 139.32/20.52 % (2440863)Time elapsed: 0.316 s % 139.32/20.52 % (2440863)Peak memory usage: 126 MB % 139.32/20.52 % (2440863)Instructions burned: 826 (million) % 139.32/20.52 % (2440773)------------------------------ % 140.95/20.88 % (2440773)------------------------------ % 140.95/20.88 % (2440868)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2241722643:cts=off:i=5469:bs=on:fsr=off_2838 on theBenchmark for (2838ds/5469Mi) % 140.95/20.88 % (2440863)------------------------------ % 140.95/20.88 % (2440863)------------------------------ % 140.95/20.88 % (2440870)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=3992247905:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2837 on theBenchmark for (2837ds/2037Mi) % 140.95/20.88 % (2440871)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=984167771:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2836 on theBenchmark for (2836ds/2110Mi) % 140.95/20.88 % (2440871)Instruction limit reached! % 140.95/20.88 % (2440871)------------------------------ % 140.95/20.88 % (2440871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/20.88 % (2440871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/20.88 % (2440871)CaDiCaL version: 2.1.3 % 140.95/20.88 % (2440871)Termination reason: Instruction limit % 140.95/20.88 % (2440871)Termination phase: Saturation % 140.95/20.88 % (2440871)Time elapsed: 0.730 s % 140.95/20.88 % (2440871)Peak memory usage: 136 MB % 140.95/20.88 % (2440871)Instructions burned: 2110 (million) % 140.95/20.88 % (2440875)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=2027804868:i=2430:add=off:aac=none:nm=16_2827 on theBenchmark for (2827ds/2430Mi) % 140.95/20.88 % (2440870)Instruction limit reached! % 140.95/20.88 % (2440870)------------------------------ % 140.95/20.88 % (2440870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/20.88 % (2440870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/20.88 % (2440870)CaDiCaL version: 2.1.3 % 140.95/20.88 % (2440870)Termination reason: Instruction limit % 140.95/20.88 % (2440870)Termination phase: Saturation % 140.95/20.88 % (2440870)Time elapsed: 1.266 s % 140.95/20.88 % (2440870)Peak memory usage: 139 MB % 140.95/20.88 % (2440870)Instructions burned: 2037 (million) % 140.95/20.88 % (2440877)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=3379854062:cond=fast:i=4891_2822 on theBenchmark for (2822ds/4891Mi) % 140.95/20.88 % (2440875)Instruction limit reached! % 140.95/20.88 % (2440875)------------------------------ % 140.95/20.88 % (2440875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/20.88 % (2440875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/20.88 % (2440875)CaDiCaL version: 2.1.3 % 140.95/20.88 % (2440875)Termination reason: Instruction limit % 140.95/20.88 % (2440875)Termination phase: Saturation % 140.95/20.88 % (2440875)Time elapsed: 1.332 s % 140.95/20.88 % (2440875)Peak memory usage: 139 MB % 140.95/20.88 % (2440875)Instructions burned: 2430 (million) % 140.95/20.88 % (2440879)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=1937425205:st=2:i=14845:sd=2:ss=included:fsd=on_2812 on theBenchmark for (2812ds/14845Mi) % 140.95/20.88 % (2440868)Instruction limit reached! % 140.95/20.88 % (2440868)------------------------------ % 140.95/20.88 % (2440868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.95/20.88 % (2440868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.95/20.88 % (2440868)CaDiCaL version: 2.1.3 % 140.95/20.88 % (2440868)Termination reason: Instruction limit % 140.95/20.88 % (2440868)Termination phase: Saturation % 140.95/20.88 % (2440868)Time elapsed: 2.828 s % 140.95/20.88 % (2440868)Peak memory usage: 113 MB % 140.95/20.88 % (2440868)Instructions burned: 5471 (million) % 140.95/20.88 [W928 06:59:51.926905720 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/20.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.95/20.88 [W928 06:59:51.926939610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:51.926974974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:51.926997951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:51.927035661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:51.927046268 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 % (2440881)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2639818813:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2808 on theBenchmark for (2808ds/7534Mi) % 146.04/21.65 % (2440879)Refutation not found, incomplete strategy % 146.04/21.65 % (2440879)------------------------------ % 146.04/21.65 % (2440879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.65 % (2440879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.65 % (2440879)CaDiCaL version: 2.1.3 % 146.04/21.65 % (2440879)Termination reason: Refutation not found, incomplete strategy % 146.04/21.65 % (2440879)Time elapsed: 0.590 s % 146.04/21.65 % (2440879)Peak memory usage: 128 MB % 146.04/21.65 % (2440879)Instructions burned: 887 (million) % 146.04/21.65 % (2440877)Instruction limit reached! % 146.04/21.65 % (2440877)------------------------------ % 146.04/21.65 % (2440877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 146.04/21.65 % (2440877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 146.04/21.65 % (2440877)CaDiCaL version: 2.1.3 % 146.04/21.65 % (2440877)Termination reason: Instruction limit % 146.04/21.65 % (2440877)Termination phase: Saturation % 146.04/21.65 % (2440877)Time elapsed: 1.766 s % 146.04/21.65 % (2440877)Peak memory usage: 167 MB % 146.04/21.65 % (2440877)Instructions burned: 4891 (million) % 146.04/21.65 [W928 06:59:52.336829410 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:52.336875627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:52.336910460 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:52.336921917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 146.04/21.65 [W928 06:59:52.336948947 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 146.04/21.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 [W928 06:59:52.336961091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 % (2440879)------------------------------ % 152.23/22.43 % (2440879)------------------------------ % 152.23/22.43 % (2440883)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=3612532781:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2803 on theBenchmark for (2803ds/10353Mi) % 152.23/22.43 % (2440881)Refutation not found, incomplete strategy % 152.23/22.43 % (2440881)------------------------------ % 152.23/22.43 % (2440881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.23/22.43 % (2440881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.23/22.43 % (2440881)CaDiCaL version: 2.1.3 % 152.23/22.43 % (2440881)Termination reason: Refutation not found, incomplete strategy % 152.23/22.43 % (2440881)Time elapsed: 0.574 s % 152.23/22.43 % (2440881)Peak memory usage: 127 MB % 152.23/22.43 % (2440881)Instructions burned: 858 (million) % 152.23/22.43 % (2440884)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=884603792:i=7860_2802 on theBenchmark for (2802ds/7860Mi) % 152.23/22.43 % (2440884)Refutation not found, incomplete strategy % 152.23/22.43 % (2440884)------------------------------ % 152.23/22.43 % (2440884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.23/22.43 % (2440884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.23/22.43 % (2440884)CaDiCaL version: 2.1.3 % 152.23/22.43 % (2440884)Termination reason: Refutation not found, incomplete strategy % 152.23/22.43 % (2440884)Time elapsed: 0.005 s % 152.23/22.43 % (2440884)Peak memory usage: 88 MB % 152.23/22.43 % (2440884)Instructions burned: 8 (million) % 152.23/22.43 [W928 06:59:52.641907380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 [W928 06:59:52.641945283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 [W928 06:59:52.641965244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 [W928 06:59:52.641972591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 [W928 06:59:52.641985658 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 [W928 06:59:52.641991137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 152.23/22.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 152.23/22.43 % (2440494)Instruction limit reached! % 152.23/22.43 % (2440494)------------------------------ % 152.23/22.43 % (2440494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 152.23/22.43 % (2440494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 152.23/22.43 % (2440494)CaDiCaL version: 2.1.3 % 153.26/22.61 % (2440494)Termination reason: Instruction limit % 153.26/22.61 % (2440494)Termination phase: Saturation % 153.26/22.61 % (2440494)Time elapsed: 9.292 s % 153.26/22.61 % (2440494)Peak memory usage: 236 MB % 153.26/22.61 % (2440494)Instructions burned: 13494 (million) % 153.26/22.61 % (2440883)Refutation not found, incomplete strategy % 153.26/22.61 % (2440883)------------------------------ % 153.26/22.61 % (2440883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.26/22.61 % (2440883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.26/22.61 % (2440883)CaDiCaL version: 2.1.3 % 153.26/22.61 % (2440883)Termination reason: Refutation not found, incomplete strategy % 153.26/22.61 % (2440883)Time elapsed: 0.317 s % 153.26/22.61 % (2440883)Peak memory usage: 128 MB % 153.26/22.61 % (2440883)Instructions burned: 856 (million) % 153.26/22.61 % (2440881)------------------------------ % 153.26/22.61 % (2440881)------------------------------ % 153.26/22.61 % (2440884)------------------------------ % 153.26/22.61 % (2440884)------------------------------ % 153.26/22.61 % (2440887)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=3907358514:i=7896:sd=2:bs=on:ss=included:sgt=20_2799 on theBenchmark for (2799ds/7896Mi) % 153.26/22.61 % (2440883)------------------------------ % 153.26/22.61 % (2440883)------------------------------ % 153.26/22.61 % (2440888)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=1886694905:i=5812:gtgl=2:gtg=all_2798 on theBenchmark for (2798ds/5812Mi) % 153.26/22.61 % (2440889)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=353825342:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2798 on theBenchmark for (2798ds/2965Mi) % 153.26/22.61 % (2440891)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=3582089942:i=2967:kws=precedence:bd=preordered:av=off_2797 on theBenchmark for (2797ds/2967Mi) % 153.26/22.61 [W928 06:59:53.268735343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.26/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.26/22.61 [W928 06:59:53.268767810 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.26/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.26/22.61 [W928 06:59:53.268803147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.26/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.26/22.61 [W928 06:59:53.268816440 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.26/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.26/22.61 [W928 06:59:53.268842294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.26/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.26/22.61 [W928 06:59:53.268854301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 153.26/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 153.26/22.61 % (2440887)Refutation not found, incomplete strategy % 153.26/22.61 % (2440887)------------------------------ % 153.26/22.61 % (2440887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 153.26/22.61 % (2440887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 153.26/22.61 % (2440887)CaDiCaL version: 2.1.3 % 153.26/22.61 % (2440887)Termination reason: Refutation not found, incomplete strategy % 160.55/23.58 % (2440887)Time elapsed: 0.572 s % 160.55/23.58 % (2440887)Peak memory usage: 128 MB % 160.55/23.58 % (2440887)Instructions burned: 856 (million) % 160.55/23.58 % (2440889)Refutation not found, incomplete strategy % 160.55/23.58 % (2440889)------------------------------ % 160.55/23.58 % (2440889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.55/23.58 % (2440889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.55/23.58 % (2440889)CaDiCaL version: 2.1.3 % 160.55/23.58 % (2440889)Termination reason: Refutation not found, incomplete strategy % 160.55/23.58 % (2440889)Time elapsed: 0.580 s % 160.55/23.58 % (2440889)Peak memory usage: 130 MB % 160.55/23.58 % (2440889)Instructions burned: 880 (million) % 160.55/23.58 % (2440887)------------------------------ % 160.55/23.58 % (2440887)------------------------------ % 160.55/23.58 % (2440889)------------------------------ % 160.55/23.58 % (2440889)------------------------------ % 160.55/23.58 % (2440895)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=247756708:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2789 on theBenchmark for (2789ds/3022Mi) % 160.55/23.58 % (2440896)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=332846616:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2788 on theBenchmark for (2788ds/3207Mi) % 160.55/23.58 % (2440891)Instruction limit reached! % 160.55/23.58 % (2440891)------------------------------ % 160.55/23.58 % (2440891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 160.55/23.58 % (2440891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 160.55/23.58 % (2440891)CaDiCaL version: 2.1.3 % 160.55/23.58 % (2440891)Termination reason: Instruction limit % 160.55/23.58 % (2440891)Termination phase: Saturation % 160.55/23.58 % (2440891)Time elapsed: 0.989 s % 160.55/23.58 % (2440891)Peak memory usage: 146 MB % 160.55/23.58 % (2440891)Instructions burned: 2970 (million) % 160.55/23.58 % (2440899)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2067560574:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2786 on theBenchmark for (2786ds/3289Mi) % 160.55/23.58 [W928 06:59:54.248324999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.55/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.55/23.58 [W928 06:59:54.248369103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.55/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.55/23.58 [W928 06:59:54.248406756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.55/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.55/23.58 [W928 06:59:54.248424970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.55/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.55/23.58 [W928 06:59:54.248451103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.55/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.55/23.58 [W928 06:59:54.248463083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 160.55/23.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 160.55/23.58 [W928 06:59:54.248488720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.248500837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.248524757 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.248546674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.248572888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.248583921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.380885424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.380930421 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.380965584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.380976971 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.381025045 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 [W928 06:59:54.381038405 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 196.71/28.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 196.71/28.69 % (2440895)Refutation not found, incomplete strategy % 196.71/28.69 % (2440895)------------------------------ % 196.71/28.69 % (2440895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 196.71/28.69 % (2440895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.71/28.69 % (2440895)CaDiCaL version: 2.1.3 % 196.71/28.69 % (2440895)Termination reason: Refutation not found, incomplete strategy % 196.71/28.69 % (2440895)Time elapsed: 0.553 s % 235.60/34.14 % (2440895)Peak memory usage: 126 MB % 235.60/34.14 % (2440895)Instructions burned: 828 (million) % 235.60/34.14 % (2440899)Refutation not found, incomplete strategy % 235.60/34.14 % (2440899)------------------------------ % 235.60/34.14 % (2440899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.60/34.14 % (2440899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.60/34.14 % (2440899)CaDiCaL version: 2.1.3 % 235.60/34.14 % (2440899)Termination reason: Refutation not found, incomplete strategy % 235.60/34.14 % (2440899)Time elapsed: 0.353 s % 235.60/34.14 % (2440899)Peak memory usage: 130 MB % 235.60/34.14 % (2440899)Instructions burned: 887 (million) % 235.60/34.14 % (2440896)Refutation not found, incomplete strategy % 235.60/34.14 % (2440896)------------------------------ % 235.60/34.14 % (2440896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.60/34.14 % (2440896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 235.60/34.14 % (2440896)CaDiCaL version: 2.1.3 % 235.60/34.14 % (2440896)Termination reason: Refutation not found, incomplete strategy % 235.60/34.14 % (2440896)Time elapsed: 0.592 s % 235.60/34.14 % (2440896)Peak memory usage: 128 MB % 235.60/34.14 % (2440896)Instructions burned: 887 (million) % 235.60/34.14 % (2440895)------------------------------ % 235.60/34.14 % (2440895)------------------------------ % 235.60/34.14 % (2440899)------------------------------ % 235.60/34.14 % (2440899)------------------------------ % 235.60/34.14 % (2440896)------------------------------ % 235.60/34.14 % (2440896)------------------------------ % 235.60/34.14 % (2440901)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3597073128:i=38569:sd=3:ss=axioms:sgt=32_2780 on theBenchmark for (2780ds/38569Mi) % 235.60/34.14 % (2440902)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2712910136:cts=off:i=3394_2779 on theBenchmark for (2779ds/3394Mi) % 235.60/34.14 % (2440903)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=1991206626:i=33824:bd=preordered_2779 on theBenchmark for (2779ds/33824Mi) % 235.60/34.14 [W928 06:59:55.211944438 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.60/34.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.60/34.14 [W928 06:59:55.211990159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.60/34.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.60/34.14 [W928 06:59:55.212036442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.60/34.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.60/34.14 [W928 06:59:55.212049699 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.60/34.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.60/34.14 [W928 06:59:55.212073656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.60/34.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.60/34.14 [W928 06:59:55.212086716 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 235.60/34.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 235.60/34.14 % (2440901)Refutation not found, incomplete strategy % 235.60/34.14 % (2440901)------------------------------ % 235.60/34.14 % (2440901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 235.60/34.14 % (2440901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.61/34.91 % (2440901)CaDiCaL version: 2.1.3 % 240.61/34.91 % (2440901)Termination reason: Refutation not found, incomplete strategy % 240.61/34.91 % (2440901)Time elapsed: 0.564 s % 240.61/34.91 % (2440901)Peak memory usage: 127 MB % 240.61/34.91 % (2440901)Instructions burned: 852 (million) % 240.61/34.91 % (2440901)------------------------------ % 240.61/34.91 % (2440901)------------------------------ % 240.61/34.91 % (2440907)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=3968557228:i=20684:bd=all:gtg=exists_sym_2770 on theBenchmark for (2770ds/20684Mi) % 240.61/34.91 % (2440902)Instruction limit reached! % 240.61/34.91 % (2440902)------------------------------ % 240.61/34.91 % (2440902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.61/34.91 % (2440902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.61/34.91 % (2440902)CaDiCaL version: 2.1.3 % 240.61/34.91 % (2440902)Termination reason: Instruction limit % 240.61/34.91 % (2440902)Termination phase: Saturation % 240.61/34.91 % (2440902)Time elapsed: 1.177 s % 240.61/34.91 % (2440902)Peak memory usage: 145 MB % 240.61/34.91 % (2440902)Instructions burned: 3396 (million) % 240.61/34.91 % (2440909)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=3888093356: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_2766 on theBenchmark for (2766ds/7222Mi) % 240.61/34.91 % (2440888)Instruction limit reached! % 240.61/34.91 % (2440888)------------------------------ % 240.61/34.91 % (2440888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.61/34.91 % (2440888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.61/34.91 % (2440888)CaDiCaL version: 2.1.3 % 240.61/34.91 % (2440888)Termination reason: Instruction limit % 240.61/34.91 % (2440888)Termination phase: Saturation % 240.61/34.91 % (2440888)Time elapsed: 3.682 s % 240.61/34.91 % (2440888)Peak memory usage: 171 MB % 240.61/34.91 % (2440888)Instructions burned: 5813 (million) % 240.61/34.91 % (2440911)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3516778946:st=4:i=7295:sd=4:ep=R:ss=axioms_2760 on theBenchmark for (2760ds/7295Mi) % 240.61/34.91 % (2440909)Instruction limit reached! % 240.61/34.91 % (2440909)------------------------------ % 240.61/34.91 % (2440909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.61/34.91 % (2440909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.61/34.91 % (2440909)CaDiCaL version: 2.1.3 % 240.61/34.91 % (2440909)Termination reason: Instruction limit % 240.61/34.91 % (2440909)Termination phase: Saturation % 240.61/34.91 % (2440909)Time elapsed: 2.441 s % 240.61/34.91 % (2440909)Peak memory usage: 197 MB % 240.61/34.91 % (2440909)Instructions burned: 7222 (million) % 240.61/34.91 % (2440913)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=1321294632:i=4036:ins=10_2740 on theBenchmark for (2740ds/4036Mi) % 240.61/34.91 % (2440913)Instruction limit reached! % 240.61/34.91 % (2440913)------------------------------ % 240.61/34.91 % (2440913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.61/34.91 % (2440913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.61/34.91 % (2440913)CaDiCaL version: 2.1.3 % 240.61/34.91 % (2440913)Termination reason: Instruction limit % 240.61/34.91 % (2440913)Termination phase: Saturation % 240.61/34.91 % (2440913)Time elapsed: 1.318 s % 240.61/34.91 % (2440913)Peak memory usage: 155 MB % 240.61/34.91 % (2440913)Instructions burned: 4037 (million) % 240.61/34.91 % (2440973)lrs+10_1_sil=128000:lcm=predicate:random_seed=672146980:st=3:i=43697:sd=5:ss=axioms_2725 on theBenchmark for (2725ds/43697Mi) % 240.61/34.91 % (2440973)Refutation not found, incomplete strategy % 240.61/34.91 % (2440973)------------------------------ % 240.61/34.91 % (2440973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 240.61/34.91 % (2440973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 240.61/34.91 % (2440973)CaDiCaL version: 2.1.3 % 240.61/34.91 % (2440973)Termination reason: Refutation not found, incomplete strategy % 240.61/34.91 % (2440973)Time elapsed: 0.001 s % 240.61/34.91 % (2440973)Peak memory usage: 88 MB % 240.61/34.91 % (2440973)------------------------------ % 240.61/34.91 % (2440973)------------------------------ % 240.61/34.91 % (2440975)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=3260247055:i=17599:gtg=all:ss=axioms:fsd=on_2722 on theBenchmark for (2722ds/17599Mi) % 246.89/36.01 % (2440512)Instruction limit reached! % 246.89/36.01 % (2440512)------------------------------ % 246.89/36.01 % (2440512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.89/36.01 % (2440512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.89/36.01 % (2440512)CaDiCaL version: 2.1.3 % 246.89/36.01 % (2440512)Termination reason: Instruction limit % 246.89/36.01 % (2440512)Termination phase: Saturation % 246.89/36.01 % (2440512)Time elapsed: 15.920 s % 246.89/36.01 % (2440512)Peak memory usage: 1254 MB % 246.89/36.01 % (2440512)Instructions burned: 26474 (million) % 246.89/36.01 % (2440977)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=2485369081:i=4547:bd=preordered_2713 on theBenchmark for (2713ds/4547Mi) % 246.89/36.01 % (2440911)Instruction limit reached! % 246.89/36.01 % (2440911)------------------------------ % 246.89/36.01 % (2440911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.89/36.01 % (2440911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.89/36.01 % (2440911)CaDiCaL version: 2.1.3 % 246.89/36.01 % (2440911)Termination reason: Instruction limit % 246.89/36.01 % (2440911)Termination phase: Saturation % 246.89/36.01 % (2440911)Time elapsed: 4.711 s % 246.89/36.01 % (2440911)Peak memory usage: 183 MB % 246.89/36.01 % (2440911)Instructions burned: 7295 (million) % 246.89/36.01 % (2440979)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=1841611723:i=9294:av=off_2711 on theBenchmark for (2711ds/9294Mi) % 246.89/36.01 % (2440977)Instruction limit reached! % 246.89/36.01 % (2440977)------------------------------ % 246.89/36.01 % (2440977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.89/36.01 % (2440977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.89/36.01 % (2440977)CaDiCaL version: 2.1.3 % 246.89/36.01 % (2440977)Termination reason: Instruction limit % 246.89/36.01 % (2440977)Termination phase: Saturation % 246.89/36.01 % (2440977)Time elapsed: 2.795 s % 246.89/36.01 % (2440977)Peak memory usage: 159 MB % 246.89/36.01 % (2440977)Instructions burned: 4547 (million) % 246.89/36.01 % (2440981)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2384107302:i=32849:add=on_2684 on theBenchmark for (2684ds/32849Mi) % 246.89/36.01 % (2440975)Instruction limit reached! % 246.89/36.01 % (2440975)------------------------------ % 246.89/36.01 % (2440975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 246.89/36.01 % (2440975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 246.89/36.01 % (2440975)CaDiCaL version: 2.1.3 % 246.89/36.01 % (2440975)Termination reason: Instruction limit % 246.89/36.01 % (2440975)Termination phase: Saturation % 246.89/36.01 % (2440975)Time elapsed: 5.106 s % 246.89/36.01 % (2440975)Peak memory usage: 177 MB % 246.89/36.01 % (2440975)Instructions burned: 17600 (million) % 246.89/36.01 % (2440983)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1337966529:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2670 on theBenchmark for (2670ds/4793Mi) % 246.89/36.01 [W928 07:00:05.957618281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 246.89/36.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.89/36.01 [W928 07:00:05.957640824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 246.89/36.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.89/36.01 [W928 07:00:05.957662621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 246.89/36.01 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 246.89/36.01 [W928 07:00:05.957669909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957684461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957690137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957703598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957716880 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957730777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957736731 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957750137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 [W928 07:00:05.957755683 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 282.21/40.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 282.21/40.73 % (2440983)Refutation not found, incomplete strategy % 282.21/40.73 % (2440983)------------------------------ % 282.21/40.73 % (2440983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.21/40.73 % (2440983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.21/40.73 % (2440983)CaDiCaL version: 2.1.3 % 282.21/40.73 % (2440983)Termination reason: Refutation not found, incomplete strategy % 282.21/40.73 % (2440983)Time elapsed: 0.317 s % 282.21/40.73 % (2440983)Peak memory usage: 126 MB % 282.21/40.73 % (2440983)Instructions burned: 826 (million) % 282.21/40.73 % (2440983)------------------------------ % 282.21/40.73 % (2440983)------------------------------ % 282.21/40.73 % (2440985)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=3397808695:i=4840:nm=4:av=off_2664 on theBenchmark for (2664ds/4840Mi) % 282.21/40.73 % (2440985)Refutation not found, incomplete strategy % 282.21/40.73 % (2440985)------------------------------ % 282.21/40.73 % (2440985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 282.21/40.73 % (2440985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 282.21/40.73 % (2440985)CaDiCaL version: 2.1.3 % 282.21/40.73 % (2440985)Termination reason: Refutation not found, incomplete strategy % 282.21/40.73 % (2440985)Time elapsed: 0.353 s % 282.21/40.73 % (2440985)Peak memory usage: 130 MB % 282.21/40.73 % (2440985)Instructions burned: 888 (million) % 300.67/43.33 % (2440985)------------------------------ % 300.67/43.33 % (2440985)------------------------------ % 300.67/43.33 % (2440987)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=1203623552:cts=off:i=5002_2657 on theBenchmark for (2657ds/5002Mi) % 300.67/43.33 % (2440979)Instruction limit reached! % 300.67/43.33 % (2440979)------------------------------ % 300.67/43.33 % (2440979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 300.67/43.33 % (2440979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.67/43.33 % (2440979)CaDiCaL version: 2.1.3 % 300.67/43.33 % (2440979)Termination reason: Instruction limit % 300.67/43.33 % (2440979)Termination phase: Saturation % 300.67/43.33 % (2440979)Time elapsed: 5.558 s % 300.67/43.33 % (2440979)Peak memory usage: 176 MB % 300.67/43.33 % (2440979)Instructions burned: 9295 (million) % 300.67/43.33 % (2440989)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=3881986935:i=30479:sd=3:ss=axioms_2653 on theBenchmark for (2653ds/30479Mi) % 300.67/43.33 [W928 07:00:07.824444239 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824489333 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824529097 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824541043 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824565507 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824576677 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824601004 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824612307 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824636881 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 300.67/43.33 [W928 07:00:07.824648247 register_special_ops.cpp:225] Warning: Creating a tensor from 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.67/43.33 Pass in a dtype argument to en % 300.67/43.34 Terminated %------------------------------------------------------------------------------