%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : GRP396+1 : TPTP v9.3.1. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n016.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 10:13:50 AM UTC 2026 % Result : Satisfiable 89.88s 14.48s % Output : Saturation 89.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : GRP396+1 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.38 % Computer : n016.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Sun Sep 27 10:06:17 UTC 2026 % 0.12/0.39 % CPUTime : % 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.12/0.42 Running first-order theorem proving % 0.12/0.42 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 % 3.10/1.38 % (2389171)Detected formulas, will run a generic FOF schedule. % 3.10/1.38 % (2389179)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3223526715:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 3.10/1.38 % (2389179)Refutation not found, incomplete strategy % 3.10/1.38 % (2389179)------------------------------ % 3.10/1.38 % (2389179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.10/1.38 % (2389179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.10/1.38 % (2389179)CaDiCaL version: 2.1.3 % 3.10/1.38 % (2389179)Termination reason: Refutation not found, incomplete strategy % 3.10/1.38 % (2389179)Time elapsed: 0.0000 s % 3.10/1.38 % (2389179)Peak memory usage: 86 MB % 3.10/1.38 % (2389180)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=815231275:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 3.10/1.38 % (2389180)Refutation not found, incomplete strategy % 3.10/1.38 % (2389180)------------------------------ % 3.10/1.38 % (2389180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.10/1.38 % (2389180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.10/1.38 % (2389180)CaDiCaL version: 2.1.3 % 3.10/1.38 % (2389180)Termination reason: Refutation not found, incomplete strategy % 3.10/1.38 % (2389180)Time elapsed: 0.0000 s % 3.10/1.38 % (2389180)Peak memory usage: 86 MB % 3.10/1.38 % (2389176)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=439849551:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 3.10/1.38 % (2389178)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=2448845043:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 3.10/1.38 % (2389177)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=1070027926:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 3.10/1.38 % (2389181)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3946826681:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 3.10/1.38 % (2389182)dis-21_1_sil=8000:lcm=predicate:random_seed=162704945:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 3.10/1.38 % (2389182)Refutation not found, incomplete strategy % 3.10/1.38 % (2389182)------------------------------ % 3.10/1.38 % (2389182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.10/1.38 % (2389182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.10/1.38 % (2389182)CaDiCaL version: 2.1.3 % 3.10/1.38 % (2389182)Termination reason: Refutation not found, incomplete strategy % 3.10/1.38 % (2389182)Time elapsed: 0.0000 s % 3.10/1.38 % (2389182)Peak memory usage: 86 MB % 3.10/1.38 % (2389181)Instruction limit reached! % 3.10/1.38 % (2389181)------------------------------ % 3.10/1.38 % (2389181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.10/1.38 % (2389181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.10/1.38 % (2389181)CaDiCaL version: 2.1.3 % 3.10/1.38 % (2389181)Termination reason: Instruction limit % 3.10/1.38 % (2389181)Termination phase: Saturation % 3.10/1.38 % (2389181)Time elapsed: 0.080 s % 3.10/1.38 % (2389181)Peak memory usage: 89 MB % 3.10/1.38 % (2389181)Instructions burned: 140 (million) % 3.10/1.38 % (2389179)------------------------------ % 3.10/1.38 % (2389179)------------------------------ % 3.10/1.38 % (2389191)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1400658658:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 3.10/1.38 % (2389191)Refutation not found, incomplete strategy % 3.10/1.38 % (2389191)------------------------------ % 3.10/1.38 % (2389191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.10/1.38 % (2389191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.10/1.38 % (2389191)CaDiCaL version: 2.1.3 % 3.10/1.38 % (2389191)Termination reason: Refutation not found, incomplete strategy % 3.10/1.38 % (2389191)Time elapsed: 0.0000 s % 3.10/1.38 % (2389191)Peak memory usage: 87 MB % 3.10/1.38 % (2389190)lrs+10_1_sil=8000:sp=occurrence:random_seed=3853814352:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi) % 4.87/1.67 % (2389190)Refutation not found, incomplete strategy % 4.87/1.67 % (2389190)------------------------------ % 4.87/1.67 % (2389190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.87/1.67 % (2389190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.87/1.67 % (2389190)CaDiCaL version: 2.1.3 % 4.87/1.67 % (2389190)Termination reason: Refutation not found, incomplete strategy % 4.87/1.67 % (2389190)Time elapsed: 0.0000 s % 4.87/1.67 % (2389190)Peak memory usage: 86 MB % 4.87/1.67 % (2389180)------------------------------ % 4.87/1.67 % (2389180)------------------------------ % 4.87/1.67 % (2389182)------------------------------ % 4.87/1.67 % (2389182)------------------------------ % 4.87/1.67 % (2389191)------------------------------ % 4.87/1.67 % (2389191)------------------------------ % 4.87/1.67 % (2389194)lrs+1011_1_sil=32000:sp=occurrence:random_seed=974617507:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 4.87/1.67 % (2389194)Refutation not found, incomplete strategy % 4.87/1.67 % (2389194)------------------------------ % 4.87/1.67 % (2389194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.87/1.67 % (2389194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.87/1.67 % (2389194)CaDiCaL version: 2.1.3 % 4.87/1.67 % (2389194)Termination reason: Refutation not found, incomplete strategy % 4.87/1.67 % (2389194)Time elapsed: 0.0000 s % 4.87/1.67 % (2389194)Peak memory usage: 86 MB % 4.87/1.67 [W927 10:06:18.156456638 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156502278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156540048 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156558005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156584132 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156595258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156621205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156631118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 4.87/1.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 4.87/1.67 [W927 10:06:18.156658848 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156669442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156700602 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156723718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156736145 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156761075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156797268 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156809548 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156833972 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156844922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156869969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156881442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156908519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.74/2.12 [W927 10:06:18.156921782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 8.74/2.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.39/2.18 [W927 10:06:18.156947182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.39/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.39/2.18 [W927 10:06:18.157024385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 9.39/2.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 9.39/2.18 % (2389195)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=1183143840:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 9.39/2.18 % (2389195)Refutation not found, incomplete strategy % 9.39/2.18 % (2389195)------------------------------ % 9.39/2.18 % (2389195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.39/2.18 % (2389195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.39/2.18 % (2389195)CaDiCaL version: 2.1.3 % 9.39/2.18 % (2389195)Termination reason: Refutation not found, incomplete strategy % 9.39/2.18 % (2389195)Time elapsed: 0.001 s % 9.39/2.18 % (2389195)Peak memory usage: 88 MB % 9.39/2.18 % (2389196)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2809395221:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 9.39/2.18 % (2389196)Refutation not found, incomplete strategy % 9.39/2.18 % (2389196)------------------------------ % 9.39/2.18 % (2389196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.39/2.18 % (2389196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.39/2.18 % (2389196)CaDiCaL version: 2.1.3 % 9.39/2.18 % (2389196)Termination reason: Refutation not found, incomplete strategy % 9.39/2.18 % (2389196)Time elapsed: 0.0000 s % 9.39/2.18 % (2389196)Peak memory usage: 86 MB % 9.39/2.18 % (2389190)------------------------------ % 9.39/2.18 % (2389190)------------------------------ % 9.39/2.18 % (2389177)Refutation not found, incomplete strategy % 9.39/2.18 % (2389177)------------------------------ % 9.39/2.18 % (2389177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.39/2.18 % (2389177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.39/2.18 % (2389177)CaDiCaL version: 2.1.3 % 9.39/2.18 % (2389177)Termination reason: Refutation not found, incomplete strategy % 9.39/2.18 % (2389177)Time elapsed: 0.557 s % 9.39/2.18 % (2389177)Peak memory usage: 124 MB % 9.39/2.18 % (2389177)Instructions burned: 824 (million) % 9.39/2.18 % (2389178)Refutation not found, incomplete strategy % 9.39/2.18 % (2389178)------------------------------ % 9.39/2.18 % (2389178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.39/2.18 % (2389178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.39/2.18 % (2389178)CaDiCaL version: 2.1.3 % 9.39/2.18 % (2389178)Termination reason: Refutation not found, incomplete strategy % 9.39/2.18 % (2389178)Time elapsed: 0.558 s % 9.39/2.18 % (2389178)Peak memory usage: 125 MB % 9.39/2.18 % (2389178)Instructions burned: 825 (million) % 9.39/2.18 % (2389196)------------------------------ % 9.39/2.18 % (2389196)------------------------------ % 9.39/2.18 % (2389200)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=451596632:i=2350_2994 on theBenchmark for (2994ds/2350Mi) % 9.39/2.18 % (2389194)------------------------------ % 9.39/2.18 % (2389194)------------------------------ % 9.39/2.18 % (2389195)------------------------------ % 9.39/2.18 % (2389195)------------------------------ % 9.39/2.18 % (2389201)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1624651356:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi) % 9.39/2.18 % (2389201)Refutation not found, incomplete strategy % 9.39/2.18 % (2389201)------------------------------ % 9.39/2.18 % (2389201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 9.39/2.18 % (2389201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 9.39/2.18 % (2389201)CaDiCaL version: 2.1.3 % 9.39/2.18 % (2389201)Termination reason: Refutation not found, incomplete strategy % 9.39/2.18 % (2389201)Time elapsed: 0.0000 s % 11.88/2.61 % (2389201)Peak memory usage: 86 MB % 11.88/2.61 % (2389204)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3459633889:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi) % 11.88/2.61 % (2389204)Refutation not found, incomplete strategy % 11.88/2.61 % (2389204)------------------------------ % 11.88/2.61 % (2389204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.61 % (2389204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.61 % (2389204)CaDiCaL version: 2.1.3 % 11.88/2.61 % (2389204)Termination reason: Refutation not found, incomplete strategy % 11.88/2.61 % (2389204)Time elapsed: 0.0000 s % 11.88/2.61 % (2389204)Peak memory usage: 86 MB % 11.88/2.61 % (2389205)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1611147978:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 11.88/2.61 % (2389205)Refutation not found, incomplete strategy % 11.88/2.61 % (2389205)------------------------------ % 11.88/2.61 % (2389205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.61 % (2389205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.61 % (2389205)CaDiCaL version: 2.1.3 % 11.88/2.61 % (2389205)Termination reason: Refutation not found, incomplete strategy % 11.88/2.61 % (2389205)Time elapsed: 0.001 s % 11.88/2.61 % (2389205)Peak memory usage: 87 MB % 11.88/2.61 % (2389177)------------------------------ % 11.88/2.61 % (2389177)------------------------------ % 11.88/2.61 % (2389178)------------------------------ % 11.88/2.61 % (2389178)------------------------------ % 11.88/2.61 % (2389201)------------------------------ % 11.88/2.61 % (2389201)------------------------------ % 11.88/2.61 % (2389211)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=498352780:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 11.88/2.61 % (2389209)lrs+10_1_sil=8000:sp=occurrence:random_seed=2461577703:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi) % 11.88/2.61 % (2389210)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1299940359:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 11.88/2.61 % (2389210)Refutation not found, incomplete strategy % 11.88/2.61 % (2389210)------------------------------ % 11.88/2.61 % (2389210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.61 % (2389209)Refutation not found, incomplete strategy % 11.88/2.61 % (2389209)------------------------------ % 11.88/2.61 % (2389209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.61 % (2389210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.61 % (2389209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.61 % (2389210)CaDiCaL version: 2.1.3 % 11.88/2.61 % (2389209)CaDiCaL version: 2.1.3 % 11.88/2.61 % (2389210)Termination reason: Refutation not found, incomplete strategy % 11.88/2.61 % (2389210)Time elapsed: 0.0000 s % 11.88/2.61 % (2389209)Termination reason: Refutation not found, incomplete strategy % 11.88/2.61 % (2389209)Time elapsed: 0.0000 s % 11.88/2.61 % (2389209)Peak memory usage: 86 MB % 11.88/2.61 % (2389210)Peak memory usage: 86 MB % 11.88/2.61 % (2389204)------------------------------ % 11.88/2.61 % (2389204)------------------------------ % 11.88/2.61 % (2389205)------------------------------ % 11.88/2.61 % (2389205)------------------------------ % 11.88/2.61 % (2389215)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1633241362:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi) % 11.88/2.61 % (2389215)Refutation not found, incomplete strategy % 11.88/2.61 % (2389215)------------------------------ % 11.88/2.61 % (2389215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.88/2.61 % (2389215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.88/2.61 % (2389215)CaDiCaL version: 2.1.3 % 11.88/2.61 % (2389215)Termination reason: Refutation not found, incomplete strategy % 11.88/2.61 % (2389215)Time elapsed: 0.001 s % 11.88/2.61 % (2389215)Peak memory usage: 86 MB % 11.88/2.61 [W927 10:06:19.890095790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 11.88/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890113439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890134735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890141001 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890153552 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890158835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890172016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890178525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890190938 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890196873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890209301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 [W927 10:06:19.890215602 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 12.34/2.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.34/2.71 % (2389210)------------------------------ % 12.34/2.71 % (2389210)------------------------------ % 12.34/2.71 % (2389209)------------------------------ % 12.34/2.71 % (2389209)------------------------------ % 12.34/2.71 % (2389216)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3475414698:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi) % 12.34/2.71 % (2389216)Refutation not found, incomplete strategy % 12.34/2.71 % (2389216)------------------------------ % 12.34/2.71 % (2389216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.34/2.71 % (2389216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.34/2.71 % (2389216)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2389216)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2389216)Time elapsed: 0.0000 s % 16.29/3.17 % (2389216)Peak memory usage: 86 MB % 16.29/3.17 % (2389211)Refutation not found, incomplete strategy % 16.29/3.17 % (2389211)------------------------------ % 16.29/3.17 % (2389211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2389211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2389211)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2389211)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2389211)Time elapsed: 0.323 s % 16.29/3.17 % (2389211)Peak memory usage: 125 MB % 16.29/3.17 % (2389211)Instructions burned: 827 (million) % 16.29/3.17 % (2389220)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=4054695075:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 16.29/3.17 % (2389220)Refutation not found, incomplete strategy % 16.29/3.17 % (2389220)------------------------------ % 16.29/3.17 % (2389220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2389220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2389220)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2389220)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2389220)Time elapsed: 0.0000 s % 16.29/3.17 % (2389220)Peak memory usage: 87 MB % 16.29/3.17 % (2389219)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2220170711:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi) % 16.29/3.17 % (2389215)------------------------------ % 16.29/3.17 % (2389215)------------------------------ % 16.29/3.17 % (2389220)------------------------------ % 16.29/3.17 % (2389220)------------------------------ % 16.29/3.17 % (2389216)------------------------------ % 16.29/3.17 % (2389216)------------------------------ % 16.29/3.17 % (2389211)------------------------------ % 16.29/3.17 % (2389211)------------------------------ % 16.29/3.17 % (2389223)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2960314342:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi) % 16.29/3.17 % (2389224)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3034553683:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 16.29/3.17 % (2389224)Refutation not found, incomplete strategy % 16.29/3.17 % (2389224)------------------------------ % 16.29/3.17 % (2389224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2389224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2389224)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2389224)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2389224)Time elapsed: 0.0000 s % 16.29/3.17 % (2389224)Peak memory usage: 86 MB % 16.29/3.17 % (2389223)Instruction limit reached! % 16.29/3.17 % (2389223)------------------------------ % 16.29/3.17 % (2389223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2389223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2389223)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2389223)Termination reason: Instruction limit % 16.29/3.17 % (2389223)Termination phase: Saturation % 16.29/3.17 % (2389223)Time elapsed: 0.049 s % 16.29/3.17 % (2389223)Peak memory usage: 89 MB % 16.29/3.17 % (2389223)Instructions burned: 137 (million) % 16.29/3.17 % (2389225)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1479875870:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/431Mi) % 16.29/3.17 % (2389225)Refutation not found, incomplete strategy % 16.29/3.17 % (2389225)------------------------------ % 16.29/3.17 % (2389225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.29/3.17 % (2389225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.29/3.17 % (2389225)CaDiCaL version: 2.1.3 % 16.29/3.17 % (2389225)Termination reason: Refutation not found, incomplete strategy % 16.29/3.17 % (2389225)Time elapsed: 0.0000 s % 16.29/3.17 % (2389225)Peak memory usage: 86 MB % 16.29/3.17 % (2389227)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=3493621688:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi) % 18.88/3.67 % (2389229)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=2098690634:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2983 on theBenchmark for (2983ds/150Mi) % 18.88/3.67 % (2389229)Refutation not found, incomplete strategy % 18.88/3.67 % (2389229)------------------------------ % 18.88/3.67 % (2389229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.88/3.67 % (2389229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.88/3.67 % (2389229)CaDiCaL version: 2.1.3 % 18.88/3.67 % (2389229)Termination reason: Refutation not found, incomplete strategy % 18.88/3.67 % (2389229)Time elapsed: 0.002 s % 18.88/3.67 % (2389229)Peak memory usage: 88 MB % 18.88/3.67 % (2389229)Instructions burned: 1 (million) % 18.88/3.67 % (2389224)------------------------------ % 18.88/3.67 % (2389224)------------------------------ % 18.88/3.67 [W927 10:06:19.485552772 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485597049 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485634732 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485651775 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485676822 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485688925 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485715555 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485727592 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485752652 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485764452 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/3.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.88/3.67 [W927 10:06:19.485789702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.86/3.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.86/3.84 [W927 10:06:19.485801649 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 19.86/3.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.86/3.84 % (2389233)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2823797429:i=14155:bd=all_2981 on theBenchmark for (2981ds/14155Mi) % 19.86/3.84 % (2389225)------------------------------ % 19.86/3.84 % (2389225)------------------------------ % 19.86/3.84 % (2389219)Refutation not found, incomplete strategy % 19.86/3.84 % (2389219)------------------------------ % 19.86/3.84 % (2389219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.86/3.84 % (2389219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.86/3.84 % (2389219)CaDiCaL version: 2.1.3 % 19.86/3.84 % (2389219)Termination reason: Refutation not found, incomplete strategy % 19.86/3.84 % (2389219)Time elapsed: 0.560 s % 19.86/3.84 % (2389219)Peak memory usage: 125 MB % 19.86/3.84 % (2389219)Instructions burned: 821 (million) % 19.86/3.84 % (2389200)Instruction limit reached! % 19.86/3.84 % (2389200)------------------------------ % 19.86/3.84 % (2389200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.86/3.84 % (2389200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.86/3.84 % (2389200)CaDiCaL version: 2.1.3 % 19.86/3.84 % (2389200)Termination reason: Instruction limit % 19.86/3.84 % (2389200)Termination phase: Saturation % 19.86/3.84 % (2389200)Time elapsed: 1.294 s % 19.86/3.84 % (2389200)Peak memory usage: 135 MB % 19.86/3.84 % (2389200)Instructions burned: 2350 (million) % 19.86/3.84 % (2389229)------------------------------ % 19.86/3.84 % (2389229)------------------------------ % 19.86/3.84 % (2389235)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1239470819:i=667:av=off:fsr=off_2980 on theBenchmark for (2980ds/667Mi) % 19.86/3.84 % (2389235)Refutation not found, incomplete strategy % 19.86/3.84 % (2389235)------------------------------ % 19.86/3.84 % (2389235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.86/3.84 % (2389235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.86/3.84 % (2389235)CaDiCaL version: 2.1.3 % 19.86/3.84 % (2389235)Termination reason: Refutation not found, incomplete strategy % 19.86/3.84 % (2389235)Time elapsed: 0.001 s % 19.86/3.84 % (2389235)Peak memory usage: 87 MB % 19.86/3.84 % (2389236)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=1699712168:s2a=on:i=185:s2at=1.8:fdi=4_2979 on theBenchmark for (2979ds/185Mi) % 19.86/3.84 % (2389237)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3176185541:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2979 on theBenchmark for (2979ds/193Mi) % 19.86/3.84 % (2389237)Refutation not found, incomplete strategy % 19.86/3.84 % (2389237)------------------------------ % 19.86/3.84 % (2389237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.86/3.84 % (2389237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.86/3.84 % (2389237)CaDiCaL version: 2.1.3 % 19.86/3.84 % (2389237)Termination reason: Refutation not found, incomplete strategy % 19.86/3.84 % (2389237)Time elapsed: 0.0000 s % 19.86/3.84 % (2389237)Peak memory usage: 86 MB % 19.86/3.84 % (2389236)Instruction limit reached! % 19.86/3.84 % (2389236)------------------------------ % 19.86/3.84 % (2389236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.86/3.84 % (2389236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.86/3.84 % (2389236)CaDiCaL version: 2.1.3 % 19.86/3.84 % (2389236)Termination reason: Instruction limit % 19.86/3.84 % (2389236)Termination phase: Saturation % 19.86/3.84 % (2389236)Time elapsed: 0.116 s % 19.86/3.84 % (2389236)Peak memory usage: 90 MB % 19.86/3.84 % (2389236)Instructions burned: 187 (million) % 19.86/3.84 % (2389219)------------------------------ % 19.86/3.84 % (2389219)------------------------------ % 19.86/3.84 % (2389235)------------------------------ % 23.55/4.16 % (2389235)------------------------------ % 23.55/4.16 % (2389237)------------------------------ % 23.55/4.16 % (2389237)------------------------------ % 23.55/4.16 % (2389241)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2947940421:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2977 on theBenchmark for (2977ds/4850Mi) % 23.55/4.16 % (2389242)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1068264318:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi) % 23.55/4.16 % (2389241)Refutation not found, incomplete strategy % 23.55/4.16 % (2389241)------------------------------ % 23.55/4.16 % (2389241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.55/4.16 % (2389241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.55/4.16 % (2389241)CaDiCaL version: 2.1.3 % 23.55/4.16 % (2389241)Termination reason: Refutation not found, incomplete strategy % 23.55/4.16 % (2389241)Time elapsed: 0.0000 s % 23.55/4.16 % (2389241)Peak memory usage: 85 MB % 23.55/4.16 % (2389243)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3535748224:i=319:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/319Mi) % 23.55/4.16 % (2389244)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2357195057:i=2064:ep=RST_2975 on theBenchmark for (2975ds/2064Mi) % 23.55/4.16 % (2389244)Refutation not found, incomplete strategy % 23.55/4.16 % (2389244)------------------------------ % 23.55/4.16 % (2389244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.55/4.16 % (2389244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.55/4.16 % (2389244)CaDiCaL version: 2.1.3 % 23.55/4.16 % (2389244)Termination reason: Refutation not found, incomplete strategy % 23.55/4.16 % (2389244)Time elapsed: 0.001 s % 23.55/4.16 % (2389244)Peak memory usage: 87 MB % 23.55/4.16 % (2389243)Instruction limit reached! % 23.55/4.16 % (2389243)------------------------------ % 23.55/4.16 % (2389243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.55/4.16 % (2389243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.55/4.16 % (2389243)CaDiCaL version: 2.1.3 % 23.55/4.16 % (2389243)Termination reason: Instruction limit % 23.55/4.16 % (2389243)Termination phase: Saturation % 23.55/4.16 % (2389243)Time elapsed: 0.165 s % 23.55/4.16 % (2389243)Peak memory usage: 92 MB % 23.55/4.16 % (2389243)Instructions burned: 321 (million) % 23.55/4.16 % (2389241)------------------------------ % 23.55/4.16 % (2389241)------------------------------ % 23.55/4.16 % (2389249)dis-1011_128_sil=32000:random_seed=608156213:i=3706:ep=RST:av=off_2973 on theBenchmark for (2973ds/3706Mi) % 23.55/4.16 % (2389249)Refutation not found, incomplete strategy % 23.55/4.16 % (2389249)------------------------------ % 23.55/4.16 % (2389249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.55/4.16 % (2389249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.55/4.16 % (2389249)CaDiCaL version: 2.1.3 % 23.55/4.16 % (2389249)Termination reason: Refutation not found, incomplete strategy % 23.55/4.16 % (2389249)Time elapsed: 0.001 s % 23.55/4.16 % (2389249)Peak memory usage: 88 MB % 23.55/4.16 % (2389244)------------------------------ % 23.55/4.16 % (2389244)------------------------------ % 23.55/4.16 % (2389250)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2157959857:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2973 on theBenchmark for (2973ds/757Mi) % 23.55/4.16 % (2389250)Refutation not found, incomplete strategy % 23.55/4.16 % (2389250)------------------------------ % 23.55/4.16 % (2389250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 23.55/4.16 % (2389250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 23.55/4.16 % (2389250)CaDiCaL version: 2.1.3 % 23.55/4.16 % (2389250)Termination reason: Refutation not found, incomplete strategy % 23.55/4.16 % (2389250)Time elapsed: 0.0000 s % 23.55/4.16 % (2389250)Peak memory usage: 86 MB % 23.55/4.16 [W927 10:06:20.442037481 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/4.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 23.55/4.16 [W927 10:06:20.442070511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442109818 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442121412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442146388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442156525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442180815 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442192675 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442216265 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442226235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442249932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 [W927 10:06:20.442259858 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.37/4.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.37/4.63 % (2389252)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2965883955:i=13913:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/13913Mi) % 26.37/4.63 % (2389249)------------------------------ % 26.37/4.63 % (2389249)------------------------------ % 26.37/4.63 % (2389242)Refutation not found, incomplete strategy % 26.37/4.63 % (2389242)------------------------------ % 26.37/4.63 % (2389242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.37/4.63 % (2389242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.37/4.63 % (2389242)CaDiCaL version: 2.1.3 % 26.37/4.63 % (2389242)Termination reason: Refutation not found, incomplete strategy % 26.37/4.63 % (2389242)Time elapsed: 0.550 s % 26.37/4.63 % (2389242)Peak memory usage: 125 MB % 26.37/4.63 % (2389242)Instructions burned: 820 (million) % 26.68/4.79 % (2389250)------------------------------ % 26.68/4.79 % (2389250)------------------------------ % 26.68/4.79 % (2389255)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1833406392:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi) % 26.68/4.79 % (2389256)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2779845192:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2969 on theBenchmark for (2969ds/2479Mi) % 26.68/4.79 % (2389256)Refutation not found, incomplete strategy % 26.68/4.79 % (2389256)------------------------------ % 26.68/4.79 % (2389256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.68/4.79 % (2389256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.68/4.79 % (2389256)CaDiCaL version: 2.1.3 % 26.68/4.79 % (2389256)Termination reason: Refutation not found, incomplete strategy % 26.68/4.79 % (2389256)Time elapsed: 0.001 s % 26.68/4.79 % (2389256)Peak memory usage: 86 MB % 26.68/4.79 % (2389242)------------------------------ % 26.68/4.79 % (2389242)------------------------------ % 26.68/4.79 [W927 10:06:21.932464999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932499049 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932537439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932549752 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932574792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932585899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932610332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932621486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932645666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 26.68/4.79 [W927 10:06:21.932656626 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 26.68/4.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.62/6.14 [W927 10:06:21.932680386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.62/6.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.62/6.14 [W927 10:06:21.932690396 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 37.62/6.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 37.62/6.14 % (2389259)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3838261745:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2967 on theBenchmark for (2967ds/440Mi) % 37.62/6.14 % (2389256)------------------------------ % 37.62/6.14 % (2389256)------------------------------ % 37.62/6.14 % (2389252)Refutation not found, incomplete strategy % 37.62/6.14 % (2389252)------------------------------ % 37.62/6.14 % (2389252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.62/6.14 % (2389252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.62/6.14 % (2389252)CaDiCaL version: 2.1.3 % 37.62/6.14 % (2389252)Termination reason: Refutation not found, incomplete strategy % 37.62/6.14 % (2389252)Time elapsed: 0.554 s % 37.62/6.14 % (2389252)Peak memory usage: 125 MB % 37.62/6.14 % (2389252)Instructions burned: 825 (million) % 37.62/6.14 % (2389261)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3681208150:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2965 on theBenchmark for (2965ds/11145Mi) % 37.62/6.14 % (2389259)Instruction limit reached! % 37.62/6.14 % (2389259)------------------------------ % 37.62/6.14 % (2389259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.62/6.14 % (2389259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.62/6.14 % (2389259)CaDiCaL version: 2.1.3 % 37.62/6.14 % (2389259)Termination reason: Instruction limit % 37.62/6.14 % (2389259)Termination phase: Saturation % 37.62/6.14 % (2389259)Time elapsed: 0.225 s % 37.62/6.14 % (2389259)Peak memory usage: 92 MB % 37.62/6.14 % (2389259)Instructions burned: 442 (million) % 37.62/6.14 % (2389255)Refutation not found, incomplete strategy % 37.62/6.14 % (2389255)------------------------------ % 37.62/6.14 % (2389255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.62/6.14 % (2389255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.62/6.14 % (2389255)CaDiCaL version: 2.1.3 % 37.62/6.14 % (2389255)Termination reason: Refutation not found, incomplete strategy % 37.62/6.14 % (2389255)Time elapsed: 0.548 s % 37.62/6.14 % (2389255)Peak memory usage: 126 MB % 37.62/6.14 % (2389255)Instructions burned: 823 (million) % 37.62/6.14 % (2389227)Instruction limit reached! % 37.62/6.14 % (2389227)------------------------------ % 37.62/6.14 % (2389227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.62/6.14 % (2389227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.62/6.14 % (2389227)CaDiCaL version: 2.1.3 % 37.62/6.14 % (2389227)Termination reason: Instruction limit % 37.62/6.14 % (2389227)Termination phase: Saturation % 37.62/6.14 % (2389227)Time elapsed: 1.922 s % 37.62/6.14 % (2389227)Peak memory usage: 159 MB % 37.62/6.14 % (2389227)Instructions burned: 6063 (million) % 37.62/6.14 % (2389252)------------------------------ % 37.62/6.14 % (2389252)------------------------------ % 37.62/6.14 % (2389263)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=9664394:cts=off:i=3034:av=off:er=known:fsd=on_2963 on theBenchmark for (2963ds/3034Mi) % 37.62/6.14 % (2389264)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2918343807:st=2:s2a=on:i=524:s2at=2:ss=axioms_2963 on theBenchmark for (2963ds/524Mi) % 37.62/6.14 % (2389264)Refutation not found, incomplete strategy % 37.62/6.14 % (2389264)------------------------------ % 37.62/6.14 % (2389264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 37.62/6.14 % (2389264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 37.62/6.14 % (2389264)CaDiCaL version: 2.1.3 % 37.62/6.14 % (2389264)Termination reason: Refutation not found, incomplete strategy % 38.01/6.28 % (2389264)Time elapsed: 0.0000 s % 38.01/6.28 % (2389264)Peak memory usage: 86 MB % 38.01/6.28 % (2389265)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=804764581:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2962 on theBenchmark for (2962ds/1016Mi) % 38.01/6.28 % (2389265)Refutation not found, incomplete strategy % 38.01/6.28 % (2389265)------------------------------ % 38.01/6.28 % (2389265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 38.01/6.28 % (2389265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 38.01/6.28 % (2389265)CaDiCaL version: 2.1.3 % 38.01/6.28 % (2389265)Termination reason: Refutation not found, incomplete strategy % 38.01/6.28 % (2389265)Time elapsed: 0.0000 s % 38.01/6.28 % (2389265)Peak memory usage: 86 MB % 38.01/6.28 % (2389255)------------------------------ % 38.01/6.28 % (2389255)------------------------------ % 38.01/6.28 % (2389264)------------------------------ % 38.01/6.28 % (2389264)------------------------------ % 38.01/6.28 [W927 10:06:22.565601415 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565647836 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565685792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565704066 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565730846 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565742756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565769466 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565781386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565806596 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565818802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 38.01/6.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 38.01/6.28 [W927 10:06:22.565844416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.22/6.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.22/6.42 [W927 10:06:22.565856502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.22/6.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.22/6.42 % (2389270)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3990143742:i=5781:kws=precedence:bd=all:rawr=on_2960 on theBenchmark for (2960ds/5781Mi) % 39.22/6.42 % (2389269)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=485043616:i=14123:bd=preordered:ins=4_2960 on theBenchmark for (2960ds/14123Mi) % 39.22/6.42 % (2389265)------------------------------ % 39.22/6.42 % (2389265)------------------------------ % 39.22/6.42 % (2389261)Refutation not found, incomplete strategy % 39.22/6.42 % (2389261)------------------------------ % 39.22/6.42 % (2389261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.22/6.42 % (2389261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.22/6.42 % (2389261)CaDiCaL version: 2.1.3 % 39.22/6.42 % (2389261)Termination reason: Refutation not found, incomplete strategy % 39.22/6.42 % (2389261)Time elapsed: 0.555 s % 39.22/6.42 % (2389261)Peak memory usage: 125 MB % 39.22/6.42 % (2389261)Instructions burned: 825 (million) % 39.22/6.42 % (2389273)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=725785822:i=2448:gtgl=5:bd=preordered:gtg=all_2958 on theBenchmark for (2958ds/2448Mi) % 39.22/6.42 % (2389261)------------------------------ % 39.22/6.42 % (2389261)------------------------------ % 39.22/6.42 % (2389275)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=972763812:i=3223:kws=precedence:fgj=on:av=off_2956 on theBenchmark for (2956ds/3223Mi) % 39.22/6.42 % (2389273)Refutation not found, incomplete strategy % 39.22/6.43 % (2389273)------------------------------ % 39.22/6.43 % (2389273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.22/6.43 % (2389273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.22/6.43 % (2389273)CaDiCaL version: 2.1.3 % 39.22/6.43 % (2389273)Termination reason: Refutation not found, incomplete strategy % 39.22/6.43 % (2389273)Time elapsed: 0.593 s % 39.22/6.43 % (2389273)Peak memory usage: 128 MB % 39.22/6.43 % (2389273)Instructions burned: 894 (million) % 39.22/6.43 % (2389270)Instruction limit reached! % 39.22/6.43 % (2389270)------------------------------ % 39.22/6.43 % (2389270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.22/6.43 % (2389270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.22/6.43 % (2389270)CaDiCaL version: 2.1.3 % 39.22/6.43 % (2389270)Termination reason: Instruction limit % 39.22/6.43 % (2389270)Termination phase: Saturation % 39.22/6.43 % (2389270)Time elapsed: 1.020 s % 39.22/6.43 % (2389270)Peak memory usage: 100 MB % 39.22/6.43 % (2389270)Instructions burned: 5782 (million) % 39.22/6.43 % (2389273)------------------------------ % 39.22/6.43 % (2389273)------------------------------ % 39.22/6.43 % (2389277)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=898632123:st=5.6:i=2033:sd=3:ss=axioms_2949 on theBenchmark for (2949ds/2033Mi) % 39.22/6.43 % (2389263)Instruction limit reached! % 39.22/6.43 % (2389263)------------------------------ % 39.22/6.43 % (2389263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.22/6.43 % (2389263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.22/6.43 % (2389263)CaDiCaL version: 2.1.3 % 39.22/6.43 % (2389263)Termination reason: Instruction limit % 39.22/6.43 % (2389263)Termination phase: Saturation % 39.22/6.43 % (2389263)Time elapsed: 1.417 s % 39.22/6.43 % (2389263)Peak memory usage: 127 MB % 39.22/6.43 % (2389263)Instructions burned: 3034 (million) % 39.22/6.43 % (2389278)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2950234695:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2949 on theBenchmark for (2949ds/2055Mi) % 39.22/6.43 % (2389280)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=1314521043:i=21611:sd=3:ss=axioms_2948 on theBenchmark for (2948ds/21611Mi) % 39.78/6.53 [W927 10:06:23.949297697 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949319031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949340010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949346889 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949360413 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949366839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949380131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949386607 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949400194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949406523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949419473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 [W927 10:06:23.949435249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 39.78/6.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.78/6.53 % (2389277)Refutation not found, incomplete strategy % 39.78/6.53 % (2389277)------------------------------ % 39.78/6.53 % (2389277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 44.07/7.08 % (2389277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 44.07/7.08 % (2389277)CaDiCaL version: 2.1.3 % 44.07/7.08 % (2389277)Termination reason: Refutation not found, incomplete strategy % 44.07/7.08 % (2389277)Time elapsed: 0.314 s % 44.07/7.08 % (2389277)Peak memory usage: 125 MB % 44.07/7.08 % (2389277)Instructions burned: 825 (million) % 44.07/7.08 [W927 10:06:23.198553898 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198598641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198636081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198654144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198679538 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198691921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198718168 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198730204 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198755471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198767238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198792318 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 44.07/7.08 [W927 10:06:23.198804151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 44.07/7.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 % (2389277)------------------------------ % 48.51/7.83 % (2389277)------------------------------ % 48.51/7.83 [W927 10:06:23.288950038 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289067925 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289113715 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289126925 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289152515 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289164118 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289189385 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289200845 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289225998 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289237262 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289262085 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 [W927 10:06:23.289273432 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/7.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 48.51/7.83 % (2389283)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=94316404:i=4835:sd=13:ss=axioms:sgt=23_2944 on theBenchmark for (2944ds/4835Mi) % 48.51/7.83 % (2389283)Refutation not found, incomplete strategy % 48.51/7.83 % (2389283)------------------------------ % 48.51/7.83 % (2389283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.24 % (2389283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.24 % (2389283)CaDiCaL version: 2.1.3 % 52.21/8.24 % (2389283)Termination reason: Refutation not found, incomplete strategy % 52.21/8.24 % (2389283)Time elapsed: 0.0000 s % 52.21/8.24 % (2389283)Peak memory usage: 86 MB % 52.21/8.24 % (2389278)Refutation not found, incomplete strategy % 52.21/8.24 % (2389278)------------------------------ % 52.21/8.24 % (2389278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.24 % (2389278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.24 % (2389278)CaDiCaL version: 2.1.3 % 52.21/8.24 % (2389278)Termination reason: Refutation not found, incomplete strategy % 52.21/8.24 % (2389278)Time elapsed: 0.546 s % 52.21/8.24 % (2389278)Peak memory usage: 125 MB % 52.21/8.24 % (2389278)Instructions burned: 821 (million) % 52.21/8.24 % (2389283)------------------------------ % 52.21/8.24 % (2389283)------------------------------ % 52.21/8.24 % (2389280)Refutation not found, incomplete strategy % 52.21/8.24 % (2389280)------------------------------ % 52.21/8.24 % (2389280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.24 % (2389280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.24 % (2389280)CaDiCaL version: 2.1.3 % 52.21/8.24 % (2389280)Termination reason: Refutation not found, incomplete strategy % 52.21/8.24 % (2389280)Time elapsed: 0.544 s % 52.21/8.24 % (2389280)Peak memory usage: 125 MB % 52.21/8.24 % (2389280)Instructions burned: 821 (million) % 52.21/8.24 % (2389285)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=1872545927:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2941 on theBenchmark for (2941ds/797Mi) % 52.21/8.24 % (2389285)Refutation not found, incomplete strategy % 52.21/8.24 % (2389285)------------------------------ % 52.21/8.24 % (2389285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.24 % (2389285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.24 % (2389285)CaDiCaL version: 2.1.3 % 52.21/8.24 % (2389285)Termination reason: Refutation not found, incomplete strategy % 52.21/8.24 % (2389285)Time elapsed: 0.0000 s % 52.21/8.24 % (2389285)Peak memory usage: 86 MB % 52.21/8.24 % (2389278)------------------------------ % 52.21/8.24 % (2389278)------------------------------ % 52.21/8.24 % (2389285)------------------------------ % 52.21/8.24 % (2389285)------------------------------ % 52.21/8.24 % (2389280)------------------------------ % 52.21/8.24 % (2389280)------------------------------ % 52.21/8.24 % (2389275)Instruction limit reached! % 52.21/8.24 % (2389275)------------------------------ % 52.21/8.24 % (2389275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.24 % (2389275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.24 % (2389275)CaDiCaL version: 2.1.3 % 52.21/8.24 % (2389275)Termination reason: Instruction limit % 52.21/8.24 % (2389275)Termination phase: Saturation % 52.21/8.24 % (2389275)Time elapsed: 1.620 s % 52.21/8.24 % (2389275)Peak memory usage: 138 MB % 52.21/8.24 % (2389275)Instructions burned: 3224 (million) % 52.21/8.24 % (2389287)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1786722887:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2940 on theBenchmark for (2940ds/2326Mi) % 52.21/8.24 % (2389287)Refutation not found, incomplete strategy % 52.21/8.24 % (2389287)------------------------------ % 52.21/8.24 % (2389287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.21/8.24 % (2389287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.21/8.24 % (2389287)CaDiCaL version: 2.1.3 % 52.21/8.24 % (2389287)Termination reason: Refutation not found, incomplete strategy % 52.21/8.24 % (2389287)Time elapsed: 0.001 s % 52.21/8.24 % (2389287)Peak memory usage: 88 MB % 52.21/8.24 % (2389288)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=453891939:i=6038:nm=6_2939 on theBenchmark for (2939ds/6038Mi) % 52.21/8.24 % (2389289)lrs+10_1_sil=32000:sp=occurrence:random_seed=3104055335:st=2:i=33334:sd=3:ss=included:sgt=32_2939 on theBenchmark for (2939ds/33334Mi) % 52.21/8.24 % (2389289)Refutation not found, incomplete strategy % 52.21/8.24 % (2389289)------------------------------ % 54.05/8.58 % (2389289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.05/8.58 % (2389289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.05/8.58 % (2389289)CaDiCaL version: 2.1.3 % 54.05/8.58 % (2389289)Termination reason: Refutation not found, incomplete strategy % 54.05/8.58 % (2389289)Time elapsed: 0.0000 s % 54.05/8.58 % (2389289)Peak memory usage: 86 MB % 54.05/8.58 % (2389290)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1827471176:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2938 on theBenchmark for (2938ds/1008Mi) % 54.05/8.58 % (2389290)Refutation not found, incomplete strategy % 54.05/8.58 % (2389290)------------------------------ % 54.05/8.58 % (2389290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.05/8.58 % (2389290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.05/8.58 % (2389290)CaDiCaL version: 2.1.3 % 54.05/8.58 % (2389290)Termination reason: Refutation not found, incomplete strategy % 54.05/8.58 % (2389290)Time elapsed: 0.0000 s % 54.05/8.58 % (2389290)Peak memory usage: 86 MB % 54.05/8.58 % (2389287)------------------------------ % 54.05/8.58 % (2389287)------------------------------ % 54.05/8.58 % (2389288)Refutation not found, incomplete strategy % 54.05/8.58 % (2389288)------------------------------ % 54.05/8.58 % (2389288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.05/8.58 % (2389288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.05/8.58 % (2389288)CaDiCaL version: 2.1.3 % 54.05/8.58 % (2389288)Termination reason: Refutation not found, incomplete strategy % 54.05/8.58 % (2389288)Time elapsed: 0.311 s % 54.05/8.58 % (2389288)Peak memory usage: 126 MB % 54.05/8.58 % (2389288)Instructions burned: 823 (million) % 54.05/8.58 % (2389289)------------------------------ % 54.05/8.58 % (2389289)------------------------------ % 54.05/8.58 % (2389295)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=3491461977:i=8327:s2at=5:bd=preordered_2936 on theBenchmark for (2936ds/8327Mi) % 54.05/8.58 % (2389290)------------------------------ % 54.05/8.58 % (2389290)------------------------------ % 54.05/8.58 % (2389296)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=3196195788:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2935 on theBenchmark for (2935ds/1083Mi) % 54.05/8.58 % (2389296)Refutation not found, incomplete strategy % 54.05/8.58 % (2389296)------------------------------ % 54.05/8.58 % (2389296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.05/8.58 % (2389296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.05/8.58 % (2389296)CaDiCaL version: 2.1.3 % 54.05/8.58 % (2389296)Termination reason: Refutation not found, incomplete strategy % 54.05/8.58 % (2389296)Time elapsed: 0.001 s % 54.05/8.58 % (2389296)Peak memory usage: 88 MB % 54.05/8.58 % (2389288)------------------------------ % 54.05/8.58 % (2389288)------------------------------ % 54.05/8.58 % (2389298)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2339272705:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2934 on theBenchmark for (2934ds/1084Mi) % 54.05/8.58 % (2389298)Refutation not found, incomplete strategy % 54.05/8.58 % (2389298)------------------------------ % 54.05/8.58 % (2389298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.05/8.58 % (2389298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.05/8.58 % (2389298)CaDiCaL version: 2.1.3 % 54.05/8.58 % (2389298)Termination reason: Refutation not found, incomplete strategy % 54.05/8.58 % (2389298)Time elapsed: 0.0000 s % 54.05/8.58 % (2389298)Peak memory usage: 86 MB % 54.05/8.58 % (2389300)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2385745118:i=6995:s2at=5:gtg=all_2933 on theBenchmark for (2933ds/6995Mi) % 54.05/8.58 % (2389296)------------------------------ % 54.05/8.58 % (2389296)------------------------------ % 54.05/8.58 % (2389298)------------------------------ % 54.05/8.58 % (2389298)------------------------------ % 54.05/8.58 % (2389303)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3494516809:st=2:i=6225:sd=15:ss=axioms_2931 on theBenchmark for (2931ds/6225Mi) % 54.05/8.58 % (2389303)Refutation not found, incomplete strategy % 60.98/9.51 % (2389303)------------------------------ % 60.98/9.51 % (2389303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 60.98/9.51 % (2389303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 60.98/9.51 % (2389303)CaDiCaL version: 2.1.3 % 60.98/9.51 % (2389303)Termination reason: Refutation not found, incomplete strategy % 60.98/9.51 % (2389303)Time elapsed: 0.001 s % 60.98/9.51 % (2389303)Peak memory usage: 86 MB % 60.98/9.51 % (2389304)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=470931832:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2931 on theBenchmark for (2931ds/3372Mi) % 60.98/9.51 % (2389303)------------------------------ % 60.98/9.51 % (2389303)------------------------------ % 60.98/9.51 % (2389307)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2398319268:st=2.3:i=26457:sd=10:ss=included:sgt=8_2927 on theBenchmark for (2927ds/26457Mi) % 60.98/9.51 [W927 10:06:25.012665894 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012709668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012748074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012760018 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012785498 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012796528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012822198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012833228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012857261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012868111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 60.98/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 60.98/9.51 [W927 10:06:25.012891791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.012902391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 % (2389304)Refutation not found, incomplete strategy % 62.27/9.85 % (2389304)------------------------------ % 62.27/9.85 % (2389304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.27/9.85 % (2389304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.27/9.85 % (2389304)CaDiCaL version: 2.1.3 % 62.27/9.85 % (2389304)Termination reason: Refutation not found, incomplete strategy % 62.27/9.85 % (2389304)Time elapsed: 0.544 s % 62.27/9.85 % (2389304)Peak memory usage: 125 MB % 62.27/9.85 % (2389304)Instructions burned: 824 (million) % 62.27/9.85 [W927 10:06:25.357902739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.357934799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.357971469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.357982646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.358017556 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.358031099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.358060612 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.358072649 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.358097246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.85 [W927 10:06:25.358109019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 [W927 10:06:25.358134173 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 [W927 10:06:25.358145186 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 % (2389304)------------------------------ % 62.27/9.89 % (2389304)------------------------------ % 62.27/9.89 % (2389307)Refutation not found, incomplete strategy % 62.27/9.89 % (2389307)------------------------------ % 62.27/9.89 % (2389307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.27/9.89 % (2389307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.27/9.89 % (2389307)CaDiCaL version: 2.1.3 % 62.27/9.89 % (2389307)Termination reason: Refutation not found, incomplete strategy % 62.27/9.89 % (2389307)Time elapsed: 0.548 s % 62.27/9.89 % (2389307)Peak memory usage: 125 MB % 62.27/9.89 % (2389307)Instructions burned: 826 (million) % 62.27/9.89 % (2389309)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=2158169031:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2921 on theBenchmark for (2921ds/13494Mi) % 62.27/9.89 % (2389307)------------------------------ % 62.27/9.89 % (2389307)------------------------------ % 62.27/9.89 % (2389311)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=3630906805:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2918 on theBenchmark for (2918ds/2503Mi) % 62.27/9.89 % (2389233)Instruction limit reached! % 62.27/9.89 % (2389233)------------------------------ % 62.27/9.89 % (2389233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.27/9.89 % (2389233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.27/9.89 % (2389233)CaDiCaL version: 2.1.3 % 62.27/9.89 % (2389233)Termination reason: Instruction limit % 62.27/9.89 % (2389233)Termination phase: Saturation % 62.27/9.89 % (2389233)Time elapsed: 6.600 s % 62.27/9.89 % (2389233)Peak memory usage: 220 MB % 62.27/9.89 % (2389233)Instructions burned: 14156 (million) % 62.27/9.89 % (2389313)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1564392833:i=2559:sd=1:ep=RSTC:ss=axioms_2914 on theBenchmark for (2914ds/2559Mi) % 62.27/9.89 [W927 10:06:26.285416007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 [W927 10:06:26.285455970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 [W927 10:06:26.285492770 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 [W927 10:06:26.285506074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 62.27/9.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.27/9.89 [W927 10:06:26.285531697 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285543470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285575294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285585324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285610717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285620627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285644680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:26.285654760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 % (2389295)Instruction limit reached! % 65.33/10.08 % (2389295)------------------------------ % 65.33/10.08 % (2389295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.33/10.08 % (2389295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.33/10.08 % (2389295)CaDiCaL version: 2.1.3 % 65.33/10.08 % (2389295)Termination reason: Instruction limit % 65.33/10.08 % (2389295)Termination phase: Saturation % 65.33/10.08 % (2389295)Time elapsed: 2.209 s % 65.33/10.08 % (2389295)Peak memory usage: 153 MB % 65.33/10.08 % (2389295)Instructions burned: 8332 (million) % 65.33/10.08 % (2389315)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4247986067:i=30753:av=off:ss=included_2912 on theBenchmark for (2912ds/30753Mi) % 65.33/10.08 % (2389311)Refutation not found, incomplete strategy % 65.33/10.08 % (2389311)------------------------------ % 65.33/10.08 % (2389311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 65.33/10.08 % (2389311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 65.33/10.08 % (2389311)CaDiCaL version: 2.1.3 % 65.33/10.08 % (2389311)Termination reason: Refutation not found, incomplete strategy % 65.33/10.08 % (2389311)Time elapsed: 0.550 s % 65.33/10.08 % (2389311)Peak memory usage: 125 MB % 65.33/10.08 % (2389311)Instructions burned: 824 (million) % 65.33/10.08 [W927 10:06:27.624935866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 65.33/10.08 [W927 10:06:27.624975395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 65.33/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.624996158 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625009826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625029619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625035322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625048139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625053523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625066058 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625071476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625084043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.625089333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.662992601 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663048341 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663087042 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663099405 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663124355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663134388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663159182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663169238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663192782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663259525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663308865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 [W927 10:06:27.663339575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.40/10.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.40/10.85 % (2389311)------------------------------ % 66.40/10.85 % (2389311)------------------------------ % 66.40/10.85 % (2389315)Refutation not found, incomplete strategy % 66.40/10.85 % (2389315)------------------------------ % 66.40/10.85 % (2389315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.40/10.85 % (2389315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.40/10.85 % (2389315)CaDiCaL version: 2.1.3 % 66.40/10.85 % (2389315)Termination reason: Refutation not found, incomplete strategy % 66.40/10.85 % (2389315)Time elapsed: 0.297 s % 66.40/10.85 % (2389315)Peak memory usage: 125 MB % 66.40/10.85 % (2389315)Instructions burned: 821 (million) % 66.40/10.85 % (2389313)Refutation not found, incomplete strategy % 66.40/10.85 % (2389313)------------------------------ % 66.40/10.85 % (2389313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.40/10.85 % (2389313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.40/10.85 % (2389313)CaDiCaL version: 2.1.3 % 66.40/10.85 % (2389313)Termination reason: Refutation not found, incomplete strategy % 66.40/10.85 % (2389313)Time elapsed: 0.552 s % 66.40/10.85 % (2389313)Peak memory usage: 125 MB % 66.40/10.85 % (2389313)Instructions burned: 825 (million) % 66.40/10.85 % (2389317)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3593121631:i=26473:ep=RSTC_2909 on theBenchmark for (2909ds/26473Mi) % 72.30/11.05 % (2389317)Refutation not found, incomplete strategy % 72.30/11.05 % (2389317)------------------------------ % 72.30/11.05 % (2389317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.30/11.05 % (2389317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.30/11.05 % (2389317)CaDiCaL version: 2.1.3 % 72.30/11.05 % (2389317)Termination reason: Refutation not found, incomplete strategy % 72.30/11.05 % (2389317)Time elapsed: 0.001 s % 72.30/11.05 % (2389317)Peak memory usage: 88 MB % 72.30/11.05 % (2389315)------------------------------ % 72.30/11.05 % (2389315)------------------------------ % 72.30/11.05 % (2389319)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=142594569:cts=off:i=2759:kws=inv_arity:fgj=on_2907 on theBenchmark for (2907ds/2759Mi) % 72.30/11.05 % (2389313)------------------------------ % 72.30/11.05 % (2389313)------------------------------ % 72.30/11.05 % (2389317)------------------------------ % 72.30/11.05 % (2389317)------------------------------ % 72.30/11.05 % (2389321)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=2319682611:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2905 on theBenchmark for (2905ds/5665Mi) % 72.30/11.05 % (2389322)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=2853681680:i=1532:ep=RS:ss=axioms_2905 on theBenchmark for (2905ds/1532Mi) % 72.30/11.05 % (2389319)Refutation not found, incomplete strategy % 72.30/11.05 % (2389319)------------------------------ % 72.30/11.05 % (2389319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.30/11.05 % (2389319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.30/11.05 % (2389319)CaDiCaL version: 2.1.3 % 72.30/11.05 % (2389319)Termination reason: Refutation not found, incomplete strategy % 72.30/11.05 % (2389319)Time elapsed: 0.362 s % 72.30/11.05 % (2389319)Peak memory usage: 127 MB % 72.30/11.05 % (2389319)Instructions burned: 825 (million) % 72.30/11.05 % (2389319)------------------------------ % 72.30/11.05 % (2389319)------------------------------ % 72.30/11.05 % (2389300)Instruction limit reached! % 72.30/11.05 % (2389300)------------------------------ % 72.30/11.05 % (2389300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 72.30/11.05 % (2389300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 72.30/11.05 % (2389300)CaDiCaL version: 2.1.3 % 72.30/11.05 % (2389300)Termination reason: Instruction limit % 72.30/11.05 % (2389300)Termination phase: Saturation % 72.30/11.05 % (2389300)Time elapsed: 3.219 s % 72.30/11.05 % (2389300)Peak memory usage: 171 MB % 72.30/11.05 % (2389300)Instructions burned: 6997 (million) % 72.30/11.05 % (2389325)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=785836769:i=1565:sd=2:ss=axioms:sgt=32_2900 on theBenchmark for (2900ds/1565Mi) % 72.30/11.05 [W927 10:06:28.622345229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 72.30/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.30/11.05 [W927 10:06:28.622376175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 72.30/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.30/11.05 [W927 10:06:28.622415072 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 72.30/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.30/11.05 [W927 10:06:28.622427985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 72.30/11.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 72.30/11.05 [W927 10:06:28.622454885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622449605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622467249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622474245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622492499 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622503855 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622511162 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622522665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622527982 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622538969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622547859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622558472 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622563759 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 73.63/11.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 73.63/11.39 [W927 10:06:28.622575132 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.622583622 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.622594102 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.622618476 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.622629446 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.622675259 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.622686402 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 % (2389326)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=84624164:i=1572:fgj=on:gsp=on_2900 on theBenchmark for (2900ds/1572Mi) % 74.98/11.59 % (2389322)Refutation not found, incomplete strategy % 74.98/11.59 % (2389322)------------------------------ % 74.98/11.59 % (2389322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.98/11.59 % (2389322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.98/11.59 % (2389322)CaDiCaL version: 2.1.3 % 74.98/11.59 % (2389322)Termination reason: Refutation not found, incomplete strategy % 74.98/11.59 % (2389322)Time elapsed: 0.546 s % 74.98/11.59 % (2389322)Peak memory usage: 125 MB % 74.98/11.59 % (2389322)Instructions burned: 821 (million) % 74.98/11.59 % (2389321)Refutation not found, incomplete strategy % 74.98/11.59 % (2389321)------------------------------ % 74.98/11.59 % (2389321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 74.98/11.59 % (2389321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 74.98/11.59 % (2389321)CaDiCaL version: 2.1.3 % 74.98/11.59 % (2389321)Termination reason: Refutation not found, incomplete strategy % 74.98/11.59 % (2389321)Time elapsed: 0.553 s % 74.98/11.59 % (2389321)Peak memory usage: 125 MB % 74.98/11.59 % (2389321)Instructions burned: 824 (million) % 74.98/11.59 [W927 10:06:28.822482139 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.822506709 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/11.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 74.98/11.59 [W927 10:06:28.822527963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822534516 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822548166 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822553744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822567431 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822572968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822585511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822591029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822603571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 [W927 10:06:28.822609031 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.78 % (2389325)Refutation not found, incomplete strategy % 75.77/11.78 % (2389325)------------------------------ % 75.77/11.78 % (2389325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 75.77/11.78 % (2389325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 75.77/11.78 % (2389325)CaDiCaL version: 2.1.3 % 75.77/11.78 % (2389325)Termination reason: Refutation not found, incomplete strategy % 75.77/11.78 % (2389325)Time elapsed: 0.305 s % 75.77/11.78 % (2389325)Peak memory usage: 125 MB % 75.77/11.78 % (2389325)Instructions burned: 824 (million) % 75.77/11.78 % (2389322)------------------------------ % 75.77/11.78 % (2389322)------------------------------ % 75.77/11.78 % (2389321)------------------------------ % 75.77/11.78 % (2389321)------------------------------ % 75.77/11.78 % (2389325)------------------------------ % 75.77/11.78 % (2389325)------------------------------ % 75.77/11.78 % (2389331)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=4163200522:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2895 on theBenchmark for (2895ds/1842Mi) % 75.77/11.79 % (2389329)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1807933062:i=6052:sd=4:ss=axioms:sgt=24_2895 on theBenchmark for (2895ds/6052Mi) % 75.77/11.79 % (2389330)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=1959663242:i=3500:sd=1:bd=preordered:sup=off:ss=included_2895 on theBenchmark for (2895ds/3500Mi) % 75.77/11.79 [W927 10:06:28.365152889 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365172939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365193298 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365199581 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365212946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365219486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365233689 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365240111 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365252843 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365266141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365279569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 75.77/11.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 75.77/11.79 [W927 10:06:28.365284982 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 % (2389269)Instruction limit reached! % 83.88/13.49 % (2389269)------------------------------ % 83.88/13.49 % (2389269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.88/13.49 % (2389269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.88/13.49 % (2389269)CaDiCaL version: 2.1.3 % 83.88/13.49 % (2389269)Termination reason: Instruction limit % 83.88/13.49 % (2389269)Termination phase: Saturation % 83.88/13.49 % (2389269)Time elapsed: 6.757 s % 83.88/13.49 % (2389269)Peak memory usage: 224 MB % 83.88/13.49 % (2389269)Instructions burned: 14124 (million) % 83.88/13.49 % (2389331)Refutation not found, incomplete strategy % 83.88/13.49 % (2389331)------------------------------ % 83.88/13.49 % (2389331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.88/13.49 % (2389331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.88/13.49 % (2389331)CaDiCaL version: 2.1.3 % 83.88/13.49 % (2389331)Termination reason: Refutation not found, incomplete strategy % 83.88/13.49 % (2389331)Time elapsed: 0.313 s % 83.88/13.49 % (2389331)Peak memory usage: 125 MB % 83.88/13.49 % (2389331)Instructions burned: 826 (million) % 83.88/13.49 [W927 10:06:29.549952830 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.549986873 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550047447 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550061777 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550093037 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550104387 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550130723 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550150340 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550175440 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/13.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.88/13.49 [W927 10:06:29.550186894 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.550211847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.550223007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560028778 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560061608 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560100038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560112895 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560138941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560150105 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560175428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560186541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560211588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560222591 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560247751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:29.560258808 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 % (2389335)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3137922476:i=66096:add=on_2891 on theBenchmark for (2891ds/66096Mi) % 86.46/13.84 % (2389326)Instruction limit reached! % 86.46/13.84 % (2389326)------------------------------ % 86.46/13.84 % (2389326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.46/13.84 % (2389326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.46/13.84 % (2389326)CaDiCaL version: 2.1.3 % 86.46/13.84 % (2389326)Termination reason: Instruction limit % 86.46/13.84 % (2389326)Termination phase: Saturation % 86.46/13.84 % (2389326)Time elapsed: 0.885 s % 86.46/13.84 % (2389326)Peak memory usage: 128 MB % 86.46/13.84 % (2389326)Instructions burned: 1574 (million) % 86.46/13.84 % (2389330)Refutation not found, incomplete strategy % 86.46/13.84 % (2389330)------------------------------ % 86.46/13.84 % (2389330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.46/13.84 % (2389330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.46/13.84 % (2389330)CaDiCaL version: 2.1.3 % 86.46/13.84 % (2389330)Termination reason: Refutation not found, incomplete strategy % 86.46/13.84 % (2389330)Time elapsed: 0.531 s % 86.46/13.84 % (2389330)Peak memory usage: 125 MB % 86.46/13.84 % (2389330)Instructions burned: 824 (million) % 86.46/13.84 % (2389337)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=340441346:i=1884:sd=1:nm=60:ss=axioms_2890 on theBenchmark for (2890ds/1884Mi) % 86.46/13.84 % (2389329)Refutation not found, incomplete strategy % 86.46/13.84 % (2389329)------------------------------ % 86.46/13.84 % (2389329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.46/13.84 % (2389329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.46/13.84 % (2389329)CaDiCaL version: 2.1.3 % 86.46/13.84 % (2389329)Termination reason: Refutation not found, incomplete strategy % 86.46/13.84 % (2389329)Time elapsed: 0.543 s % 86.46/13.84 % (2389329)Peak memory usage: 125 MB % 86.46/13.84 % (2389329)Instructions burned: 820 (million) % 86.46/13.84 % (2389330)------------------------------ % 86.46/13.84 % (2389330)------------------------------ % 86.46/13.84 % (2389331)------------------------------ % 86.46/13.84 % (2389331)------------------------------ % 86.46/13.84 % (2389329)------------------------------ % 86.46/13.84 % (2389329)------------------------------ % 86.46/13.84 % (2389339)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1435967189:cts=off:i=5469:bs=on:fsr=off_2882 on theBenchmark for (2882ds/5469Mi) % 86.46/13.84 % (2389342)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4227997713:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2881 on theBenchmark for (2881ds/2110Mi) % 86.46/13.84 % (2389341)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=1379143947:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2881 on theBenchmark for (2881ds/2037Mi) % 86.46/13.84 [W927 10:06:30.262430413 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:30.262463917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 86.46/13.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.46/13.84 [W927 10:06:30.262501633 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262525170 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262551354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262562307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262591840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262602730 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262627334 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262638410 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262662257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:30.262679050 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 % (2389337)Refutation not found, incomplete strategy % 88.11/14.04 % (2389337)------------------------------ % 88.11/14.04 % (2389337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.11/14.04 % (2389337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.11/14.04 % (2389337)CaDiCaL version: 2.1.3 % 88.11/14.04 % (2389337)Termination reason: Refutation not found, incomplete strategy % 88.11/14.04 % (2389337)Time elapsed: 1.716 s % 88.11/14.04 % (2389337)Peak memory usage: 125 MB % 88.11/14.04 % (2389337)Instructions burned: 821 (million) % 88.11/14.04 [W927 10:06:31.614359098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:31.614402984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.11/14.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.11/14.04 [W927 10:06:31.614441121 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614453674 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614479051 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614543221 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614579355 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614590581 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614615095 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614625911 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614650028 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.614660811 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615373016 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615398539 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615434433 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615445273 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615470153 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615480126 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615504406 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615517876 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615542089 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615552009 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615575229 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 [W927 10:06:31.615585013 register_special_ops.cpp:225] Warning: Creating a tensor from 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.88/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.88/14.48 % (2389337)------------------------------ % 89.88/14.48 % (2389337)------------------------------ % 89.88/14.48 % (2389342)Refutation not found, incomplete strategy % 89.88/14.48 % (2389342)------------------------------ % 89.88/14.48 % (2389342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.88/14.48 % (2389342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.88/14.48 % (2389342)CaDiCaL version: 2.1.3 % 89.88/14.48 % (2389342)Termination reason: Refutation not found, incomplete strategy % 89.88/14.48 % (2389342)Time elapsed: 0.548 s % 89.88/14.48 % (2389342)Peak memory usage: 124 MB % 89.88/14.48 % (2389342)Instructions burned: 825 (million) % 89.88/14.48 % (2389341)First to succeed. % 89.88/14.48 % (2389341)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2389171" % 89.88/14.48 % (2389309)Instruction limit reached! % 89.88/14.48 % (2389309)------------------------------ % 89.88/14.48 % (2389309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.88/14.48 % (2389309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.88/14.48 % (2389309)CaDiCaL version: 2.1.3 % 89.88/14.48 % (2389309)Termination reason: Instruction limit % 89.88/14.48 % (2389309)Termination phase: Saturation % 89.88/14.48 % (2389309)Time elapsed: 5.235 s % 89.88/14.48 % (2389309)Peak memory usage: 153 MB % 89.88/14.48 % (2389309)Instructions burned: 13497 (million) % 89.88/14.48 % (2389345)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=393656840:i=2430:add=off:aac=none:nm=16_2869 on theBenchmark for (2869ds/2430Mi) % 89.88/14.48 % (2389346)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=2689119087:cond=fast:i=4891_2868 on theBenchmark for (2868ds/4891Mi) % 89.88/14.48 % (2389342)------------------------------ % 89.88/14.48 % (2389342)------------------------------ % 89.88/14.48 % SZS status Satisfiable for theBenchmark % 89.88/14.48 % SZS output start Saturation. % 89.88/14.48 % SZS output end Saturation. % 89.88/14.48 % SZS output start Definitions and Model Updates. % 89.88/14.48 for all groundings, % 89.88/14.48 whenever multiply(X0,multiply(X0,X1,X2),X3) = multiply(X0,X1,multiply(X0,X2,X3)) | ~group_member(X1,X0) | ~group_member(X2,X0) | ~group_member(X3,X0) is false, set ~group_member(X1,X0) to true % 89.88/14.48 for all groundings, until fixed point, % 89.88/14.48 whenever group_member(multiply(X0,X1,X2),X0) | ~group_member(X1,X0) | ~group_member(X2,X0) is false, set ~group_member(X1,X0) to true % 89.88/14.48 % SZS output end Definitions and Model Updates. % 89.88/14.48 % (2389341)------------------------------ % 89.88/14.48 % (2389341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.88/14.48 % (2389341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.88/14.48 % (2389341)CaDiCaL version: 2.1.3 % 89.88/14.48 % (2389341)Termination reason: Satisfiable % 89.88/14.48 % (2389341)Time elapsed: 0.551 s % 89.88/14.48 % (2389341)Peak memory usage: 125 MB % 89.88/14.48 % (2389341)Instructions burned: 826 (million) % 89.88/14.48 % (2389341)------------------------------ % 89.88/14.48 % (2389341)------------------------------ % 89.88/14.48 % (2389171)Success in time 13.537 s % 89.88/14.48 % Vampire exiting %------------------------------------------------------------------------------