%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWB031+3 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:00:15 PM UTC 2026 % Result : Timeout 290.41s 41.85s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : SWB031+3 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.03/0.31 % Computer : n012.cluster.edu % 0.03/0.31 % Model : x86_64 x86_64 % 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.31 % Memory : 8046.5625MB % 0.03/0.31 % OS : Linux 6.8.0-71-generic % 0.03/0.31 % CPULimit : 300 % 0.03/0.31 % WCLimit : 300 % 0.03/0.31 % DateTime : Mon Sep 28 07:07:49 UTC 2026 % 0.03/0.31 % CPUTime : % 0.03/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.07/0.33 Running first-order theorem proving % 0.07/0.33 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 4.23/1.15 % (3205249)Detected formulas, will run a generic FOF schedule. % 4.23/1.15 % (3205256)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=1469149152:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 4.23/1.15 % (3205255)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=2485652573:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 4.23/1.15 % (3205258)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2086780620:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 4.23/1.15 % (3205260)dis-21_1_sil=8000:lcm=predicate:random_seed=2436485761: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) % 4.23/1.15 % (3205254)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=1155919385:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 4.23/1.15 % (3205257)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=84592884:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 4.23/1.15 % (3205258)Refutation not found, incomplete strategy % 4.23/1.15 % (3205258)------------------------------ % 4.23/1.15 % (3205258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.23/1.15 % (3205258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.23/1.15 % (3205258)CaDiCaL version: 2.1.3 % 4.23/1.15 % (3205257)Refutation not found, incomplete strategy % 4.23/1.15 % (3205257)------------------------------ % 4.23/1.15 % (3205257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.23/1.15 % (3205258)Termination reason: Refutation not found, incomplete strategy % 4.23/1.15 % (3205258)Time elapsed: 0.0000 s % 4.23/1.15 % (3205258)Peak memory usage: 86 MB % 4.23/1.15 % (3205257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.23/1.15 % (3205257)CaDiCaL version: 2.1.3 % 4.23/1.15 % (3205257)Termination reason: Refutation not found, incomplete strategy % 4.23/1.16 % (3205257)Time elapsed: 0.0000 s % 4.23/1.16 % (3205257)Peak memory usage: 86 MB % 4.23/1.16 % (3205259)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2618960467:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 4.23/1.16 % (3205260)Instruction limit reached! % 4.23/1.16 % (3205260)------------------------------ % 4.23/1.16 % (3205260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.23/1.16 % (3205260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.23/1.16 % (3205260)CaDiCaL version: 2.1.3 % 4.23/1.16 % (3205260)Termination reason: Instruction limit % 4.23/1.16 % (3205260)Termination phase: Saturation % 4.23/1.16 % (3205260)Time elapsed: 0.039 s % 4.23/1.16 % (3205260)Peak memory usage: 88 MB % 4.23/1.16 % (3205260)Instructions burned: 129 (million) % 4.23/1.16 % (3205259)Instruction limit reached! % 4.23/1.16 % (3205259)------------------------------ % 4.23/1.16 % (3205259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.23/1.16 % (3205259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.23/1.16 % (3205259)CaDiCaL version: 2.1.3 % 4.23/1.16 % (3205259)Termination reason: Instruction limit % 4.23/1.16 % (3205259)Termination phase: Saturation % 4.23/1.16 % (3205259)Time elapsed: 0.058 s % 4.23/1.16 % (3205259)Peak memory usage: 90 MB % 4.23/1.16 % (3205259)Instructions burned: 140 (million) % 4.23/1.16 % (3205268)lrs+10_1_sil=8000:sp=occurrence:random_seed=1942360389:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 4.23/1.16 % (3205268)Refutation not found, incomplete strategy % 4.23/1.16 % (3205268)------------------------------ % 4.23/1.16 % (3205268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.23/1.16 % (3205268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.23/1.16 % (3205268)CaDiCaL version: 2.1.3 % 4.23/1.16 % (3205268)Termination reason: Refutation not found, incomplete strategy % 4.23/1.16 % (3205268)Time elapsed: 0.0000 s % 4.23/1.16 % (3205268)Peak memory usage: 86 MB % 4.23/1.16 % (3205258)------------------------------ % 4.23/1.16 % (3205258)------------------------------ % 4.23/1.16 % (3205257)------------------------------ % 4.23/1.16 % (3205257)------------------------------ % 6.47/1.53 % (3205269)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2114277787:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi) % 6.47/1.53 % (3205269)Refutation not found, incomplete strategy % 6.47/1.53 % (3205269)------------------------------ % 6.47/1.53 % (3205269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.53 % (3205269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.53 % (3205269)CaDiCaL version: 2.1.3 % 6.47/1.53 % (3205269)Termination reason: Refutation not found, incomplete strategy % 6.47/1.53 % (3205269)Time elapsed: 0.0000 s % 6.47/1.53 % (3205269)Peak memory usage: 87 MB % 6.47/1.53 % (3205269)Instructions burned: 1 (million) % 6.47/1.53 [W928 07:07:50.049283746 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049323885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049361455 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049367850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049381451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049387975 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049402175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049408428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049421955 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049428130 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.53 [W928 07:07:50.049441961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.55 [W928 07:07:50.049448150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 6.47/1.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 6.47/1.55 % (3205272)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2512671664:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi) % 6.47/1.55 % (3205273)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=2948165019:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi) % 6.47/1.55 % (3205272)Refutation not found, incomplete strategy % 6.47/1.55 % (3205272)------------------------------ % 6.47/1.55 % (3205272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.55 % (3205272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.55 % (3205272)CaDiCaL version: 2.1.3 % 6.47/1.55 % (3205272)Termination reason: Refutation not found, incomplete strategy % 6.47/1.55 % (3205272)Time elapsed: 0.0000 s % 6.47/1.55 % (3205272)Peak memory usage: 86 MB % 6.47/1.55 % (3205268)------------------------------ % 6.47/1.55 % (3205268)------------------------------ % 6.47/1.55 % (3205256)Refutation not found, incomplete strategy % 6.47/1.55 % (3205256)------------------------------ % 6.47/1.55 % (3205256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.55 % (3205256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.55 % (3205256)CaDiCaL version: 2.1.3 % 6.47/1.55 % (3205256)Termination reason: Refutation not found, incomplete strategy % 6.47/1.55 % (3205256)Time elapsed: 0.310 s % 6.47/1.55 % (3205256)Peak memory usage: 124 MB % 6.47/1.55 % (3205256)Instructions burned: 823 (million) % 6.47/1.55 % (3205269)------------------------------ % 6.47/1.55 % (3205269)------------------------------ % 6.47/1.55 % (3205273)Instruction limit reached! % 6.47/1.55 % (3205273)------------------------------ % 6.47/1.55 % (3205273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.55 % (3205273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.55 % (3205273)CaDiCaL version: 2.1.3 % 6.47/1.55 % (3205273)Termination reason: Instruction limit % 6.47/1.55 % (3205273)Termination phase: Saturation % 6.47/1.55 % (3205273)Time elapsed: 0.067 s % 6.47/1.55 % (3205273)Peak memory usage: 92 MB % 6.47/1.55 % (3205273)Instructions burned: 249 (million) % 6.47/1.55 % (3205276)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=30815618:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi) % 6.47/1.55 % (3205276)Refutation not found, incomplete strategy % 6.47/1.55 % (3205276)------------------------------ % 6.47/1.55 % (3205276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.55 % (3205276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.55 % (3205276)CaDiCaL version: 2.1.3 % 6.47/1.55 % (3205276)Termination reason: Refutation not found, incomplete strategy % 6.47/1.55 % (3205276)Time elapsed: 0.0000 s % 6.47/1.55 % (3205276)Peak memory usage: 86 MB % 6.47/1.55 % (3205277)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3253990789:i=2350_2995 on theBenchmark for (2995ds/2350Mi) % 6.47/1.55 % (3205272)------------------------------ % 6.47/1.55 % (3205272)------------------------------ % 6.47/1.55 % (3205278)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=423979273:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi) % 6.47/1.55 % (3205278)Refutation not found, incomplete strategy % 6.47/1.55 % (3205278)------------------------------ % 6.47/1.55 % (3205278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.47/1.55 % (3205278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.47/1.55 % (3205278)CaDiCaL version: 2.1.3 % 6.47/1.55 % (3205278)Termination reason: Refutation not found, incomplete strategy % 6.47/1.55 % (3205278)Time elapsed: 0.001 s % 6.47/1.55 % (3205278)Peak memory usage: 88 MB % 6.47/1.55 % (3205278)Instructions burned: 1 (million) % 6.47/1.55 % (3205256)------------------------------ % 6.47/1.55 % (3205256)------------------------------ % 6.47/1.55 % (3205282)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3498536642:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi) % 7.83/1.80 % (3205282)Refutation not found, incomplete strategy % 7.83/1.80 % (3205282)------------------------------ % 7.83/1.80 % (3205282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.83/1.80 % (3205282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.83/1.80 % (3205282)CaDiCaL version: 2.1.3 % 7.83/1.80 % (3205282)Termination reason: Refutation not found, incomplete strategy % 7.83/1.80 % (3205282)Time elapsed: 0.009 s % 7.83/1.80 % (3205282)Peak memory usage: 87 MB % 7.83/1.80 % (3205282)Instructions burned: 35 (million) % 7.83/1.80 % (3205276)------------------------------ % 7.83/1.80 % (3205276)------------------------------ % 7.83/1.80 % (3205283)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1429970621:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi) % 7.83/1.80 % (3205278)------------------------------ % 7.83/1.80 % (3205278)------------------------------ % 7.83/1.80 % (3205283)Instruction limit reached! % 7.83/1.80 % (3205283)------------------------------ % 7.83/1.80 % (3205283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.83/1.80 % (3205283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.83/1.80 % (3205283)CaDiCaL version: 2.1.3 % 7.83/1.80 % (3205283)Termination reason: Instruction limit % 7.83/1.80 % (3205283)Termination phase: Saturation % 7.83/1.80 % (3205283)Time elapsed: 0.033 s % 7.83/1.80 % (3205283)Peak memory usage: 89 MB % 7.83/1.80 % (3205283)Instructions burned: 116 (million) % 7.83/1.80 % (3205285)lrs+10_1_sil=8000:sp=occurrence:random_seed=1527392389:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi) % 7.83/1.80 % (3205285)Refutation not found, incomplete strategy % 7.83/1.80 % (3205285)------------------------------ % 7.83/1.80 % (3205285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.83/1.80 % (3205285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.83/1.80 % (3205285)CaDiCaL version: 2.1.3 % 7.83/1.80 % (3205285)Termination reason: Refutation not found, incomplete strategy % 7.83/1.80 % (3205285)Time elapsed: 0.0000 s % 7.83/1.80 % (3205285)Peak memory usage: 86 MB % 7.83/1.80 % (3205287)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2567133279:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi) % 7.83/1.80 % (3205287)Refutation not found, incomplete strategy % 7.83/1.80 % (3205287)------------------------------ % 7.83/1.80 % (3205287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.83/1.80 % (3205287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.83/1.80 % (3205287)CaDiCaL version: 2.1.3 % 7.83/1.80 % (3205287)Termination reason: Refutation not found, incomplete strategy % 7.83/1.80 % (3205287)Time elapsed: 0.0000 s % 7.83/1.80 % (3205287)Peak memory usage: 87 MB % 7.83/1.80 % (3205282)------------------------------ % 7.83/1.80 % (3205282)------------------------------ % 7.83/1.80 % (3205288)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1466592413:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi) % 7.83/1.80 % (3205291)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3762478346:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi) % 7.83/1.80 % (3205291)Refutation not found, incomplete strategy % 7.83/1.80 % (3205291)------------------------------ % 7.83/1.80 % (3205291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 7.83/1.80 % (3205291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 7.83/1.80 % (3205291)CaDiCaL version: 2.1.3 % 7.83/1.80 % (3205291)Termination reason: Refutation not found, incomplete strategy % 7.83/1.80 % (3205291)Time elapsed: 0.001 s % 7.83/1.80 % (3205291)Peak memory usage: 88 MB % 7.83/1.80 % (3205291)Instructions burned: 2 (million) % 7.83/1.80 % (3205285)------------------------------ % 7.83/1.80 % (3205285)------------------------------ % 7.83/1.80 % (3205287)------------------------------ % 7.83/1.80 % (3205287)------------------------------ % 7.83/1.80 % (3205294)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4172348335:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi) % 7.83/1.80 % (3205294)Refutation not found, incomplete strategy % 7.83/1.80 % (3205294)------------------------------ % 7.83/1.80 % (3205294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.08/1.90 % (3205294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.90 % (3205294)CaDiCaL version: 2.1.3 % 8.08/1.90 % (3205294)Termination reason: Refutation not found, incomplete strategy % 8.08/1.90 % (3205294)Time elapsed: 0.0000 s % 8.08/1.90 % (3205294)Peak memory usage: 86 MB % 8.08/1.90 % (3205255)Refutation not found, incomplete strategy % 8.08/1.90 % (3205255)------------------------------ % 8.08/1.90 % (3205255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.08/1.90 % (3205255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.08/1.90 % (3205255)CaDiCaL version: 2.1.3 % 8.08/1.90 % (3205255)Termination reason: Refutation not found, incomplete strategy % 8.08/1.90 % (3205255)Time elapsed: 0.909 s % 8.08/1.90 % (3205255)Peak memory usage: 138 MB % 8.08/1.90 % (3205255)Instructions burned: 2763 (million) % 8.08/1.90 [W928 07:07:51.755493783 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755513882 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755554512 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755560709 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755574846 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755581629 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755596256 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755602713 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755616313 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755622721 register_special_ops.cpp:225] Warning: Creating a tensor from 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.08/1.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.08/1.90 [W928 07:07:51.755636641 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 [W928 07:07:51.755642875 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 % (3205295)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2078054581:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi) % 11.12/2.16 % (3205291)------------------------------ % 11.12/2.16 % (3205291)------------------------------ % 11.12/2.16 % (3205288)Refutation not found, incomplete strategy % 11.12/2.16 % (3205288)------------------------------ % 11.12/2.16 % (3205288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.12/2.16 % (3205288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.12/2.16 % (3205288)CaDiCaL version: 2.1.3 % 11.12/2.16 % (3205288)Termination reason: Refutation not found, incomplete strategy % 11.12/2.16 % (3205288)Time elapsed: 0.325 s % 11.12/2.16 % (3205288)Peak memory usage: 125 MB % 11.12/2.16 % (3205288)Instructions burned: 824 (million) % 11.12/2.16 % (3205294)------------------------------ % 11.12/2.16 % (3205294)------------------------------ % 11.12/2.16 % (3205255)------------------------------ % 11.12/2.16 % (3205255)------------------------------ % 11.12/2.16 % (3205298)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=377802806:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2989 on theBenchmark for (2989ds/125Mi) % 11.12/2.16 % (3205298)Refutation not found, incomplete strategy % 11.12/2.16 % (3205298)------------------------------ % 11.12/2.16 % (3205298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.12/2.16 % (3205298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.12/2.16 % (3205298)CaDiCaL version: 2.1.3 % 11.12/2.16 % (3205298)Termination reason: Refutation not found, incomplete strategy % 11.12/2.16 % (3205298)Time elapsed: 0.001 s % 11.12/2.16 % (3205298)Peak memory usage: 87 MB % 11.12/2.16 % (3205298)Instructions burned: 1 (million) % 11.12/2.16 % (3205299)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2765237081:i=134:gtgl=5:slsql=off:gtg=exists_sym_2988 on theBenchmark for (2988ds/134Mi) % 11.12/2.16 [W928 07:07:51.002409612 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 [W928 07:07:51.002430632 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 [W928 07:07:51.002470097 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 [W928 07:07:51.002476454 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 [W928 07:07:51.002518632 register_special_ops.cpp:225] Warning: Creating a tensor from 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.12/2.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 11.12/2.16 [W928 07:07:51.002524731 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 [W928 07:07:51.002539807 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 [W928 07:07:51.002545481 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 [W928 07:07:51.002558330 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 [W928 07:07:51.002564045 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 [W928 07:07:51.002577195 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 [W928 07:07:51.002582911 register_special_ops.cpp:225] Warning: Creating a tensor from 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.72/2.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.72/2.48 % (3205301)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3179278443:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/141Mi) % 12.72/2.48 % (3205301)Refutation not found, incomplete strategy % 12.72/2.48 % (3205301)------------------------------ % 12.72/2.48 % (3205301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.72/2.48 % (3205301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.72/2.48 % (3205301)CaDiCaL version: 2.1.3 % 12.72/2.48 % (3205301)Termination reason: Refutation not found, incomplete strategy % 12.72/2.48 % (3205301)Time elapsed: 0.0000 s % 12.72/2.48 % (3205301)Peak memory usage: 86 MB % 12.72/2.48 % (3205288)------------------------------ % 12.72/2.48 % (3205288)------------------------------ % 12.72/2.48 % (3205299)Instruction limit reached! % 12.72/2.48 % (3205299)------------------------------ % 12.72/2.48 % (3205299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.72/2.48 % (3205299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.72/2.48 % (3205299)CaDiCaL version: 2.1.3 % 12.72/2.48 % (3205299)Termination reason: Instruction limit % 12.72/2.48 % (3205299)Termination phase: Saturation % 12.72/2.48 % (3205299)Time elapsed: 0.045 s % 12.72/2.48 % (3205299)Peak memory usage: 90 MB % 12.72/2.48 % (3205299)Instructions burned: 137 (million) % 12.72/2.48 % (3205298)------------------------------ % 12.72/2.48 % (3205298)------------------------------ % 12.72/2.48 % (3205277)Instruction limit reached! % 12.72/2.48 % (3205277)------------------------------ % 12.72/2.48 % (3205277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.72/2.48 % (3205277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 12.72/2.48 % (3205277)CaDiCaL version: 2.1.3 % 12.72/2.48 % (3205277)Termination reason: Instruction limit % 12.72/2.48 % (3205277)Termination phase: Saturation % 12.72/2.48 % (3205277)Time elapsed: 0.845 s % 12.72/2.48 % (3205277)Peak memory usage: 143 MB % 12.72/2.48 % (3205277)Instructions burned: 2352 (million) % 12.72/2.48 % (3205295)Refutation not found, incomplete strategy % 12.72/2.48 % (3205295)------------------------------ % 12.72/2.48 % (3205295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 12.72/2.48 % (3205295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.77/2.66 % (3205295)CaDiCaL version: 2.1.3 % 13.77/2.66 % (3205295)Termination reason: Refutation not found, incomplete strategy % 13.77/2.66 % (3205295)Time elapsed: 0.318 s % 13.77/2.66 % (3205295)Peak memory usage: 125 MB % 13.77/2.66 % (3205295)Instructions burned: 827 (million) % 13.77/2.66 % (3205304)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1568382557:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/431Mi) % 13.77/2.66 % (3205304)Refutation not found, incomplete strategy % 13.77/2.66 % (3205304)------------------------------ % 13.77/2.66 % (3205304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.77/2.66 % (3205304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.77/2.66 % (3205304)CaDiCaL version: 2.1.3 % 13.77/2.66 % (3205304)Termination reason: Refutation not found, incomplete strategy % 13.77/2.66 % (3205304)Time elapsed: 0.0000 s % 13.77/2.66 % (3205304)Peak memory usage: 86 MB % 13.77/2.66 % (3205305)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=923655398:i=6060:aac=none:ins=25_2986 on theBenchmark for (2986ds/6060Mi) % 13.77/2.66 % (3205301)------------------------------ % 13.77/2.66 % (3205301)------------------------------ % 13.77/2.66 % (3205306)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=2094719550:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2986 on theBenchmark for (2986ds/150Mi) % 13.77/2.66 % (3205307)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=269623729:i=14155:bd=all_2986 on theBenchmark for (2986ds/14155Mi) % 13.77/2.66 % (3205306)Instruction limit reached! % 13.77/2.66 % (3205306)------------------------------ % 13.77/2.66 % (3205306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.77/2.66 % (3205306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.77/2.66 % (3205306)CaDiCaL version: 2.1.3 % 13.77/2.66 % (3205306)Termination reason: Instruction limit % 13.77/2.66 % (3205306)Termination phase: Saturation % 13.77/2.66 % (3205306)Time elapsed: 0.044 s % 13.77/2.66 % (3205306)Peak memory usage: 91 MB % 13.77/2.66 % (3205306)Instructions burned: 150 (million) % 13.77/2.66 % (3205295)------------------------------ % 13.77/2.66 % (3205295)------------------------------ % 13.77/2.66 % (3205311)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=394707325:i=667:av=off:fsr=off_2985 on theBenchmark for (2985ds/667Mi) % 13.77/2.66 % (3205311)Refutation not found, incomplete strategy % 13.77/2.66 % (3205311)------------------------------ % 13.77/2.66 % (3205311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.77/2.66 % (3205311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.77/2.66 % (3205311)CaDiCaL version: 2.1.3 % 13.77/2.66 % (3205311)Termination reason: Refutation not found, incomplete strategy % 13.77/2.66 % (3205311)Time elapsed: 0.002 s % 13.77/2.66 % (3205311)Peak memory usage: 87 MB % 13.77/2.66 % (3205311)Instructions burned: 7 (million) % 13.77/2.66 % (3205304)------------------------------ % 13.77/2.66 % (3205304)------------------------------ % 13.77/2.66 % (3205313)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=2475211958:s2a=on:i=185:s2at=1.8:fdi=4_2985 on theBenchmark for (2985ds/185Mi) % 13.77/2.66 % (3205315)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2779038331:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2984 on theBenchmark for (2984ds/193Mi) % 13.77/2.66 % (3205315)Refutation not found, incomplete strategy % 13.77/2.66 % (3205315)------------------------------ % 13.77/2.66 % (3205315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.77/2.66 % (3205315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.77/2.66 % (3205315)CaDiCaL version: 2.1.3 % 13.77/2.66 % (3205315)Termination reason: Refutation not found, incomplete strategy % 13.77/2.66 % (3205315)Time elapsed: 0.0000 s % 13.77/2.66 % (3205315)Peak memory usage: 86 MB % 13.77/2.66 % (3205313)Instruction limit reached! % 13.77/2.66 % (3205313)------------------------------ % 13.77/2.66 % (3205313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.87 % (3205313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.87 % (3205313)CaDiCaL version: 2.1.3 % 15.23/2.87 % (3205313)Termination reason: Instruction limit % 15.23/2.87 % (3205313)Termination phase: Saturation % 15.23/2.87 % (3205313)Time elapsed: 0.052 s % 15.23/2.87 % (3205313)Peak memory usage: 90 MB % 15.23/2.87 % (3205313)Instructions burned: 185 (million) % 15.23/2.87 % (3205316)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=597624695:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2984 on theBenchmark for (2984ds/4850Mi) % 15.23/2.87 % (3205316)Refutation not found, incomplete strategy % 15.23/2.87 % (3205316)------------------------------ % 15.23/2.87 % (3205316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.87 % (3205316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.87 % (3205316)CaDiCaL version: 2.1.3 % 15.23/2.87 % (3205316)Termination reason: Refutation not found, incomplete strategy % 15.23/2.87 % (3205316)Time elapsed: 0.003 s % 15.23/2.87 % (3205316)Peak memory usage: 88 MB % 15.23/2.87 % (3205316)Instructions burned: 8 (million) % 15.23/2.87 % (3205311)------------------------------ % 15.23/2.87 % (3205311)------------------------------ % 15.23/2.87 % (3205319)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1049888206:i=12111:sd=1:ss=included_2983 on theBenchmark for (2983ds/12111Mi) % 15.23/2.87 % (3205315)------------------------------ % 15.23/2.87 % (3205315)------------------------------ % 15.23/2.87 % (3205321)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3181167135:i=319:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/319Mi) % 15.23/2.87 % (3205316)------------------------------ % 15.23/2.87 % (3205316)------------------------------ % 15.23/2.87 % (3205323)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1352464514:i=2064:ep=RST_2982 on theBenchmark for (2982ds/2064Mi) % 15.23/2.87 % (3205323)Refutation not found, incomplete strategy % 15.23/2.87 % (3205323)------------------------------ % 15.23/2.87 % (3205323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.87 % (3205323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.87 % (3205323)CaDiCaL version: 2.1.3 % 15.23/2.87 % (3205323)Termination reason: Refutation not found, incomplete strategy % 15.23/2.87 % (3205323)Time elapsed: 0.003 s % 15.23/2.87 % (3205323)Peak memory usage: 88 MB % 15.23/2.87 % (3205323)Instructions burned: 8 (million) % 15.23/2.87 % (3205321)Instruction limit reached! % 15.23/2.87 % (3205321)------------------------------ % 15.23/2.87 % (3205321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 15.23/2.87 % (3205321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 15.23/2.87 % (3205321)CaDiCaL version: 2.1.3 % 15.23/2.87 % (3205321)Termination reason: Instruction limit % 15.23/2.87 % (3205321)Termination phase: Saturation % 15.23/2.87 % (3205321)Time elapsed: 0.101 s % 15.23/2.87 % (3205321)Peak memory usage: 92 MB % 15.23/2.87 % (3205321)Instructions burned: 320 (million) % 15.23/2.87 % (3205325)dis-1011_128_sil=32000:random_seed=1658608568:i=3706:ep=RST:av=off_2981 on theBenchmark for (2981ds/3706Mi) % 15.23/2.87 [W928 07:07:52.684701771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.23/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.23/2.87 [W928 07:07:52.684722300 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.23/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.23/2.87 [W928 07:07:52.684744607 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 15.23/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 15.23/2.87 [W928 07:07:52.684751809 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684766266 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684771779 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684785213 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684826739 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684847970 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684854078 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684867435 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 [W928 07:07:52.684873159 register_special_ops.cpp:225] Warning: Creating a tensor from 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.70/3.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 19.70/3.44 % (3205327)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1942068086:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2981 on theBenchmark for (2981ds/757Mi) % 19.70/3.44 % (3205327)Refutation not found, incomplete strategy % 19.70/3.44 % (3205327)------------------------------ % 19.70/3.44 % (3205327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.70/3.44 % (3205327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.70/3.44 % (3205327)CaDiCaL version: 2.1.3 % 19.70/3.44 % (3205327)Termination reason: Refutation not found, incomplete strategy % 19.70/3.44 % (3205327)Time elapsed: 0.0000 s % 19.70/3.44 % (3205327)Peak memory usage: 86 MB % 19.70/3.44 % (3205323)------------------------------ % 19.70/3.44 % (3205323)------------------------------ % 19.70/3.44 % (3205319)Refutation not found, incomplete strategy % 19.70/3.44 % (3205319)------------------------------ % 19.70/3.44 % (3205319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.70/3.44 % (3205319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.70/3.44 % (3205319)CaDiCaL version: 2.1.3 % 19.70/3.44 % (3205319)Termination reason: Refutation not found, incomplete strategy % 19.70/3.44 % (3205319)Time elapsed: 0.316 s % 19.70/3.44 % (3205319)Peak memory usage: 126 MB % 19.70/3.44 % (3205319)Instructions burned: 828 (million) % 19.70/3.44 % (3205327)------------------------------ % 19.70/3.44 % (3205327)------------------------------ % 19.70/3.44 % (3205330)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2152638742:i=13913:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/13913Mi) % 20.34/3.58 % (3205319)------------------------------ % 20.34/3.58 % (3205319)------------------------------ % 20.34/3.58 % (3205332)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1414262493:i=9925:aac=none_2978 on theBenchmark for (2978ds/9925Mi) % 20.34/3.58 % (3205333)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3401979320:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2977 on theBenchmark for (2977ds/2479Mi) % 20.34/3.58 % (3205333)Refutation not found, incomplete strategy % 20.34/3.58 % (3205333)------------------------------ % 20.34/3.58 % (3205333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 20.34/3.58 % (3205333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 20.34/3.58 % (3205333)CaDiCaL version: 2.1.3 % 20.34/3.58 % (3205333)Termination reason: Refutation not found, incomplete strategy % 20.34/3.58 % (3205333)Time elapsed: 0.0000 s % 20.34/3.58 % (3205333)Peak memory usage: 86 MB % 20.34/3.58 [W928 07:07:52.074068956 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074091576 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074113582 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074121148 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074136914 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074143659 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074158107 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074164789 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074178855 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 20.34/3.58 [W928 07:07:52.074185307 register_special_ops.cpp:225] Warning: Creating a tensor from 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.34/3.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.41/4.61 [W928 07:07:52.074199580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.41/4.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.41/4.61 [W928 07:07:52.074205507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.41/4.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.41/4.61 % (3205330)Refutation not found, incomplete strategy % 28.41/4.61 % (3205330)------------------------------ % 28.41/4.61 % (3205330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.41/4.61 % (3205330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.61 % (3205330)CaDiCaL version: 2.1.3 % 28.41/4.61 % (3205330)Termination reason: Refutation not found, incomplete strategy % 28.41/4.61 % (3205330)Time elapsed: 0.307 s % 28.41/4.61 % (3205330)Peak memory usage: 125 MB % 28.41/4.61 % (3205330)Instructions burned: 826 (million) % 28.41/4.61 % (3205333)------------------------------ % 28.41/4.61 % (3205333)------------------------------ % 28.41/4.61 % (3205332)Refutation not found, incomplete strategy % 28.41/4.61 % (3205332)------------------------------ % 28.41/4.61 % (3205332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.41/4.61 % (3205332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.61 % (3205332)CaDiCaL version: 2.1.3 % 28.41/4.61 % (3205332)Termination reason: Refutation not found, incomplete strategy % 28.41/4.61 % (3205332)Time elapsed: 0.318 s % 28.41/4.61 % (3205332)Peak memory usage: 128 MB % 28.41/4.61 % (3205332)Instructions burned: 856 (million) % 28.41/4.61 % (3205336)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=93697058:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2975 on theBenchmark for (2975ds/440Mi) % 28.41/4.61 % (3205330)------------------------------ % 28.41/4.61 % (3205330)------------------------------ % 28.41/4.61 % (3205336)Instruction limit reached! % 28.41/4.61 % (3205336)------------------------------ % 28.41/4.61 % (3205336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.41/4.61 % (3205336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.61 % (3205336)CaDiCaL version: 2.1.3 % 28.41/4.61 % (3205336)Termination reason: Instruction limit % 28.41/4.61 % (3205336)Termination phase: Saturation % 28.41/4.61 % (3205336)Time elapsed: 0.113 s % 28.41/4.61 % (3205336)Peak memory usage: 92 MB % 28.41/4.61 % (3205336)Instructions burned: 440 (million) % 28.41/4.61 % (3205332)------------------------------ % 28.41/4.61 % (3205332)------------------------------ % 28.41/4.61 % (3205338)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1973278443:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2973 on theBenchmark for (2973ds/11145Mi) % 28.41/4.61 % (3205339)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=1544601020:cts=off:i=3034:av=off:er=known:fsd=on_2973 on theBenchmark for (2973ds/3034Mi) % 28.41/4.61 % (3205341)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=789903492:st=2:s2a=on:i=524:s2at=2:ss=axioms_2972 on theBenchmark for (2972ds/524Mi) % 28.41/4.61 % (3205341)Refutation not found, incomplete strategy % 28.41/4.61 % (3205341)------------------------------ % 28.41/4.61 % (3205341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.41/4.61 % (3205341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.41/4.61 % (3205341)CaDiCaL version: 2.1.3 % 28.41/4.61 % (3205341)Termination reason: Refutation not found, incomplete strategy % 28.41/4.61 % (3205341)Time elapsed: 0.0000 s % 28.41/4.61 % (3205341)Peak memory usage: 87 MB % 28.41/4.61 % (3205341)Instructions burned: 1 (million) % 28.41/4.61 [W928 07:07:53.645350490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.41/4.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.41/4.61 [W928 07:07:53.645370873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645392094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645398480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645412441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645451387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645480574 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645488913 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645502246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645508119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645520956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 [W928 07:07:53.645526745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 28.97/4.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 28.97/4.74 % (3205341)------------------------------ % 28.97/4.74 % (3205341)------------------------------ % 28.97/4.74 % (3205338)Refutation not found, incomplete strategy % 28.97/4.74 % (3205338)------------------------------ % 28.97/4.74 % (3205338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 28.97/4.74 % (3205338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 28.97/4.74 % (3205338)CaDiCaL version: 2.1.3 % 28.97/4.74 % (3205338)Termination reason: Refutation not found, incomplete strategy % 28.97/4.74 % (3205338)Time elapsed: 0.310 s % 28.97/4.74 % (3205338)Peak memory usage: 125 MB % 28.97/4.74 % (3205338)Instructions burned: 827 (million) % 28.97/4.74 % (3205344)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3204191053:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2970 on theBenchmark for (2970ds/1016Mi) % 30.55/4.96 % (3205344)Refutation not found, incomplete strategy % 30.55/4.96 % (3205344)------------------------------ % 30.55/4.96 % (3205344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.55/4.96 % (3205344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.55/4.96 % (3205344)CaDiCaL version: 2.1.3 % 30.55/4.96 % (3205344)Termination reason: Refutation not found, incomplete strategy % 30.55/4.96 % (3205344)Time elapsed: 0.0000 s % 30.55/4.96 % (3205344)Peak memory usage: 87 MB % 30.55/4.96 % (3205325)Instruction limit reached! % 30.55/4.96 % (3205325)------------------------------ % 30.55/4.96 % (3205325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.55/4.96 % (3205325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.55/4.96 % (3205325)CaDiCaL version: 2.1.3 % 30.55/4.96 % (3205325)Termination reason: Instruction limit % 30.55/4.96 % (3205325)Termination phase: Saturation % 30.55/4.96 % (3205325)Time elapsed: 1.177 s % 30.55/4.96 % (3205325)Peak memory usage: 105 MB % 30.55/4.96 % (3205325)Instructions burned: 3709 (million) % 30.55/4.96 % (3205338)------------------------------ % 30.55/4.96 % (3205338)------------------------------ % 30.55/4.96 % (3205346)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3337244884:i=14123:bd=preordered:ins=4_2969 on theBenchmark for (2969ds/14123Mi) % 30.55/4.96 % (3205344)------------------------------ % 30.55/4.96 % (3205344)------------------------------ % 30.55/4.96 % (3205348)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=484193763:i=5781:kws=precedence:bd=all:rawr=on_2968 on theBenchmark for (2968ds/5781Mi) % 30.55/4.96 % (3205349)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=2940588816:i=2448:gtgl=5:bd=preordered:gtg=all_2967 on theBenchmark for (2967ds/2448Mi) % 30.55/4.96 % (3205305)Instruction limit reached! % 30.55/4.96 % (3205305)------------------------------ % 30.55/4.96 % (3205305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.55/4.96 % (3205305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.55/4.96 % (3205305)CaDiCaL version: 2.1.3 % 30.55/4.96 % (3205305)Termination reason: Instruction limit % 30.55/4.96 % (3205305)Termination phase: Saturation % 30.55/4.96 % (3205305)Time elapsed: 2.027 s % 30.55/4.96 % (3205305)Peak memory usage: 151 MB % 30.55/4.96 % (3205305)Instructions burned: 6064 (million) % 30.55/4.96 % (3205352)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1790840223:i=3223:kws=precedence:fgj=on:av=off_2965 on theBenchmark for (2965ds/3223Mi) % 30.55/4.96 % (3205339)Instruction limit reached! % 30.55/4.96 % (3205339)------------------------------ % 30.55/4.96 % (3205339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 30.55/4.96 % (3205339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 30.55/4.96 % (3205339)CaDiCaL version: 2.1.3 % 30.55/4.96 % (3205339)Termination reason: Instruction limit % 30.55/4.96 % (3205339)Termination phase: Saturation % 30.55/4.96 % (3205339)Time elapsed: 0.993 s % 30.55/4.96 % (3205339)Peak memory usage: 144 MB % 30.55/4.96 % (3205339)Instructions burned: 3037 (million) % 30.55/4.96 % (3205354)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3821205340:st=5.6:i=2033:sd=3:ss=axioms_2962 on theBenchmark for (2962ds/2033Mi) % 30.55/4.96 [W928 07:07:54.817658622 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 30.55/4.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.55/4.96 [W928 07:07:54.817680785 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 30.55/4.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 30.55/4.96 [W928 07:07:54.817718995 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817725029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817745877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817760957 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817775917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817781451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817794418 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817799837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817813414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 [W928 07:07:54.817818871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 32.38/5.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 32.38/5.17 % (3205349)Instruction limit reached! % 32.38/5.17 % (3205349)------------------------------ % 32.38/5.17 % (3205349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.38/5.17 % (3205349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.38/5.17 % (3205349)CaDiCaL version: 2.1.3 % 32.38/5.17 % (3205349)Termination reason: Instruction limit % 32.38/5.17 % (3205349)Termination phase: Saturation % 32.38/5.17 % (3205349)Time elapsed: 0.791 s % 32.38/5.17 % (3205349)Peak memory usage: 152 MB % 32.38/5.17 % (3205349)Instructions burned: 2449 (million) % 32.38/5.17 % (3205354)Refutation not found, incomplete strategy % 32.38/5.17 % (3205354)------------------------------ % 32.38/5.17 % (3205354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 32.38/5.17 % (3205354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 32.38/5.17 % (3205354)CaDiCaL version: 2.1.3 % 32.38/5.17 % (3205354)Termination reason: Refutation not found, incomplete strategy % 32.38/5.17 % (3205354)Time elapsed: 0.309 s % 32.38/5.17 % (3205354)Peak memory usage: 125 MB % 32.38/5.17 % (3205354)Instructions burned: 827 (million) % 32.38/5.17 % (3205356)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3784064640:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2958 on theBenchmark for (2958ds/2055Mi) % 34.62/5.58 % (3205354)------------------------------ % 34.62/5.58 % (3205354)------------------------------ % 34.62/5.58 [W928 07:07:54.152085572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152106812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152128114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152135514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152149802 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152156295 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152170781 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152177329 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152191451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152197684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152212077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 [W928 07:07:54.152218312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 34.62/5.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 34.62/5.58 % (3205358)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=2718031330:i=21611:sd=3:ss=axioms_2956 on theBenchmark for (2956ds/21611Mi) % 39.77/6.21 % (3205356)Refutation not found, incomplete strategy % 39.77/6.21 % (3205356)------------------------------ % 39.77/6.21 % (3205356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 39.77/6.21 % (3205356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 39.77/6.21 % (3205356)CaDiCaL version: 2.1.3 % 39.77/6.21 % (3205356)Termination reason: Refutation not found, incomplete strategy % 39.77/6.21 % (3205356)Time elapsed: 0.303 s % 39.77/6.21 % (3205356)Peak memory usage: 126 MB % 39.77/6.21 % (3205356)Instructions burned: 823 (million) % 39.77/6.21 [W928 07:07:54.376407839 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376431284 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376452803 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376460672 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376475866 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376482913 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376497593 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376504563 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376518553 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376525733 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376539763 register_special_ops.cpp:225] Warning: Creating a tensor from 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.77/6.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 39.77/6.21 [W928 07:07:54.376546749 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 41.92/6.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 41.92/6.60 % (3205356)------------------------------ % 41.92/6.60 % (3205356)------------------------------ % 41.92/6.60 % (3205352)Instruction limit reached! % 41.92/6.60 % (3205352)------------------------------ % 41.92/6.60 % (3205352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.92/6.60 % (3205352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.92/6.60 % (3205352)CaDiCaL version: 2.1.3 % 41.92/6.60 % (3205352)Termination reason: Instruction limit % 41.92/6.60 % (3205352)Termination phase: Saturation % 41.92/6.60 % (3205352)Time elapsed: 1.186 s % 41.92/6.60 % (3205352)Peak memory usage: 148 MB % 41.92/6.60 % (3205352)Instructions burned: 3225 (million) % 41.92/6.60 % (3205358)Refutation not found, incomplete strategy % 41.92/6.60 % (3205358)------------------------------ % 41.92/6.60 % (3205358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.92/6.60 % (3205358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.92/6.60 % (3205358)CaDiCaL version: 2.1.3 % 41.92/6.60 % (3205358)Termination reason: Refutation not found, incomplete strategy % 41.92/6.60 % (3205358)Time elapsed: 0.311 s % 41.92/6.60 % (3205358)Peak memory usage: 125 MB % 41.92/6.60 % (3205358)Instructions burned: 826 (million) % 41.92/6.60 % (3205360)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3682380116:i=4835:sd=13:ss=axioms:sgt=23_2953 on theBenchmark for (2953ds/4835Mi) % 41.92/6.60 % (3205360)Refutation not found, incomplete strategy % 41.92/6.60 % (3205360)------------------------------ % 41.92/6.60 % (3205360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.92/6.60 % (3205360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.92/6.60 % (3205360)CaDiCaL version: 2.1.3 % 41.92/6.60 % (3205360)Termination reason: Refutation not found, incomplete strategy % 41.92/6.60 % (3205360)Time elapsed: 0.0000 s % 41.92/6.60 % (3205360)Peak memory usage: 86 MB % 41.92/6.60 % (3205361)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=1968123171:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2952 on theBenchmark for (2952ds/797Mi) % 41.92/6.60 % (3205348)Instruction limit reached! % 41.92/6.60 % (3205348)------------------------------ % 41.92/6.60 % (3205348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.92/6.60 % (3205348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.92/6.60 % (3205348)CaDiCaL version: 2.1.3 % 41.92/6.60 % (3205348)Termination reason: Instruction limit % 41.92/6.60 % (3205348)Termination phase: Saturation % 41.92/6.60 % (3205348)Time elapsed: 1.590 s % 41.92/6.60 % (3205348)Peak memory usage: 129 MB % 41.92/6.60 % (3205348)Instructions burned: 5785 (million) % 41.92/6.60 % (3205358)------------------------------ % 41.92/6.60 % (3205358)------------------------------ % 41.92/6.60 % (3205360)------------------------------ % 41.92/6.60 % (3205360)------------------------------ % 41.92/6.60 % (3205364)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3469038108:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2951 on theBenchmark for (2951ds/2326Mi) % 41.92/6.60 % (3205364)Refutation not found, incomplete strategy % 41.92/6.60 % (3205364)------------------------------ % 41.92/6.60 % (3205364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.92/6.60 % (3205364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.92/6.60 % (3205364)CaDiCaL version: 2.1.3 % 41.92/6.60 % (3205364)Termination reason: Refutation not found, incomplete strategy % 41.92/6.60 % (3205364)Time elapsed: 0.004 s % 41.92/6.60 % (3205364)Peak memory usage: 88 MB % 41.92/6.60 % (3205364)Instructions burned: 13 (million) % 41.92/6.60 % (3205365)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1154314859:i=6038:nm=6_2950 on theBenchmark for (2950ds/6038Mi) % 41.92/6.60 % (3205366)lrs+10_1_sil=32000:sp=occurrence:random_seed=1845496000:st=2:i=33334:sd=3:ss=included:sgt=32_2950 on theBenchmark for (2950ds/33334Mi) % 41.92/6.60 % (3205361)Instruction limit reached! % 41.92/6.60 % (3205361)------------------------------ % 41.92/6.60 % (3205361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.48/7.38 % (3205361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.48/7.38 % (3205361)CaDiCaL version: 2.1.3 % 47.48/7.38 % (3205361)Termination reason: Instruction limit % 47.48/7.38 % (3205361)Termination phase: Saturation % 47.48/7.38 % (3205361)Time elapsed: 0.241 s % 47.48/7.38 % (3205361)Peak memory usage: 96 MB % 47.48/7.38 % (3205361)Instructions burned: 798 (million) % 47.48/7.38 % (3205364)------------------------------ % 47.48/7.38 % (3205364)------------------------------ % 47.48/7.38 % (3205370)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2418234962:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2949 on theBenchmark for (2949ds/1008Mi) % 47.48/7.38 % (3205370)Refutation not found, incomplete strategy % 47.48/7.38 % (3205370)------------------------------ % 47.48/7.38 % (3205370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.48/7.38 % (3205370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.48/7.38 % (3205370)CaDiCaL version: 2.1.3 % 47.48/7.38 % (3205370)Termination reason: Refutation not found, incomplete strategy % 47.48/7.38 % (3205370)Time elapsed: 0.0000 s % 47.48/7.38 % (3205370)Peak memory usage: 86 MB % 47.48/7.38 % (3205370)Instructions burned: 1 (million) % 47.48/7.38 % (3205371)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=2225681699:i=8327:s2at=5:bd=preordered_2948 on theBenchmark for (2948ds/8327Mi) % 47.48/7.38 % (3205370)------------------------------ % 47.48/7.38 % (3205370)------------------------------ % 47.48/7.38 % (3205365)Refutation not found, incomplete strategy % 47.48/7.38 % (3205365)------------------------------ % 47.48/7.38 % (3205365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.48/7.38 % (3205365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.48/7.38 % (3205365)CaDiCaL version: 2.1.3 % 47.48/7.38 % (3205365)Termination reason: Refutation not found, incomplete strategy % 47.48/7.38 % (3205365)Time elapsed: 0.319 s % 47.48/7.38 % (3205365)Peak memory usage: 129 MB % 47.48/7.38 % (3205365)Instructions burned: 854 (million) % 47.48/7.38 % (3205374)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=1047729176:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2946 on theBenchmark for (2946ds/1083Mi) % 47.48/7.38 % (3205365)------------------------------ % 47.48/7.38 % (3205365)------------------------------ % 47.48/7.38 % (3205307)Instruction limit reached! % 47.48/7.38 % (3205307)------------------------------ % 47.48/7.38 % (3205307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.48/7.38 % (3205307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.48/7.38 % (3205307)CaDiCaL version: 2.1.3 % 47.48/7.38 % (3205307)Termination reason: Instruction limit % 47.48/7.38 % (3205307)Termination phase: Saturation % 47.48/7.38 % (3205307)Time elapsed: 4.100 s % 47.48/7.38 % (3205307)Peak memory usage: 217 MB % 47.48/7.38 % (3205307)Instructions burned: 14158 (million) % 47.48/7.38 % (3205376)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=324139413:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2944 on theBenchmark for (2944ds/1084Mi) % 47.48/7.38 % (3205376)Refutation not found, incomplete strategy % 47.48/7.38 % (3205376)------------------------------ % 47.48/7.38 % (3205376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.48/7.38 % (3205376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.48/7.38 % (3205376)CaDiCaL version: 2.1.3 % 47.48/7.38 % (3205376)Termination reason: Refutation not found, incomplete strategy % 47.48/7.38 % (3205376)Time elapsed: 0.0000 s % 47.48/7.38 % (3205376)Peak memory usage: 86 MB % 47.48/7.38 % (3205374)Instruction limit reached! % 47.48/7.38 % (3205374)------------------------------ % 47.48/7.38 % (3205374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 47.48/7.38 % (3205374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 47.48/7.38 % (3205374)CaDiCaL version: 2.1.3 % 47.48/7.38 % (3205374)Termination reason: Instruction limit % 47.48/7.38 % (3205374)Termination phase: Saturation % 47.48/7.38 % (3205374)Time elapsed: 0.270 s % 47.48/7.38 % (3205374)Peak memory usage: 98 MB % 47.48/7.38 % (3205374)Instructions burned: 1086 (million) % 47.48/7.38 % (3205377)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=711112233:i=6995:s2at=5:gtg=all_2944 on theBenchmark for (2944ds/6995Mi) % 51.66/7.93 % (3205376)------------------------------ % 51.66/7.93 % (3205376)------------------------------ % 51.66/7.93 % (3205380)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=4288287015:st=2:i=6225:sd=15:ss=axioms_2943 on theBenchmark for (2943ds/6225Mi) % 51.66/7.93 % (3205380)Refutation not found, incomplete strategy % 51.66/7.93 % (3205380)------------------------------ % 51.66/7.93 % (3205380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 51.66/7.93 % (3205380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 51.66/7.93 % (3205380)CaDiCaL version: 2.1.3 % 51.66/7.93 % (3205380)Termination reason: Refutation not found, incomplete strategy % 51.66/7.93 % (3205380)Time elapsed: 0.0000 s % 51.66/7.93 % (3205380)Peak memory usage: 86 MB % 51.66/7.93 % (3205381)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3851783300:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2942 on theBenchmark for (2942ds/3372Mi) % 51.66/7.93 % (3205380)------------------------------ % 51.66/7.93 % (3205380)------------------------------ % 51.66/7.93 % (3205384)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1758706661:st=2.3:i=26457:sd=10:ss=included:sgt=8_2940 on theBenchmark for (2940ds/26457Mi) % 51.66/7.93 [W928 07:07:56.810477503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810497445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810534953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810541536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810555236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810561871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810575493 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810581988 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 51.66/7.93 [W928 07:07:56.810595722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 51.66/7.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.810602074 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.810620239 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.810625731 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 % (3205381)Refutation not found, incomplete strategy % 54.61/8.34 % (3205381)------------------------------ % 54.61/8.34 % (3205381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.61/8.34 % (3205381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.61/8.34 % (3205381)CaDiCaL version: 2.1.3 % 54.61/8.34 % (3205381)Termination reason: Refutation not found, incomplete strategy % 54.61/8.34 % (3205381)Time elapsed: 0.306 s % 54.61/8.34 % (3205381)Peak memory usage: 126 MB % 54.61/8.34 % (3205381)Instructions burned: 829 (million) % 54.61/8.34 % (3205381)------------------------------ % 54.61/8.34 % (3205381)------------------------------ % 54.61/8.34 % (3205384)Refutation not found, incomplete strategy % 54.61/8.34 % (3205384)------------------------------ % 54.61/8.34 % (3205384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.61/8.34 % (3205384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.61/8.34 % (3205384)CaDiCaL version: 2.1.3 % 54.61/8.34 % (3205384)Termination reason: Refutation not found, incomplete strategy % 54.61/8.34 % (3205384)Time elapsed: 0.334 s % 54.61/8.34 % (3205384)Peak memory usage: 129 MB % 54.61/8.34 % (3205384)Instructions burned: 852 (million) % 54.61/8.34 % (3205386)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=2445266417:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2936 on theBenchmark for (2936ds/13494Mi) % 54.61/8.34 % (3205384)------------------------------ % 54.61/8.34 % (3205384)------------------------------ % 54.61/8.34 % (3205388)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=1496874403:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2934 on theBenchmark for (2934ds/2503Mi) % 54.61/8.34 [W928 07:07:56.580715138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.580737873 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.580778972 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.580785582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 54.61/8.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.61/8.34 [W928 07:07:56.580799939 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580806819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580830735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580845801 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580860224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580865909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580879338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:56.580884921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 % (3205388)Refutation not found, incomplete strategy % 59.95/9.13 % (3205388)------------------------------ % 59.95/9.13 % (3205388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 59.95/9.13 % (3205388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 59.95/9.13 % (3205388)CaDiCaL version: 2.1.3 % 59.95/9.13 % (3205388)Termination reason: Refutation not found, incomplete strategy % 59.95/9.13 % (3205388)Time elapsed: 0.306 s % 59.95/9.13 % (3205388)Peak memory usage: 125 MB % 59.95/9.13 % (3205388)Instructions burned: 826 (million) % 59.95/9.13 % (3205388)------------------------------ % 59.95/9.13 % (3205388)------------------------------ % 59.95/9.13 % (3205390)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1665385130:i=2559:sd=1:ep=RSTC:ss=axioms_2928 on theBenchmark for (2928ds/2559Mi) % 59.95/9.13 [W928 07:07:57.136805883 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:57.136845490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 59.95/9.13 [W928 07:07:57.136866371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 59.95/9.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136872537 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136891826 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136897343 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136910659 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136916156 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136929106 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136934756 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136948450 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 [W928 07:07:57.136954141 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 62.22/9.43 % (3205390)Refutation not found, incomplete strategy % 62.22/9.43 % (3205390)------------------------------ % 62.22/9.43 % (3205390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.22/9.43 % (3205390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.22/9.43 % (3205390)CaDiCaL version: 2.1.3 % 62.22/9.43 % (3205390)Termination reason: Refutation not found, incomplete strategy % 62.22/9.43 % (3205390)Time elapsed: 0.306 s % 62.22/9.43 % (3205390)Peak memory usage: 126 MB % 62.22/9.43 % (3205390)Instructions burned: 826 (million) % 62.22/9.43 % (3205390)------------------------------ % 62.22/9.43 % (3205390)------------------------------ % 62.22/9.43 % (3205392)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1879056044:i=30753:av=off:ss=included_2923 on theBenchmark for (2923ds/30753Mi) % 62.22/9.43 % (3205371)Instruction limit reached! % 62.22/9.43 % (3205371)------------------------------ % 62.22/9.43 % (3205371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 62.22/9.43 % (3205371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 62.22/9.43 % (3205371)CaDiCaL version: 2.1.3 % 62.22/9.43 % (3205371)Termination reason: Instruction limit % 62.22/9.43 % (3205371)Termination phase: Saturation % 62.22/9.43 % (3205371)Time elapsed: 2.576 s % 62.22/9.43 % (3205371)Peak memory usage: 188 MB % 62.22/9.43 % (3205371)Instructions burned: 8329 (million) % 63.19/9.69 % (3205394)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=1034945420:i=26473:ep=RSTC_2921 on theBenchmark for (2921ds/26473Mi) % 63.19/9.69 % (3205377)Instruction limit reached! % 63.19/9.69 % (3205377)------------------------------ % 63.19/9.69 % (3205377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.19/9.69 % (3205377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.19/9.69 % (3205377)CaDiCaL version: 2.1.3 % 63.19/9.69 % (3205377)Termination reason: Instruction limit % 63.19/9.69 % (3205377)Termination phase: Saturation % 63.19/9.69 % (3205377)Time elapsed: 2.330 s % 63.19/9.69 % (3205377)Peak memory usage: 170 MB % 63.19/9.69 % (3205377)Instructions burned: 6997 (million) % 63.19/9.69 % (3205396)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=3483080103:cts=off:i=2759:kws=inv_arity:fgj=on_2919 on theBenchmark for (2919ds/2759Mi) % 63.19/9.69 % (3205346)Instruction limit reached! % 63.19/9.69 % (3205346)------------------------------ % 63.19/9.69 % (3205346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.19/9.69 % (3205346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.19/9.69 % (3205346)CaDiCaL version: 2.1.3 % 63.19/9.69 % (3205346)Termination reason: Instruction limit % 63.19/9.69 % (3205346)Termination phase: Saturation % 63.19/9.69 % (3205346)Time elapsed: 5.102 s % 63.19/9.69 % (3205346)Peak memory usage: 246 MB % 63.19/9.69 % (3205346)Instructions burned: 14125 (million) % 63.19/9.69 % (3205398)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=2822531487:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2916 on theBenchmark for (2916ds/5665Mi) % 63.19/9.69 % (3205396)Refutation not found, incomplete strategy % 63.19/9.69 % (3205396)------------------------------ % 63.19/9.69 % (3205396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 63.19/9.69 % (3205396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 63.19/9.69 % (3205396)CaDiCaL version: 2.1.3 % 63.19/9.69 % (3205396)Termination reason: Refutation not found, incomplete strategy % 63.19/9.69 % (3205396)Time elapsed: 0.315 s % 63.19/9.69 % (3205396)Peak memory usage: 129 MB % 63.19/9.69 % (3205396)Instructions burned: 855 (million) % 63.19/9.69 % (3205396)------------------------------ % 63.19/9.69 % (3205396)------------------------------ % 63.19/9.69 [W928 07:07:58.331335503 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.19/9.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.19/9.69 [W928 07:07:58.331362746 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.19/9.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.19/9.69 [W928 07:07:58.331385062 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.19/9.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.19/9.69 [W928 07:07:58.331391738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.19/9.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.19/9.69 [W928 07:07:58.331407272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 63.19/9.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 63.19/9.69 [W928 07:07:58.331413666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:58.331426578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:58.331432076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:58.331444453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:58.331453833 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:58.331467555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:58.331472956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 % (3205400)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=2320684868:i=1532:ep=RS:ss=axioms_2914 on theBenchmark for (2914ds/1532Mi) % 68.06/10.26 % (3205398)Refutation not found, incomplete strategy % 68.06/10.26 % (3205398)------------------------------ % 68.06/10.26 % (3205398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.06/10.26 % (3205398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.06/10.26 % (3205398)CaDiCaL version: 2.1.3 % 68.06/10.26 % (3205398)Termination reason: Refutation not found, incomplete strategy % 68.06/10.26 % (3205398)Time elapsed: 0.307 s % 68.06/10.26 % (3205398)Peak memory usage: 125 MB % 68.06/10.26 % (3205398)Instructions burned: 823 (million) % 68.06/10.26 % (3205398)------------------------------ % 68.06/10.26 % (3205398)------------------------------ % 68.06/10.26 [W928 07:07:59.634144907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:59.634165434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:59.634186511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:59.634193551 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.06/10.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.06/10.26 [W928 07:07:59.634207171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634213487 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634227327 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634241028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634255511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634261606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634274499 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.634280469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 % (3205402)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1466684294:i=1565:sd=2:ss=axioms:sgt=32_2911 on theBenchmark for (2911ds/1565Mi) % 68.78/10.36 % (3205400)Refutation not found, incomplete strategy % 68.78/10.36 % (3205400)------------------------------ % 68.78/10.36 % (3205400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 68.78/10.36 % (3205400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 68.78/10.36 % (3205400)CaDiCaL version: 2.1.3 % 68.78/10.36 % (3205400)Termination reason: Refutation not found, incomplete strategy % 68.78/10.36 % (3205400)Time elapsed: 0.313 s % 68.78/10.36 % (3205400)Peak memory usage: 126 MB % 68.78/10.36 % (3205400)Instructions burned: 823 (million) % 68.78/10.36 % (3205400)------------------------------ % 68.78/10.36 % (3205400)------------------------------ % 68.78/10.36 [W928 07:07:59.894795870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.894815617 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 68.78/10.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 68.78/10.36 [W928 07:07:59.894837282 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894844576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894859328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894872223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894887326 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894892986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894906272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894912106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894925952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 [W928 07:07:59.894931946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 70.62/10.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 70.62/10.69 % (3205402)Refutation not found, incomplete strategy % 70.62/10.69 % (3205402)------------------------------ % 70.62/10.69 % (3205402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 70.62/10.69 % (3205402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 70.62/10.69 % (3205402)CaDiCaL version: 2.1.3 % 70.62/10.69 % (3205402)Termination reason: Refutation not found, incomplete strategy % 70.62/10.69 % (3205402)Time elapsed: 0.311 s % 70.62/10.69 % (3205402)Peak memory usage: 125 MB % 70.62/10.69 % (3205402)Instructions burned: 827 (million) % 70.62/10.69 % (3205404)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=2162934246:i=1572:fgj=on:gsp=on_2908 on theBenchmark for (2908ds/1572Mi) % 70.62/10.69 % (3205402)------------------------------ % 70.62/10.69 % (3205402)------------------------------ % 70.62/10.69 % (3205406)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2100178674:i=6052:sd=4:ss=axioms:sgt=24_2905 on theBenchmark for (2905ds/6052Mi) % 70.62/10.69 [W928 07:07:59.464127118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464153054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464174714 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464181270 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464195474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464200998 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464214753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464220118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464232666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464243029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464256739 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 [W928 07:07:59.464262097 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 71.63/10.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 71.63/10.81 % (3205406)Refutation not found, incomplete strategy % 71.63/10.81 % (3205406)------------------------------ % 71.63/10.81 % (3205406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 71.63/10.81 % (3205406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 71.63/10.81 % (3205406)CaDiCaL version: 2.1.3 % 71.63/10.81 % (3205406)Termination reason: Refutation not found, incomplete strategy % 71.63/10.81 % (3205406)Time elapsed: 0.306 s % 71.63/10.81 % (3205406)Peak memory usage: 125 MB % 76.18/11.48 % (3205406)Instructions burned: 827 (million) % 76.18/11.48 % (3205404)Instruction limit reached! % 76.18/11.48 % (3205404)------------------------------ % 76.18/11.48 % (3205404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.18/11.48 % (3205404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.18/11.48 % (3205404)CaDiCaL version: 2.1.3 % 76.18/11.48 % (3205404)Termination reason: Instruction limit % 76.18/11.48 % (3205404)Termination phase: Saturation % 76.18/11.48 % (3205404)Time elapsed: 0.584 s % 76.18/11.48 % (3205404)Peak memory usage: 135 MB % 76.18/11.48 % (3205404)Instructions burned: 1573 (million) % 76.18/11.48 % (3205408)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=2931640056:i=3500:sd=1:bd=preordered:sup=off:ss=included_2901 on theBenchmark for (2901ds/3500Mi) % 76.18/11.48 % (3205406)------------------------------ % 76.18/11.48 % (3205406)------------------------------ % 76.18/11.48 % (3205410)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=485170643:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2900 on theBenchmark for (2900ds/1842Mi) % 76.18/11.48 [W928 07:08:00.899753918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899774448 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899795242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899802241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899817808 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899824492 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899839331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899846204 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899860540 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 76.18/11.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.18/11.48 [W928 07:08:00.899866985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.899881058 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.899886825 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 % (3205408)Refutation not found, incomplete strategy % 85.97/12.87 % (3205408)------------------------------ % 85.97/12.87 % (3205408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 85.97/12.87 % (3205408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 85.97/12.87 % (3205408)CaDiCaL version: 2.1.3 % 85.97/12.87 % (3205408)Termination reason: Refutation not found, incomplete strategy % 85.97/12.87 % (3205408)Time elapsed: 0.303 s % 85.97/12.87 % (3205408)Peak memory usage: 125 MB % 85.97/12.87 % (3205408)Instructions burned: 826 (million) % 85.97/12.87 [W928 07:08:00.013610206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013630357 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013670583 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013676918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013692202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013698606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013713280 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013719526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 85.97/12.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 85.97/12.87 [W928 07:08:00.013733503 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:00.013739846 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:00.013753209 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:00.013758668 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 % (3205410)Refutation not found, incomplete strategy % 86.57/12.97 % (3205410)------------------------------ % 86.57/12.97 % (3205410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.57/12.97 % (3205410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.57/12.97 % (3205410)CaDiCaL version: 2.1.3 % 86.57/12.97 % (3205410)Termination reason: Refutation not found, incomplete strategy % 86.57/12.97 % (3205410)Time elapsed: 0.307 s % 86.57/12.97 % (3205410)Peak memory usage: 125 MB % 86.57/12.97 % (3205410)Instructions burned: 828 (million) % 86.57/12.97 % (3205408)------------------------------ % 86.57/12.97 % (3205408)------------------------------ % 86.57/12.97 % (3205412)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3404412250:i=66096:add=on_2895 on theBenchmark for (2895ds/66096Mi) % 86.57/12.97 % (3205410)------------------------------ % 86.57/12.97 % (3205410)------------------------------ % 86.57/12.97 % (3205414)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=350270770:i=1884:sd=1:nm=60:ss=axioms_2894 on theBenchmark for (2894ds/1884Mi) % 86.57/12.97 % (3205386)Instruction limit reached! % 86.57/12.97 % (3205386)------------------------------ % 86.57/12.97 % (3205386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 86.57/12.97 % (3205386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 86.57/12.97 % (3205386)CaDiCaL version: 2.1.3 % 86.57/12.97 % (3205386)Termination reason: Instruction limit % 86.57/12.97 % (3205386)Termination phase: Saturation % 86.57/12.97 % (3205386)Time elapsed: 4.496 s % 86.57/12.97 % (3205386)Peak memory usage: 240 MB % 86.57/12.97 % (3205386)Instructions burned: 13496 (million) % 86.57/12.97 [W928 07:08:01.689743988 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:01.689781274 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:01.689803197 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:01.689809332 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 86.57/12.97 [W928 07:08:01.689823519 register_special_ops.cpp:225] Warning: Creating a tensor from 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.57/12.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689830564 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689844920 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689850625 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689863870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689869665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689882891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 [W928 07:08:01.689888794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 103.49/15.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.49/15.34 % (3205416)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3476044109:cts=off:i=5469:bs=on:fsr=off_2890 on theBenchmark for (2890ds/5469Mi) % 103.49/15.34 % (3205414)Refutation not found, incomplete strategy % 103.49/15.34 % (3205414)------------------------------ % 103.49/15.34 % (3205414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.49/15.34 % (3205414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.49/15.34 % (3205414)CaDiCaL version: 2.1.3 % 103.49/15.34 % (3205414)Termination reason: Refutation not found, incomplete strategy % 103.49/15.34 % (3205414)Time elapsed: 0.452 s % 103.49/15.34 % (3205414)Peak memory usage: 125 MB % 103.49/15.34 % (3205414)Instructions burned: 827 (million) % 103.49/15.34 % (3205414)------------------------------ % 103.49/15.34 % (3205414)------------------------------ % 103.49/15.34 % (3205418)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=679467657:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2887 on theBenchmark for (2887ds/2037Mi) % 103.49/15.34 % (3205418)Instruction limit reached! % 103.49/15.34 % (3205418)------------------------------ % 103.49/15.34 % (3205418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.49/15.34 % (3205418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.49/15.34 % (3205418)CaDiCaL version: 2.1.3 % 103.49/15.34 % (3205418)Termination reason: Instruction limit % 103.49/15.34 % (3205418)Termination phase: Saturation % 103.49/15.34 % (3205418)Time elapsed: 0.703 s % 103.49/15.34 % (3205418)Peak memory usage: 139 MB % 103.49/15.34 % (3205418)Instructions burned: 2038 (million) % 103.49/15.34 % (3205420)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=879585578:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2879 on theBenchmark for (2879ds/2110Mi) % 103.49/15.34 [W928 07:08:02.076038480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076059139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076080712 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076087152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076100469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076106101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076119664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076125795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076138985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076178642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076207095 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 [W928 07:08:02.076224384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 93.97/15.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 93.97/15.42 % (3205420)Refutation not found, incomplete strategy % 93.97/15.42 % (3205420)------------------------------ % 93.97/15.42 % (3205420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 93.97/15.42 % (3205420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 93.97/15.42 % (3205420)CaDiCaL version: 2.1.3 % 93.97/15.42 % (3205420)Termination reason: Refutation not found, incomplete strategy % 93.97/15.42 % (3205420)Time elapsed: 0.308 s % 93.97/15.42 % (3205420)Peak memory usage: 125 MB % 111.61/16.57 % (3205420)Instructions burned: 826 (million) % 111.61/16.57 % (3205416)Instruction limit reached! % 111.61/16.57 % (3205416)------------------------------ % 111.61/16.57 % (3205416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.61/16.57 % (3205416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.61/16.57 % (3205416)CaDiCaL version: 2.1.3 % 111.61/16.57 % (3205416)Termination reason: Instruction limit % 111.61/16.57 % (3205416)Termination phase: Saturation % 111.61/16.57 % (3205416)Time elapsed: 1.455 s % 111.61/16.57 % (3205416)Peak memory usage: 111 MB % 111.61/16.57 % (3205416)Instructions burned: 5475 (million) % 111.61/16.57 % (3205420)------------------------------ % 111.61/16.57 % (3205420)------------------------------ % 111.61/16.57 % (3205422)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=593740208:i=2430:add=off:aac=none:nm=16_2874 on theBenchmark for (2874ds/2430Mi) % 111.61/16.57 % (3205423)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=3712428904:cond=fast:i=4891_2873 on theBenchmark for (2873ds/4891Mi) % 111.61/16.57 % (3205422)Instruction limit reached! % 111.61/16.57 % (3205422)------------------------------ % 111.61/16.57 % (3205422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.61/16.57 % (3205422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.61/16.57 % (3205422)CaDiCaL version: 2.1.3 % 111.61/16.57 % (3205422)Termination reason: Instruction limit % 111.61/16.57 % (3205422)Termination phase: Saturation % 111.61/16.57 % (3205422)Time elapsed: 0.871 s % 111.61/16.57 % (3205422)Peak memory usage: 138 MB % 111.61/16.57 % (3205422)Instructions burned: 2430 (million) % 111.61/16.57 % (3205426)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=1344705930:st=2:i=14845:sd=2:ss=included:fsd=on_2864 on theBenchmark for (2864ds/14845Mi) % 111.61/16.57 % (3205426)Refutation not found, incomplete strategy % 111.61/16.57 % (3205426)------------------------------ % 111.61/16.57 % (3205426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.61/16.57 % (3205426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.61/16.57 % (3205426)CaDiCaL version: 2.1.3 % 111.61/16.57 % (3205426)Termination reason: Refutation not found, incomplete strategy % 111.61/16.57 % (3205426)Time elapsed: 0.315 s % 111.61/16.57 % (3205426)Peak memory usage: 128 MB % 111.61/16.57 % (3205426)Instructions burned: 848 (million) % 111.61/16.57 % (3205426)------------------------------ % 111.61/16.57 % (3205426)------------------------------ % 111.61/16.57 % (3205428)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=1586524145:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2858 on theBenchmark for (2858ds/7534Mi) % 111.61/16.57 % (3205428)Refutation not found, incomplete strategy % 111.61/16.57 % (3205428)------------------------------ % 111.61/16.57 % (3205428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.61/16.57 % (3205428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.61/16.57 % (3205428)CaDiCaL version: 2.1.3 % 111.61/16.57 % (3205428)Termination reason: Refutation not found, incomplete strategy % 111.61/16.57 % (3205428)Time elapsed: 0.337 s % 111.61/16.57 % (3205428)Peak memory usage: 128 MB % 111.61/16.57 % (3205428)Instructions burned: 908 (million) % 111.61/16.57 % (3205423)Instruction limit reached! % 111.61/16.57 % (3205423)------------------------------ % 111.61/16.57 % (3205423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 111.61/16.57 % (3205423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 111.61/16.57 % (3205423)CaDiCaL version: 2.1.3 % 111.61/16.57 % (3205423)Termination reason: Instruction limit % 111.61/16.57 % (3205423)Termination phase: Saturation % 111.61/16.57 % (3205423)Time elapsed: 1.869 s % 111.61/16.57 % (3205423)Peak memory usage: 160 MB % 111.61/16.57 % (3205423)Instructions burned: 4892 (million) % 111.61/16.57 % (3205430)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=1522314182:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2854 on theBenchmark for (2854ds/10353Mi) % 111.61/16.57 % (3205428)------------------------------ % 111.61/16.57 % (3205428)------------------------------ % 111.61/16.57 % (3205432)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=86341467:i=7860_2852 on theBenchmark for (2852ds/7860Mi) % 113.12/16.82 % (3205432)Refutation not found, incomplete strategy % 113.12/16.82 % (3205432)------------------------------ % 113.12/16.82 % (3205432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.12/16.82 % (3205432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.12/16.82 % (3205432)CaDiCaL version: 2.1.3 % 113.12/16.82 % (3205432)Termination reason: Refutation not found, incomplete strategy % 113.12/16.82 % (3205432)Time elapsed: 0.003 s % 113.12/16.82 % (3205432)Peak memory usage: 88 MB % 113.12/16.82 % (3205432)Instructions burned: 8 (million) % 113.12/16.82 % (3205366)Instruction limit reached! % 113.12/16.82 % (3205366)------------------------------ % 113.12/16.82 % (3205366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 113.12/16.82 % (3205366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 113.12/16.82 % (3205366)CaDiCaL version: 2.1.3 % 113.12/16.82 % (3205366)Termination reason: Instruction limit % 113.12/16.82 % (3205366)Termination phase: Saturation % 113.12/16.82 % (3205366)Time elapsed: 9.835 s % 113.12/16.82 % (3205366)Peak memory usage: 365 MB % 113.12/16.82 % (3205366)Instructions burned: 33335 (million) % 113.12/16.82 [W928 07:08:05.623979674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.623999008 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624047011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624057327 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624072343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624079248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624093660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624100486 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624114159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 113.12/16.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 113.12/16.82 [W928 07:08:05.624120919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.43/17.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.43/17.14 [W928 07:08:05.624134891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.43/17.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.43/17.14 [W928 07:08:05.624140923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 116.43/17.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 116.43/17.14 % (3205432)------------------------------ % 116.43/17.14 % (3205432)------------------------------ % 116.43/17.14 % (3205434)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=3009578384:i=7896:sd=2:bs=on:ss=included:sgt=20_2851 on theBenchmark for (2851ds/7896Mi) % 116.43/17.14 % (3205430)Refutation not found, incomplete strategy % 116.43/17.14 % (3205430)------------------------------ % 116.43/17.14 % (3205430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.43/17.14 % (3205430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.43/17.14 % (3205430)CaDiCaL version: 2.1.3 % 116.43/17.14 % (3205430)Termination reason: Refutation not found, incomplete strategy % 116.43/17.14 % (3205430)Time elapsed: 0.312 s % 116.43/17.14 % (3205430)Peak memory usage: 125 MB % 116.43/17.14 % (3205430)Instructions burned: 823 (million) % 116.43/17.14 % (3205435)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=268381486:i=5812:gtgl=2:gtg=all_2850 on theBenchmark for (2850ds/5812Mi) % 116.43/17.14 % (3205430)------------------------------ % 116.43/17.14 % (3205430)------------------------------ % 116.43/17.14 % (3205438)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=3804744432:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2848 on theBenchmark for (2848ds/2965Mi) % 116.43/17.14 % (3205434)Refutation not found, incomplete strategy % 116.43/17.14 % (3205434)------------------------------ % 116.43/17.14 % (3205434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.43/17.14 % (3205434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.43/17.14 % (3205434)CaDiCaL version: 2.1.3 % 116.43/17.14 % (3205434)Termination reason: Refutation not found, incomplete strategy % 116.43/17.14 % (3205434)Time elapsed: 0.501 s % 116.43/17.14 % (3205434)Peak memory usage: 131 MB % 116.43/17.14 % (3205434)Instructions burned: 1334 (million) % 116.43/17.14 % (3205438)Refutation not found, incomplete strategy % 116.43/17.14 % (3205438)------------------------------ % 116.43/17.14 % (3205438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 116.43/17.14 % (3205438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 116.43/17.14 % (3205438)CaDiCaL version: 2.1.3 % 116.43/17.14 % (3205438)Termination reason: Refutation not found, incomplete strategy % 116.43/17.14 % (3205438)Time elapsed: 0.320 s % 116.43/17.14 % (3205438)Peak memory usage: 129 MB % 116.43/17.14 % (3205438)Instructions burned: 858 (million) % 116.43/17.14 % (3205434)------------------------------ % 116.43/17.14 % (3205434)------------------------------ % 116.43/17.14 % (3205438)------------------------------ % 116.43/17.14 % (3205438)------------------------------ % 116.43/17.14 % (3205440)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3589572831:i=2967:kws=precedence:bd=preordered:av=off_2843 on theBenchmark for (2843ds/2967Mi) % 116.43/17.14 % (3205442)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=3412242664:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2842 on theBenchmark for (2842ds/3022Mi) % 116.43/17.14 [W928 07:08:06.779666139 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779722909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779744382 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779750681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779763637 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779769150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779782507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779787978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779800737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779806308 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779819384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 [W928 07:08:06.779860741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 118.42/17.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 118.42/17.55 % (3205442)Refutation not found, incomplete strategy % 118.42/17.55 % (3205442)------------------------------ % 118.42/17.55 % (3205442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 118.42/17.55 % (3205442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 118.42/17.55 % (3205442)CaDiCaL version: 2.1.3 % 118.42/17.55 % (3205442)Termination reason: Refutation not found, incomplete strategy % 118.42/17.55 % (3205442)Time elapsed: 0.306 s % 118.42/17.55 % (3205442)Peak memory usage: 125 MB % 118.42/17.55 % (3205442)Instructions burned: 827 (million) % 118.42/17.55 % (3205442)------------------------------ % 110.25/17.75 % (3205442)------------------------------ % 110.25/17.75 % (3205444)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=3633929847:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2836 on theBenchmark for (2836ds/3207Mi) % 110.25/17.75 % (3205394)Instruction limit reached! % 110.25/17.75 % (3205394)------------------------------ % 110.25/17.75 % (3205394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 110.25/17.75 % (3205394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 110.25/17.75 % (3205394)CaDiCaL version: 2.1.3 % 110.25/17.75 % (3205394)Termination reason: Instruction limit % 110.25/17.75 % (3205394)Termination phase: Saturation % 110.25/17.75 % (3205394)Time elapsed: 8.512 s % 110.25/17.75 % (3205394)Peak memory usage: 1246 MB % 110.25/17.75 % (3205394)Instructions burned: 26474 (million) % 110.25/17.75 % (3205446)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=2470558881:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2834 on theBenchmark for (2834ds/3289Mi) % 110.25/17.75 [W928 07:08:06.350463926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350481169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350503533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350510826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350525852 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350532643 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350547969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350554239 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350568036 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 110.25/17.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 110.25/17.75 [W928 07:08:06.350574387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 [W928 07:08:06.350588316 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 [W928 07:08:06.350602687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 % (3205440)Instruction limit reached! % 123.51/18.13 % (3205440)------------------------------ % 123.51/18.13 % (3205440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.51/18.13 % (3205440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.51/18.13 % (3205440)CaDiCaL version: 2.1.3 % 123.51/18.13 % (3205440)Termination reason: Instruction limit % 123.51/18.13 % (3205440)Termination phase: Saturation % 123.51/18.13 % (3205440)Time elapsed: 0.974 s % 123.51/18.13 % (3205440)Peak memory usage: 144 MB % 123.51/18.13 % (3205440)Instructions burned: 2967 (million) % 123.51/18.13 % (3205444)Refutation not found, incomplete strategy % 123.51/18.13 % (3205444)------------------------------ % 123.51/18.13 % (3205444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.51/18.13 % (3205444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.51/18.13 % (3205444)CaDiCaL version: 2.1.3 % 123.51/18.13 % (3205444)Termination reason: Refutation not found, incomplete strategy % 123.51/18.13 % (3205444)Time elapsed: 0.311 s % 123.51/18.13 % (3205444)Peak memory usage: 125 MB % 123.51/18.13 % (3205444)Instructions burned: 827 (million) % 123.51/18.13 % (3205448)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3008500994:i=38569:sd=3:ss=axioms:sgt=32_2832 on theBenchmark for (2832ds/38569Mi) % 123.51/18.13 % (3205444)------------------------------ % 123.51/18.13 % (3205444)------------------------------ % 123.51/18.13 % (3205446)Refutation not found, incomplete strategy % 123.51/18.13 % (3205446)------------------------------ % 123.51/18.13 % (3205446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 123.51/18.13 % (3205446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 123.51/18.13 % (3205446)CaDiCaL version: 2.1.3 % 123.51/18.13 % (3205446)Termination reason: Refutation not found, incomplete strategy % 123.51/18.13 % (3205446)Time elapsed: 0.321 s % 123.51/18.13 % (3205446)Peak memory usage: 129 MB % 123.51/18.13 % (3205446)Instructions burned: 856 (million) % 123.51/18.13 % (3205450)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=131752318:cts=off:i=3394_2831 on theBenchmark for (2831ds/3394Mi) % 123.51/18.13 [W928 07:08:07.756881261 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 [W928 07:08:07.756908736 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 [W928 07:08:07.756931694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 [W928 07:08:07.756937652 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 123.51/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.51/18.13 [W928 07:08:07.756951102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.756956619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.756970069 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.756975956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.756988985 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.756994559 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.757014596 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 [W928 07:08:07.757020628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 139.57/20.49 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.57/20.49 % (3205446)------------------------------ % 139.57/20.49 % (3205446)------------------------------ % 139.57/20.49 % (3205448)Refutation not found, incomplete strategy % 139.57/20.49 % (3205448)------------------------------ % 139.57/20.49 % (3205448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.57/20.49 % (3205448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.57/20.49 % (3205448)CaDiCaL version: 2.1.3 % 139.57/20.49 % (3205448)Termination reason: Refutation not found, incomplete strategy % 139.57/20.49 % (3205448)Time elapsed: 0.321 s % 139.57/20.49 % (3205448)Peak memory usage: 125 MB % 139.57/20.49 % (3205448)Instructions burned: 823 (million) % 139.57/20.49 % (3205392)Instruction limit reached! % 139.57/20.49 % (3205392)------------------------------ % 139.57/20.49 % (3205392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.57/20.49 % (3205392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.57/20.49 % (3205392)CaDiCaL version: 2.1.3 % 139.57/20.49 % (3205392)Termination reason: Instruction limit % 139.57/20.49 % (3205392)Termination phase: Saturation % 139.57/20.49 % (3205392)Time elapsed: 9.397 s % 139.57/20.49 % (3205392)Peak memory usage: 398 MB % 139.57/20.49 % (3205392)Instructions burned: 30753 (million) % 139.57/20.49 % (3205452)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=2311834789:i=33824:bd=preordered_2828 on theBenchmark for (2828ds/33824Mi) % 139.57/20.49 % (3205435)Instruction limit reached! % 139.57/20.49 % (3205435)------------------------------ % 139.57/20.49 % (3205435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.57/20.49 % (3205435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.57/20.49 % (3205435)CaDiCaL version: 2.1.3 % 139.57/20.49 % (3205435)Termination reason: Instruction limit % 139.57/20.49 % (3205435)Termination phase: Saturation % 165.08/24.02 % (3205435)Time elapsed: 2.150 s % 165.08/24.02 % (3205435)Peak memory usage: 174 MB % 165.08/24.02 % (3205435)Instructions burned: 5814 (million) % 165.08/24.02 % (3205453)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=971370090:i=20684:bd=all:gtg=exists_sym_2828 on theBenchmark for (2828ds/20684Mi) % 165.08/24.02 % (3205448)------------------------------ % 165.08/24.02 % (3205448)------------------------------ % 165.08/24.02 % (3205455)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=2444996266:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2827 on theBenchmark for (2827ds/7222Mi) % 165.08/24.02 % (3205457)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3301365641:st=4:i=7295:sd=4:ep=R:ss=axioms_2826 on theBenchmark for (2826ds/7295Mi) % 165.08/24.02 [W928 07:08:07.334300439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334323315 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334344688 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334352732 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334367467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334374381 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334388264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334394608 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334408373 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 165.08/24.02 [W928 07:08:07.334414797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 165.08/24.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.80/24.96 [W928 07:08:07.334428450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.80/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.80/24.96 [W928 07:08:07.334442195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 163.80/24.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 163.80/24.96 % (3205457)Refutation not found, incomplete strategy % 163.80/24.96 % (3205457)------------------------------ % 163.80/24.96 % (3205457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.80/24.96 % (3205457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.80/24.96 % (3205457)CaDiCaL version: 2.1.3 % 163.80/24.96 % (3205457)Termination reason: Refutation not found, incomplete strategy % 163.80/24.96 % (3205457)Time elapsed: 0.303 s % 163.80/24.96 % (3205457)Peak memory usage: 125 MB % 163.80/24.96 % (3205457)Instructions burned: 823 (million) % 163.80/24.96 % (3205457)------------------------------ % 163.80/24.96 % (3205457)------------------------------ % 163.80/24.96 % (3205460)lrs+32_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:fde=none:sp=occurrence:urr=ec_only:fd=preordered:random_seed=2403944552:i=4036:ins=10_2821 on theBenchmark for (2821ds/4036Mi) % 163.80/24.96 % (3205450)Instruction limit reached! % 163.80/24.96 % (3205450)------------------------------ % 163.80/24.96 % (3205450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.80/24.96 % (3205450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.80/24.96 % (3205450)CaDiCaL version: 2.1.3 % 163.80/24.96 % (3205450)Termination reason: Instruction limit % 163.80/24.96 % (3205450)Termination phase: Saturation % 163.80/24.96 % (3205450)Time elapsed: 1.121 s % 163.80/24.96 % (3205450)Peak memory usage: 141 MB % 163.80/24.96 % (3205450)Instructions burned: 3396 (million) % 163.80/24.96 % (3205462)lrs+10_1_sil=128000:lcm=predicate:random_seed=1218242072:st=3:i=43697:sd=5:ss=axioms_2819 on theBenchmark for (2819ds/43697Mi) % 163.80/24.96 % (3205462)Refutation not found, incomplete strategy % 163.80/24.96 % (3205462)------------------------------ % 163.80/24.96 % (3205462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.80/24.96 % (3205462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.80/24.96 % (3205462)CaDiCaL version: 2.1.3 % 163.80/24.96 % (3205462)Termination reason: Refutation not found, incomplete strategy % 163.80/24.96 % (3205462)Time elapsed: 0.0000 s % 163.80/24.96 % (3205462)Peak memory usage: 86 MB % 163.80/24.96 % (3205462)------------------------------ % 163.80/24.96 % (3205462)------------------------------ % 163.80/24.96 % (3205464)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:sp=const_frequency:sos=all:lcm=predicate:urr=on:s2agt=20:sac=on:random_seed=668005454:i=17599:gtg=all:ss=axioms:fsd=on_2816 on theBenchmark for (2816ds/17599Mi) % 163.80/24.96 % (3205460)Instruction limit reached! % 163.80/24.96 % (3205460)------------------------------ % 163.80/24.96 % (3205460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.80/24.96 % (3205460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.80/24.96 % (3205460)CaDiCaL version: 2.1.3 % 163.80/24.96 % (3205460)Termination reason: Instruction limit % 163.80/24.96 % (3205460)Termination phase: Saturation % 163.80/24.96 % (3205460)Time elapsed: 1.298 s % 163.80/24.96 % (3205460)Peak memory usage: 156 MB % 163.80/24.96 % (3205460)Instructions burned: 4037 (million) % 163.80/24.96 % (3205466)lrs+1011_1_to=lpo:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=occurrence:lcm=reverse:urr=ec_only:gs=on:random_seed=3459726370:i=4547:bd=preordered_2807 on theBenchmark for (2807ds/4547Mi) % 163.80/24.96 % (3205455)Instruction limit reached! % 163.80/24.96 % (3205455)------------------------------ % 163.80/24.96 % (3205455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 163.80/24.96 % (3205455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 163.80/24.96 % (3205455)CaDiCaL version: 2.1.3 % 163.80/24.96 % (3205455)Termination reason: Instruction limit % 163.80/24.96 % (3205455)Termination phase: Saturation % 163.80/24.96 % (3205455)Time elapsed: 2.642 s % 163.80/24.96 % (3205455)Peak memory usage: 183 MB % 172.81/25.17 % (3205455)Instructions burned: 7224 (million) % 172.81/25.17 % (3205468)lrs+1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:urr=ec_only:newcnf=on:random_seed=279097436:i=9294:av=off_2800 on theBenchmark for (2800ds/9294Mi) % 172.81/25.17 % (3205466)Instruction limit reached! % 172.81/25.17 % (3205466)------------------------------ % 172.81/25.17 % (3205466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 172.81/25.17 % (3205466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.81/25.17 % (3205466)CaDiCaL version: 2.1.3 % 172.81/25.17 % (3205466)Termination reason: Instruction limit % 172.81/25.17 % (3205466)Termination phase: Saturation % 172.81/25.17 % (3205466)Time elapsed: 1.633 s % 172.81/25.17 % (3205466)Peak memory usage: 161 MB % 172.81/25.17 % (3205466)Instructions burned: 4548 (million) % 172.81/25.17 % (3205471)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=4190091144:i=32849:add=on_2790 on theBenchmark for (2790ds/32849Mi) % 172.81/25.17 % (3205468)Instruction limit reached! % 172.81/25.17 % (3205468)------------------------------ % 172.81/25.17 % (3205468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 172.81/25.17 % (3205468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 172.81/25.17 % (3205468)CaDiCaL version: 2.1.3 % 172.81/25.17 % (3205468)Termination reason: Instruction limit % 172.81/25.17 % (3205468)Termination phase: Saturation % 172.81/25.17 % (3205468)Time elapsed: 3.097 s % 172.81/25.17 % (3205468)Peak memory usage: 169 MB % 172.81/25.17 % (3205468)Instructions burned: 9295 (million) % 172.81/25.17 % (3205473)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=899197230:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2768 on theBenchmark for (2768ds/4793Mi) % 172.81/25.17 [W928 07:08:13.220470637 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220500501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220522840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220529043 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220543177 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220548676 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220562182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 172.81/25.17 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 172.81/25.17 [W928 07:08:13.220567922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.31/29.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.31/29.02 [W928 07:08:13.220581113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.31/29.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.31/29.02 [W928 07:08:13.220586835 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.31/29.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.31/29.02 [W928 07:08:13.220599885 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.31/29.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.31/29.02 [W928 07:08:13.220605442 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 200.31/29.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 200.31/29.02 % (3205473)Refutation not found, incomplete strategy % 200.31/29.02 % (3205473)------------------------------ % 200.31/29.02 % (3205473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.31/29.02 % (3205473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.31/29.02 % (3205473)CaDiCaL version: 2.1.3 % 200.31/29.02 % (3205473)Termination reason: Refutation not found, incomplete strategy % 200.31/29.02 % (3205473)Time elapsed: 0.306 s % 200.31/29.02 % (3205473)Peak memory usage: 125 MB % 200.31/29.02 % (3205473)Instructions burned: 823 (million) % 200.31/29.02 % (3205473)------------------------------ % 200.31/29.02 % (3205473)------------------------------ % 200.31/29.02 % (3205475)dis+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:prc=on:drc=off:sims=off:sp=const_frequency:sos=on:spb=non_intro:gs=on:updr=off:newcnf=on:random_seed=423144436:i=4840:nm=4:av=off_2762 on theBenchmark for (2762ds/4840Mi) % 200.31/29.02 % (3205464)Instruction limit reached! % 200.31/29.02 % (3205464)------------------------------ % 200.31/29.02 % (3205464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.31/29.02 % (3205464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.31/29.02 % (3205464)CaDiCaL version: 2.1.3 % 200.31/29.02 % (3205464)Termination reason: Instruction limit % 200.31/29.02 % (3205464)Termination phase: Saturation % 200.31/29.02 % (3205464)Time elapsed: 5.622 s % 200.31/29.02 % (3205464)Peak memory usage: 217 MB % 200.31/29.02 % (3205464)Instructions burned: 17599 (million) % 200.31/29.02 % (3205475)Refutation not found, incomplete strategy % 200.31/29.02 % (3205475)------------------------------ % 200.31/29.02 % (3205475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.31/29.02 % (3205475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.31/29.02 % (3205475)CaDiCaL version: 2.1.3 % 200.31/29.02 % (3205475)Termination reason: Refutation not found, incomplete strategy % 200.31/29.02 % (3205475)Time elapsed: 0.323 s % 200.31/29.02 % (3205475)Peak memory usage: 129 MB % 200.31/29.02 % (3205475)Instructions burned: 857 (million) % 200.31/29.02 % (3205477)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2431588978:cts=off:i=5002_2759 on theBenchmark for (2759ds/5002Mi) % 200.31/29.02 % (3205475)------------------------------ % 200.31/29.02 % (3205475)------------------------------ % 200.31/29.02 % (3205453)Instruction limit reached! % 200.31/29.02 % (3205453)------------------------------ % 200.31/29.02 % (3205453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 200.31/29.02 % (3205453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 200.31/29.02 % (3205453)CaDiCaL version: 2.1.3 % 200.31/29.02 % (3205453)Termination reason: Instruction limit % 200.31/29.02 % (3205453)Termination phase: Saturation % 200.31/29.02 % (3205453)Time elapsed: 7.072 s % 200.31/29.02 % (3205453)Peak memory usage: 285 MB % 200.31/29.02 % (3205453)Instructions burned: 20687 (million) % 200.31/29.02 % (3205479)dis+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3437525317:i=30479:sd=3:ss=axioms_2756 on theBenchmark for (2756ds/30479Mi) % 238.87/34.52 % (3205480)lrs+1011_1_anc=none:ncem=casc2026/models/loop2.pt:sil=32000:tgt=full:npcc=on:fde=unused:sas=cadical:sp=const_frequency:spb=non_intro:lsd=10:lcm=predicate:rp=on:sac=on:newcnf=on:random_seed=2114947488:i=11035:s2at=5:kws=inv_arity:bs=on:gsp=on_2756 on theBenchmark for (2756ds/11035Mi) % 238.87/34.52 [W928 07:08:14.375800949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375830004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375870917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375877589 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375891039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375898119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375913896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375920709 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375934777 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375941439 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375955799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 238.87/34.52 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 238.87/34.52 [W928 07:08:14.375962353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 236.24/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 236.24/34.96 % (3205479)Refutation not found, incomplete strategy % 236.24/34.96 % (3205479)------------------------------ % 236.24/34.96 % (3205479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.24/34.96 % (3205479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.24/34.96 % (3205479)CaDiCaL version: 2.1.3 % 236.24/34.96 % (3205479)Termination reason: Refutation not found, incomplete strategy % 236.24/34.96 % (3205479)Time elapsed: 0.308 s % 236.24/34.96 % (3205479)Peak memory usage: 125 MB % 236.24/34.96 % (3205479)Instructions burned: 823 (million) % 236.24/34.96 % (3205479)------------------------------ % 236.24/34.96 % (3205479)------------------------------ % 236.24/34.96 % (3205483)lrs+1010_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:random_seed=1415360073:i=5835_2750 on theBenchmark for (2750ds/5835Mi) % 236.24/34.96 % (3205477)Instruction limit reached! % 236.24/34.96 % (3205477)------------------------------ % 236.24/34.96 % (3205477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.24/34.96 % (3205477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.24/34.96 % (3205477)CaDiCaL version: 2.1.3 % 236.24/34.96 % (3205477)Termination reason: Instruction limit % 236.24/34.96 % (3205477)Termination phase: Saturation % 236.24/34.96 % (3205477)Time elapsed: 1.869 s % 236.24/34.96 % (3205477)Peak memory usage: 166 MB % 236.24/34.96 % (3205477)Instructions burned: 5004 (million) % 236.24/34.96 % (3205485)ott+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:urr=on:bsr=on:fd=preordered:foolp=on:random_seed=3205047861:i=5890:s2at=2:kws=inv_precedence:ins=4:av=off_2739 on theBenchmark for (2739ds/5890Mi) % 236.24/34.96 % (3205483)Instruction limit reached! % 236.24/34.96 % (3205483)------------------------------ % 236.24/34.96 % (3205483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.24/34.96 % (3205483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.24/34.96 % (3205483)CaDiCaL version: 2.1.3 % 236.24/34.96 % (3205483)Termination reason: Instruction limit % 236.24/34.96 % (3205483)Termination phase: Saturation % 236.24/34.96 % (3205483)Time elapsed: 2.039 s % 236.24/34.96 % (3205483)Peak memory usage: 174 MB % 236.24/34.96 % (3205483)Instructions burned: 5837 (million) % 236.24/34.96 % (3205487)lrs+10_1_sil=32000:sos=all:lma=off:random_seed=659015424:cts=off:i=19910:ep=RS_2729 on theBenchmark for (2729ds/19910Mi) % 236.24/34.96 % (3205487)Refutation not found, incomplete strategy % 236.24/34.96 % (3205487)------------------------------ % 236.24/34.96 % (3205487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.24/34.96 % (3205487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.24/34.96 % (3205487)CaDiCaL version: 2.1.3 % 236.24/34.96 % (3205487)Termination reason: Refutation not found, incomplete strategy % 236.24/34.96 % (3205487)Time elapsed: 0.002 s % 236.24/34.96 % (3205487)Peak memory usage: 88 MB % 236.24/34.96 % (3205487)Instructions burned: 6 (million) % 236.24/34.96 % (3205487)------------------------------ % 236.24/34.96 % (3205487)------------------------------ % 236.24/34.96 % (3205489)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=arity:fd=preordered:s2agt=16:sac=on:random_seed=3005669853:i=20312:bd=preordered:fsr=off:er=filter_2726 on theBenchmark for (2726ds/20312Mi) % 236.24/34.96 % (3205485)Instruction limit reached! % 236.24/34.96 % (3205485)------------------------------ % 236.24/34.96 % (3205485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.24/34.96 % (3205485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.24/34.96 % (3205485)CaDiCaL version: 2.1.3 % 236.24/34.96 % (3205485)Termination reason: Instruction limit % 236.24/34.96 % (3205485)Termination phase: Saturation % 236.24/34.96 % (3205485)Time elapsed: 1.608 s % 236.24/34.96 % (3205485)Peak memory usage: 152 MB % 236.24/34.96 % (3205485)Instructions burned: 5895 (million) % 236.24/34.96 % (3205491)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal_then_units:urr=on:gs=on:sac=on:random_seed=3657894339:i=13822:kws=inv_arity_squared:bd=preordered:ins=5_2721 on theBenchmark for (2721ds/13822Mi) % 236.24/34.96 % (3205480)Instruction limit reached! % 236.24/34.96 % (3205480)------------------------------ % 236.24/34.96 % (3205480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.24/34.96 % (3205480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.84/36.96 % (3205480)CaDiCaL version: 2.1.3 % 255.84/36.96 % (3205480)Termination reason: Instruction limit % 255.84/36.96 % (3205480)Termination phase: Saturation % 255.84/36.96 % (3205480)Time elapsed: 4.016 s % 255.84/36.96 % (3205480)Peak memory usage: 175 MB % 255.84/36.96 % (3205480)Instructions burned: 11036 (million) % 255.84/36.96 % (3205493)ott-1011_91_sil=128000:prc=on:sims=off:sp=unary_first:urr=on:random_seed=627078072:st=2:i=7144:kws=inv_arity_squared:bd=all:ins=1:ss=included:sgt=10_2714 on theBenchmark for (2714ds/7144Mi) % 255.84/36.96 % (3205452)Instruction limit reached! % 255.84/36.96 % (3205452)------------------------------ % 255.84/36.96 % (3205452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.84/36.96 % (3205452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.84/36.96 % (3205452)CaDiCaL version: 2.1.3 % 255.84/36.96 % (3205452)Termination reason: Instruction limit % 255.84/36.96 % (3205452)Termination phase: Saturation % 255.84/36.96 % (3205452)Time elapsed: 12.337 s % 255.84/36.96 % (3205452)Peak memory usage: 294 MB % 255.84/36.96 % (3205452)Instructions burned: 33827 (million) % 255.84/36.96 % (3205495)lrs+21_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3790584659:i=15184:kws=inv_frequency:bd=preordered:av=off:er=known_2704 on theBenchmark for (2704ds/15184Mi) % 255.84/36.96 % (3205493)Instruction limit reached! % 255.84/36.96 % (3205493)------------------------------ % 255.84/36.96 % (3205493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.84/36.96 % (3205493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.84/36.96 % (3205493)CaDiCaL version: 2.1.3 % 255.84/36.96 % (3205493)Termination reason: Instruction limit % 255.84/36.96 % (3205493)Termination phase: Saturation % 255.84/36.96 % (3205493)Time elapsed: 1.872 s % 255.84/36.96 % (3205493)Peak memory usage: 195 MB % 255.84/36.96 % (3205493)Instructions burned: 7147 (million) % 255.84/36.96 % (3205497)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=2525857375:i=107375_2695 on theBenchmark for (2695ds/107375Mi) % 255.84/36.96 % (3205471)Instruction limit reached! % 255.84/36.96 % (3205471)------------------------------ % 255.84/36.96 % (3205471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.84/36.96 % (3205471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.84/36.96 % (3205471)CaDiCaL version: 2.1.3 % 255.84/36.96 % (3205471)Termination reason: Instruction limit % 255.84/36.96 % (3205471)Termination phase: Saturation % 255.84/36.96 % (3205471)Time elapsed: 10.274 s % 255.84/36.96 % (3205471)Peak memory usage: 309 MB % 255.84/36.96 % (3205471)Instructions burned: 32851 (million) % 255.84/36.96 % (3205499)dis+11_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=full:npcc=on:sp=const_frequency:spb=units:lcm=predicate:fd=off:sac=on:newcnf=on:random_seed=3111717528:cts=off:i=7958:kws=inv_frequency:fgj=on:bs=unit_only:ins=1:fsr=off_2686 on theBenchmark for (2686ds/7958Mi) % 255.84/36.96 % (3205491)Instruction limit reached! % 255.84/36.96 % (3205491)------------------------------ % 255.84/36.96 % (3205491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.84/36.96 % (3205491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.84/36.96 % (3205491)CaDiCaL version: 2.1.3 % 255.84/36.96 % (3205491)Termination reason: Instruction limit % 255.84/36.96 % (3205491)Termination phase: Saturation % 255.84/36.96 % (3205491)Time elapsed: 3.730 s % 255.84/36.96 % (3205491)Peak memory usage: 211 MB % 255.84/36.96 % (3205491)Instructions burned: 13824 (million) % 255.84/36.96 % (3205501)dis+10_128_sil=16000:nwc=0.7:random_seed=1418549554:i=15999:nm=2:gsp=on_2683 on theBenchmark for (2683ds/15999Mi) % 255.84/36.96 % (3205412)Instruction limit reached! % 255.84/36.96 % (3205412)------------------------------ % 255.84/36.96 % (3205412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 255.84/36.96 % (3205412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 255.84/36.96 % (3205412)CaDiCaL version: 2.1.3 % 255.84/36.96 % (3205412)Termination reason: Instruction limit % 255.84/36.96 % (3205412)Termination phase: Saturation % 255.84/36.96 % (3205412)Time elapsed: 23.350 s % 255.84/36.96 % (3205412)Peak memory usage: 339 MB % 255.84/36.96 % (3205412)Instructions burned: 66097 (million) % 255.84/36.96 % (3205503)ott+10_64_sil=128000:plsq=on:drc=off:plsqc=2:nwc=1:random_seed=1043743518:st=3:i=8139:fgj=on:bd=all:av=off:fsr=off:ss=included:sgt=8_2661 on theBenchmark for (2661ds/8139Mi) % 272.04/39.23 % (3205499)Instruction limit reached! % 272.04/39.23 % (3205499)------------------------------ % 272.04/39.23 % (3205499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.04/39.23 % (3205499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.04/39.23 % (3205499)CaDiCaL version: 2.1.3 % 272.04/39.23 % (3205499)Termination reason: Instruction limit % 272.04/39.23 % (3205499)Termination phase: Saturation % 272.04/39.23 % (3205499)Time elapsed: 2.638 s % 272.04/39.23 % (3205499)Peak memory usage: 198 MB % 272.04/39.23 % (3205499)Instructions burned: 7959 (million) % 272.04/39.23 % (3205505)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=occurrence:sos=on:urr=on:sac=on:random_seed=1396062810:st=4:i=8950:sd=5:ss=axioms_2658 on theBenchmark for (2658ds/8950Mi) % 272.04/39.23 % (3205495)Instruction limit reached! % 272.04/39.23 % (3205495)------------------------------ % 272.04/39.23 % (3205495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 272.04/39.23 % (3205495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 272.04/39.23 % (3205495)CaDiCaL version: 2.1.3 % 272.04/39.23 % (3205495)Termination reason: Instruction limit % 272.04/39.23 % (3205495)Termination phase: Saturation % 272.04/39.23 % (3205495)Time elapsed: 4.699 s % 272.04/39.23 % (3205495)Peak memory usage: 205 MB % 272.04/39.23 % (3205495)Instructions burned: 15187 (million) % 272.04/39.23 [W928 07:08:24.161620168 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161642572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161664248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161671922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161686742 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161693128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161707404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161713614 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 272.04/39.23 [W928 07:08:24.161727342 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 272.04/39.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.41/41.85 [W928 07:08:24.161733584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.41/41.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.41/41.85 [W928 07:08:24.161746587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.41/41.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.41/41.85 [W928 07:08:24.161752095 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 290.41/41.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 290.41/41.85 % (3205507)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:drc=off:spb=goal:random_seed=3910660529:i=9809:ins=10:av=off_2656 on theBenchmark for (2656ds/9809Mi) % 290.41/41.85 % (3205505)Refutation not found, incomplete strategy % 290.41/41.85 % (3205505)------------------------------ % 290.41/41.85 % (3205505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.41/41.85 % (3205505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.41/41.85 % (3205505)CaDiCaL version: 2.1.3 % 290.41/41.85 % (3205505)Termination reason: Refutation not found, incomplete strategy % 290.41/41.85 % (3205505)Time elapsed: 0.307 s % 290.41/41.85 % (3205505)Peak memory usage: 125 MB % 290.41/41.85 % (3205505)Instructions burned: 826 (million) % 290.41/41.85 % (3205489)Instruction limit reached! % 290.41/41.85 % (3205489)------------------------------ % 290.41/41.85 % (3205489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.41/41.85 % (3205489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.41/41.85 % (3205489)CaDiCaL version: 2.1.3 % 290.41/41.85 % (3205489)Termination reason: Instruction limit % 290.41/41.85 % (3205489)Termination phase: Saturation % 290.41/41.85 % (3205489)Time elapsed: 7.166 s % 290.41/41.85 % (3205489)Peak memory usage: 278 MB % 290.41/41.85 % (3205489)Instructions burned: 20313 (million) % 290.41/41.85 % (3205505)------------------------------ % 290.41/41.85 % (3205505)------------------------------ % 290.41/41.85 % (3205509)ott+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=arity:acc=on:fd=off:newcnf=on:random_seed=2292603181:st=2.6:cond=fast:i=9885:s2at=1.5:sd=2:fgj=on:ins=3:ss=included_2653 on theBenchmark for (2653ds/9885Mi) % 290.41/41.85 % (3205510)ott+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:etr=on:kmz=on:flr=on:random_seed=1320137839:cond=fast:i=32078:fgj=on:av=off_2653 on theBenchmark for (2653ds/32078Mi) % 290.41/41.85 % (3205501)Instruction limit reached! % 290.41/41.85 % (3205501)------------------------------ % 290.41/41.85 % (3205501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.41/41.85 % (3205501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.41/41.85 % (3205501)CaDiCaL version: 2.1.3 % 290.41/41.85 % (3205501)Termination reason: Instruction limit % 290.41/41.85 % (3205501)Termination phase: Saturation % 290.41/41.85 % (3205501)Time elapsed: 4.574 s % 290.41/41.85 % (3205501)Peak memory usage: 224 MB % 290.41/41.85 % (3205501)Instructions burned: 16003 (million) % 290.41/41.85 % (3205503)Instruction limit reached! % 290.41/41.85 % (3205503)------------------------------ % 290.41/41.85 % (3205503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 290.41/41.85 % (3205503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 290.41/41.85 % (3205503)CaDiCaL version: 2.1.3 % 290.41/41.85 % (3205503)Termination reason: Instruction limit % 290.41/41.85 % (3205503)Termination phase: Saturation % 290.41/41.85 % (3205503)Time elapsed: 2.397 s % 290.41/41.85 % (3205503)Peak memory usage: 156 MB % 290.41/41.85 % (3205503)Instructions burned: 8141 (million) % 290.41/41.85 % (3205513)dis-1010_64_to=lpo:sil=16000:tgt=ground:prc=on:fde=none:spb=goal_then_units:nwc=1:random_seed=1881379404:i=11101:bd=all:ss=axioms:sgt=8_2636 on theBenchmark for (2636ds/11101Mi) % 290.41/41.85 % (3205513)Refutation not found, incomplete strategy % 290.41/41.85 % (3205513)------------------------------ % 290.41/41.85 % (3205513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +020Terminated % 300.27/43.24 % Vampire exiting % 300.27/43.24 Terminated %------------------------------------------------------------------------------