%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : LAT055-2 : 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 : n001.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 11:45:55 AM UTC 2026 % Result : Timeout 300.22s 43.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LAT055-2 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.14/0.40 % Computer : n001.cluster.edu % 0.14/0.40 % Model : x86_64 x86_64 % 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.40 % Memory : 8046.5625MB % 0.14/0.40 % OS : Linux 6.8.0-71-generic % 0.14/0.40 % CPULimit : 300 % 0.14/0.40 % WCLimit : 300 % 0.14/0.40 % DateTime : Sun Sep 27 14:04:15 UTC 2026 % 0.14/0.40 % CPUTime : % 0.14/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.14/0.46 Running first-order theorem proving % 0.14/0.46 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 % 8.50/2.30 % (3593059)Detected a unit-equality problem, will run specialized UEQ schedule. % 8.50/2.30 % (3593068)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2567664065:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi) % 8.50/2.30 % (3593069)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=785956879:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi) % 8.50/2.30 % (3593068)Instruction limit reached! % 8.50/2.30 % (3593068)------------------------------ % 8.50/2.30 % (3593068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.50/2.30 % (3593068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.50/2.30 % (3593068)CaDiCaL version: 2.1.3 % 8.50/2.30 % (3593068)Termination reason: Instruction limit % 8.50/2.30 % (3593068)Termination phase: Saturation % 8.50/2.30 % (3593068)Time elapsed: 0.056 s % 8.50/2.30 % (3593068)Peak memory usage: 88 MB % 8.50/2.30 % (3593068)Instructions burned: 182 (million) % 8.50/2.30 % (3593066)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1498345846:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi) % 8.50/2.30 % (3593065)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3053737849:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi) % 8.50/2.30 % (3593064)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1893603732:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi) % 8.50/2.30 % (3593067)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2780738279:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi) % 8.50/2.30 % (3593070)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3828415819:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi) % 8.50/2.30 % (3593070)Refutation not found, incomplete strategy % 8.50/2.30 % (3593070)------------------------------ % 8.50/2.30 % (3593070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.50/2.30 % (3593070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.50/2.30 % (3593070)CaDiCaL version: 2.1.3 % 8.50/2.30 % (3593070)Termination reason: Refutation not found, incomplete strategy % 8.50/2.30 % (3593070)Time elapsed: 0.001 s % 8.50/2.30 % (3593070)Peak memory usage: 86 MB % 8.50/2.30 % (3593067)Instruction limit reached! % 8.50/2.30 % (3593067)------------------------------ % 8.50/2.30 % (3593067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.50/2.30 % (3593067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.50/2.30 % (3593067)CaDiCaL version: 2.1.3 % 8.50/2.30 % (3593067)Termination reason: Instruction limit % 8.50/2.30 % (3593067)Termination phase: Saturation % 8.50/2.30 % (3593067)Time elapsed: 0.132 s % 8.50/2.30 % (3593067)Peak memory usage: 88 MB % 8.50/2.30 % (3593067)Instructions burned: 137 (million) % 8.50/2.30 % (3593069)Instruction limit reached! % 8.50/2.30 % (3593069)------------------------------ % 8.50/2.30 % (3593069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.50/2.30 % (3593069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.50/2.30 % (3593069)CaDiCaL version: 2.1.3 % 8.50/2.30 % (3593069)Termination reason: Instruction limit % 8.50/2.30 % (3593069)Termination phase: Saturation % 8.50/2.30 % (3593069)Time elapsed: 0.255 s % 8.50/2.30 % (3593069)Peak memory usage: 89 MB % 8.50/2.30 % (3593069)Instructions burned: 257 (million) % 8.50/2.30 % (3593073)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1827761799:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi) % 8.50/2.30 % (3593079)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3800711029:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi) % 8.50/2.30 % (3593070)------------------------------ % 8.50/2.30 % (3593070)------------------------------ % 8.50/2.30 % (3593080)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3473819266:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi) % 11.98/3.05 % (3593080)Refutation not found, incomplete strategy % 11.98/3.05 % (3593080)------------------------------ % 11.98/3.05 % (3593080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.98/3.05 % (3593080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.98/3.05 % (3593080)CaDiCaL version: 2.1.3 % 11.98/3.05 % (3593080)Termination reason: Refutation not found, incomplete strategy % 11.98/3.05 % (3593080)Time elapsed: 0.002 s % 11.98/3.05 % (3593080)Peak memory usage: 87 MB % 11.98/3.05 [W927 14:04:17.378545388 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.378678222 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.378771163 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.378819943 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.378891710 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.378937161 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.379025775 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.379075595 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.379154032 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.379201949 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.379276707 register_special_ops.cpp:225] Warning: Creating a tensor from 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.98/3.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.98/3.05 [W927 14:04:17.379322280 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 % (3593083)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2958088351:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi) % 17.46/3.46 % (3593065)Refutation not found, incomplete strategy % 17.46/3.46 % (3593065)------------------------------ % 17.46/3.46 % (3593065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.46/3.46 % (3593065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.46/3.46 % (3593065)CaDiCaL version: 2.1.3 % 17.46/3.46 % (3593065)Termination reason: Refutation not found, incomplete strategy % 17.46/3.46 % (3593065)Time elapsed: 0.876 s % 17.46/3.46 % (3593065)Peak memory usage: 125 MB % 17.46/3.46 % (3593065)Instructions burned: 820 (million) % 17.46/3.46 % (3593080)------------------------------ % 17.46/3.46 % (3593080)------------------------------ % 17.46/3.46 % (3593083)Instruction limit reached! % 17.46/3.46 % (3593083)------------------------------ % 17.46/3.46 % (3593083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.46/3.46 % (3593083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.46/3.46 % (3593083)CaDiCaL version: 2.1.3 % 17.46/3.46 % (3593083)Termination reason: Instruction limit % 17.46/3.46 % (3593083)Termination phase: Saturation % 17.46/3.46 % (3593083)Time elapsed: 0.280 s % 17.46/3.46 % (3593083)Peak memory usage: 90 MB % 17.46/3.46 % (3593083)Instructions burned: 317 (million) % 17.46/3.46 [W927 14:04:17.784471254 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.784606948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.784710932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.784767000 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.784848137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.784899257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.784978514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 17.46/3.46 [W927 14:04:17.785051695 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 17.46/3.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 [W927 14:04:17.785164812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 20.82/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 [W927 14:04:17.785212613 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 20.82/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 [W927 14:04:17.785286787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 20.82/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 [W927 14:04:17.785331654 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 20.82/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 % (3593087)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3901237053:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2988 on theBenchmark for (2988ds/2836Mi) % 20.82/3.98 % (3593086)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=315299289:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2988 on theBenchmark for (2988ds/12125Mi) % 20.82/3.98 % (3593065)------------------------------ % 20.82/3.98 % (3593065)------------------------------ % 20.82/3.98 % (3593079)Refutation not found, incomplete strategy % 20.82/3.98 % (3593079)------------------------------ % 20.82/3.98 % (3593079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.98 % (3593079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.98 % (3593079)CaDiCaL version: 2.1.3 % 20.82/3.98 % (3593079)Termination reason: Refutation not found, incomplete strategy % 20.82/3.98 % (3593079)Time elapsed: 0.902 s % 20.82/3.98 % (3593079)Peak memory usage: 125 MB % 20.82/3.98 % (3593079)Instructions burned: 825 (million) % 20.82/3.98 % (3593073)Instruction limit reached! % 20.82/3.98 % (3593073)------------------------------ % 20.82/3.98 % (3593073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.82/3.98 % (3593073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.82/3.98 % (3593073)CaDiCaL version: 2.1.3 % 20.82/3.98 % (3593073)Termination reason: Instruction limit % 20.82/3.98 % (3593073)Termination phase: Saturation % 20.82/3.98 % (3593073)Time elapsed: 1.150 s % 20.82/3.98 % (3593073)Peak memory usage: 142 MB % 20.82/3.98 % (3593073)Instructions burned: 2053 (million) % 20.82/3.98 % (3593090)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2534583445:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2984 on theBenchmark for (2984ds/14534Mi) % 20.82/3.98 % (3593091)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=775274462:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/11832Mi) % 20.82/3.98 % (3593079)------------------------------ % 20.82/3.98 % (3593079)------------------------------ % 20.82/3.98 [W927 14:04:18.539718249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 20.82/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 [W927 14:04:18.539786646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 20.82/3.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.82/3.98 [W927 14:04:18.539846143 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.539864363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.539907577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.539924873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.539967997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.539985021 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.540158465 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.540217062 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.540292899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.540344280 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 % (3593094)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=1912997297:i=2279:fgj=on:bd=all_2980 on theBenchmark for (2980ds/2279Mi) % 25.48/4.60 % (3593086)Refutation not found, incomplete strategy % 25.48/4.60 % (3593086)------------------------------ % 25.48/4.60 % (3593086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.48/4.60 % (3593086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.48/4.60 % (3593086)CaDiCaL version: 2.1.3 % 25.48/4.60 % (3593086)Termination reason: Refutation not found, incomplete strategy % 25.48/4.60 % (3593086)Time elapsed: 0.887 s % 25.48/4.60 % (3593086)Peak memory usage: 125 MB % 25.48/4.60 % (3593086)Instructions burned: 824 (million) % 25.48/4.60 [W927 14:04:18.953632899 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 25.48/4.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 25.48/4.60 [W927 14:04:18.953682599 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953740310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953762167 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953803790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953820137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953861024 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953877527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953916264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953932088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953970711 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 [W927 14:04:18.953986748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.05/8.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.05/8.78 % (3593086)------------------------------ % 55.05/8.78 % (3593086)------------------------------ % 55.05/8.78 % (3593090)Refutation not found, incomplete strategy % 55.05/8.78 % (3593090)------------------------------ % 55.05/8.78 % (3593090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.05/8.78 % (3593090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.05/8.78 % (3593090)CaDiCaL version: 2.1.3 % 55.05/8.78 % (3593090)Termination reason: Refutation not found, incomplete strategy % 55.05/8.78 % (3593090)Time elapsed: 0.887 s % 55.05/8.78 % (3593090)Peak memory usage: 125 MB % 55.05/8.78 % (3593090)Instructions burned: 825 (million) % 55.05/8.78 % (3593096)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=3957754025:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2972 on theBenchmark for (2972ds/6225Mi) % 61.79/9.75 % (3593090)------------------------------ % 61.79/9.75 % (3593090)------------------------------ % 61.79/9.75 % (3593100)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=3756443893:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2968 on theBenchmark for (2968ds/21755Mi) % 61.79/9.75 [W927 14:04:20.090707606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090758650 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090818054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090839687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090885674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090905054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090948131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.090966968 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.091022942 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.091054649 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.091099412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.79/9.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.79/9.75 [W927 14:04:20.091116589 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.28/21.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.28/21.88 % (3593096)Refutation not found, incomplete strategy % 148.28/21.88 % (3593096)------------------------------ % 148.28/21.88 % (3593096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.28/21.88 % (3593096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.28/21.88 % (3593096)CaDiCaL version: 2.1.3 % 148.28/21.88 % (3593096)Termination reason: Refutation not found, incomplete strategy % 148.28/21.88 % (3593096)Time elapsed: 0.878 s % 148.28/21.88 % (3593096)Peak memory usage: 126 MB % 148.28/21.88 % (3593096)Instructions burned: 825 (million) % 148.28/21.88 % (3593096)------------------------------ % 148.28/21.88 % (3593096)------------------------------ % 148.28/21.88 % (3593087)Instruction limit reached! % 148.28/21.88 % (3593087)------------------------------ % 148.28/21.88 % (3593087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.28/21.88 % (3593087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.28/21.89 % (3593087)CaDiCaL version: 2.1.3 % 148.28/21.89 % (3593087)Termination reason: Instruction limit % 148.28/21.89 % (3593087)Termination phase: Saturation % 148.28/21.89 % (3593087)Time elapsed: 2.912 s % 148.28/21.89 % (3593087)Peak memory usage: 130 MB % 148.28/21.89 % (3593087)Instructions burned: 2839 (million) % 148.28/21.89 % (3593105)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=1112404322:i=9356:fgj=on:bd=preordered:av=off_2956 on theBenchmark for (2956ds/9356Mi) % 148.28/21.89 % (3593104)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=792139942:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2957 on theBenchmark for (2957ds/16427Mi) % 148.28/21.89 % (3593094)Instruction limit reached! % 148.28/21.89 % (3593094)------------------------------ % 148.28/21.89 % (3593094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.28/21.89 % (3593094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.28/21.89 % (3593094)CaDiCaL version: 2.1.3 % 148.28/21.89 % (3593094)Termination reason: Instruction limit % 148.28/21.89 % (3593094)Termination phase: Saturation % 148.28/21.89 % (3593094)Time elapsed: 2.360 s % 148.28/21.89 % (3593094)Peak memory usage: 139 MB % 148.28/21.89 % (3593094)Instructions burned: 2279 (million) % 148.28/21.89 % (3593108)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=4153421531:i=2070:kws=inv_precedence:slsql=off:bd=all_2953 on theBenchmark for (2953ds/2070Mi) % 148.28/21.89 % (3593108)Instruction limit reached! % 148.28/21.89 % (3593108)------------------------------ % 148.28/21.89 % (3593108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 148.28/21.89 % (3593108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 148.28/21.89 % (3593108)CaDiCaL version: 2.1.3 % 148.28/21.89 % (3593108)Termination reason: Instruction limit % 148.28/21.89 % (3593108)Termination phase: Saturation % 148.28/21.89 % (3593108)Time elapsed: 2.014 s % 148.28/21.89 % (3593108)Peak memory usage: 119 MB % 148.28/21.89 % (3593108)Instructions burned: 2071 (million) % 148.28/21.89 % (3593115)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=2982945937:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2931 on theBenchmark for (2931ds/6461Mi) % 148.28/21.89 [W927 14:04:24.268931300 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.28/21.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.28/21.89 [W927 14:04:24.268988274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.28/21.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 148.28/21.89 [W927 14:04:24.269057314 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 148.28/21.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269077444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269121748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269137812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269177692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269194002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269235086 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269251902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269293309 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 [W927 14:04:24.269309946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 217.19/31.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 217.19/31.54 % (3593115)Refutation not found, incomplete strategy % 217.19/31.54 % (3593115)------------------------------ % 217.19/31.54 % (3593115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.19/31.54 % (3593115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.19/31.54 % (3593115)CaDiCaL version: 2.1.3 % 217.19/31.54 % (3593115)Termination reason: Refutation not found, incomplete strategy % 217.19/31.54 % (3593115)Time elapsed: 0.892 s % 217.19/31.54 % (3593115)Peak memory usage: 125 MB % 217.19/31.54 % (3593115)Instructions burned: 820 (million) % 217.19/31.54 % (3593115)------------------------------ % 217.19/31.54 % (3593115)------------------------------ % 217.19/31.54 % (3593091)Instruction limit reached! % 217.19/31.54 % (3593091)------------------------------ % 217.19/31.54 % (3593091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 217.19/31.54 % (3593091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 217.19/31.54 % (3593091)CaDiCaL version: 2.1.3 % 217.19/31.54 % (3593091)Termination reason: Instruction limit % 217.19/31.54 % (3593091)Termination phase: Saturation % 217.19/31.54 % (3593091)Time elapsed: 6.645 s % 217.19/31.54 % (3593091)Peak memory usage: 209 MB % 217.19/31.54 % (3593091)Instructions burned: 11833 (million) % 217.19/31.54 % (3593119)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=3057051547:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2914 on theBenchmark for (2914ds/2616Mi) % 250.52/36.21 % (3593119)Refutation not found, incomplete strategy % 250.52/36.21 % (3593119)------------------------------ % 250.52/36.21 % (3593119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.52/36.21 % (3593119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.52/36.21 % (3593119)CaDiCaL version: 2.1.3 % 250.52/36.21 % (3593119)Termination reason: Refutation not found, incomplete strategy % 250.52/36.21 % (3593119)Time elapsed: 0.0000 s % 250.52/36.21 % (3593119)Peak memory usage: 86 MB % 250.52/36.21 % (3593118)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=1490285910:i=2310:bd=all:ss=included_2915 on theBenchmark for (2915ds/2310Mi) % 250.52/36.21 % (3593118)Refutation not found, incomplete strategy % 250.52/36.21 % (3593118)------------------------------ % 250.52/36.21 % (3593118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.52/36.21 % (3593118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.52/36.21 % (3593118)CaDiCaL version: 2.1.3 % 250.52/36.21 % (3593118)Termination reason: Refutation not found, incomplete strategy % 250.52/36.21 % (3593118)Time elapsed: 0.001 s % 250.52/36.21 % (3593118)Peak memory usage: 86 MB % 250.52/36.21 % (3593119)------------------------------ % 250.52/36.21 % (3593119)------------------------------ % 250.52/36.21 % (3593118)------------------------------ % 250.52/36.21 % (3593118)------------------------------ % 250.52/36.21 % (3593122)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2966973260:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2910 on theBenchmark for (2910ds/30521Mi) % 250.52/36.21 % (3593123)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=3962467604:i=3258:fgj=on:bd=all:ins=1_2908 on theBenchmark for (2908ds/3258Mi) % 250.52/36.21 % (3593123)Instruction limit reached! % 250.52/36.21 % (3593123)------------------------------ % 250.52/36.21 % (3593123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.52/36.21 % (3593123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.52/36.21 % (3593123)CaDiCaL version: 2.1.3 % 250.52/36.21 % (3593123)Termination reason: Instruction limit % 250.52/36.21 % (3593123)Termination phase: Saturation % 250.52/36.21 % (3593123)Time elapsed: 3.295 s % 250.52/36.21 % (3593123)Peak memory usage: 154 MB % 250.52/36.21 % (3593123)Instructions burned: 3258 (million) % 250.52/36.21 % (3593132)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=3412423618:i=5037:kws=precedence_2872 on theBenchmark for (2872ds/5037Mi) % 250.52/36.21 % (3593105)Instruction limit reached! % 250.52/36.21 % (3593105)------------------------------ % 250.52/36.21 % (3593105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.52/36.21 % (3593105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.52/36.21 % (3593105)CaDiCaL version: 2.1.3 % 250.52/36.21 % (3593105)Termination reason: Instruction limit % 250.52/36.21 % (3593105)Termination phase: Saturation % 250.52/36.21 % (3593105)Time elapsed: 9.197 s % 250.52/36.21 % (3593105)Peak memory usage: 204 MB % 250.52/36.21 % (3593105)Instructions burned: 9356 (million) % 250.52/36.21 % (3593134)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=130581020:i=65240_2862 on theBenchmark for (2862ds/65240Mi) % 250.52/36.21 % (3593132)Instruction limit reached! % 250.52/36.21 % (3593132)------------------------------ % 250.52/36.21 % (3593132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 250.52/36.21 % (3593132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 250.52/36.21 % (3593132)CaDiCaL version: 2.1.3 % 250.52/36.21 % (3593132)Termination reason: Instruction limit % 250.52/36.21 % (3593132)Termination phase: Saturation % 250.52/36.21 % (3593132)Time elapsed: 5.012 s % 250.52/36.21 % (3593132)Peak memory usage: 163 MB % 250.52/36.21 % (3593132)Instructions burned: 5037 (million) % 250.52/36.21 % (3593137)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=976946084:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2819 on theBenchmark for (2819ds/16502Mi) % 250.52/36.21 % (3593104)Instruction limit reached! % 250.52/36.21 % (3593104)------------------------------ % 276.29/39.94 % (3593104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.94 % (3593104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.94 % (3593104)CaDiCaL version: 2.1.3 % 276.29/39.94 % (3593104)Termination reason: Instruction limit % 276.29/39.94 % (3593104)Termination phase: Saturation % 276.29/39.94 % (3593104)Time elapsed: 16.367 s % 276.29/39.94 % (3593104)Peak memory usage: 240 MB % 276.29/39.94 % (3593104)Instructions burned: 16427 (million) % 276.29/39.94 % (3593141)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=3081087182:i=7623:bd=preordered:er=filter_2790 on theBenchmark for (2790ds/7623Mi) % 276.29/39.94 % (3593122)Instruction limit reached! % 276.29/39.94 % (3593122)------------------------------ % 276.29/39.94 % (3593122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.94 % (3593122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.94 % (3593122)CaDiCaL version: 2.1.3 % 276.29/39.94 % (3593122)Termination reason: Instruction limit % 276.29/39.94 % (3593122)Termination phase: Saturation % 276.29/39.94 % (3593122)Time elapsed: 15.074 s % 276.29/39.94 % (3593122)Peak memory usage: 301 MB % 276.29/39.94 % (3593122)Instructions burned: 30523 (million) % 276.29/39.94 % (3593143)dis+1010_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:tgt=full:npcc=on:sp=const_min:spb=non_intro:lcm=predicate:acc=on:urr=ec_only:rp=on:gs=on:random_seed=2629890352:i=8183:kws=frequency:add=off:gsp=on_2756 on theBenchmark for (2756ds/8183Mi) % 276.29/39.94 % (3593100)Instruction limit reached! % 276.29/39.94 % (3593100)------------------------------ % 276.29/39.94 % (3593100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.94 % (3593100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.94 % (3593100)CaDiCaL version: 2.1.3 % 276.29/39.94 % (3593100)Termination reason: Instruction limit % 276.29/39.94 % (3593100)Termination phase: Saturation % 276.29/39.94 % (3593100)Time elapsed: 21.456 s % 276.29/39.94 % (3593100)Peak memory usage: 224 MB % 276.29/39.94 % (3593100)Instructions burned: 21755 (million) % 276.29/39.94 % (3593145)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:bsr=unit_only:random_seed=1663027725:i=8387_2751 on theBenchmark for (2751ds/8387Mi) % 276.29/39.94 % (3593143)Instruction limit reached! % 276.29/39.94 % (3593143)------------------------------ % 276.29/39.94 % (3593143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.94 % (3593143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.94 % (3593143)CaDiCaL version: 2.1.3 % 276.29/39.94 % (3593143)Termination reason: Instruction limit % 276.29/39.94 % (3593143)Termination phase: Saturation % 276.29/39.94 % (3593143)Time elapsed: 3.679 s % 276.29/39.94 % (3593143)Peak memory usage: 189 MB % 276.29/39.94 % (3593143)Instructions burned: 8185 (million) % 276.29/39.94 % (3593253)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3364341636:i=53964:kws=inv_arity_squared:fgj=on:bd=preordered_2717 on theBenchmark for (2717ds/53964Mi) % 276.29/39.94 % (3593141)Instruction limit reached! % 276.29/39.94 % (3593141)------------------------------ % 276.29/39.94 % (3593141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.94 % (3593141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.94 % (3593141)CaDiCaL version: 2.1.3 % 276.29/39.94 % (3593141)Termination reason: Instruction limit % 276.29/39.94 % (3593141)Termination phase: Saturation % 276.29/39.94 % (3593141)Time elapsed: 7.203 s % 276.29/39.94 % (3593141)Peak memory usage: 188 MB % 276.29/39.94 % (3593141)Instructions burned: 7623 (million) % 276.29/39.94 % (3593302)lrs-1011_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=reverse_frequency:spb=goal:lsd=20:urr=on:flr=on:random_seed=3888476054:i=10575:s2at=5:gtg=position_2715 on theBenchmark for (2715ds/10575Mi) % 276.29/39.94 % (3593145)Instruction limit reached! % 276.29/39.94 % (3593145)------------------------------ % 276.29/39.94 % (3593145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 276.29/39.94 % (3593145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.29/39.94 % (3593145)CaDiCaL version: 2.1.3 % 276.29/39.94 % (3593145)Termination reason: Instruction limit % 276.29/39.94 % (3593145)Termination phase: Saturation % 280.92/40.54 % (3593145)Time elapsed: 5.399 s % 280.92/40.54 % (3593145)Peak memory usage: 165 MB % 280.92/40.54 % (3593145)Instructions burned: 8389 (million) % 280.92/40.54 % (3593304)ott-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:lsd=50:urr=ec_only:random_seed=1647292039:i=12036:s2at=3:gtgl=2:kws=frequency:add=off:fgj=on:bd=preordered:ins=2:gtg=exists_sym_2694 on theBenchmark for (2694ds/12036Mi) % 280.92/40.54 % (3593137)Instruction limit reached! % 280.92/40.54 % (3593137)------------------------------ % 280.92/40.54 % (3593137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.92/40.54 % (3593137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.92/40.54 % (3593137)CaDiCaL version: 2.1.3 % 280.92/40.54 % (3593137)Termination reason: Instruction limit % 280.92/40.54 % (3593137)Termination phase: Saturation % 280.92/40.54 % (3593137)Time elapsed: 13.564 s % 280.92/40.54 % (3593137)Peak memory usage: 270 MB % 280.92/40.54 % (3593137)Instructions burned: 16503 (million) % 280.92/40.54 % (3593306)lrs+1011_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=4064760860:i=16065:fgj=on:bd=preordered:av=off_2681 on theBenchmark for (2681ds/16065Mi) % 280.92/40.54 % (3593302)Instruction limit reached! % 280.92/40.54 % (3593302)------------------------------ % 280.92/40.54 % (3593302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 280.92/40.54 % (3593302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 280.92/40.54 % (3593302)CaDiCaL version: 2.1.3 % 280.92/40.54 % (3593302)Termination reason: Instruction limit % 280.92/40.54 % (3593302)Termination phase: Saturation % 280.92/40.54 % (3593302)Time elapsed: 6.015 s % 280.92/40.54 % (3593302)Peak memory usage: 182 MB % 280.92/40.54 % (3593302)Instructions burned: 10576 (million) % 280.92/40.54 % (3593308)dis-1011_1_to=kbo:ncem=casc2026/models/loop4.pt:sil=64000:tgt=ground:npcc=on:sp=arity:spb=non_intro:random_seed=1288082505:st=8.34:cond=on:i=28442:gtgl=3:sd=8:gtg=all:ss=included_2653 on theBenchmark for (2653ds/28442Mi) % 280.92/40.54 [W927 14:04:51.699542436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699590026 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699628216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699639370 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699664217 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699675643 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699701103 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 280.92/40.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 280.92/40.54 [W927 14:04:51.699712810 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 284.84/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 284.84/41.09 [W927 14:04:51.699738144 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 284.84/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 284.84/41.09 [W927 14:04:51.699748280 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 284.84/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 284.84/41.09 [W927 14:04:51.699780067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 284.84/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 284.84/41.09 [W927 14:04:51.699790274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 284.84/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 284.84/41.09 % (3593308)Refutation not found, incomplete strategy % 284.84/41.09 % (3593308)------------------------------ % 284.84/41.09 % (3593308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.84/41.09 % (3593308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.84/41.09 % (3593308)CaDiCaL version: 2.1.3 % 284.84/41.09 % (3593308)Termination reason: Refutation not found, incomplete strategy % 284.84/41.09 % (3593308)Time elapsed: 0.548 s % 284.84/41.09 % (3593308)Peak memory usage: 125 MB % 284.84/41.09 % (3593308)Instructions burned: 825 (million) % 284.84/41.09 % (3593308)------------------------------ % 284.84/41.09 % (3593308)------------------------------ % 284.84/41.09 % (3593310)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=3085603467:i=122896_2643 on theBenchmark for (2643ds/122896Mi) % 284.84/41.09 % (3593304)Instruction limit reached! % 284.84/41.09 % (3593304)------------------------------ % 284.84/41.09 % (3593304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.84/41.09 % (3593304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.84/41.09 % (3593304)CaDiCaL version: 2.1.3 % 284.84/41.09 % (3593304)Termination reason: Instruction limit % 284.84/41.09 % (3593304)Termination phase: Saturation % 284.84/41.09 % (3593304)Time elapsed: 7.238 s % 284.84/41.09 % (3593304)Peak memory usage: 231 MB % 284.84/41.09 % (3593304)Instructions burned: 12036 (million) % 284.84/41.09 % (3593312)lrs+35_4096_sil=64000:sp=occurrence:updr=off:random_seed=798650946:i=40171:ss=included:sgt=8_2620 on theBenchmark for (2620ds/40171Mi) % 284.84/41.09 % (3593312)Refutation not found, incomplete strategy % 284.84/41.09 % (3593312)------------------------------ % 284.84/41.09 % (3593312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 284.84/41.09 % (3593312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 284.84/41.09 % (3593312)CaDiCaL version: 2.1.3 % 284.84/41.09 % (3593312)Termination reason: Refutation not found, incomplete strategy % 284.84/41.09 % (3593312)Time elapsed: 0.001 s % 284.84/41.09 % (3593312)Peak memory usage: 86 MB % 284.84/41.09 % (3593312)------------------------------ % 284.84/41.09 % (3593312)------------------------------ % 284.84/41.09 % (3593314)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:npcc=on:random_seed=3960110049:i=81507:sd=3:ss=included:sgt=32_2616 on theBenchmark for (2616ds/81507Mi) % 284.84/41.09 [W927 14:04:55.432042014 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 284.84/41.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 284.84/41.09 [W927 14:04:55.432076764 register_speciaTerminated %------------------------------------------------------------------------------