%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWB015+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 : n026.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:05 PM UTC 2026 % Result : Timeout 286.91s 41.36s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWB015+3 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.12/0.40 % Computer : n026.cluster.edu % 0.12/0.40 % Model : x86_64 x86_64 % 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.40 % Memory : 8046.5625MB % 0.12/0.40 % OS : Linux 6.8.0-71-generic % 0.12/0.40 % CPULimit : 300 % 0.12/0.40 % WCLimit : 300 % 0.12/0.40 % DateTime : Mon Sep 28 07:02:57 UTC 2026 % 0.12/0.40 % CPUTime : % 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.12/0.43 Running first-order theorem proving % 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.52/1.40 % (3663450)Detected formulas, will run a generic FOF schedule. % 3.52/1.40 % (3663461)dis-21_1_sil=8000:lcm=predicate:random_seed=3553742997:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi) % 3.52/1.40 % (3663458)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=631895110:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi) % 3.52/1.40 % (3663458)Refutation not found, incomplete strategy % 3.52/1.40 % (3663458)------------------------------ % 3.52/1.40 % (3663458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.40 % (3663458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.40 % (3663458)CaDiCaL version: 2.1.3 % 3.52/1.40 % (3663458)Termination reason: Refutation not found, incomplete strategy % 3.52/1.40 % (3663458)Time elapsed: 0.001 s % 3.52/1.40 % (3663458)Peak memory usage: 87 MB % 3.52/1.40 % (3663456)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=2222128261:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi) % 3.52/1.40 % (3663455)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=4164654857:i=141193_2999 on theBenchmark for (2999ds/141193Mi) % 3.52/1.40 % (3663457)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=2789811624:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi) % 3.52/1.40 % (3663459)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2289280477:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi) % 3.52/1.40 % (3663459)Refutation not found, incomplete strategy % 3.52/1.40 % (3663459)------------------------------ % 3.52/1.40 % (3663459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.40 % (3663459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.40 % (3663459)CaDiCaL version: 2.1.3 % 3.52/1.40 % (3663459)Termination reason: Refutation not found, incomplete strategy % 3.52/1.40 % (3663459)Time elapsed: 0.001 s % 3.52/1.40 % (3663459)Peak memory usage: 87 MB % 3.52/1.40 % (3663461)Instruction limit reached! % 3.52/1.40 % (3663461)------------------------------ % 3.52/1.40 % (3663461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.40 % (3663461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.40 % (3663461)CaDiCaL version: 2.1.3 % 3.52/1.40 % (3663461)Termination reason: Instruction limit % 3.52/1.40 % (3663461)Termination phase: Saturation % 3.52/1.40 % (3663461)Time elapsed: 0.042 s % 3.52/1.40 % (3663461)Peak memory usage: 89 MB % 3.52/1.40 % (3663461)Instructions burned: 131 (million) % 3.52/1.40 % (3663460)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2682933073:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi) % 3.52/1.40 % (3663468)lrs+10_1_sil=8000:sp=occurrence:random_seed=1280850596:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi) % 3.52/1.40 % (3663468)Refutation not found, incomplete strategy % 3.52/1.40 % (3663468)------------------------------ % 3.52/1.40 % (3663468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.40 % (3663468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.40 % (3663468)CaDiCaL version: 2.1.3 % 3.52/1.40 % (3663468)Termination reason: Refutation not found, incomplete strategy % 3.52/1.40 % (3663468)Time elapsed: 0.0000 s % 3.52/1.40 % (3663468)Peak memory usage: 87 MB % 3.52/1.40 % (3663460)Instruction limit reached! % 3.52/1.40 % (3663460)------------------------------ % 3.52/1.40 % (3663460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.52/1.40 % (3663460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.52/1.40 % (3663460)CaDiCaL version: 2.1.3 % 3.52/1.40 % (3663460)Termination reason: Instruction limit % 3.52/1.40 % (3663460)Termination phase: Saturation % 3.52/1.40 % (3663460)Time elapsed: 0.085 s % 3.52/1.40 % (3663460)Peak memory usage: 90 MB % 3.52/1.40 % (3663460)Instructions burned: 139 (million) % 3.52/1.40 % (3663458)------------------------------ % 3.52/1.40 % (3663458)------------------------------ % 3.52/1.40 % (3663471)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3346435331:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi) % 5.01/1.66 % (3663471)Refutation not found, incomplete strategy % 5.01/1.66 % (3663471)------------------------------ % 5.01/1.66 % (3663471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.66 % (3663471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.66 % (3663471)CaDiCaL version: 2.1.3 % 5.01/1.66 % (3663471)Termination reason: Refutation not found, incomplete strategy % 5.01/1.66 % (3663471)Time elapsed: 0.001 s % 5.01/1.66 % (3663471)Peak memory usage: 87 MB % 5.01/1.66 % (3663471)Instructions burned: 1 (million) % 5.01/1.66 % (3663459)------------------------------ % 5.01/1.66 % (3663459)------------------------------ % 5.01/1.66 % (3663468)------------------------------ % 5.01/1.66 % (3663468)------------------------------ % 5.01/1.66 % (3663473)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3072421524:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi) % 5.01/1.66 % (3663473)Refutation not found, incomplete strategy % 5.01/1.66 % (3663473)------------------------------ % 5.01/1.66 % (3663473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.01/1.66 % (3663473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.01/1.66 % (3663473)CaDiCaL version: 2.1.3 % 5.01/1.66 % (3663473)Termination reason: Refutation not found, incomplete strategy % 5.01/1.66 % (3663473)Time elapsed: 0.001 s % 5.01/1.66 % (3663473)Peak memory usage: 87 MB % 5.01/1.66 [W928 07:02:58.621477002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621508952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621523396 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621546682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621552086 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621558009 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621587336 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621589339 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 5.01/1.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 5.01/1.66 [W928 07:02:58.621598946 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621600649 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621624283 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621625436 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621634393 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621635433 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621657969 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621659843 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621667946 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621670179 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621691593 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621694173 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621701676 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 8.62/2.06 [W928 07:02:58.621704333 register_special_ops.cpp:225] Warning: Creating a tensor from 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.62/2.06 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.31/2.31 [W928 07:02:58.621731569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.31/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.31/2.31 [W928 07:02:58.621741696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 10.31/2.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 10.31/2.31 % (3663475)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=652101975:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi) % 10.31/2.31 % (3663474)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=1376519371:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi) % 10.31/2.31 % (3663475)Refutation not found, incomplete strategy % 10.31/2.31 % (3663475)------------------------------ % 10.31/2.31 % (3663475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.31 % (3663475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.31 % (3663475)CaDiCaL version: 2.1.3 % 10.31/2.31 % (3663475)Termination reason: Refutation not found, incomplete strategy % 10.31/2.31 % (3663475)Time elapsed: 0.001 s % 10.31/2.31 % (3663475)Peak memory usage: 87 MB % 10.31/2.31 % (3663475)Instructions burned: 1 (million) % 10.31/2.31 % (3663471)------------------------------ % 10.31/2.31 % (3663471)------------------------------ % 10.31/2.31 % (3663474)Instruction limit reached! % 10.31/2.31 % (3663474)------------------------------ % 10.31/2.31 % (3663474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.31 % (3663474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.31 % (3663474)CaDiCaL version: 2.1.3 % 10.31/2.31 % (3663474)Termination reason: Instruction limit % 10.31/2.31 % (3663474)Termination phase: Saturation % 10.31/2.31 % (3663474)Time elapsed: 0.122 s % 10.31/2.31 % (3663474)Peak memory usage: 92 MB % 10.31/2.31 % (3663474)Instructions burned: 248 (million) % 10.31/2.31 % (3663475)------------------------------ % 10.31/2.31 % (3663475)------------------------------ % 10.31/2.31 % (3663457)Refutation not found, incomplete strategy % 10.31/2.31 % (3663457)------------------------------ % 10.31/2.31 % (3663457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.31 % (3663457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.31 % (3663457)CaDiCaL version: 2.1.3 % 10.31/2.31 % (3663457)Termination reason: Refutation not found, incomplete strategy % 10.31/2.31 % (3663457)Time elapsed: 0.560 s % 10.31/2.31 % (3663457)Peak memory usage: 125 MB % 10.31/2.31 % (3663457)Instructions burned: 823 (million) % 10.31/2.31 % (3663456)Refutation not found, incomplete strategy % 10.31/2.31 % (3663456)------------------------------ % 10.31/2.31 % (3663456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.31 % (3663456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.31 % (3663456)CaDiCaL version: 2.1.3 % 10.31/2.31 % (3663456)Termination reason: Refutation not found, incomplete strategy % 10.31/2.31 % (3663456)Time elapsed: 0.560 s % 10.31/2.31 % (3663456)Peak memory usage: 124 MB % 10.31/2.31 % (3663456)Instructions burned: 823 (million) % 10.31/2.31 % (3663473)------------------------------ % 10.31/2.31 % (3663473)------------------------------ % 10.31/2.31 % (3663479)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1484168105:i=2350_2993 on theBenchmark for (2993ds/2350Mi) % 10.31/2.31 % (3663481)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3133456662:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi) % 10.31/2.31 % (3663480)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3942158223:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi) % 10.31/2.31 % (3663480)Refutation not found, incomplete strategy % 10.31/2.31 % (3663480)------------------------------ % 10.31/2.31 % (3663480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.31 % (3663480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.37 % (3663480)CaDiCaL version: 2.1.3 % 10.31/2.37 % (3663480)Termination reason: Refutation not found, incomplete strategy % 10.31/2.37 % (3663480)Time elapsed: 0.001 s % 10.31/2.37 % (3663480)Peak memory usage: 87 MB % 10.31/2.37 % (3663481)Instruction limit reached! % 10.31/2.37 % (3663481)------------------------------ % 10.31/2.37 % (3663481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.37 % (3663481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.37 % (3663481)CaDiCaL version: 2.1.3 % 10.31/2.37 % (3663481)Termination reason: Instruction limit % 10.31/2.37 % (3663481)Termination phase: Saturation % 10.31/2.37 % (3663481)Time elapsed: 0.034 s % 10.31/2.37 % (3663481)Peak memory usage: 89 MB % 10.31/2.37 % (3663481)Instructions burned: 130 (million) % 10.31/2.37 % (3663482)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=953092638:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi) % 10.31/2.37 % (3663486)lrs+10_1_sil=8000:sp=occurrence:random_seed=706704901:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi) % 10.31/2.37 % (3663486)Refutation not found, incomplete strategy % 10.31/2.37 % (3663486)------------------------------ % 10.31/2.37 % (3663486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.37 % (3663486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.37 % (3663486)CaDiCaL version: 2.1.3 % 10.31/2.37 % (3663486)Termination reason: Refutation not found, incomplete strategy % 10.31/2.37 % (3663486)Time elapsed: 0.0000 s % 10.31/2.37 % (3663486)Peak memory usage: 87 MB % 10.31/2.37 % (3663482)Instruction limit reached! % 10.31/2.37 % (3663482)------------------------------ % 10.31/2.37 % (3663482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.37 % (3663482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.37 % (3663482)CaDiCaL version: 2.1.3 % 10.31/2.37 % (3663482)Termination reason: Instruction limit % 10.31/2.37 % (3663482)Termination phase: Saturation % 10.31/2.37 % (3663482)Time elapsed: 0.061 s % 10.31/2.37 % (3663482)Peak memory usage: 89 MB % 10.31/2.37 % (3663482)Instructions burned: 115 (million) % 10.31/2.37 % (3663457)------------------------------ % 10.31/2.37 % (3663457)------------------------------ % 10.31/2.37 % (3663456)------------------------------ % 10.31/2.37 % (3663456)------------------------------ % 10.31/2.37 % (3663480)------------------------------ % 10.31/2.37 % (3663480)------------------------------ % 10.31/2.37 % (3663486)------------------------------ % 10.31/2.37 % (3663486)------------------------------ % 10.31/2.37 % (3663489)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=647134951:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi) % 10.31/2.37 % (3663489)Refutation not found, incomplete strategy % 10.31/2.37 % (3663489)------------------------------ % 10.31/2.37 % (3663489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.37 % (3663489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.37 % (3663489)CaDiCaL version: 2.1.3 % 10.31/2.37 % (3663489)Termination reason: Refutation not found, incomplete strategy % 10.31/2.37 % (3663489)Time elapsed: 0.001 s % 10.31/2.37 % (3663489)Peak memory usage: 87 MB % 10.31/2.37 % (3663491)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2165020840:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi) % 10.31/2.37 % (3663491)Refutation not found, incomplete strategy % 10.31/2.37 % (3663491)------------------------------ % 10.31/2.37 % (3663491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.31/2.37 % (3663491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.31/2.37 % (3663491)CaDiCaL version: 2.1.3 % 10.31/2.37 % (3663491)Termination reason: Refutation not found, incomplete strategy % 10.31/2.37 % (3663491)Time elapsed: 0.001 s % 10.31/2.37 % (3663491)Peak memory usage: 87 MB % 10.31/2.37 % (3663490)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1720872589:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi) % 10.31/2.37 % (3663494)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=751866958:st=3:i=13193:sd=3:ss=axioms_2989 on theBenchmark for (2989ds/13193Mi) % 10.31/2.37 % (3663492)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2644507024:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi) % 12.18/2.61 % (3663489)------------------------------ % 12.18/2.61 % (3663489)------------------------------ % 12.18/2.61 % (3663491)------------------------------ % 12.18/2.61 % (3663491)------------------------------ % 12.18/2.61 [W928 07:02:59.458788284 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458823470 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458844260 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458851247 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458864278 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458870164 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458883290 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458890184 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458902861 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458909593 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458922980 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 [W928 07:02:59.458929688 register_special_ops.cpp:225] Warning: Creating a tensor from 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.18/2.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 12.18/2.61 % (3663499)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=4240647976:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi) % 16.63/3.21 % (3663499)Refutation not found, incomplete strategy % 16.63/3.21 % (3663499)------------------------------ % 16.63/3.21 % (3663499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.63/3.21 % (3663499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.63/3.21 % (3663499)CaDiCaL version: 2.1.3 % 16.63/3.21 % (3663499)Termination reason: Refutation not found, incomplete strategy % 16.63/3.21 % (3663499)Time elapsed: 0.001 s % 16.63/3.21 % (3663499)Peak memory usage: 87 MB % 16.63/3.21 % (3663499)Instructions burned: 1 (million) % 16.63/3.21 % (3663500)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=552635786:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi) % 16.63/3.21 % (3663494)Refutation not found, incomplete strategy % 16.63/3.21 % (3663494)------------------------------ % 16.63/3.21 % (3663494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 16.63/3.21 % (3663494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 16.63/3.21 % (3663494)CaDiCaL version: 2.1.3 % 16.63/3.21 % (3663494)Termination reason: Refutation not found, incomplete strategy % 16.63/3.21 % (3663494)Time elapsed: 0.317 s % 16.63/3.21 % (3663494)Peak memory usage: 125 MB % 16.63/3.21 % (3663494)Instructions burned: 826 (million) % 16.63/3.21 [W928 07:02:59.598857030 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.598889756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.598927926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.598941150 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.598967576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.598979530 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.599015923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.599028570 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 16.63/3.21 [W928 07:02:59.599055236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 16.63/3.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.20/3.66 [W928 07:02:59.599067153 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.20/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.20/3.66 [W928 07:02:59.599092310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.20/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.20/3.66 [W928 07:02:59.599103283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 18.20/3.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 18.20/3.66 % (3663492)Instruction limit reached! % 18.20/3.66 % (3663492)------------------------------ % 18.20/3.66 % (3663492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.20/3.66 % (3663492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/3.66 % (3663492)CaDiCaL version: 2.1.3 % 18.20/3.66 % (3663492)Termination reason: Instruction limit % 18.20/3.66 % (3663492)Termination phase: Saturation % 18.20/3.66 % (3663492)Time elapsed: 0.355 s % 18.20/3.66 % (3663492)Peak memory usage: 91 MB % 18.20/3.66 % (3663492)Instructions burned: 592 (million) % 18.20/3.66 % (3663500)Instruction limit reached! % 18.20/3.66 % (3663500)------------------------------ % 18.20/3.66 % (3663500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.20/3.66 % (3663500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/3.66 % (3663500)CaDiCaL version: 2.1.3 % 18.20/3.66 % (3663500)Termination reason: Instruction limit % 18.20/3.66 % (3663500)Termination phase: Saturation % 18.20/3.66 % (3663500)Time elapsed: 0.080 s % 18.20/3.66 % (3663500)Peak memory usage: 90 MB % 18.20/3.66 % (3663500)Instructions burned: 136 (million) % 18.20/3.66 % (3663494)------------------------------ % 18.20/3.66 % (3663494)------------------------------ % 18.20/3.66 % (3663503)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1488342937:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/141Mi) % 18.20/3.66 % (3663503)Refutation not found, incomplete strategy % 18.20/3.66 % (3663503)------------------------------ % 18.20/3.66 % (3663503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.20/3.66 % (3663503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/3.66 % (3663503)CaDiCaL version: 2.1.3 % 18.20/3.66 % (3663503)Termination reason: Refutation not found, incomplete strategy % 18.20/3.66 % (3663503)Time elapsed: 0.001 s % 18.20/3.66 % (3663503)Peak memory usage: 87 MB % 18.20/3.66 % (3663490)Refutation not found, incomplete strategy % 18.20/3.66 % (3663490)------------------------------ % 18.20/3.66 % (3663490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.20/3.66 % (3663490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/3.66 % (3663490)CaDiCaL version: 2.1.3 % 18.20/3.66 % (3663490)Termination reason: Refutation not found, incomplete strategy % 18.20/3.66 % (3663490)Time elapsed: 0.567 s % 18.20/3.66 % (3663490)Peak memory usage: 125 MB % 18.20/3.66 % (3663490)Instructions burned: 823 (million) % 18.20/3.66 % (3663504)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=567932384:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2984 on theBenchmark for (2984ds/431Mi) % 18.20/3.66 % (3663499)------------------------------ % 18.20/3.66 % (3663499)------------------------------ % 18.20/3.66 % (3663504)Refutation not found, incomplete strategy % 18.20/3.66 % (3663504)------------------------------ % 18.20/3.66 % (3663504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 18.20/3.66 % (3663504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 18.20/3.66 % (3663504)CaDiCaL version: 2.1.3 % 18.20/3.66 % (3663504)Termination reason: Refutation not found, incomplete strategy % 18.20/3.66 % (3663504)Time elapsed: 0.001 s % 18.20/3.66 % (3663504)Peak memory usage: 87 MB % 18.20/3.66 % (3663505)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=2388256511:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi) % 26.21/4.67 % (3663508)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=3151199982:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2983 on theBenchmark for (2983ds/150Mi) % 26.21/4.67 % (3663508)Instruction limit reached! % 26.21/4.67 % (3663508)------------------------------ % 26.21/4.67 % (3663508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.21/4.67 % (3663508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.21/4.67 % (3663508)CaDiCaL version: 2.1.3 % 26.21/4.67 % (3663508)Termination reason: Instruction limit % 26.21/4.67 % (3663508)Termination phase: Saturation % 26.21/4.67 % (3663508)Time elapsed: 0.079 s % 26.21/4.67 % (3663508)Peak memory usage: 91 MB % 26.21/4.67 % (3663508)Instructions burned: 151 (million) % 26.21/4.67 % (3663503)------------------------------ % 26.21/4.67 % (3663503)------------------------------ % 26.21/4.67 % (3663504)------------------------------ % 26.21/4.67 % (3663504)------------------------------ % 26.21/4.67 % (3663490)------------------------------ % 26.21/4.67 % (3663490)------------------------------ % 26.21/4.67 % (3663511)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2042899814:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi) % 26.21/4.67 % (3663512)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3888467466:i=667:av=off:fsr=off_2980 on theBenchmark for (2980ds/667Mi) % 26.21/4.67 % (3663513)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=3930335318:s2a=on:i=185:s2at=1.8:fdi=4_2980 on theBenchmark for (2980ds/185Mi) % 26.21/4.67 % (3663514)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2986664330:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2980 on theBenchmark for (2980ds/193Mi) % 26.21/4.67 % (3663514)Refutation not found, incomplete strategy % 26.21/4.67 % (3663514)------------------------------ % 26.21/4.67 % (3663514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.21/4.67 % (3663514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.21/4.67 % (3663514)CaDiCaL version: 2.1.3 % 26.21/4.67 % (3663514)Termination reason: Refutation not found, incomplete strategy % 26.21/4.67 % (3663514)Time elapsed: 0.001 s % 26.21/4.67 % (3663514)Peak memory usage: 87 MB % 26.21/4.67 % (3663513)Instruction limit reached! % 26.21/4.67 % (3663513)------------------------------ % 26.21/4.67 % (3663513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.21/4.67 % (3663513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.21/4.67 % (3663513)CaDiCaL version: 2.1.3 % 26.21/4.67 % (3663513)Termination reason: Instruction limit % 26.21/4.67 % (3663513)Termination phase: Saturation % 26.21/4.67 % (3663513)Time elapsed: 0.096 s % 26.21/4.67 % (3663513)Peak memory usage: 91 MB % 26.21/4.67 % (3663513)Instructions burned: 185 (million) % 26.21/4.67 % (3663519)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=664591572:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2978 on theBenchmark for (2978ds/4850Mi) % 26.21/4.67 % (3663479)Instruction limit reached! % 26.21/4.67 % (3663479)------------------------------ % 26.21/4.67 % (3663479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.21/4.67 % (3663479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.21/4.67 % (3663479)CaDiCaL version: 2.1.3 % 26.21/4.67 % (3663479)Termination reason: Instruction limit % 26.21/4.67 % (3663479)Termination phase: Saturation % 26.21/4.67 % (3663479)Time elapsed: 1.505 s % 26.21/4.67 % (3663479)Peak memory usage: 143 MB % 26.21/4.67 % (3663479)Instructions burned: 2350 (million) % 26.21/4.67 % (3663514)------------------------------ % 26.21/4.67 % (3663514)------------------------------ % 26.21/4.67 % (3663512)Instruction limit reached! % 26.21/4.67 % (3663512)------------------------------ % 26.21/4.67 % (3663512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 26.21/4.67 % (3663512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 26.21/4.67 % (3663512)CaDiCaL version: 2.1.3 % 26.21/4.67 % (3663512)Termination reason: Instruction limit % 26.21/4.67 % (3663512)Termination phase: Saturation % 27.00/4.85 % (3663512)Time elapsed: 0.305 s % 27.00/4.85 % (3663512)Peak memory usage: 112 MB % 27.00/4.85 % (3663512)Instructions burned: 667 (million) % 27.00/4.85 % (3663521)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3861204885:i=12111:sd=1:ss=included_2977 on theBenchmark for (2977ds/12111Mi) % 27.00/4.85 % (3663522)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=221752686:i=319:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/319Mi) % 27.00/4.85 % (3663523)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1472139307:i=2064:ep=RST_2976 on theBenchmark for (2976ds/2064Mi) % 27.00/4.85 % (3663522)Instruction limit reached! % 27.00/4.85 % (3663522)------------------------------ % 27.00/4.85 % (3663522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.00/4.85 % (3663522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.00/4.85 % (3663522)CaDiCaL version: 2.1.3 % 27.00/4.85 % (3663522)Termination reason: Instruction limit % 27.00/4.85 % (3663522)Termination phase: Saturation % 27.00/4.85 % (3663522)Time elapsed: 0.176 s % 27.00/4.85 % (3663522)Peak memory usage: 92 MB % 27.00/4.85 % (3663522)Instructions burned: 319 (million) % 27.00/4.85 % (3663527)dis-1011_128_sil=32000:random_seed=4143745579:i=3706:ep=RST:av=off_2973 on theBenchmark for (2973ds/3706Mi) % 27.00/4.85 [W928 07:03:00.888626838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888657141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888694608 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888707824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888736078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888747861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888774131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888785824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 27.00/4.85 [W928 07:03:00.888812081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 27.00/4.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.28/5.35 [W928 07:03:00.888823824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 31.28/5.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.28/5.35 [W928 07:03:00.888854274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 31.28/5.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.28/5.35 [W928 07:03:00.888864944 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 31.28/5.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.28/5.35 % (3663521)Refutation not found, incomplete strategy % 31.28/5.35 % (3663521)------------------------------ % 31.28/5.35 % (3663521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.35 % (3663521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.35 % (3663521)CaDiCaL version: 2.1.3 % 31.28/5.35 % (3663521)Termination reason: Refutation not found, incomplete strategy % 31.28/5.35 % (3663521)Time elapsed: 0.544 s % 31.28/5.35 % (3663521)Peak memory usage: 126 MB % 31.28/5.35 % (3663521)Instructions burned: 827 (million) % 31.28/5.35 % (3663521)------------------------------ % 31.28/5.35 % (3663521)------------------------------ % 31.28/5.35 % (3663523)Instruction limit reached! % 31.28/5.35 % (3663523)------------------------------ % 31.28/5.35 % (3663523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.35 % (3663523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.35 % (3663523)CaDiCaL version: 2.1.3 % 31.28/5.35 % (3663523)Termination reason: Instruction limit % 31.28/5.35 % (3663523)Termination phase: Saturation % 31.28/5.35 % (3663523)Time elapsed: 0.812 s % 31.28/5.35 % (3663523)Peak memory usage: 90 MB % 31.28/5.35 % (3663523)Instructions burned: 2064 (million) % 31.28/5.35 % (3663529)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2954606136:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2967 on theBenchmark for (2967ds/757Mi) % 31.28/5.35 % (3663529)Refutation not found, incomplete strategy % 31.28/5.35 % (3663529)------------------------------ % 31.28/5.35 % (3663529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.35 % (3663529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.35 % (3663529)CaDiCaL version: 2.1.3 % 31.28/5.35 % (3663529)Termination reason: Refutation not found, incomplete strategy % 31.28/5.35 % (3663529)Time elapsed: 0.001 s % 31.28/5.35 % (3663529)Peak memory usage: 87 MB % 31.28/5.35 % (3663530)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=545594010:i=13913:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/13913Mi) % 31.28/5.35 % (3663529)------------------------------ % 31.28/5.35 % (3663529)------------------------------ % 31.28/5.35 % (3663533)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1538055843:i=9925:aac=none_2964 on theBenchmark for (2964ds/9925Mi) % 31.28/5.35 % (3663505)Instruction limit reached! % 31.28/5.35 % (3663505)------------------------------ % 31.28/5.35 % (3663505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.28/5.35 % (3663505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.28/5.35 % (3663505)CaDiCaL version: 2.1.3 % 31.28/5.35 % (3663505)Termination reason: Instruction limit % 31.28/5.35 % (3663505)Termination phase: Saturation % 31.28/5.35 % (3663505)Time elapsed: 1.970 s % 31.28/5.35 % (3663505)Peak memory usage: 157 MB % 31.28/5.35 % (3663505)Instructions burned: 6062 (million) % 31.28/5.35 [W928 07:03:01.896207550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 31.28/5.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 31.28/5.35 [W928 07:03:01.896251896 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896291826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896303273 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896328333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896339183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896375663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896386350 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896409517 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896420080 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896443563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 [W928 07:03:01.896454417 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 35.07/5.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 35.07/5.94 % (3663535)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=435224392:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2962 on theBenchmark for (2962ds/2479Mi) % 35.07/5.94 % (3663535)Refutation not found, incomplete strategy % 35.07/5.94 % (3663535)------------------------------ % 35.07/5.94 % (3663535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 35.07/5.94 % (3663535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 35.07/5.94 % (3663535)CaDiCaL version: 2.1.3 % 35.07/5.94 % (3663535)Termination reason: Refutation not found, incomplete strategy % 35.07/5.94 % (3663535)Time elapsed: 0.0000 s % 35.07/5.94 % (3663535)Peak memory usage: 87 MB % 35.07/5.94 % (3663535)------------------------------ % 35.07/5.94 % (3663535)------------------------------ % 35.07/5.94 % (3663530)Refutation not found, incomplete strategy % 52.98/8.30 % (3663530)------------------------------ % 52.98/8.30 % (3663530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.98/8.30 % (3663530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.98/8.30 % (3663530)CaDiCaL version: 2.1.3 % 52.98/8.30 % (3663530)Termination reason: Refutation not found, incomplete strategy % 52.98/8.30 % (3663530)Time elapsed: 0.555 s % 52.98/8.30 % (3663530)Peak memory usage: 125 MB % 52.98/8.30 % (3663530)Instructions burned: 827 (million) % 52.98/8.30 % (3663537)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2048795836:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2960 on theBenchmark for (2960ds/440Mi) % 52.98/8.30 % (3663537)Instruction limit reached! % 52.98/8.30 % (3663537)------------------------------ % 52.98/8.30 % (3663537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 52.98/8.30 % (3663537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 52.98/8.30 % (3663537)CaDiCaL version: 2.1.3 % 52.98/8.30 % (3663537)Termination reason: Instruction limit % 52.98/8.30 % (3663537)Termination phase: Saturation % 52.98/8.30 % (3663537)Time elapsed: 0.109 s % 52.98/8.30 % (3663537)Peak memory usage: 92 MB % 52.98/8.30 % (3663537)Instructions burned: 444 (million) % 52.98/8.30 % (3663530)------------------------------ % 52.98/8.30 % (3663530)------------------------------ % 52.98/8.30 % (3663539)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=970568010:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/11145Mi) % 52.98/8.30 % (3663540)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=2797143902:cts=off:i=3034:av=off:er=known:fsd=on_2957 on theBenchmark for (2957ds/3034Mi) % 52.98/8.30 [W928 07:03:02.576061642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576082065 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576102567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576109135 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576122560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576129410 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576143320 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 52.98/8.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 52.98/8.30 [W928 07:03:02.576150120 register_special_ops.cpp:225] Warning: Creating a tensor from 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.85/8.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.85/8.62 [W928 07:03:02.576163022 register_special_ops.cpp:225] Warning: Creating a tensor from 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.85/8.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.85/8.62 [W928 07:03:02.576170287 register_special_ops.cpp:225] Warning: Creating a tensor from 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.85/8.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.85/8.62 [W928 07:03:02.576183291 register_special_ops.cpp:225] Warning: Creating a tensor from 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.85/8.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.85/8.62 [W928 07:03:02.576189138 register_special_ops.cpp:225] Warning: Creating a tensor from 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.85/8.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 54.85/8.62 % (3663539)Refutation not found, incomplete strategy % 54.85/8.62 % (3663539)------------------------------ % 54.85/8.62 % (3663539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.85/8.62 % (3663539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.85/8.62 % (3663539)CaDiCaL version: 2.1.3 % 54.85/8.62 % (3663539)Termination reason: Refutation not found, incomplete strategy % 54.85/8.62 % (3663539)Time elapsed: 0.316 s % 54.85/8.62 % (3663539)Peak memory usage: 126 MB % 54.85/8.62 % (3663539)Instructions burned: 828 (million) % 54.85/8.62 % (3663539)------------------------------ % 54.85/8.62 % (3663539)------------------------------ % 54.85/8.62 % (3663543)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2805896033:st=2:s2a=on:i=524:s2at=2:ss=axioms_2952 on theBenchmark for (2952ds/524Mi) % 54.85/8.62 % (3663543)Refutation not found, incomplete strategy % 54.85/8.62 % (3663543)------------------------------ % 54.85/8.62 % (3663543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.85/8.62 % (3663543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.85/8.62 % (3663543)CaDiCaL version: 2.1.3 % 54.85/8.62 % (3663543)Termination reason: Refutation not found, incomplete strategy % 54.85/8.62 % (3663543)Time elapsed: 0.001 s % 54.85/8.62 % (3663543)Peak memory usage: 87 MB % 54.85/8.62 % (3663543)Instructions burned: 1 (million) % 54.85/8.62 % (3663527)Instruction limit reached! % 54.85/8.62 % (3663527)------------------------------ % 54.85/8.62 % (3663527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.85/8.62 % (3663527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.85/8.62 % (3663527)CaDiCaL version: 2.1.3 % 54.85/8.62 % (3663527)Termination reason: Instruction limit % 54.85/8.62 % (3663527)Termination phase: Saturation % 54.85/8.62 % (3663527)Time elapsed: 2.183 s % 54.85/8.62 % (3663527)Peak memory usage: 105 MB % 54.85/8.62 % (3663527)Instructions burned: 3707 (million) % 54.85/8.62 % (3663519)Instruction limit reached! % 54.85/8.62 % (3663519)------------------------------ % 54.85/8.62 % (3663519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 54.85/8.62 % (3663519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 54.85/8.62 % (3663519)CaDiCaL version: 2.1.3 % 54.85/8.62 % (3663519)Termination reason: Instruction limit % 54.85/8.62 % (3663519)Termination phase: Saturation % 54.85/8.62 % (3663519)Time elapsed: 2.723 s % 54.85/8.62 % (3663519)Peak memory usage: 109 MB % 54.85/8.62 % (3663519)Instructions burned: 4850 (million) % 54.85/8.62 % (3663543)------------------------------ % 54.85/8.62 % (3663543)------------------------------ % 54.85/8.62 % (3663545)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=221205136:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2950 on theBenchmark for (2950ds/1016Mi) % 54.85/8.62 % (3663545)Refutation not found, incomplete strategy % 54.85/8.62 % (3663545)------------------------------ % 54.85/8.62 % (3663545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.48/8.72 % (3663545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.48/8.72 % (3663545)CaDiCaL version: 2.1.3 % 55.48/8.72 % (3663545)Termination reason: Refutation not found, incomplete strategy % 55.48/8.72 % (3663545)Time elapsed: 0.001 s % 55.48/8.72 % (3663545)Peak memory usage: 87 MB % 55.48/8.72 % (3663547)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1387686593:i=5781:kws=precedence:bd=all:rawr=on_2949 on theBenchmark for (2949ds/5781Mi) % 55.48/8.72 % (3663546)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1095979222:i=14123:bd=preordered:ins=4_2949 on theBenchmark for (2949ds/14123Mi) % 55.48/8.72 % (3663545)------------------------------ % 55.48/8.72 % (3663545)------------------------------ % 55.48/8.72 % (3663551)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=2158009860:i=2448:gtgl=5:bd=preordered:gtg=all_2946 on theBenchmark for (2946ds/2448Mi) % 55.48/8.72 % (3663540)Instruction limit reached! % 55.48/8.72 % (3663540)------------------------------ % 55.48/8.72 % (3663540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.48/8.72 % (3663540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.48/8.72 % (3663540)CaDiCaL version: 2.1.3 % 55.48/8.72 % (3663540)Termination reason: Instruction limit % 55.48/8.72 % (3663540)Termination phase: Saturation % 55.48/8.72 % (3663540)Time elapsed: 1.800 s % 55.48/8.72 % (3663540)Peak memory usage: 143 MB % 55.48/8.72 % (3663540)Instructions burned: 3035 (million) % 55.48/8.72 % (3663553)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=333151100:i=3223:kws=precedence:fgj=on:av=off_2938 on theBenchmark for (2938ds/3223Mi) % 55.48/8.72 % (3663547)Instruction limit reached! % 55.48/8.72 % (3663547)------------------------------ % 55.48/8.72 % (3663547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.48/8.72 % (3663547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.48/8.72 % (3663547)CaDiCaL version: 2.1.3 % 55.48/8.72 % (3663547)Termination reason: Instruction limit % 55.48/8.72 % (3663547)Termination phase: Saturation % 55.48/8.72 % (3663547)Time elapsed: 1.545 s % 55.48/8.72 % (3663547)Peak memory usage: 130 MB % 55.48/8.72 % (3663547)Instructions burned: 5783 (million) % 55.48/8.72 % (3663555)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4181163381:st=5.6:i=2033:sd=3:ss=axioms_2933 on theBenchmark for (2933ds/2033Mi) % 55.48/8.72 % (3663551)Instruction limit reached! % 55.48/8.72 % (3663551)------------------------------ % 55.48/8.72 % (3663551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 55.48/8.72 % (3663551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 55.48/8.72 % (3663551)CaDiCaL version: 2.1.3 % 55.48/8.72 % (3663551)Termination reason: Instruction limit % 55.48/8.72 % (3663551)Termination phase: Saturation % 55.48/8.72 % (3663551)Time elapsed: 1.477 s % 55.48/8.72 % (3663551)Peak memory usage: 143 MB % 55.48/8.72 % (3663551)Instructions burned: 2449 (million) % 55.48/8.72 % (3663557)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=200141560:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2930 on theBenchmark for (2930ds/2055Mi) % 55.48/8.72 [W928 07:03:05.523157315 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.48/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.48/8.72 [W928 07:03:05.523198239 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.48/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.48/8.72 [W928 07:03:05.523241689 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 55.48/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 55.48/8.72 [W928 07:03:05.523253646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523279936 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523290756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523315682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523326299 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523350246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523360946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523385322 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 [W928 07:03:05.523396072 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 61.05/9.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 61.05/9.59 % (3663555)Instruction limit reached! % 61.05/9.59 % (3663555)------------------------------ % 61.05/9.59 % (3663555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.05/9.59 % (3663555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.05/9.59 % (3663555)CaDiCaL version: 2.1.3 % 61.05/9.59 % (3663555)Termination reason: Instruction limit % 61.05/9.59 % (3663555)Termination phase: Saturation % 61.05/9.59 % (3663555)Time elapsed: 0.715 s % 61.05/9.59 % (3663555)Peak memory usage: 133 MB % 61.05/9.59 % (3663555)Instructions burned: 2036 (million) % 61.05/9.59 % (3663559)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=941444805:i=21611:sd=3:ss=axioms_2925 on theBenchmark for (2925ds/21611Mi) % 61.05/9.59 % (3663557)Refutation not found, incomplete strategy % 61.05/9.59 % (3663557)------------------------------ % 61.05/9.59 % (3663557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 61.05/9.59 % (3663557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 61.05/9.59 % (3663557)CaDiCaL version: 2.1.3 % 61.05/9.59 % (3663557)Termination reason: Refutation not found, incomplete strategy % 61.05/9.59 % (3663557)Time elapsed: 0.548 s % 61.05/9.59 % (3663557)Peak memory usage: 126 MB % 61.05/9.59 % (3663557)Instructions burned: 828 (million) % 61.05/9.59 [W928 07:03:05.846936060 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.846973041 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.846995743 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847021680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847036416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847042779 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847056200 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847061804 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847074603 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847080283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847093384 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 [W928 07:03:05.847099053 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 66.96/10.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 66.96/10.37 % (3663557)------------------------------ % 66.96/10.37 % (3663557)------------------------------ % 66.96/10.37 % (3663559)Refutation not found, incomplete strategy % 66.96/10.37 % (3663559)------------------------------ % 66.96/10.37 % (3663559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 66.96/10.37 % (3663559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 66.96/10.37 % (3663559)CaDiCaL version: 2.1.3 % 69.11/10.83 % (3663559)Termination reason: Refutation not found, incomplete strategy % 69.11/10.83 % (3663559)Time elapsed: 0.302 s % 69.11/10.83 % (3663559)Peak memory usage: 126 MB % 69.11/10.83 % (3663559)Instructions burned: 828 (million) % 69.11/10.83 % (3663561)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=986960304:i=4835:sd=13:ss=axioms:sgt=23_2921 on theBenchmark for (2921ds/4835Mi) % 69.11/10.83 % (3663561)Refutation not found, incomplete strategy % 69.11/10.83 % (3663561)------------------------------ % 69.11/10.83 % (3663561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.11/10.83 % (3663561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.11/10.83 % (3663561)CaDiCaL version: 2.1.3 % 69.11/10.83 % (3663561)Termination reason: Refutation not found, incomplete strategy % 69.11/10.83 % (3663561)Time elapsed: 0.001 s % 69.11/10.83 % (3663561)Peak memory usage: 87 MB % 69.11/10.83 % (3663559)------------------------------ % 69.11/10.83 % (3663559)------------------------------ % 69.11/10.83 % (3663563)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=2726912181:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2919 on theBenchmark for (2919ds/797Mi) % 69.11/10.83 % (3663561)------------------------------ % 69.11/10.83 % (3663561)------------------------------ % 69.11/10.83 % (3663563)Instruction limit reached! % 69.11/10.83 % (3663563)------------------------------ % 69.11/10.83 % (3663563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.11/10.83 % (3663563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.11/10.83 % (3663563)CaDiCaL version: 2.1.3 % 69.11/10.83 % (3663563)Termination reason: Instruction limit % 69.11/10.83 % (3663563)Termination phase: Saturation % 69.11/10.83 % (3663563)Time elapsed: 0.239 s % 69.11/10.83 % (3663563)Peak memory usage: 95 MB % 69.11/10.83 % (3663563)Instructions burned: 799 (million) % 69.11/10.83 % (3663565)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2617838975:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2917 on theBenchmark for (2917ds/2326Mi) % 69.11/10.83 % (3663565)Refutation not found, incomplete strategy % 69.11/10.83 % (3663565)------------------------------ % 69.11/10.83 % (3663565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.11/10.83 % (3663565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.11/10.83 % (3663565)CaDiCaL version: 2.1.3 % 69.11/10.83 % (3663565)Termination reason: Refutation not found, incomplete strategy % 69.11/10.83 % (3663565)Time elapsed: 0.008 s % 69.11/10.83 % (3663565)Peak memory usage: 88 MB % 69.11/10.83 % (3663565)Instructions burned: 13 (million) % 69.11/10.83 % (3663566)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3944127385:i=6038:nm=6_2916 on theBenchmark for (2916ds/6038Mi) % 69.11/10.83 % (3663553)Instruction limit reached! % 69.11/10.83 % (3663553)------------------------------ % 69.11/10.83 % (3663553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.11/10.83 % (3663553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.11/10.83 % (3663553)CaDiCaL version: 2.1.3 % 69.11/10.83 % (3663553)Termination reason: Instruction limit % 69.11/10.83 % (3663553)Termination phase: Saturation % 69.11/10.83 % (3663553)Time elapsed: 2.185 s % 69.11/10.83 % (3663553)Peak memory usage: 147 MB % 69.11/10.83 % (3663553)Instructions burned: 3223 (million) % 69.11/10.83 % (3663565)------------------------------ % 69.11/10.83 % (3663565)------------------------------ % 69.11/10.83 % (3663569)lrs+10_1_sil=32000:sp=occurrence:random_seed=3025649874:st=2:i=33334:sd=3:ss=included:sgt=32_2915 on theBenchmark for (2915ds/33334Mi) % 69.11/10.83 % (3663569)Refutation not found, incomplete strategy % 69.11/10.83 % (3663569)------------------------------ % 69.11/10.83 % (3663569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.11/10.83 % (3663569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.11/10.83 % (3663569)CaDiCaL version: 2.1.3 % 69.11/10.83 % (3663569)Termination reason: Refutation not found, incomplete strategy % 69.11/10.83 % (3663569)Time elapsed: 0.001 s % 69.11/10.83 % (3663569)Peak memory usage: 87 MB % 69.11/10.83 % (3663570)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=336976239:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2914 on theBenchmark for (2914ds/1008Mi) % 69.42/11.01 % (3663570)Refutation not found, incomplete strategy % 69.42/11.01 % (3663570)------------------------------ % 69.42/11.01 % (3663570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.42/11.01 % (3663570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.42/11.01 % (3663570)CaDiCaL version: 2.1.3 % 69.42/11.01 % (3663570)Termination reason: Refutation not found, incomplete strategy % 69.42/11.01 % (3663570)Time elapsed: 0.001 s % 69.42/11.01 % (3663570)Peak memory usage: 87 MB % 69.42/11.01 % (3663570)Instructions burned: 1 (million) % 69.42/11.01 % (3663566)Refutation not found, incomplete strategy % 69.42/11.01 % (3663566)------------------------------ % 69.42/11.01 % (3663566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.42/11.01 % (3663566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.42/11.01 % (3663566)CaDiCaL version: 2.1.3 % 69.42/11.01 % (3663566)Termination reason: Refutation not found, incomplete strategy % 69.42/11.01 % (3663566)Time elapsed: 0.337 s % 69.42/11.01 % (3663566)Peak memory usage: 130 MB % 69.42/11.01 % (3663566)Instructions burned: 884 (million) % 69.42/11.01 % (3663569)------------------------------ % 69.42/11.01 % (3663569)------------------------------ % 69.42/11.01 % (3663566)------------------------------ % 69.42/11.01 % (3663566)------------------------------ % 69.42/11.01 % (3663570)------------------------------ % 69.42/11.01 % (3663570)------------------------------ % 69.42/11.01 % (3663574)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=457579116:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2910 on theBenchmark for (2910ds/1083Mi) % 69.42/11.01 % (3663573)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=979481651:i=8327:s2at=5:bd=preordered_2911 on theBenchmark for (2911ds/8327Mi) % 69.42/11.01 % (3663575)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=4067516189:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2910 on theBenchmark for (2910ds/1084Mi) % 69.42/11.01 % (3663575)Refutation not found, incomplete strategy % 69.42/11.01 % (3663575)------------------------------ % 69.42/11.01 % (3663575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.42/11.01 % (3663575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.42/11.01 % (3663575)CaDiCaL version: 2.1.3 % 69.42/11.01 % (3663575)Termination reason: Refutation not found, incomplete strategy % 69.42/11.01 % (3663575)Time elapsed: 0.001 s % 69.42/11.01 % (3663575)Peak memory usage: 86 MB % 69.42/11.01 % (3663574)Instruction limit reached! % 69.42/11.01 % (3663574)------------------------------ % 69.42/11.01 % (3663574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.42/11.01 % (3663574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.42/11.01 % (3663574)CaDiCaL version: 2.1.3 % 69.42/11.01 % (3663574)Termination reason: Instruction limit % 69.42/11.01 % (3663574)Termination phase: Saturation % 69.42/11.01 % (3663574)Time elapsed: 0.265 s % 69.42/11.01 % (3663574)Peak memory usage: 99 MB % 69.42/11.01 % (3663574)Instructions burned: 1087 (million) % 69.42/11.01 % (3663575)------------------------------ % 69.42/11.01 % (3663575)------------------------------ % 69.42/11.01 % (3663579)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3957099363:i=6995:s2at=5:gtg=all_2907 on theBenchmark for (2907ds/6995Mi) % 69.42/11.01 % (3663511)Instruction limit reached! % 69.42/11.01 % (3663511)------------------------------ % 69.42/11.01 % (3663511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 69.42/11.01 % (3663511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.42/11.01 % (3663511)CaDiCaL version: 2.1.3 % 69.42/11.01 % (3663511)Termination reason: Instruction limit % 69.42/11.01 % (3663511)Termination phase: Saturation % 69.42/11.01 % (3663511)Time elapsed: 7.410 s % 69.42/11.01 % (3663511)Peak memory usage: 232 MB % 69.42/11.01 % (3663511)Instructions burned: 14155 (million) % 69.42/11.01 % (3663580)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1482668889:st=2:i=6225:sd=15:ss=axioms_2906 on theBenchmark for (2906ds/6225Mi) % 69.42/11.01 % (3663580)Refutation not found, incomplete strategy % 69.42/11.01 % (3663580)------------------------------ % 69.42/11.01 % (3663580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.38/11.77 % (3663580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.38/11.77 % (3663580)CaDiCaL version: 2.1.3 % 76.38/11.77 % (3663580)Termination reason: Refutation not found, incomplete strategy % 76.38/11.77 % (3663580)Time elapsed: 0.001 s % 76.38/11.77 % (3663580)Peak memory usage: 87 MB % 76.38/11.77 % (3663582)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1410418164:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2905 on theBenchmark for (2905ds/3372Mi) % 76.38/11.77 % (3663533)Instruction limit reached! % 76.38/11.77 % (3663533)------------------------------ % 76.38/11.77 % (3663533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 76.38/11.77 % (3663533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 76.38/11.77 % (3663533)CaDiCaL version: 2.1.3 % 76.38/11.77 % (3663533)Termination reason: Instruction limit % 76.38/11.77 % (3663533)Termination phase: Saturation % 76.38/11.77 % (3663533)Time elapsed: 5.909 s % 76.38/11.77 % (3663533)Peak memory usage: 163 MB % 76.38/11.77 % (3663533)Instructions burned: 9927 (million) % 76.38/11.77 % (3663580)------------------------------ % 76.38/11.77 % (3663580)------------------------------ % 76.38/11.77 % (3663585)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2395469283:st=2.3:i=26457:sd=10:ss=included:sgt=8_2903 on theBenchmark for (2903ds/26457Mi) % 76.38/11.77 % (3663586)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=3737895284:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2902 on theBenchmark for (2902ds/13494Mi) % 76.38/11.77 [W928 07:03:08.052031797 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052078324 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052116337 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052127604 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052157044 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052167284 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052191194 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 76.38/11.77 [W928 07:03:08.052201381 register_special_ops.cpp:225] Warning: Creating a tensor from 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.38/11.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.052225467 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.052236377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.052259934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.052269987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232784671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232825324 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232864054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232874917 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232899784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232909977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232934414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232944787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232968674 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 77.39/11.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 77.39/11.94 [W928 07:03:08.232979067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 [W928 07:03:08.233012254 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 [W928 07:03:08.233023227 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 % (3663582)Refutation not found, incomplete strategy % 82.31/12.59 % (3663582)------------------------------ % 82.31/12.59 % (3663582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.31/12.59 % (3663582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.31/12.59 % (3663582)CaDiCaL version: 2.1.3 % 82.31/12.59 % (3663582)Termination reason: Refutation not found, incomplete strategy % 82.31/12.59 % (3663582)Time elapsed: 0.568 s % 82.31/12.59 % (3663582)Peak memory usage: 126 MB % 82.31/12.59 % (3663582)Instructions burned: 827 (million) % 82.31/12.59 % (3663585)Refutation not found, incomplete strategy % 82.31/12.59 % (3663585)------------------------------ % 82.31/12.59 % (3663585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 82.31/12.59 % (3663585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 82.31/12.59 % (3663585)CaDiCaL version: 2.1.3 % 82.31/12.59 % (3663585)Termination reason: Refutation not found, incomplete strategy % 82.31/12.59 % (3663585)Time elapsed: 0.545 s % 82.31/12.59 % (3663585)Peak memory usage: 125 MB % 82.31/12.59 % (3663585)Instructions burned: 827 (million) % 82.31/12.59 % (3663582)------------------------------ % 82.31/12.59 % (3663582)------------------------------ % 82.31/12.59 % (3663589)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=3800191740:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2896 on theBenchmark for (2896ds/2503Mi) % 82.31/12.59 % (3663585)------------------------------ % 82.31/12.59 % (3663585)------------------------------ % 82.31/12.59 % (3663591)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=3635226870:i=2559:sd=1:ep=RSTC:ss=axioms_2894 on theBenchmark for (2894ds/2559Mi) % 82.31/12.59 [W928 07:03:08.990991075 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 [W928 07:03:08.991033258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 [W928 07:03:08.991071345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 [W928 07:03:08.991084245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 82.31/12.59 [W928 07:03:08.991111435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 82.31/12.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991123148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991158385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991168951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991194195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991204681 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991229895 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:08.991240398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 % (3663589)Refutation not found, incomplete strategy % 83.55/12.88 % (3663589)------------------------------ % 83.55/12.88 % (3663589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 83.55/12.88 % (3663589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 83.55/12.88 % (3663589)CaDiCaL version: 2.1.3 % 83.55/12.88 % (3663589)Termination reason: Refutation not found, incomplete strategy % 83.55/12.88 % (3663589)Time elapsed: 0.545 s % 83.55/12.88 % (3663589)Peak memory usage: 126 MB % 83.55/12.88 % (3663589)Instructions burned: 823 (million) % 83.55/12.88 [W928 07:03:09.167608458 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:09.167648921 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:09.167686748 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:09.167699818 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 83.55/12.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 83.55/12.88 [W928 07:03:09.167726694 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167738328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167770118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167780378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167805718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167815678 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167839314 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 [W928 07:03:09.167849618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 88.02/13.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 88.02/13.36 % (3663591)Refutation not found, incomplete strategy % 88.02/13.36 % (3663591)------------------------------ % 88.02/13.36 % (3663591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.02/13.36 % (3663591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.02/13.36 % (3663591)CaDiCaL version: 2.1.3 % 88.02/13.36 % (3663591)Termination reason: Refutation not found, incomplete strategy % 88.02/13.36 % (3663591)Time elapsed: 0.545 s % 88.02/13.36 % (3663591)Peak memory usage: 125 MB % 88.02/13.36 % (3663591)Instructions burned: 827 (million) % 88.02/13.36 % (3663589)------------------------------ % 88.02/13.36 % (3663589)------------------------------ % 88.02/13.36 % (3663593)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2636637836:i=30753:av=off:ss=included_2886 on theBenchmark for (2886ds/30753Mi) % 88.02/13.36 % (3663591)------------------------------ % 88.02/13.36 % (3663591)------------------------------ % 88.02/13.36 % (3663595)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2991474346:i=26473:ep=RSTC_2885 on theBenchmark for (2885ds/26473Mi) % 88.02/13.36 % (3663579)Instruction limit reached! % 88.02/13.36 % (3663579)------------------------------ % 88.02/13.36 % (3663579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 88.02/13.36 % (3663579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 88.02/13.36 % (3663579)CaDiCaL version: 2.1.3 % 88.02/13.36 % (3663579)Termination reason: Instruction limit % 88.02/13.36 % (3663579)Termination phase: Saturation % 88.02/13.36 % (3663579)Time elapsed: 2.267 s % 88.02/13.36 % (3663579)Peak memory usage: 165 MB % 88.02/13.36 % (3663579)Instructions burned: 6997 (million) % 88.02/13.36 % (3663597)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=2377080837:cts=off:i=2759:kws=inv_arity:fgj=on_2883 on theBenchmark for (2883ds/2759Mi) % 89.56/13.66 [W928 07:03:09.937900306 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.937938123 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.937975333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.937986566 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938027770 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938041137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938066977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938078130 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938102553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938113663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938139970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 [W928 07:03:09.938149823 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 89.56/13.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 89.56/13.66 % (3663593)Refutation not found, incomplete strategy % 89.56/13.66 % (3663593)------------------------------ % 89.56/13.66 % (3663593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.56/13.66 % (3663593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.67/13.93 % (3663593)CaDiCaL version: 2.1.3 % 91.67/13.93 % (3663593)Termination reason: Refutation not found, incomplete strategy % 91.67/13.93 % (3663593)Time elapsed: 0.549 s % 91.67/13.93 % (3663593)Peak memory usage: 125 MB % 91.67/13.93 % (3663593)Instructions burned: 826 (million) % 91.67/13.93 % (3663597)Refutation not found, incomplete strategy % 91.67/13.93 % (3663597)------------------------------ % 91.67/13.93 % (3663597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 91.67/13.93 % (3663597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 91.67/13.93 % (3663597)CaDiCaL version: 2.1.3 % 91.67/13.93 % (3663597)Termination reason: Refutation not found, incomplete strategy % 91.67/13.93 % (3663597)Time elapsed: 0.318 s % 91.67/13.93 % (3663597)Peak memory usage: 129 MB % 91.67/13.93 % (3663597)Instructions burned: 880 (million) % 91.67/13.93 % (3663597)------------------------------ % 91.67/13.93 % (3663597)------------------------------ % 91.67/13.93 % (3663593)------------------------------ % 91.67/13.93 % (3663593)------------------------------ % 91.67/13.93 % (3663599)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=372712296:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2878 on theBenchmark for (2878ds/5665Mi) % 91.67/13.93 % (3663601)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=1759876817:i=1532:ep=RS:ss=axioms_2877 on theBenchmark for (2877ds/1532Mi) % 91.67/13.93 [W928 07:03:10.583602991 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583656874 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583677725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583684238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583697511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583703008 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583716686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583723192 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 91.67/13.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 91.67/13.93 [W928 07:03:10.583735916 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.583742202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.583755222 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.583760524 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 % (3663599)Refutation not found, incomplete strategy % 95.67/14.48 % (3663599)------------------------------ % 95.67/14.48 % (3663599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 95.67/14.48 % (3663599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 95.67/14.48 % (3663599)CaDiCaL version: 2.1.3 % 95.67/14.48 % (3663599)Termination reason: Refutation not found, incomplete strategy % 95.67/14.48 % (3663599)Time elapsed: 0.314 s % 95.67/14.48 % (3663599)Peak memory usage: 126 MB % 95.67/14.48 % (3663599)Instructions burned: 828 (million) % 95.67/14.48 % (3663599)------------------------------ % 95.67/14.48 % (3663599)------------------------------ % 95.67/14.48 [W928 07:03:10.888329805 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888370205 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888406975 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888420188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888446305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888457875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888483948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 95.67/14.48 [W928 07:03:10.888495605 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 95.67/14.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:10.888521268 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:10.888531632 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:10.888555265 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:10.888565198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 % (3663603)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=32179061:i=1565:sd=2:ss=axioms:sgt=32_2872 on theBenchmark for (2872ds/1565Mi) % 98.22/14.85 % (3663601)Refutation not found, incomplete strategy % 98.22/14.85 % (3663601)------------------------------ % 98.22/14.85 % (3663601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 98.22/14.85 % (3663601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 98.22/14.85 % (3663601)CaDiCaL version: 2.1.3 % 98.22/14.85 % (3663601)Termination reason: Refutation not found, incomplete strategy % 98.22/14.85 % (3663601)Time elapsed: 0.551 s % 98.22/14.85 % (3663601)Peak memory usage: 126 MB % 98.22/14.85 % (3663601)Instructions burned: 827 (million) % 98.22/14.85 [W928 07:03:11.152273010 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:11.152294238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:11.152314563 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:11.152320701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:11.152334085 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:11.152340776 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 98.22/14.85 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 98.22/14.85 [W928 07:03:11.152354769 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.152361158 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.152374536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.152379839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.152392618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.152404092 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 % (3663603)Refutation not found, incomplete strategy % 101.83/15.23 % (3663603)------------------------------ % 101.83/15.23 % (3663603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 101.83/15.23 % (3663603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.83/15.23 % (3663603)CaDiCaL version: 2.1.3 % 101.83/15.23 % (3663603)Termination reason: Refutation not found, incomplete strategy % 101.83/15.23 % (3663603)Time elapsed: 0.295 s % 101.83/15.23 % (3663603)Peak memory usage: 126 MB % 101.83/15.23 % (3663603)Instructions burned: 822 (million) % 101.83/15.23 % (3663601)------------------------------ % 101.83/15.23 % (3663601)------------------------------ % 101.83/15.23 % (3663603)------------------------------ % 101.83/15.23 % (3663603)------------------------------ % 101.83/15.23 % (3663605)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=596569471:i=1572:fgj=on:gsp=on_2867 on theBenchmark for (2867ds/1572Mi) % 101.83/15.23 % (3663606)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1946541438:i=6052:sd=4:ss=axioms:sgt=24_2866 on theBenchmark for (2866ds/6052Mi) % 101.83/15.23 [W928 07:03:11.702458621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.702477784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.702516713 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.702524830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 101.83/15.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 101.83/15.23 [W928 07:03:11.702538182 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702543884 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702557339 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702562884 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702588634 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702594693 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702607836 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 [W928 07:03:11.702613289 register_special_ops.cpp:225] Warning: Creating a tensor from 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.06/15.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 103.06/15.41 % (3663606)Refutation not found, incomplete strategy % 103.06/15.41 % (3663606)------------------------------ % 103.06/15.41 % (3663606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.06/15.41 % (3663606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.41 % (3663606)CaDiCaL version: 2.1.3 % 103.06/15.41 % (3663606)Termination reason: Refutation not found, incomplete strategy % 103.06/15.41 % (3663606)Time elapsed: 0.312 s % 103.06/15.41 % (3663606)Peak memory usage: 125 MB % 103.06/15.41 % (3663606)Instructions burned: 826 (million) % 103.06/15.41 % (3663573)Instruction limit reached! % 103.06/15.41 % (3663573)------------------------------ % 103.06/15.41 % (3663573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 103.06/15.41 % (3663573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 103.06/15.41 % (3663573)CaDiCaL version: 2.1.3 % 103.06/15.41 % (3663573)Termination reason: Instruction limit % 103.06/15.41 % (3663573)Termination phase: Saturation % 103.06/15.41 % (3663573)Time elapsed: 4.813 s % 103.06/15.41 % (3663573)Peak memory usage: 192 MB % 103.06/15.41 % (3663573)Instructions burned: 8328 (million) % 103.06/15.41 % (3663606)------------------------------ % 103.06/15.41 % (3663606)------------------------------ % 103.06/15.41 % (3663610)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=587517062:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2861 on theBenchmark for (2861ds/1842Mi) % 103.06/15.41 % (3663609)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=840914233:i=3500:sd=1:bd=preordered:sup=off:ss=included_2861 on theBenchmark for (2861ds/3500Mi) % 104.54/15.78 % (3663546)Instruction limit reached! % 104.54/15.78 % (3663546)------------------------------ % 104.54/15.78 % (3663546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.54/15.78 % (3663546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.54/15.78 % (3663546)CaDiCaL version: 2.1.3 % 104.54/15.78 % (3663546)Termination reason: Instruction limit % 104.54/15.78 % (3663546)Termination phase: Saturation % 104.54/15.78 % (3663546)Time elapsed: 8.903 s % 104.54/15.78 % (3663546)Peak memory usage: 255 MB % 104.54/15.78 % (3663546)Instructions burned: 14123 (million) % 104.54/15.78 [W928 07:03:12.263688916 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.263723441 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.263743321 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.263749822 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.263762897 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.263768187 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 % (3663613)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2382664037:i=66096:add=on_2859 on theBenchmark for (2859ds/66096Mi) % 104.54/15.78 % (3663610)Refutation not found, incomplete strategy % 104.54/15.78 % (3663610)------------------------------ % 104.54/15.78 % (3663610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 104.54/15.78 % (3663610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 104.54/15.78 % (3663610)CaDiCaL version: 2.1.3 % 104.54/15.78 % (3663610)Termination reason: Refutation not found, incomplete strategy % 104.54/15.78 % (3663610)Time elapsed: 0.320 s % 104.54/15.78 % (3663610)Peak memory usage: 127 MB % 104.54/15.78 % (3663610)Instructions burned: 857 (million) % 104.54/15.78 [W928 07:03:12.452291904 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.452331804 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.452369104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 104.54/15.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 104.54/15.78 [W928 07:03:12.452380161 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452407171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452417434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452442131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452452071 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452476544 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452486491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452510368 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 [W928 07:03:12.452520395 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 121.90/18.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 121.90/18.13 % (3663605)Instruction limit reached! % 121.90/18.13 % (3663605)------------------------------ % 121.90/18.13 % (3663605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/18.13 % (3663605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/18.13 % (3663605)CaDiCaL version: 2.1.3 % 121.90/18.13 % (3663605)Termination reason: Instruction limit % 121.90/18.13 % (3663605)Termination phase: Saturation % 121.90/18.13 % (3663605)Time elapsed: 1.043 s % 121.90/18.13 % (3663605)Peak memory usage: 135 MB % 121.90/18.13 % (3663605)Instructions burned: 1572 (million) % 121.90/18.13 % (3663610)------------------------------ % 121.90/18.13 % (3663610)------------------------------ % 121.90/18.13 % (3663615)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=159062936:i=1884:sd=1:nm=60:ss=axioms_2856 on theBenchmark for (2856ds/1884Mi) % 121.90/18.13 % (3663616)lrs-1011_4:1_sil=16000:bsr=on:random_seed=320469064:cts=off:i=5469:bs=on:fsr=off_2855 on theBenchmark for (2855ds/5469Mi) % 121.90/18.13 % (3663609)Refutation not found, incomplete strategy % 121.90/18.13 % (3663609)------------------------------ % 121.90/18.13 % (3663609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 121.90/18.13 % (3663609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 121.90/18.13 % (3663609)CaDiCaL version: 2.1.3 % 121.90/18.13 % (3663609)Termination reason: Refutation not found, incomplete strategy % 123.10/18.22 % (3663609)Time elapsed: 0.557 s % 123.10/18.22 % (3663609)Peak memory usage: 125 MB % 123.10/18.22 % (3663609)Instructions burned: 826 (million) % 123.10/18.22 % (3663609)------------------------------ % 123.10/18.22 % (3663609)------------------------------ % 123.10/18.22 [W928 07:03:12.994241508 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994272815 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994311761 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994324718 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994352378 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994363891 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994389935 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994401285 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994426218 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994437448 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994463018 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 [W928 07:03:12.994474355 register_special_ops.cpp:225] Warning: Creating a tensor from 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.10/18.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 123.10/18.22 % (3663619)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=3094800815:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2852 on theBenchmark for (2852ds/2037Mi) % 124.50/18.44 % (3663615)Refutation not found, incomplete strategy % 124.50/18.44 % (3663615)------------------------------ % 124.50/18.44 % (3663615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.50/18.44 % (3663615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.50/18.44 % (3663615)CaDiCaL version: 2.1.3 % 124.50/18.44 % (3663615)Termination reason: Refutation not found, incomplete strategy % 124.50/18.44 % (3663615)Time elapsed: 0.548 s % 124.50/18.44 % (3663615)Peak memory usage: 125 MB % 124.50/18.44 % (3663615)Instructions burned: 823 (million) % 124.50/18.44 % (3663615)------------------------------ % 124.50/18.44 % (3663615)------------------------------ % 124.50/18.44 % (3663622)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2353190274:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2846 on theBenchmark for (2846ds/2110Mi) % 124.50/18.44 % (3663616)Instruction limit reached! % 124.50/18.44 % (3663616)------------------------------ % 124.50/18.44 % (3663616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.50/18.44 % (3663616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.50/18.44 % (3663616)CaDiCaL version: 2.1.3 % 124.50/18.44 % (3663616)Termination reason: Instruction limit % 124.50/18.44 % (3663616)Termination phase: Saturation % 124.50/18.44 % (3663616)Time elapsed: 1.473 s % 124.50/18.44 % (3663616)Peak memory usage: 110 MB % 124.50/18.44 % (3663616)Instructions burned: 5471 (million) % 124.50/18.44 % (3663624)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=2429549385:i=2430:add=off:aac=none:nm=16_2839 on theBenchmark for (2839ds/2430Mi) % 124.50/18.44 % (3663619)Instruction limit reached! % 124.50/18.44 % (3663619)------------------------------ % 124.50/18.44 % (3663619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.50/18.44 % (3663619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.50/18.44 % (3663619)CaDiCaL version: 2.1.3 % 124.50/18.44 % (3663619)Termination reason: Instruction limit % 124.50/18.44 % (3663619)Termination phase: Saturation % 124.50/18.44 % (3663619)Time elapsed: 1.259 s % 124.50/18.44 % (3663619)Peak memory usage: 139 MB % 124.50/18.44 % (3663619)Instructions burned: 2037 (million) % 124.50/18.44 % (3663626)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=2313596613:cond=fast:i=4891_2838 on theBenchmark for (2838ds/4891Mi) % 124.50/18.44 % (3663622)Instruction limit reached! % 124.50/18.44 % (3663622)------------------------------ % 124.50/18.44 % (3663622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.50/18.44 % (3663622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.50/18.44 % (3663622)CaDiCaL version: 2.1.3 % 124.50/18.44 % (3663622)Termination reason: Instruction limit % 124.50/18.44 % (3663622)Termination phase: Saturation % 124.50/18.44 % (3663622)Time elapsed: 1.421 s % 124.50/18.44 % (3663622)Peak memory usage: 138 MB % 124.50/18.44 % (3663622)Instructions burned: 2110 (million) % 124.50/18.44 % (3663624)Instruction limit reached! % 124.50/18.44 % (3663624)------------------------------ % 124.50/18.44 % (3663624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 124.50/18.45 % (3663624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 124.50/18.45 % (3663624)CaDiCaL version: 2.1.3 % 124.50/18.45 % (3663624)Termination reason: Instruction limit % 124.50/18.45 % (3663624)Termination phase: Saturation % 124.50/18.45 % (3663624)Time elapsed: 0.848 s % 124.50/18.45 % (3663624)Peak memory usage: 139 MB % 124.50/18.45 % (3663624)Instructions burned: 2433 (million) % 124.50/18.45 % (3663628)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=3446981753:st=2:i=14845:sd=2:ss=included:fsd=on_2831 on theBenchmark for (2831ds/14845Mi) % 124.50/18.45 % (3663629)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=499174406:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2830 on theBenchmark for (2830ds/7534Mi) % 124.50/18.45 [W928 07:03:15.350959892 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.350995356 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351023450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351031492 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351045172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351050928 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351063919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351069750 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351095479 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351101253 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351114216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 [W928 07:03:15.351119832 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 125.72/18.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 125.72/18.68 % (3663629)Refutation not found, incomplete strategy % 125.72/18.68 % (3663629)------------------------------ % 125.72/18.68 % (3663629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 125.72/18.68 % (3663629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 125.72/18.68 % (3663629)CaDiCaL version: 2.1.3 % 125.72/18.68 % (3663629)Termination reason: Refutation not found, incomplete strategy % 125.72/18.68 % (3663629)Time elapsed: 0.295 s % 125.72/18.68 % (3663629)Peak memory usage: 126 MB % 125.72/18.68 % (3663629)Instructions burned: 826 (million) % 130.24/19.35 [W928 07:03:15.495391660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495423647 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495460800 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495473077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495500130 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495511517 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495538690 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495550037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495576067 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495587240 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495612594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 [W928 07:03:15.495623747 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 130.24/19.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 130.24/19.35 % (3663629)------------------------------ % 130.24/19.35 % (3663629)------------------------------ % 130.24/19.35 % (3663628)Refutation not found, incomplete strategy % 130.24/19.35 % (3663628)------------------------------ % 130.24/19.35 % (3663628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 130.24/19.35 % (3663628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 137.16/20.24 % (3663628)CaDiCaL version: 2.1.3 % 137.16/20.24 % (3663628)Termination reason: Refutation not found, incomplete strategy % 137.16/20.24 % (3663628)Time elapsed: 0.553 s % 137.16/20.24 % (3663628)Peak memory usage: 125 MB % 137.16/20.24 % (3663628)Instructions burned: 827 (million) % 137.16/20.24 % (3663632)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=1251340332:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2824 on theBenchmark for (2824ds/10353Mi) % 137.16/20.24 [W928 07:03:15.900849490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900887310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900907203 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900915171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900928333 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900933770 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900946908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900953750 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900967305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900973535 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900986495 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 137.16/20.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 137.16/20.24 [W928 07:03:15.900992974 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.50/20.62 % (3663628)------------------------------ % 139.50/20.62 % (3663628)------------------------------ % 139.50/20.62 % (3663632)Refutation not found, incomplete strategy % 139.50/20.62 % (3663632)------------------------------ % 139.50/20.62 % (3663632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.50/20.62 % (3663632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/20.62 % (3663632)CaDiCaL version: 2.1.3 % 139.50/20.62 % (3663632)Termination reason: Refutation not found, incomplete strategy % 139.50/20.62 % (3663632)Time elapsed: 0.313 s % 139.50/20.62 % (3663632)Peak memory usage: 125 MB % 139.50/20.62 % (3663632)Instructions burned: 826 (million) % 139.50/20.62 % (3663634)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=716948181:i=7860_2821 on theBenchmark for (2821ds/7860Mi) % 139.50/20.62 % (3663634)Refutation not found, incomplete strategy % 139.50/20.62 % (3663634)------------------------------ % 139.50/20.62 % (3663634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.50/20.62 % (3663634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/20.62 % (3663634)CaDiCaL version: 2.1.3 % 139.50/20.62 % (3663634)Termination reason: Refutation not found, incomplete strategy % 139.50/20.62 % (3663634)Time elapsed: 0.005 s % 139.50/20.62 % (3663634)Peak memory usage: 88 MB % 139.50/20.62 % (3663634)Instructions burned: 8 (million) % 139.50/20.62 % (3663632)------------------------------ % 139.50/20.62 % (3663632)------------------------------ % 139.50/20.62 % (3663634)------------------------------ % 139.50/20.62 % (3663634)------------------------------ % 139.50/20.62 % (3663586)Instruction limit reached! % 139.50/20.62 % (3663586)------------------------------ % 139.50/20.62 % (3663586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 139.50/20.62 % (3663586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 139.50/20.62 % (3663586)CaDiCaL version: 2.1.3 % 139.50/20.62 % (3663586)Termination reason: Instruction limit % 139.50/20.62 % (3663586)Termination phase: Saturation % 139.50/20.62 % (3663586)Time elapsed: 8.345 s % 139.50/20.62 % (3663586)Peak memory usage: 238 MB % 139.50/20.62 % (3663586)Instructions burned: 13495 (million) % 139.50/20.62 % (3663636)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=854820957:i=7896:sd=2:bs=on:ss=included:sgt=20_2818 on theBenchmark for (2818ds/7896Mi) % 139.50/20.62 % (3663637)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=151347569:i=5812:gtgl=2:gtg=all_2817 on theBenchmark for (2817ds/5812Mi) % 139.50/20.62 % (3663638)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=2678409751:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2817 on theBenchmark for (2817ds/2965Mi) % 139.50/20.62 [W928 07:03:16.572970308 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.50/20.62 [W928 07:03:16.573010220 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.50/20.62 [W928 07:03:16.573031103 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.50/20.62 [W928 07:03:16.573037687 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/20.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 139.50/20.62 [W928 07:03:16.573051007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573056420 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573070746 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573076143 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573088707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573094070 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573107037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 [W928 07:03:16.573112761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 140.85/20.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 140.85/20.99 % (3663636)Refutation not found, incomplete strategy % 140.85/20.99 % (3663636)------------------------------ % 140.85/20.99 % (3663636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.85/20.99 % (3663636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.85/20.99 % (3663636)CaDiCaL version: 2.1.3 % 140.85/20.99 % (3663636)Termination reason: Refutation not found, incomplete strategy % 140.85/20.99 % (3663636)Time elapsed: 0.317 s % 140.85/20.99 % (3663636)Peak memory usage: 125 MB % 140.85/20.99 % (3663636)Instructions burned: 828 (million) % 140.85/20.99 % (3663636)------------------------------ % 140.85/20.99 % (3663636)------------------------------ % 140.85/20.99 % (3663642)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=609167885:i=2967:kws=precedence:bd=preordered:av=off_2812 on theBenchmark for (2812ds/2967Mi) % 140.85/20.99 % (3663638)Refutation not found, incomplete strategy % 140.85/20.99 % (3663638)------------------------------ % 140.85/20.99 % (3663638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 140.85/20.99 % (3663638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 140.85/20.99 % (3663638)CaDiCaL version: 2.1.3 % 140.85/20.99 % (3663638)Termination reason: Refutation not found, incomplete strategy % 140.85/20.99 % (3663638)Time elapsed: 0.600 s % 140.85/20.99 % (3663638)Peak memory usage: 130 MB % 140.85/20.99 % (3663638)Instructions burned: 885 (million) % 140.85/20.99 % (3663638)------------------------------ % 140.85/20.99 % (3663638)------------------------------ % 140.85/20.99 % (3663644)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=888064195:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2807 on theBenchmark for (2807ds/3022Mi) % 145.76/21.57 % (3663626)Instruction limit reached! % 145.76/21.57 % (3663626)------------------------------ % 145.76/21.57 % (3663626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 145.76/21.57 % (3663626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 145.76/21.57 % (3663626)CaDiCaL version: 2.1.3 % 145.76/21.57 % (3663626)Termination reason: Instruction limit % 145.76/21.57 % (3663626)Termination phase: Saturation % 145.76/21.57 % (3663626)Time elapsed: 3.289 s % 145.76/21.57 % (3663626)Peak memory usage: 165 MB % 145.76/21.57 % (3663626)Instructions burned: 4892 (million) % 145.76/21.57 % (3663646)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=308709732:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2803 on theBenchmark for (2803ds/3207Mi) % 145.76/21.57 [W928 07:03:17.846467044 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846496004 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846532951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846554931 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846580528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846592108 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846618158 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846634288 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846659824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846671208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 145.76/21.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 145.76/21.57 [W928 07:03:17.846696558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:17.846707861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 % (3663642)Instruction limit reached! % 155.63/22.88 % (3663642)------------------------------ % 155.63/22.88 % (3663642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.63/22.88 % (3663642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.63/22.88 % (3663642)CaDiCaL version: 2.1.3 % 155.63/22.88 % (3663642)Termination reason: Instruction limit % 155.63/22.88 % (3663642)Termination phase: Saturation % 155.63/22.88 % (3663642)Time elapsed: 0.985 s % 155.63/22.88 % (3663642)Peak memory usage: 147 MB % 155.63/22.88 % (3663642)Instructions burned: 2971 (million) % 155.63/22.88 % (3663644)Refutation not found, incomplete strategy % 155.63/22.88 % (3663644)------------------------------ % 155.63/22.88 % (3663644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 155.63/22.88 % (3663644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 155.63/22.88 % (3663644)CaDiCaL version: 2.1.3 % 155.63/22.88 % (3663644)Termination reason: Refutation not found, incomplete strategy % 155.63/22.88 % (3663644)Time elapsed: 0.545 s % 155.63/22.88 % (3663644)Peak memory usage: 125 MB % 155.63/22.88 % (3663644)Instructions burned: 822 (million) % 155.63/22.88 % (3663648)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=3581923796:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2801 on theBenchmark for (2801ds/3289Mi) % 155.63/22.88 [W928 07:03:18.217984541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218026034 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218064084 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218077488 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218103844 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218115271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218141471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 155.63/22.88 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 155.63/22.88 [W928 07:03:18.218152701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 [W928 07:03:18.218177318 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 [W928 07:03:18.218199311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 [W928 07:03:18.218225414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 [W928 07:03:18.218235701 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 % (3663644)------------------------------ % 193.86/28.30 % (3663644)------------------------------ % 193.86/28.30 % (3663646)Refutation not found, incomplete strategy % 193.86/28.30 % (3663646)------------------------------ % 193.86/28.30 % (3663646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.86/28.30 % (3663646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.86/28.30 % (3663646)CaDiCaL version: 2.1.3 % 193.86/28.30 % (3663646)Termination reason: Refutation not found, incomplete strategy % 193.86/28.30 % (3663646)Time elapsed: 0.535 s % 193.86/28.30 % (3663646)Peak memory usage: 126 MB % 193.86/28.30 % (3663646)Instructions burned: 826 (million) % 193.86/28.30 % (3663648)Refutation not found, incomplete strategy % 193.86/28.30 % (3663648)------------------------------ % 193.86/28.30 % (3663648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 193.86/28.30 % (3663648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 193.86/28.30 % (3663648)CaDiCaL version: 2.1.3 % 193.86/28.30 % (3663648)Termination reason: Refutation not found, incomplete strategy % 193.86/28.30 % (3663648)Time elapsed: 0.351 s % 193.86/28.30 % (3663648)Peak memory usage: 128 MB % 193.86/28.30 % (3663648)Instructions burned: 885 (million) % 193.86/28.30 % (3663650)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=3221838437:i=38569:sd=3:ss=axioms:sgt=32_2798 on theBenchmark for (2798ds/38569Mi) % 193.86/28.30 % (3663646)------------------------------ % 193.86/28.30 % (3663646)------------------------------ % 193.86/28.30 % (3663648)------------------------------ % 193.86/28.30 % (3663648)------------------------------ % 193.86/28.30 % (3663652)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=648213710:cts=off:i=3394_2795 on theBenchmark for (2795ds/3394Mi) % 193.86/28.30 % (3663654)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=1191484384:i=33824:bd=preordered_2794 on theBenchmark for (2794ds/33824Mi) % 193.86/28.30 [W928 07:03:18.798377937 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 [W928 07:03:18.798413354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 193.86/28.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 193.86/28.30 [W928 07:03:18.798451647 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798464451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798490141 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798512394 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798540391 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798550771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798575378 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798585741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798611698 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 [W928 07:03:18.798622274 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 218.33/31.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 218.33/31.71 % (3663650)Refutation not found, incomplete strategy % 218.33/31.71 % (3663650)------------------------------ % 218.33/31.71 % (3663650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.33/31.71 % (3663650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.33/31.71 % (3663650)CaDiCaL version: 2.1.3 % 218.33/31.71 % (3663650)Termination reason: Refutation not found, incomplete strategy % 218.33/31.71 % (3663650)Time elapsed: 0.539 s % 218.33/31.71 % (3663650)Peak memory usage: 125 MB % 218.33/31.71 % (3663650)Instructions burned: 823 (million) % 218.33/31.71 % (3663650)------------------------------ % 218.33/31.71 % (3663650)------------------------------ % 218.33/31.71 % (3663656)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=1198007059:i=20684:bd=all:gtg=exists_sym_2789 on theBenchmark for (2789ds/20684Mi) % 218.33/31.71 % (3663637)Instruction limit reached! % 218.33/31.71 % (3663637)------------------------------ % 218.33/31.71 % (3663637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 218.33/31.71 % (3663637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 218.33/31.71 % (3663637)CaDiCaL version: 2.1.3 % 218.33/31.71 % (3663637)Termination reason: Instruction limit % 236.49/34.25 % (3663637)Termination phase: Saturation % 236.49/34.25 % (3663637)Time elapsed: 3.683 s % 236.49/34.25 % (3663637)Peak memory usage: 172 MB % 236.49/34.25 % (3663637)Instructions burned: 5813 (million) % 236.49/34.25 % (3663658)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=975133646: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_2779 on theBenchmark for (2779ds/7222Mi) % 236.49/34.25 % (3663652)Instruction limit reached! % 236.49/34.25 % (3663652)------------------------------ % 236.49/34.25 % (3663652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.49/34.25 % (3663652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.49/34.25 % (3663652)CaDiCaL version: 2.1.3 % 236.49/34.25 % (3663652)Termination reason: Instruction limit % 236.49/34.25 % (3663652)Termination phase: Saturation % 236.49/34.25 % (3663652)Time elapsed: 1.934 s % 236.49/34.25 % (3663652)Peak memory usage: 146 MB % 236.49/34.25 % (3663652)Instructions burned: 3395 (million) % 236.49/34.25 % (3663660)ott-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:spb=goal_then_units:random_seed=3404936829:st=4:i=7295:sd=4:ep=R:ss=axioms_2775 on theBenchmark for (2775ds/7295Mi) % 236.49/34.25 % (3663658)Instruction limit reached! % 236.49/34.25 % (3663658)------------------------------ % 236.49/34.25 % (3663658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.49/34.25 % (3663658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.49/34.25 % (3663658)CaDiCaL version: 2.1.3 % 236.49/34.25 % (3663658)Termination reason: Instruction limit % 236.49/34.25 % (3663658)Termination phase: Saturation % 236.49/34.25 % (3663658)Time elapsed: 2.869 s % 236.49/34.25 % (3663658)Peak memory usage: 131 MB % 236.49/34.25 % (3663658)Instructions burned: 7223 (million) % 236.49/34.25 % (3663662)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=1227246859:i=4036:ins=10_2749 on theBenchmark for (2749ds/4036Mi) % 236.49/34.25 % (3663595)Instruction limit reached! % 236.49/34.25 % (3663595)------------------------------ % 236.49/34.25 % (3663595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.49/34.25 % (3663595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.49/34.25 % (3663595)CaDiCaL version: 2.1.3 % 236.49/34.25 % (3663595)Termination reason: Instruction limit % 236.49/34.25 % (3663595)Termination phase: Saturation % 236.49/34.25 % (3663595)Time elapsed: 15.066 s % 236.49/34.25 % (3663595)Peak memory usage: 1253 MB % 236.49/34.25 % (3663595)Instructions burned: 26473 (million) % 236.49/34.25 % (3663664)lrs+10_1_sil=128000:lcm=predicate:random_seed=1094295123:st=3:i=43697:sd=5:ss=axioms_2731 on theBenchmark for (2731ds/43697Mi) % 236.49/34.25 % (3663664)Refutation not found, incomplete strategy % 236.49/34.25 % (3663664)------------------------------ % 236.49/34.25 % (3663664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.49/34.25 % (3663664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.49/34.25 % (3663664)CaDiCaL version: 2.1.3 % 236.49/34.25 % (3663664)Termination reason: Refutation not found, incomplete strategy % 236.49/34.25 % (3663664)Time elapsed: 0.001 s % 236.49/34.25 % (3663664)Peak memory usage: 87 MB % 236.49/34.25 % (3663664)------------------------------ % 236.49/34.25 % (3663664)------------------------------ % 236.49/34.25 % (3663660)Instruction limit reached! % 236.49/34.25 % (3663660)------------------------------ % 236.49/34.25 % (3663660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 236.49/34.25 % (3663660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 236.49/34.25 % (3663660)CaDiCaL version: 2.1.3 % 236.49/34.25 % (3663660)Termination reason: Instruction limit % 236.49/34.25 % (3663660)Termination phase: Saturation % 236.49/34.25 % (3663660)Time elapsed: 4.655 s % 236.49/34.25 % (3663660)Peak memory usage: 166 MB % 236.49/34.25 % (3663660)Instructions burned: 7295 (million) % 236.49/34.25 % (3663666)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=1708864626:i=17599:gtg=all:ss=axioms:fsd=on_2727 on theBenchmark for (2727ds/17599Mi) % 236.49/34.25 % (3663667)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=1915316494:i=4547:bd=preordered_2727 on theBenchmark for (2727ds/4547Mi) % 239.52/34.80 % (3663662)Instruction limit reached! % 239.52/34.80 % (3663662)------------------------------ % 239.52/34.80 % (3663662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.80 % (3663662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.80 % (3663662)CaDiCaL version: 2.1.3 % 239.52/34.80 % (3663662)Termination reason: Instruction limit % 239.52/34.80 % (3663662)Termination phase: Saturation % 239.52/34.80 % (3663662)Time elapsed: 2.396 s % 239.52/34.80 % (3663662)Peak memory usage: 156 MB % 239.52/34.80 % (3663662)Instructions burned: 4036 (million) % 239.52/34.80 % (3663670)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=1794602261:i=9294:av=off_2724 on theBenchmark for (2724ds/9294Mi) % 239.52/34.80 % (3663656)Instruction limit reached! % 239.52/34.80 % (3663656)------------------------------ % 239.52/34.80 % (3663656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.80 % (3663656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.80 % (3663656)CaDiCaL version: 2.1.3 % 239.52/34.80 % (3663656)Termination reason: Instruction limit % 239.52/34.80 % (3663656)Termination phase: Saturation % 239.52/34.80 % (3663656)Time elapsed: 6.828 s % 239.52/34.80 % (3663656)Peak memory usage: 303 MB % 239.52/34.80 % (3663656)Instructions burned: 20686 (million) % 239.52/34.80 % (3663672)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=358425471:i=32849:add=on_2720 on theBenchmark for (2720ds/32849Mi) % 239.52/34.80 % (3663667)Instruction limit reached! % 239.52/34.80 % (3663667)------------------------------ % 239.52/34.80 % (3663667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 239.52/34.80 % (3663667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 239.52/34.80 % (3663667)CaDiCaL version: 2.1.3 % 239.52/34.80 % (3663667)Termination reason: Instruction limit % 239.52/34.80 % (3663667)Termination phase: Saturation % 239.52/34.80 % (3663667)Time elapsed: 2.901 s % 239.52/34.80 % (3663667)Peak memory usage: 161 MB % 239.52/34.80 % (3663667)Instructions burned: 4547 (million) % 239.52/34.80 % (3663674)dis-1011_1_ncem=casc2026/models/loop5.pt:sil=64000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1430115845:st=1.5:i=4793:s2at=3:sd=3:fsr=off:ss=axioms_2696 on theBenchmark for (2696ds/4793Mi) % 239.52/34.80 [W928 07:03:28.931663500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.52/34.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.52/34.80 [W928 07:03:28.931704950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.52/34.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.52/34.80 [W928 07:03:28.931746604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.52/34.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.52/34.80 [W928 07:03:28.931758387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.52/34.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.52/34.80 [W928 07:03:28.931783871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.52/34.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 239.52/34.80 [W928 07:03:28.931793881 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 239.52/34.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 [W928 07:03:28.931818557 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 286.91/41.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 [W928 07:03:28.931829221 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 286.91/41.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 [W928 07:03:28.931860264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 286.91/41.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 [W928 07:03:28.931870427 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 286.91/41.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 [W928 07:03:28.931895304 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 286.91/41.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 [W928 07:03:28.931905291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript. % 286.91/41.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList) % 286.91/41.36 % (3663674)Refutation not found, incomplete strategy % 286.91/41.36 % (3663674)------------------------------ % 286.91/41.36 % (3663674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.91/41.36 % (3663674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.91/41.36 % (3663674)CaDiCaL version: 2.1.3 % 286.91/41.36 % (3663674)Termination reason: Refutation not found, incomplete strategy % 286.91/41.36 % (3663674)Time elapsed: 0.550 s % 286.91/41.36 % (3663674)Peak memory usage: 126 MB % 286.91/41.36 % (3663674)Instructions burned: 826 (million) % 286.91/41.36 % (3663674)------------------------------ % 286.91/41.36 % (3663674)------------------------------ % 286.91/41.36 % (3663676)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=2846938061:i=4840:nm=4:av=off_2687 on theBenchmark for (2687ds/4840Mi) % 286.91/41.36 % (3663676)Refutation not found, incomplete strategy % 286.91/41.36 % (3663676)------------------------------ % 286.91/41.36 % (3663676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.91/41.36 % (3663676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.91/41.36 % (3663676)CaDiCaL version: 2.1.3 % 286.91/41.36 % (3663676)Termination reason: Refutation not found, incomplete strategy % 286.91/41.36 % (3663676)Time elapsed: 0.587 s % 286.91/41.36 % (3663676)Peak memory usage: 128 MB % 286.91/41.36 % (3663676)Instructions burned: 887 (million) % 286.91/41.36 % (3663676)------------------------------ % 286.91/41.36 % (3663676)------------------------------ % 286.91/41.36 % (3663678)lrs-1004_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:gs=on:newcnf=on:random_seed=2861551761:cts=off:i=5002_2677 on theBenchmark for (2677ds/5002Mi) % 286.91/41.36 % (3663670)Instruction limit reached! % 286.91/41.36 % (3663670)------------------------------ % 286.91/41.36 % (3663670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 286.91/41.36 % (3663670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 286.91/41.36 % (3663670)CaDiCaL version: 2.1.3 % 286.91/41.36 % (3663670)Termination reason: Instruction limit % 286.91/41.36 % (3663670)Termination phase: Saturation % 286.91/41.36 % (3663670)Time elapsed: 5.542 s % 286.91/41.36 % (3663670)Peak memory usage: 175 MB % 286.91/41.36 % (3663670)Instructions burned: 9294 (million) % 286.91/41.36 % (3663680)dis+1010_1_ncem=cascTerminated %------------------------------------------------------------------------------