%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HAL007+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:18:53 AM UTC 2026
% Result : Satisfiable 68.65s 10.70s
% Output : Saturation 68.65s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u31,axiom,
( ~ element(X2,X0)
| ~ element(X1,X0)
| subtract(X0,X1,subtract(X0,X1,X2)) = X2 ) ).
cnf(u30,axiom,
( ~ element(X1,X0)
| subtract(X0,X1,X1) = zero(X0) ) ).
cnf(u29,axiom,
( ~ element(X2,X0)
| ~ element(X1,X0)
| element(subtract(X0,X1,X2),X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HAL007+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n017.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 10:44:35 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.73/1.43 % (2364059)Detected formulas, will run a generic FOF schedule.
% 3.73/1.43 % (2364068)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2917821975:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.73/1.43 % (2364068)Refutation not found, incomplete strategy
% 3.73/1.43 % (2364068)------------------------------
% 3.73/1.43 % (2364068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.43 % (2364068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.43 % (2364068)CaDiCaL version: 2.1.3
% 3.73/1.43 % (2364068)Termination reason: Refutation not found, incomplete strategy
% 3.73/1.43 % (2364068)Time elapsed: 0.0000 s
% 3.73/1.43 % (2364068)Peak memory usage: 86 MB
% 3.73/1.43 % (2364066)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=2285705192:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.73/1.43 % (2364065)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=3163478820:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.73/1.43 % (2364064)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=723648022:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.73/1.43 % (2364070)dis-21_1_sil=8000:lcm=predicate:random_seed=3743393872: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.73/1.43 % (2364067)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2568419078:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.73/1.43 % (2364069)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2825509582:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.73/1.43 % (2364067)Refutation not found, incomplete strategy
% 3.73/1.43 % (2364067)------------------------------
% 3.73/1.43 % (2364067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.43 % (2364070)Refutation not found, incomplete strategy
% 3.73/1.43 % (2364070)------------------------------
% 3.73/1.43 % (2364070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.43 % (2364067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.43 % (2364070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.43 % (2364070)CaDiCaL version: 2.1.3
% 3.73/1.43 % (2364067)CaDiCaL version: 2.1.3
% 3.73/1.43 % (2364070)Termination reason: Refutation not found, incomplete strategy
% 3.73/1.43 % (2364070)Time elapsed: 0.0000 s
% 3.73/1.43 % (2364067)Termination reason: Refutation not found, incomplete strategy
% 3.73/1.43 % (2364067)Time elapsed: 0.0000 s
% 3.73/1.43 % (2364067)Peak memory usage: 86 MB
% 3.73/1.43 % (2364070)Peak memory usage: 86 MB
% 3.73/1.43 % (2364069)Refutation not found, incomplete strategy
% 3.73/1.43 % (2364069)------------------------------
% 3.73/1.43 % (2364069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.43 % (2364069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.43 % (2364069)CaDiCaL version: 2.1.3
% 3.73/1.43 % (2364069)Termination reason: Refutation not found, incomplete strategy
% 3.73/1.43 % (2364069)Time elapsed: 0.001 s
% 3.73/1.43 % (2364069)Peak memory usage: 88 MB
% 3.73/1.43 % (2364068)------------------------------
% 3.73/1.43 % (2364068)------------------------------
% 3.73/1.43 % (2364078)lrs+10_1_sil=8000:sp=occurrence:random_seed=116977230:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.73/1.43 % (2364078)Refutation not found, incomplete strategy
% 3.73/1.43 % (2364078)------------------------------
% 3.73/1.43 % (2364078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.43 % (2364078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.43 % (2364078)CaDiCaL version: 2.1.3
% 3.73/1.43 % (2364078)Termination reason: Refutation not found, incomplete strategy
% 3.73/1.43 % (2364078)Time elapsed: 0.0000 s
% 3.73/1.43 % (2364078)Peak memory usage: 86 MB
% 3.73/1.43 % (2364069)------------------------------
% 3.73/1.43 % (2364069)------------------------------
% 3.73/1.43 % (2364067)------------------------------
% 3.73/1.43 % (2364067)------------------------------
% 6.80/1.83 % (2364070)------------------------------
% 6.80/1.83 % (2364070)------------------------------
% 6.80/1.83 [W927 10:44:36.289998470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290045717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290083047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290105990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290133284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290143461 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290167951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290178068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290202624 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290212908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290237581 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290248178 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.80/1.83 [W927 10:44:36.290450893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.80/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290474830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290511567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290523210 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290551660 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290561934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290586604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290596587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290620561 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290630437 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290654034 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 [W927 10:44:36.290664034 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 9.79/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.79/2.24 % (2364078)------------------------------
% 9.79/2.24 % (2364078)------------------------------
% 9.79/2.24 % (2364081)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3428015984:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 9.79/2.24 % (2364080)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3239863864:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 9.79/2.24 % (2364082)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=3891943965:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.79/2.24 % (2364081)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364081)------------------------------
% 10.20/2.32 % (2364081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364080)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364080)------------------------------
% 10.20/2.32 % (2364080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364081)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364081)Termination reason: Refutation not found, incomplete strategy
% 10.20/2.32 % (2364081)Time elapsed: 0.001 s
% 10.20/2.32 % (2364080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364081)Peak memory usage: 86 MB
% 10.20/2.32 % (2364080)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364080)Termination reason: Refutation not found, incomplete strategy
% 10.20/2.32 % (2364080)Time elapsed: 0.001 s
% 10.20/2.32 % (2364080)Peak memory usage: 86 MB
% 10.20/2.32 % (2364082)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364082)------------------------------
% 10.20/2.32 % (2364082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364082)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364082)Termination reason: Refutation not found, incomplete strategy
% 10.20/2.32 % (2364082)Time elapsed: 0.001 s
% 10.20/2.32 % (2364082)Peak memory usage: 88 MB
% 10.20/2.32 % (2364083)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1381705293:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 10.20/2.32 % (2364083)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364083)------------------------------
% 10.20/2.32 % (2364083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364083)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364083)Termination reason: Refutation not found, incomplete strategy
% 10.20/2.32 % (2364083)Time elapsed: 0.0000 s
% 10.20/2.32 % (2364083)Peak memory usage: 86 MB
% 10.20/2.32 % (2364065)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364065)------------------------------
% 10.20/2.32 % (2364065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364065)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364065)Termination reason: Refutation not found, incomplete strategy
% 10.20/2.32 % (2364065)Time elapsed: 0.554 s
% 10.20/2.32 % (2364065)Peak memory usage: 124 MB
% 10.20/2.32 % (2364065)Instructions burned: 821 (million)
% 10.20/2.32 % (2364066)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364066)------------------------------
% 10.20/2.32 % (2364066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364066)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364066)Termination reason: Refutation not found, incomplete strategy
% 10.20/2.32 % (2364066)Time elapsed: 0.555 s
% 10.20/2.32 % (2364066)Peak memory usage: 124 MB
% 10.20/2.32 % (2364066)Instructions burned: 821 (million)
% 10.20/2.32 % (2364081)------------------------------
% 10.20/2.32 % (2364081)------------------------------
% 10.20/2.32 % (2364080)------------------------------
% 10.20/2.32 % (2364080)------------------------------
% 10.20/2.32 % (2364082)------------------------------
% 10.20/2.32 % (2364082)------------------------------
% 10.20/2.32 % (2364083)------------------------------
% 10.20/2.32 % (2364083)------------------------------
% 10.20/2.32 % (2364065)------------------------------
% 10.20/2.32 % (2364065)------------------------------
% 10.20/2.32 % (2364066)------------------------------
% 10.20/2.32 % (2364066)------------------------------
% 10.20/2.32 % (2364091)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3464611026:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 10.20/2.32 % (2364091)Refutation not found, incomplete strategy
% 10.20/2.32 % (2364091)------------------------------
% 10.20/2.32 % (2364091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.20/2.32 % (2364091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.20/2.32 % (2364091)CaDiCaL version: 2.1.3
% 10.20/2.32 % (2364091)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.79 % (2364091)Time elapsed: 0.0000 s
% 12.52/2.79 % (2364091)Peak memory usage: 87 MB
% 12.52/2.79 % (2364088)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3184159687:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 12.52/2.79 % (2364090)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2426428745:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 12.52/2.79 % (2364089)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=665396039:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 12.52/2.79 % (2364089)Refutation not found, incomplete strategy
% 12.52/2.79 % (2364089)------------------------------
% 12.52/2.79 % (2364089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.79 % (2364089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.79 % (2364089)CaDiCaL version: 2.1.3
% 12.52/2.79 % (2364089)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.79 % (2364089)Time elapsed: 0.0000 s
% 12.52/2.79 % (2364089)Peak memory usage: 86 MB
% 12.52/2.79 % (2364090)Refutation not found, incomplete strategy
% 12.52/2.79 % (2364090)------------------------------
% 12.52/2.79 % (2364090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.79 % (2364090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.79 % (2364090)CaDiCaL version: 2.1.3
% 12.52/2.79 % (2364090)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.79 % (2364090)Time elapsed: 0.0000 s
% 12.52/2.79 % (2364090)Peak memory usage: 87 MB
% 12.52/2.79 % (2364091)------------------------------
% 12.52/2.79 % (2364091)------------------------------
% 12.52/2.79 % (2364097)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1788610025:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 12.52/2.79 % (2364096)lrs+10_1_sil=8000:sp=occurrence:random_seed=3071302755:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 12.52/2.79 % (2364097)Refutation not found, incomplete strategy
% 12.52/2.79 % (2364097)------------------------------
% 12.52/2.79 % (2364097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.79 % (2364096)Refutation not found, incomplete strategy
% 12.52/2.79 % (2364096)------------------------------
% 12.52/2.79 % (2364096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.79 % (2364097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.79 % (2364096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.79 % (2364096)CaDiCaL version: 2.1.3
% 12.52/2.79 % (2364097)CaDiCaL version: 2.1.3
% 12.52/2.79 % (2364097)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.79 % (2364097)Time elapsed: 0.001 s
% 12.52/2.79 % (2364096)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.79 % (2364096)Time elapsed: 0.001 s
% 12.52/2.79 % (2364097)Peak memory usage: 86 MB
% 12.52/2.79 % (2364096)Peak memory usage: 86 MB
% 12.52/2.79 % (2364089)------------------------------
% 12.52/2.79 % (2364089)------------------------------
% 12.52/2.79 % (2364090)------------------------------
% 12.52/2.79 % (2364090)------------------------------
% 12.52/2.79 % (2364098)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4026005964:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 12.52/2.79 % (2364097)------------------------------
% 12.52/2.79 % (2364097)------------------------------
% 12.52/2.79 % (2364096)------------------------------
% 12.52/2.79 % (2364096)------------------------------
% 12.52/2.79 % (2364101)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1751078943:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 12.52/2.79 % (2364102)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2839621202:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 12.52/2.79 % (2364101)Refutation not found, incomplete strategy
% 12.52/2.79 % (2364101)------------------------------
% 12.52/2.79 % (2364101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.79 % (2364101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.79 % (2364102)Refutation not found, incomplete strategy
% 12.52/2.79 % (2364102)------------------------------
% 12.52/2.79 % (2364102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.95/2.90 % (2364101)CaDiCaL version: 2.1.3
% 12.95/2.90 % (2364102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.95/2.90 % (2364101)Termination reason: Refutation not found, incomplete strategy
% 12.95/2.90 % (2364101)Time elapsed: 0.0000 s
% 12.95/2.90 % (2364101)Peak memory usage: 86 MB
% 12.95/2.90 % (2364102)CaDiCaL version: 2.1.3
% 12.95/2.90 % (2364102)Termination reason: Refutation not found, incomplete strategy
% 12.95/2.90 % (2364102)Time elapsed: 0.001 s
% 12.95/2.90 % (2364102)Peak memory usage: 86 MB
% 12.95/2.90 [W927 10:44:37.215187158 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215214698 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215235486 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215242040 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215255441 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215262043 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215275329 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215281710 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215294919 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215301409 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215314139 register_special_ops.cpp:225] Warning: Creating a tensor from 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.95/2.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.95/2.90 [W927 10:44:37.215320412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 17.09/3.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.09/3.36 % (2364107)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=172615612:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 17.09/3.36 % (2364106)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2010432843:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 17.09/3.36 % (2364107)Refutation not found, incomplete strategy
% 17.09/3.36 % (2364107)------------------------------
% 17.09/3.36 % (2364107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.36 % (2364107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.36 % (2364107)CaDiCaL version: 2.1.3
% 17.09/3.36 % (2364107)Termination reason: Refutation not found, incomplete strategy
% 17.09/3.36 % (2364107)Time elapsed: 0.001 s
% 17.09/3.36 % (2364107)Peak memory usage: 87 MB
% 17.09/3.36 % (2364098)Refutation not found, incomplete strategy
% 17.09/3.36 % (2364098)------------------------------
% 17.09/3.36 % (2364098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.36 % (2364098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.36 % (2364098)CaDiCaL version: 2.1.3
% 17.09/3.36 % (2364098)Termination reason: Refutation not found, incomplete strategy
% 17.09/3.36 % (2364098)Time elapsed: 0.311 s
% 17.09/3.36 % (2364098)Peak memory usage: 125 MB
% 17.09/3.36 % (2364098)Instructions burned: 826 (million)
% 17.09/3.36 % (2364101)------------------------------
% 17.09/3.36 % (2364101)------------------------------
% 17.09/3.36 % (2364102)------------------------------
% 17.09/3.36 % (2364102)------------------------------
% 17.09/3.36 % (2364098)------------------------------
% 17.09/3.36 % (2364098)------------------------------
% 17.09/3.36 % (2364107)------------------------------
% 17.09/3.36 % (2364107)------------------------------
% 17.09/3.36 % (2364111)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3234103338:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 17.09/3.36 % (2364110)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=430209508:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 17.09/3.36 % (2364111)Refutation not found, incomplete strategy
% 17.09/3.36 % (2364111)------------------------------
% 17.09/3.36 % (2364111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.36 % (2364111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.36 % (2364111)CaDiCaL version: 2.1.3
% 17.09/3.36 % (2364111)Termination reason: Refutation not found, incomplete strategy
% 17.09/3.36 % (2364111)Time elapsed: 0.0000 s
% 17.09/3.36 % (2364111)Peak memory usage: 86 MB
% 17.09/3.36 % (2364112)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=608263791:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 17.09/3.36 % (2364112)Refutation not found, incomplete strategy
% 17.09/3.36 % (2364112)------------------------------
% 17.09/3.36 % (2364112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.36 % (2364112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.36 % (2364112)CaDiCaL version: 2.1.3
% 17.09/3.36 % (2364112)Termination reason: Refutation not found, incomplete strategy
% 17.09/3.36 % (2364112)Time elapsed: 0.0000 s
% 17.09/3.36 % (2364112)Peak memory usage: 86 MB
% 17.09/3.36 % (2364110)Instruction limit reached!
% 17.09/3.36 % (2364110)------------------------------
% 17.09/3.36 % (2364110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.09/3.36 % (2364110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.09/3.36 % (2364110)CaDiCaL version: 2.1.3
% 17.09/3.36 % (2364110)Termination reason: Instruction limit
% 17.09/3.36 % (2364110)Termination phase: Saturation
% 17.09/3.36 % (2364110)Time elapsed: 0.073 s
% 17.09/3.36 % (2364110)Peak memory usage: 89 MB
% 17.09/3.36 % (2364110)Instructions burned: 136 (million)
% 17.09/3.36 [W927 10:44:37.683162470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683196434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683236544 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683247757 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683335791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683353518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683380385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683390531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683414628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683424735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683448749 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 [W927 10:44:37.683458862 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.85/3.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.85/3.81 % (2364115)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=3204803046:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 19.85/3.81 % (2364112)------------------------------
% 19.85/3.81 % (2364112)------------------------------
% 19.85/3.81 % (2364111)------------------------------
% 19.85/3.81 % (2364111)------------------------------
% 19.85/3.81 % (2364117)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=193270519:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2981 on theBenchmark for (2981ds/150Mi)
% 19.85/3.85 % (2364117)Refutation not found, incomplete strategy
% 19.85/3.85 % (2364117)------------------------------
% 19.85/3.85 % (2364117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/3.85 % (2364117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/3.85 % (2364117)CaDiCaL version: 2.1.3
% 19.85/3.85 % (2364117)Termination reason: Refutation not found, incomplete strategy
% 19.85/3.85 % (2364117)Time elapsed: 0.002 s
% 19.85/3.85 % (2364117)Peak memory usage: 88 MB
% 19.85/3.85 % (2364106)Refutation not found, incomplete strategy
% 19.85/3.85 % (2364106)------------------------------
% 19.85/3.85 % (2364106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/3.85 % (2364106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/3.85 % (2364106)CaDiCaL version: 2.1.3
% 19.85/3.85 % (2364106)Termination reason: Refutation not found, incomplete strategy
% 19.85/3.85 % (2364106)Time elapsed: 0.560 s
% 19.85/3.85 % (2364106)Peak memory usage: 125 MB
% 19.85/3.85 % (2364106)Instructions burned: 825 (million)
% 19.85/3.85 % (2364119)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=403713892:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi)
% 19.85/3.85 % (2364121)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1703496551:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi)
% 19.85/3.85 % (2364121)Refutation not found, incomplete strategy
% 19.85/3.85 % (2364121)------------------------------
% 19.85/3.85 % (2364121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/3.85 % (2364121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/3.85 % (2364121)CaDiCaL version: 2.1.3
% 19.85/3.85 % (2364121)Termination reason: Refutation not found, incomplete strategy
% 19.85/3.85 % (2364121)Time elapsed: 0.001 s
% 19.85/3.85 % (2364121)Peak memory usage: 87 MB
% 19.85/3.85 % (2364117)------------------------------
% 19.85/3.85 % (2364117)------------------------------
% 19.85/3.85 % (2364088)Instruction limit reached!
% 19.85/3.85 % (2364088)------------------------------
% 19.85/3.85 % (2364088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/3.85 % (2364088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/3.85 % (2364088)CaDiCaL version: 2.1.3
% 19.85/3.85 % (2364088)Termination reason: Instruction limit
% 19.85/3.85 % (2364088)Termination phase: Saturation
% 19.85/3.85 % (2364088)Time elapsed: 1.369 s
% 19.85/3.85 % (2364088)Peak memory usage: 136 MB
% 19.85/3.85 % (2364088)Instructions burned: 2351 (million)
% 19.85/3.85 % (2364106)------------------------------
% 19.85/3.85 % (2364106)------------------------------
% 19.85/3.85 % (2364121)------------------------------
% 19.85/3.85 % (2364121)------------------------------
% 19.85/3.85 % (2364124)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=2017241313:s2a=on:i=185:s2at=1.8:fdi=4_2976 on theBenchmark for (2976ds/185Mi)
% 19.85/3.85 % (2364124)Refutation not found, incomplete strategy
% 19.85/3.85 % (2364124)------------------------------
% 19.85/3.85 % (2364124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/3.85 % (2364124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/3.85 % (2364124)CaDiCaL version: 2.1.3
% 19.85/3.85 % (2364124)Termination reason: Refutation not found, incomplete strategy
% 19.85/3.85 % (2364124)Time elapsed: 0.002 s
% 19.85/3.85 % (2364124)Peak memory usage: 89 MB
% 19.85/3.85 % (2364119)Refutation not found, incomplete strategy
% 19.85/3.85 % (2364119)------------------------------
% 19.85/3.85 % (2364119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.85/3.85 % (2364119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.85/3.85 % (2364119)CaDiCaL version: 2.1.3
% 19.85/3.85 % (2364119)Termination reason: Refutation not found, incomplete strategy
% 19.85/3.85 % (2364119)Time elapsed: 0.351 s
% 19.85/3.85 % (2364119)Peak memory usage: 128 MB
% 19.85/3.85 % (2364119)Instructions burned: 894 (million)
% 19.85/3.85 % (2364125)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3886985333:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2976 on theBenchmark for (2976ds/193Mi)
% 23.77/4.24 % (2364125)Refutation not found, incomplete strategy
% 23.77/4.24 % (2364125)------------------------------
% 23.77/4.24 % (2364125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.77/4.24 % (2364125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.77/4.24 % (2364125)CaDiCaL version: 2.1.3
% 23.77/4.24 % (2364125)Termination reason: Refutation not found, incomplete strategy
% 23.77/4.24 % (2364125)Time elapsed: 0.001 s
% 23.77/4.24 % (2364125)Peak memory usage: 86 MB
% 23.77/4.24 % (2364126)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2697384605:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2976 on theBenchmark for (2976ds/4850Mi)
% 23.77/4.24 % (2364126)Refutation not found, incomplete strategy
% 23.77/4.24 % (2364126)------------------------------
% 23.77/4.24 % (2364126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.77/4.24 % (2364126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.77/4.24 % (2364126)CaDiCaL version: 2.1.3
% 23.77/4.24 % (2364126)Termination reason: Refutation not found, incomplete strategy
% 23.77/4.24 % (2364126)Time elapsed: 0.0000 s
% 23.77/4.24 % (2364126)Peak memory usage: 86 MB
% 23.77/4.24 % (2364115)Refutation not found, incomplete strategy
% 23.77/4.24 % (2364115)------------------------------
% 23.77/4.24 % (2364115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.77/4.24 % (2364115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.77/4.24 % (2364115)CaDiCaL version: 2.1.3
% 23.77/4.24 % (2364115)Termination reason: Refutation not found, incomplete strategy
% 23.77/4.24 % (2364115)Time elapsed: 0.611 s
% 23.77/4.24 % (2364115)Peak memory usage: 128 MB
% 23.77/4.24 % (2364115)Instructions burned: 897 (million)
% 23.77/4.24 % (2364127)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1957985450:i=12111:sd=1:ss=included_2975 on theBenchmark for (2975ds/12111Mi)
% 23.77/4.24 % (2364119)------------------------------
% 23.77/4.24 % (2364119)------------------------------
% 23.77/4.24 % (2364124)------------------------------
% 23.77/4.24 % (2364124)------------------------------
% 23.77/4.24 % (2364125)------------------------------
% 23.77/4.24 % (2364125)------------------------------
% 23.77/4.24 % (2364126)------------------------------
% 23.77/4.24 % (2364126)------------------------------
% 23.77/4.24 % (2364132)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3552010993:i=319:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/319Mi)
% 23.77/4.24 % (2364115)------------------------------
% 23.77/4.24 % (2364115)------------------------------
% 23.77/4.24 % (2364133)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=642270024:i=2064:ep=RST_2972 on theBenchmark for (2972ds/2064Mi)
% 23.77/4.24 % (2364133)Refutation not found, incomplete strategy
% 23.77/4.24 % (2364133)------------------------------
% 23.77/4.24 % (2364133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.77/4.24 % (2364133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.77/4.24 % (2364133)CaDiCaL version: 2.1.3
% 23.77/4.24 % (2364133)Termination reason: Refutation not found, incomplete strategy
% 23.77/4.24 % (2364133)Time elapsed: 0.001 s
% 23.77/4.24 % (2364133)Peak memory usage: 88 MB
% 23.77/4.24 % (2364134)dis-1011_128_sil=32000:random_seed=1633757830:i=3706:ep=RST:av=off_2972 on theBenchmark for (2972ds/3706Mi)
% 23.77/4.24 % (2364134)Refutation not found, incomplete strategy
% 23.77/4.24 % (2364134)------------------------------
% 23.77/4.24 % (2364134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.77/4.24 % (2364134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.77/4.24 % (2364134)CaDiCaL version: 2.1.3
% 23.77/4.24 % (2364134)Termination reason: Refutation not found, incomplete strategy
% 23.77/4.24 % (2364134)Time elapsed: 0.001 s
% 23.77/4.24 % (2364134)Peak memory usage: 88 MB
% 23.77/4.24 % (2364136)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2082720138:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2971 on theBenchmark for (2971ds/757Mi)
% 23.77/4.24 % (2364136)Refutation not found, incomplete strategy
% 23.77/4.24 % (2364136)------------------------------
% 23.77/4.24 % (2364136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.77/4.24 % (2364136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.65/4.41 % (2364136)CaDiCaL version: 2.1.3
% 24.65/4.41 % (2364136)Termination reason: Refutation not found, incomplete strategy
% 24.65/4.41 % (2364136)Time elapsed: 0.001 s
% 24.65/4.41 % (2364136)Peak memory usage: 86 MB
% 24.65/4.41 % (2364132)Instruction limit reached!
% 24.65/4.41 % (2364132)------------------------------
% 24.65/4.41 % (2364132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.65/4.41 % (2364132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.65/4.41 % (2364132)CaDiCaL version: 2.1.3
% 24.65/4.41 % (2364132)Termination reason: Instruction limit
% 24.65/4.41 % (2364132)Termination phase: Saturation
% 24.65/4.41 % (2364132)Time elapsed: 0.180 s
% 24.65/4.41 % (2364132)Peak memory usage: 92 MB
% 24.65/4.41 % (2364132)Instructions burned: 322 (million)
% 24.65/4.41 [W927 10:44:38.741174151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741207495 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741245332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741258515 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741284202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741295376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741322109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741333259 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741358446 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741369616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 24.65/4.41 [W927 10:44:38.741396096 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 24.65/4.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.52/4.62 [W927 10:44:38.741407443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.52/4.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.52/4.62 % (2364137)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4012469586:i=13913:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/13913Mi)
% 25.52/4.62 % (2364141)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=254594179:i=9925:aac=none_2970 on theBenchmark for (2970ds/9925Mi)
% 25.52/4.62 % (2364133)------------------------------
% 25.52/4.62 % (2364133)------------------------------
% 25.52/4.62 % (2364134)------------------------------
% 25.52/4.62 % (2364134)------------------------------
% 25.52/4.62 % (2364127)Refutation not found, incomplete strategy
% 25.52/4.62 % (2364127)------------------------------
% 25.52/4.62 % (2364127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.62 % (2364127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.62 % (2364127)CaDiCaL version: 2.1.3
% 25.52/4.62 % (2364127)Termination reason: Refutation not found, incomplete strategy
% 25.52/4.62 % (2364127)Time elapsed: 0.562 s
% 25.52/4.62 % (2364127)Peak memory usage: 125 MB
% 25.52/4.62 % (2364127)Instructions burned: 822 (million)
% 25.52/4.62 % (2364136)------------------------------
% 25.52/4.62 % (2364136)------------------------------
% 25.52/4.62 % (2364144)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3591628850:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2968 on theBenchmark for (2968ds/2479Mi)
% 25.52/4.62 % (2364144)Refutation not found, incomplete strategy
% 25.52/4.62 % (2364144)------------------------------
% 25.52/4.62 % (2364144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.62 % (2364144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.62 % (2364144)CaDiCaL version: 2.1.3
% 25.52/4.62 % (2364144)Termination reason: Refutation not found, incomplete strategy
% 25.52/4.62 % (2364144)Time elapsed: 0.001 s
% 25.52/4.62 % (2364144)Peak memory usage: 86 MB
% 25.52/4.62 % (2364145)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3658182071:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2968 on theBenchmark for (2968ds/440Mi)
% 25.52/4.62 % (2364145)Refutation not found, incomplete strategy
% 25.52/4.62 % (2364145)------------------------------
% 25.52/4.62 % (2364145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/4.62 % (2364145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/4.62 % (2364145)CaDiCaL version: 2.1.3
% 25.52/4.62 % (2364145)Termination reason: Refutation not found, incomplete strategy
% 25.52/4.62 % (2364145)Time elapsed: 0.002 s
% 25.52/4.62 % (2364145)Peak memory usage: 88 MB
% 25.52/4.62 % (2364145)Instructions burned: 1 (million)
% 25.52/4.62 % (2364146)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2215915189:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/11145Mi)
% 25.52/4.62 [W927 10:44:39.129223751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.52/4.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.52/4.62 [W927 10:44:39.129257715 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.52/4.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.52/4.62 [W927 10:44:39.129304458 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.52/4.62 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.52/4.62 [W927 10:44:39.129317532 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129343125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129358399 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129383172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129394539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129419313 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129438923 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129464449 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 [W927 10:44:39.129475720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.98/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.98/5.23 % (2364141)Refutation not found, incomplete strategy
% 30.98/5.23 % (2364141)------------------------------
% 30.98/5.23 % (2364141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/5.23 % (2364141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/5.23 % (2364141)CaDiCaL version: 2.1.3
% 30.98/5.23 % (2364141)Termination reason: Refutation not found, incomplete strategy
% 30.98/5.23 % (2364141)Time elapsed: 0.304 s
% 30.98/5.23 % (2364141)Peak memory usage: 127 MB
% 30.98/5.23 % (2364141)Instructions burned: 824 (million)
% 30.98/5.23 % (2364127)------------------------------
% 30.98/5.23 % (2364127)------------------------------
% 30.98/5.23 % (2364144)------------------------------
% 30.98/5.23 % (2364144)------------------------------
% 30.98/5.23 % (2364145)------------------------------
% 30.98/5.23 % (2364145)------------------------------
% 30.98/5.23 % (2364137)Refutation not found, incomplete strategy
% 30.98/5.23 % (2364137)------------------------------
% 30.98/5.23 % (2364137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/5.23 % (2364137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/5.23 % (2364137)CaDiCaL version: 2.1.3
% 30.98/5.23 % (2364137)Termination reason: Refutation not found, incomplete strategy
% 30.98/5.23 % (2364137)Time elapsed: 0.559 s
% 30.98/5.23 % (2364137)Peak memory usage: 125 MB
% 30.98/5.23 % (2364137)Instructions burned: 826 (million)
% 30.98/5.23 % (2364141)------------------------------
% 30.98/5.23 % (2364141)------------------------------
% 32.21/5.50 % (2364150)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=3528005156:cts=off:i=3034:av=off:er=known:fsd=on_2965 on theBenchmark for (2965ds/3034Mi)
% 32.21/5.50 % (2364151)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1881784711:st=2:s2a=on:i=524:s2at=2:ss=axioms_2964 on theBenchmark for (2964ds/524Mi)
% 32.21/5.50 % (2364151)Refutation not found, incomplete strategy
% 32.21/5.50 % (2364151)------------------------------
% 32.21/5.50 % (2364151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.50 % (2364151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.50 % (2364151)CaDiCaL version: 2.1.3
% 32.21/5.50 % (2364151)Termination reason: Refutation not found, incomplete strategy
% 32.21/5.50 % (2364151)Time elapsed: 0.001 s
% 32.21/5.50 % (2364151)Peak memory usage: 86 MB
% 32.21/5.50 % (2364153)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3794328059:i=14123:bd=preordered:ins=4_2964 on theBenchmark for (2964ds/14123Mi)
% 32.21/5.50 % (2364152)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=744416844:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2964 on theBenchmark for (2964ds/1016Mi)
% 32.21/5.50 % (2364152)Refutation not found, incomplete strategy
% 32.21/5.50 % (2364152)------------------------------
% 32.21/5.50 % (2364152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.21/5.50 % (2364152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.21/5.50 % (2364152)CaDiCaL version: 2.1.3
% 32.21/5.50 % (2364152)Termination reason: Refutation not found, incomplete strategy
% 32.21/5.50 % (2364152)Time elapsed: 0.001 s
% 32.21/5.50 % (2364152)Peak memory usage: 86 MB
% 32.21/5.50 [W927 10:44:39.510934332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.510981429 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.511031109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.511043049 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.511068159 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.511078246 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.511106750 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.21/5.50 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.21/5.50 [W927 10:44:39.511117573 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.61 [W927 10:44:39.511141737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.61 [W927 10:44:39.511162023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.61 [W927 10:44:39.511186077 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.61 [W927 10:44:39.511251021 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.61 % (2364137)------------------------------
% 32.61/5.61 % (2364137)------------------------------
% 32.61/5.61 % (2364151)------------------------------
% 32.61/5.61 % (2364151)------------------------------
% 32.61/5.61 % (2364146)Refutation not found, incomplete strategy
% 32.61/5.61 % (2364146)------------------------------
% 32.61/5.61 % (2364146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.61/5.61 % (2364146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.61/5.61 % (2364146)CaDiCaL version: 2.1.3
% 32.61/5.61 % (2364146)Termination reason: Refutation not found, incomplete strategy
% 32.61/5.61 % (2364146)Time elapsed: 0.573 s
% 32.61/5.61 % (2364146)Peak memory usage: 125 MB
% 32.61/5.61 % (2364146)Instructions burned: 822 (million)
% 32.61/5.61 % (2364152)------------------------------
% 32.61/5.61 % (2364152)------------------------------
% 32.61/5.61 % (2364158)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1143317590:i=5781:kws=precedence:bd=all:rawr=on_2961 on theBenchmark for (2961ds/5781Mi)
% 32.61/5.61 % (2364153)Refutation not found, incomplete strategy
% 32.61/5.61 % (2364153)------------------------------
% 32.61/5.61 % (2364153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.61/5.61 % (2364153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.61/5.61 % (2364153)CaDiCaL version: 2.1.3
% 32.61/5.61 % (2364153)Termination reason: Refutation not found, incomplete strategy
% 32.61/5.61 % (2364153)Time elapsed: 0.365 s
% 32.61/5.61 % (2364153)Peak memory usage: 127 MB
% 32.61/5.61 % (2364153)Instructions burned: 894 (million)
% 32.61/5.61 % (2364159)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=4086539837:i=2448:gtgl=5:bd=preordered:gtg=all_2960 on theBenchmark for (2960ds/2448Mi)
% 32.61/5.61 % (2364160)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3190432010:i=3223:kws=precedence:fgj=on:av=off_2960 on theBenchmark for (2960ds/3223Mi)
% 32.61/5.61 % (2364150)Refutation not found, incomplete strategy
% 32.61/5.61 % (2364150)------------------------------
% 32.61/5.61 % (2364150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.61/5.61 % (2364150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.61/5.61 % (2364150)CaDiCaL version: 2.1.3
% 32.61/5.61 % (2364150)Termination reason: Refutation not found, incomplete strategy
% 32.61/5.61 % (2364150)Time elapsed: 0.567 s
% 32.61/5.61 % (2364150)Peak memory usage: 127 MB
% 32.61/5.61 % (2364150)Instructions burned: 900 (million)
% 32.61/5.61 % (2364146)------------------------------
% 32.61/5.61 % (2364146)------------------------------
% 32.61/5.61 % (2364153)------------------------------
% 32.61/5.61 % (2364153)------------------------------
% 32.61/5.61 % (2364150)------------------------------
% 32.61/5.61 % (2364150)------------------------------
% 32.61/5.61 % (2364164)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4113526399:st=5.6:i=2033:sd=3:ss=axioms_2957 on theBenchmark for (2957ds/2033Mi)
% 32.61/5.68 % (2364166)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=988119552:i=21611:sd=3:ss=axioms_2956 on theBenchmark for (2956ds/21611Mi)
% 32.61/5.68 % (2364165)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2819802907:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2956 on theBenchmark for (2956ds/2055Mi)
% 32.61/5.68 [W927 10:44:40.392043196 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392067936 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392089230 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392095925 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392109541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392116081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392128971 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392134876 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392147854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392153639 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392166434 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.61/5.68 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.61/5.68 [W927 10:44:40.392172295 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 % (2364159)Refutation not found, incomplete strategy
% 34.24/5.97 % (2364159)------------------------------
% 34.24/5.97 % (2364159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.24/5.97 % (2364159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.24/5.97 % (2364159)CaDiCaL version: 2.1.3
% 34.24/5.97 % (2364159)Termination reason: Refutation not found, incomplete strategy
% 34.24/5.97 % (2364159)Time elapsed: 0.602 s
% 34.24/5.97 % (2364159)Peak memory usage: 128 MB
% 34.24/5.97 % (2364159)Instructions burned: 890 (million)
% 34.24/5.97 % (2364160)Refutation not found, incomplete strategy
% 34.24/5.97 % (2364160)------------------------------
% 34.24/5.97 % (2364160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.24/5.97 % (2364160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.24/5.97 % (2364160)CaDiCaL version: 2.1.3
% 34.24/5.97 % (2364160)Termination reason: Refutation not found, incomplete strategy
% 34.24/5.97 % (2364160)Time elapsed: 0.578 s
% 34.24/5.97 % (2364160)Peak memory usage: 127 MB
% 34.24/5.97 % (2364160)Instructions burned: 857 (million)
% 34.24/5.97 % (2364166)Refutation not found, incomplete strategy
% 34.24/5.97 % (2364166)------------------------------
% 34.24/5.97 % (2364166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.24/5.97 % (2364166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.24/5.97 % (2364166)CaDiCaL version: 2.1.3
% 34.24/5.97 % (2364166)Termination reason: Refutation not found, incomplete strategy
% 34.24/5.97 % (2364166)Time elapsed: 0.314 s
% 34.24/5.97 % (2364166)Peak memory usage: 125 MB
% 34.24/5.97 % (2364166)Instructions burned: 826 (million)
% 34.24/5.97 [W927 10:44:40.503524815 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503565809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503603412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503615706 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503643276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503655339 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503681916 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 34.24/5.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 34.24/5.97 [W927 10:44:40.503693819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.503719250 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.503730180 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.503754210 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.503776970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569100604 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569137318 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569177015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569190228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569217722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569238152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569266932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569277832 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.58/6.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.58/6.64 [W927 10:44:40.569302432 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 44.06/7.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.05 [W927 10:44:40.569312476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 44.06/7.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.05 [W927 10:44:40.569336236 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 44.06/7.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.05 [W927 10:44:40.569350013 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 44.06/7.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.05 % (2364166)------------------------------
% 44.06/7.05 % (2364166)------------------------------
% 44.06/7.05 % (2364159)------------------------------
% 44.06/7.05 % (2364159)------------------------------
% 44.06/7.05 % (2364160)------------------------------
% 44.06/7.05 % (2364160)------------------------------
% 44.06/7.05 % (2364164)Refutation not found, incomplete strategy
% 44.06/7.05 % (2364164)------------------------------
% 44.06/7.05 % (2364164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.05 % (2364164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.05 % (2364164)CaDiCaL version: 2.1.3
% 44.06/7.05 % (2364164)Termination reason: Refutation not found, incomplete strategy
% 44.06/7.05 % (2364164)Time elapsed: 0.574 s
% 44.06/7.05 % (2364164)Peak memory usage: 125 MB
% 44.06/7.05 % (2364164)Instructions burned: 825 (million)
% 44.06/7.05 % (2364165)Refutation not found, incomplete strategy
% 44.06/7.05 % (2364165)------------------------------
% 44.06/7.05 % (2364165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.05 % (2364165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.05 % (2364165)CaDiCaL version: 2.1.3
% 44.06/7.05 % (2364165)Termination reason: Refutation not found, incomplete strategy
% 44.06/7.05 % (2364165)Time elapsed: 0.550 s
% 44.06/7.05 % (2364165)Peak memory usage: 125 MB
% 44.06/7.05 % (2364165)Instructions burned: 823 (million)
% 44.06/7.05 % (2364170)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3555896182:i=4835:sd=13:ss=axioms:sgt=23_2950 on theBenchmark for (2950ds/4835Mi)
% 44.06/7.05 % (2364170)Refutation not found, incomplete strategy
% 44.06/7.05 % (2364170)------------------------------
% 44.06/7.05 % (2364170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.05 % (2364170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.05 % (2364170)CaDiCaL version: 2.1.3
% 44.06/7.05 % (2364170)Termination reason: Refutation not found, incomplete strategy
% 44.06/7.05 % (2364170)Time elapsed: 0.0000 s
% 44.06/7.05 % (2364170)Peak memory usage: 86 MB
% 44.06/7.05 % (2364171)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=840593665:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2950 on theBenchmark for (2950ds/797Mi)
% 44.06/7.05 % (2364172)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=20819653:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2950 on theBenchmark for (2950ds/2326Mi)
% 44.06/7.05 % (2364171)Refutation not found, incomplete strategy
% 44.06/7.05 % (2364171)------------------------------
% 44.06/7.05 % (2364171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.05 % (2364171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.05 % (2364171)CaDiCaL version: 2.1.3
% 44.06/7.05 % (2364171)Termination reason: Refutation not found, incomplete strategy
% 44.06/7.05 % (2364171)Time elapsed: 0.001 s
% 44.06/7.05 % (2364171)Peak memory usage: 86 MB
% 44.06/7.05 % (2364172)Refutation not found, incomplete strategy
% 44.06/7.05 % (2364172)------------------------------
% 44.06/7.05 % (2364172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.14/7.26 % (2364172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/7.26 % (2364172)CaDiCaL version: 2.1.3
% 45.14/7.26 % (2364172)Termination reason: Refutation not found, incomplete strategy
% 45.14/7.26 % (2364172)Time elapsed: 0.001 s
% 45.14/7.26 % (2364172)Peak memory usage: 88 MB
% 45.14/7.26 % (2364170)------------------------------
% 45.14/7.26 % (2364170)------------------------------
% 45.14/7.26 % (2364164)------------------------------
% 45.14/7.26 % (2364164)------------------------------
% 45.14/7.26 % (2364165)------------------------------
% 45.14/7.26 % (2364165)------------------------------
% 45.14/7.26 % (2364176)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=726743461:i=6038:nm=6_2948 on theBenchmark for (2948ds/6038Mi)
% 45.14/7.26 % (2364171)------------------------------
% 45.14/7.26 % (2364171)------------------------------
% 45.14/7.26 % (2364172)------------------------------
% 45.14/7.26 % (2364172)------------------------------
% 45.14/7.26 % (2364177)lrs+10_1_sil=32000:sp=occurrence:random_seed=2946462548:st=2:i=33334:sd=3:ss=included:sgt=32_2947 on theBenchmark for (2947ds/33334Mi)
% 45.14/7.26 % (2364177)Refutation not found, incomplete strategy
% 45.14/7.26 % (2364177)------------------------------
% 45.14/7.26 % (2364177)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.14/7.26 % (2364177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/7.26 % (2364177)CaDiCaL version: 2.1.3
% 45.14/7.26 % (2364177)Termination reason: Refutation not found, incomplete strategy
% 45.14/7.26 % (2364177)Time elapsed: 0.001 s
% 45.14/7.26 % (2364177)Peak memory usage: 86 MB
% 45.14/7.26 % (2364178)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3623226073:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2947 on theBenchmark for (2947ds/1008Mi)
% 45.14/7.26 % (2364178)Refutation not found, incomplete strategy
% 45.14/7.26 % (2364178)------------------------------
% 45.14/7.26 % (2364178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.14/7.26 % (2364178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/7.26 % (2364178)CaDiCaL version: 2.1.3
% 45.14/7.26 % (2364178)Termination reason: Refutation not found, incomplete strategy
% 45.14/7.26 % (2364178)Time elapsed: 0.001 s
% 45.14/7.26 % (2364178)Peak memory usage: 86 MB
% 45.14/7.26 % (2364181)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=4183474336:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2946 on theBenchmark for (2946ds/1083Mi)
% 45.14/7.26 % (2364180)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=385819577:i=8327:s2at=5:bd=preordered_2946 on theBenchmark for (2946ds/8327Mi)
% 45.14/7.26 % (2364181)Refutation not found, incomplete strategy
% 45.14/7.26 % (2364181)------------------------------
% 45.14/7.26 % (2364181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.14/7.26 % (2364181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/7.26 % (2364181)CaDiCaL version: 2.1.3
% 45.14/7.26 % (2364181)Termination reason: Refutation not found, incomplete strategy
% 45.14/7.26 % (2364181)Time elapsed: 0.002 s
% 45.14/7.26 % (2364181)Peak memory usage: 88 MB
% 45.14/7.26 % (2364177)------------------------------
% 45.14/7.26 % (2364177)------------------------------
% 45.14/7.26 % (2364176)Refutation not found, incomplete strategy
% 45.14/7.26 % (2364176)------------------------------
% 45.14/7.26 % (2364176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.14/7.26 % (2364176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/7.26 % (2364176)CaDiCaL version: 2.1.3
% 45.14/7.26 % (2364176)Termination reason: Refutation not found, incomplete strategy
% 45.14/7.26 % (2364176)Time elapsed: 0.326 s
% 45.14/7.26 % (2364176)Peak memory usage: 126 MB
% 45.14/7.26 % (2364176)Instructions burned: 828 (million)
% 45.14/7.26 % (2364178)------------------------------
% 45.14/7.26 % (2364178)------------------------------
% 45.14/7.26 % (2364181)------------------------------
% 45.14/7.26 % (2364181)------------------------------
% 45.14/7.26 % (2364186)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1877254944:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2943 on theBenchmark for (2943ds/1084Mi)
% 46.30/7.46 % (2364186)Refutation not found, incomplete strategy
% 46.30/7.46 % (2364186)------------------------------
% 46.30/7.46 % (2364186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.30/7.46 % (2364186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.30/7.46 % (2364186)CaDiCaL version: 2.1.3
% 46.30/7.46 % (2364186)Termination reason: Refutation not found, incomplete strategy
% 46.30/7.46 % (2364186)Time elapsed: 0.0000 s
% 46.30/7.46 % (2364186)Peak memory usage: 86 MB
% 46.30/7.46 % (2364187)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=417019773:i=6995:s2at=5:gtg=all_2943 on theBenchmark for (2943ds/6995Mi)
% 46.30/7.46 % (2364158)Instruction limit reached!
% 46.30/7.46 % (2364158)------------------------------
% 46.30/7.46 % (2364158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.30/7.46 % (2364158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.30/7.46 % (2364158)CaDiCaL version: 2.1.3
% 46.30/7.46 % (2364158)Termination reason: Instruction limit
% 46.30/7.46 % (2364158)Termination phase: Saturation
% 46.30/7.46 % (2364158)Time elapsed: 1.878 s
% 46.30/7.46 % (2364158)Peak memory usage: 101 MB
% 46.30/7.46 % (2364158)Instructions burned: 5783 (million)
% 46.30/7.46 % (2364176)------------------------------
% 46.30/7.46 % (2364176)------------------------------
% 46.30/7.46 % (2364188)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1367149893:st=2:i=6225:sd=15:ss=axioms_2942 on theBenchmark for (2942ds/6225Mi)
% 46.30/7.46 % (2364188)Refutation not found, incomplete strategy
% 46.30/7.46 % (2364188)------------------------------
% 46.30/7.46 % (2364188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.30/7.46 % (2364188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.30/7.46 % (2364188)CaDiCaL version: 2.1.3
% 46.30/7.46 % (2364188)Termination reason: Refutation not found, incomplete strategy
% 46.30/7.46 % (2364188)Time elapsed: 0.001 s
% 46.30/7.46 % (2364188)Peak memory usage: 86 MB
% 46.30/7.46 % (2364192)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2956060276:st=2.3:i=26457:sd=10:ss=included:sgt=8_2941 on theBenchmark for (2941ds/26457Mi)
% 46.30/7.46 % (2364186)------------------------------
% 46.30/7.46 % (2364186)------------------------------
% 46.30/7.46 % (2364191)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3145111278:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2941 on theBenchmark for (2941ds/3372Mi)
% 46.30/7.46 % (2364188)------------------------------
% 46.30/7.46 % (2364188)------------------------------
% 46.30/7.46 % (2364196)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=1740486235:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2939 on theBenchmark for (2939ds/13494Mi)
% 46.30/7.46 [W927 10:44:41.939594595 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.30/7.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.30/7.46 [W927 10:44:41.939626307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.30/7.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.30/7.46 [W927 10:44:41.939646727 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.30/7.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.30/7.46 [W927 10:44:41.939652941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 46.30/7.46 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 46.30/7.46 [W927 10:44:41.939666171 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939673104 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939686406 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939692531 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939705202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939710967 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939723646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:41.939729506 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 % (2364192)Refutation not found, incomplete strategy
% 47.25/7.66 % (2364192)------------------------------
% 47.25/7.66 % (2364192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.25/7.66 % (2364192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.25/7.66 % (2364192)CaDiCaL version: 2.1.3
% 47.25/7.66 % (2364192)Termination reason: Refutation not found, incomplete strategy
% 47.25/7.66 % (2364192)Time elapsed: 0.319 s
% 47.25/7.66 % (2364192)Peak memory usage: 125 MB
% 47.25/7.66 % (2364192)Instructions burned: 827 (million)
% 47.25/7.66 % (2364198)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=3507635047:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2937 on theBenchmark for (2937ds/2503Mi)
% 47.25/7.66 [W927 10:44:42.149052909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:42.149091823 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:42.149131510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.25/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.25/7.66 [W927 10:44:42.149144997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149170450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149180970 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149205370 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149215720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149239721 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149249797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149273907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 [W927 10:44:42.149293984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 47.64/7.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 47.64/7.76 % (2364187)Refutation not found, incomplete strategy
% 47.64/7.76 % (2364187)------------------------------
% 47.64/7.76 % (2364187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.64/7.76 % (2364187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.64/7.76 % (2364187)CaDiCaL version: 2.1.3
% 47.64/7.76 % (2364187)Termination reason: Refutation not found, incomplete strategy
% 47.64/7.76 % (2364187)Time elapsed: 0.600 s
% 47.64/7.76 % (2364187)Peak memory usage: 127 MB
% 47.64/7.76 % (2364187)Instructions burned: 892 (million)
% 47.64/7.76 % (2364192)------------------------------
% 47.64/7.76 % (2364192)------------------------------
% 47.64/7.76 % (2364191)Refutation not found, incomplete strategy
% 47.64/7.76 % (2364191)------------------------------
% 47.64/7.76 % (2364191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.64/7.76 % (2364191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.64/7.76 % (2364191)CaDiCaL version: 2.1.3
% 47.64/7.76 % (2364191)Termination reason: Refutation not found, incomplete strategy
% 47.64/7.76 % (2364191)Time elapsed: 0.560 s
% 47.64/7.76 % (2364191)Peak memory usage: 126 MB
% 47.64/7.76 % (2364191)Instructions burned: 825 (million)
% 47.64/7.76 % (2364200)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1047178276:i=2559:sd=1:ep=RSTC:ss=axioms_2935 on theBenchmark for (2935ds/2559Mi)
% 50.14/8.11 % (2364187)------------------------------
% 50.14/8.11 % (2364187)------------------------------
% 50.14/8.11 [W927 10:44:42.480808979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480857829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480896129 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480909023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480933953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480954646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480981353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.480991583 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.481030773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.481042367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.481066647 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.481079267 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 50.14/8.11 [W927 10:44:42.557060787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 50.14/8.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557089179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557111219 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557117312 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557130922 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557136749 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557150120 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557155960 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557168687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557174553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557187584 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 [W927 10:44:42.557193380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 53.61/8.59 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 53.61/8.59 % (2364191)------------------------------
% 53.61/8.59 % (2364191)------------------------------
% 53.61/8.59 % (2364202)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3988120782:i=30753:av=off:ss=included_2932 on theBenchmark for (2932ds/30753Mi)
% 53.61/8.59 % (2364200)Refutation not found, incomplete strategy
% 53.61/8.59 % (2364200)------------------------------
% 53.61/8.59 % (2364200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.61/8.59 % (2364200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.61/8.59 % (2364200)CaDiCaL version: 2.1.3
% 54.02/8.66 % (2364200)Termination reason: Refutation not found, incomplete strategy
% 54.02/8.66 % (2364200)Time elapsed: 0.304 s
% 54.02/8.66 % (2364200)Peak memory usage: 125 MB
% 54.02/8.66 % (2364200)Instructions burned: 822 (million)
% 54.02/8.66 % (2364198)Refutation not found, incomplete strategy
% 54.02/8.66 % (2364198)------------------------------
% 54.02/8.66 % (2364198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.02/8.66 % (2364198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.02/8.66 % (2364198)CaDiCaL version: 2.1.3
% 54.02/8.66 % (2364198)Termination reason: Refutation not found, incomplete strategy
% 54.02/8.66 % (2364198)Time elapsed: 0.577 s
% 54.02/8.66 % (2364198)Peak memory usage: 125 MB
% 54.02/8.66 % (2364198)Instructions burned: 826 (million)
% 54.02/8.66 % (2364203)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3304815205:i=26473:ep=RSTC_2931 on theBenchmark for (2931ds/26473Mi)
% 54.02/8.66 % (2364203)Refutation not found, incomplete strategy
% 54.02/8.66 % (2364203)------------------------------
% 54.02/8.66 % (2364203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.02/8.66 % (2364203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.02/8.66 % (2364203)CaDiCaL version: 2.1.3
% 54.02/8.66 % (2364203)Termination reason: Refutation not found, incomplete strategy
% 54.02/8.66 % (2364203)Time elapsed: 0.002 s
% 54.02/8.66 % (2364203)Peak memory usage: 88 MB
% 54.02/8.66 % (2364200)------------------------------
% 54.02/8.66 % (2364200)------------------------------
% 54.02/8.66 % (2364198)------------------------------
% 54.02/8.66 % (2364198)------------------------------
% 54.02/8.66 % (2364206)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=1480813932:cts=off:i=2759:kws=inv_arity:fgj=on_2929 on theBenchmark for (2929ds/2759Mi)
% 54.02/8.66 % (2364203)------------------------------
% 54.02/8.66 % (2364203)------------------------------
% 54.02/8.66 [W927 10:44:42.000043217 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000083177 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000126831 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000138724 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000164335 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000175325 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000201255 register_special_ops.cpp:225] Warning: Creating a tensor from 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.02/8.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.02/8.66 [W927 10:44:42.000214805 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 [W927 10:44:42.000239418 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 [W927 10:44:42.000250515 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 [W927 10:44:42.000274632 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 [W927 10:44:42.000285409 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 % (2364207)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=174740635:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2927 on theBenchmark for (2927ds/5665Mi)
% 54.96/9.02 % (2364209)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=3072997754:i=1532:ep=RS:ss=axioms_2927 on theBenchmark for (2927ds/1532Mi)
% 54.96/9.02 % (2364202)Refutation not found, incomplete strategy
% 54.96/9.02 % (2364202)------------------------------
% 54.96/9.02 % (2364202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.96/9.02 % (2364202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.96/9.02 % (2364202)CaDiCaL version: 2.1.3
% 54.96/9.02 % (2364202)Termination reason: Refutation not found, incomplete strategy
% 54.96/9.02 % (2364202)Time elapsed: 0.560 s
% 54.96/9.02 % (2364202)Peak memory usage: 125 MB
% 54.96/9.02 % (2364202)Instructions burned: 825 (million)
% 54.96/9.02 % (2364206)Refutation not found, incomplete strategy
% 54.96/9.02 % (2364206)------------------------------
% 54.96/9.02 % (2364206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.96/9.02 % (2364206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.96/9.02 % (2364206)CaDiCaL version: 2.1.3
% 54.96/9.02 % (2364206)Termination reason: Refutation not found, incomplete strategy
% 54.96/9.02 % (2364206)Time elapsed: 0.319 s
% 54.96/9.02 % (2364206)Peak memory usage: 127 MB
% 54.96/9.02 % (2364206)Instructions burned: 826 (million)
% 54.96/9.02 % (2364202)------------------------------
% 54.96/9.02 % (2364202)------------------------------
% 54.96/9.02 % (2364206)------------------------------
% 54.96/9.02 % (2364206)------------------------------
% 54.96/9.02 [W927 10:44:43.485286761 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 [W927 10:44:43.485333508 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.96/9.02 [W927 10:44:43.485373339 register_special_ops.cpp:225] Warning: Creating a tensor from 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.96/9.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485396775 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485422949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485438992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485464616 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485474796 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485498826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485509016 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485532983 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.485543296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.554310457 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.554365154 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.554402861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.554414661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 58.20/9.05 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.20/9.05 [W927 10:44:43.554439218 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554465115 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554491052 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554502128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554525572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554536272 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554561296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 [W927 10:44:43.554571849 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.51 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.51 % (2364213)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=97630335:i=1572:fgj=on:gsp=on_2922 on theBenchmark for (2922ds/1572Mi)
% 60.35/9.51 % (2364212)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1427880978:i=1565:sd=2:ss=axioms:sgt=32_2923 on theBenchmark for (2923ds/1565Mi)
% 60.35/9.51 % (2364207)Refutation not found, incomplete strategy
% 60.35/9.51 % (2364207)------------------------------
% 60.35/9.51 % (2364207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.35/9.51 % (2364207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.35/9.51 % (2364207)CaDiCaL version: 2.1.3
% 60.35/9.51 % (2364207)Termination reason: Refutation not found, incomplete strategy
% 60.35/9.51 % (2364207)Time elapsed: 0.584 s
% 60.35/9.51 % (2364207)Peak memory usage: 125 MB
% 60.35/9.51 % (2364207)Instructions burned: 825 (million)
% 60.35/9.51 % (2364209)Refutation not found, incomplete strategy
% 60.35/9.51 % (2364209)------------------------------
% 60.35/9.51 % (2364209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.35/9.51 % (2364209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.35/9.51 % (2364209)CaDiCaL version: 2.1.3
% 60.35/9.51 % (2364209)Termination reason: Refutation not found, incomplete strategy
% 60.35/9.51 % (2364209)Time elapsed: 0.558 s
% 60.35/9.51 % (2364209)Peak memory usage: 125 MB
% 60.35/9.51 % (2364209)Instructions burned: 826 (million)
% 60.35/9.51 % (2364213)Refutation not found, incomplete strategy
% 60.35/9.51 % (2364213)------------------------------
% 60.35/9.51 % (2364213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.35/9.60 % (2364213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.35/9.60 % (2364213)CaDiCaL version: 2.1.3
% 60.35/9.60 % (2364213)Termination reason: Refutation not found, incomplete strategy
% 60.35/9.60 % (2364213)Time elapsed: 0.351 s
% 60.35/9.60 % (2364213)Peak memory usage: 128 MB
% 60.35/9.60 % (2364213)Instructions burned: 896 (million)
% 60.35/9.60 % (2364207)------------------------------
% 60.35/9.60 % (2364207)------------------------------
% 60.35/9.60 [W927 10:44:43.943031311 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943068805 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943107119 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943119619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943147269 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943158629 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943184606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943196032 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943221183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943232569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943257610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.35/9.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.35/9.60 [W927 10:44:43.943268980 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 % (2364209)------------------------------
% 60.65/9.64 % (2364209)------------------------------
% 60.65/9.64 % (2364213)------------------------------
% 60.65/9.64 % (2364213)------------------------------
% 60.65/9.64 % (2364216)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=146227361:i=6052:sd=4:ss=axioms:sgt=24_2917 on theBenchmark for (2917ds/6052Mi)
% 60.65/9.64 % (2364212)Refutation not found, incomplete strategy
% 60.65/9.64 % (2364212)------------------------------
% 60.65/9.64 % (2364212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.65/9.64 % (2364212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.65/9.64 % (2364212)CaDiCaL version: 2.1.3
% 60.65/9.64 % (2364212)Termination reason: Refutation not found, incomplete strategy
% 60.65/9.64 % (2364212)Time elapsed: 0.554 s
% 60.65/9.64 % (2364212)Peak memory usage: 125 MB
% 60.65/9.64 % (2364212)Instructions burned: 824 (million)
% 60.65/9.64 % (2364217)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=3875557012:i=3500:sd=1:bd=preordered:sup=off:ss=included_2917 on theBenchmark for (2917ds/3500Mi)
% 60.65/9.64 % (2364218)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=4167616949:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2916 on theBenchmark for (2916ds/1842Mi)
% 60.65/9.64 % (2364212)------------------------------
% 60.65/9.64 % (2364212)------------------------------
% 60.65/9.64 [W927 10:44:44.398514456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398539592 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398561023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398568553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398581696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398588098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398602854 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 60.65/9.64 [W927 10:44:44.398609154 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 60.65/9.64 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.398622172 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.398627717 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.398640647 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.398646142 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488046909 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488085253 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488123913 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488136857 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488163820 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488185050 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488215924 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488226264 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 66.23/10.23 [W927 10:44:44.488250131 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/10.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.488266251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.488291188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.488301621 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 % (2364218)Refutation not found, incomplete strategy
% 67.03/10.42 % (2364218)------------------------------
% 67.03/10.42 % (2364218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.03/10.42 % (2364218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.03/10.42 % (2364218)CaDiCaL version: 2.1.3
% 67.03/10.42 % (2364218)Termination reason: Refutation not found, incomplete strategy
% 67.03/10.42 % (2364218)Time elapsed: 0.319 s
% 67.03/10.42 % (2364218)Peak memory usage: 125 MB
% 67.03/10.42 % (2364218)Instructions burned: 826 (million)
% 67.03/10.42 [W927 10:44:44.530714465 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530747229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530784526 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530797629 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530823323 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530834379 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530859990 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530870963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.03/10.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.03/10.42 [W927 10:44:44.530895363 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:44.530906307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:44.530930400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:44.530999054 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 % (2364222)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=1980389728:i=66096:add=on_2913 on theBenchmark for (2913ds/66096Mi)
% 68.65/10.70 % (2364216)Refutation not found, incomplete strategy
% 68.65/10.70 % (2364216)------------------------------
% 68.65/10.70 % (2364216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.65/10.70 % (2364216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.70 % (2364216)CaDiCaL version: 2.1.3
% 68.65/10.70 % (2364216)Termination reason: Refutation not found, incomplete strategy
% 68.65/10.70 % (2364216)Time elapsed: 0.541 s
% 68.65/10.70 % (2364216)Peak memory usage: 125 MB
% 68.65/10.70 % (2364216)Instructions burned: 825 (million)
% 68.65/10.70 % (2364217)Refutation not found, incomplete strategy
% 68.65/10.70 % (2364217)------------------------------
% 68.65/10.70 % (2364217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.65/10.70 % (2364217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.70 % (2364217)CaDiCaL version: 2.1.3
% 68.65/10.70 % (2364217)Termination reason: Refutation not found, incomplete strategy
% 68.65/10.70 % (2364217)Time elapsed: 0.551 s
% 68.65/10.70 % (2364217)Peak memory usage: 125 MB
% 68.65/10.70 % (2364217)Instructions burned: 824 (million)
% 68.65/10.70 % (2364218)------------------------------
% 68.65/10.70 % (2364218)------------------------------
% 68.65/10.70 % (2364216)------------------------------
% 68.65/10.70 % (2364216)------------------------------
% 68.65/10.70 % (2364225)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2564285433:cts=off:i=5469:bs=on:fsr=off_2909 on theBenchmark for (2909ds/5469Mi)
% 68.65/10.70 % (2364225)Refutation not found, incomplete strategy
% 68.65/10.70 % (2364225)------------------------------
% 68.65/10.70 % (2364225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.65/10.70 % (2364225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.70 % (2364225)CaDiCaL version: 2.1.3
% 68.65/10.70 % (2364225)Termination reason: Refutation not found, incomplete strategy
% 68.65/10.70 % (2364225)Time elapsed: 0.001 s
% 68.65/10.70 % (2364225)Peak memory usage: 88 MB
% 68.65/10.70 % (2364224)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=122174522:i=1884:sd=1:nm=60:ss=axioms_2909 on theBenchmark for (2909ds/1884Mi)
% 68.65/10.70 % (2364217)------------------------------
% 68.65/10.70 % (2364217)------------------------------
% 68.65/10.70 % (2364180)Instruction limit reached!
% 68.65/10.70 % (2364180)------------------------------
% 68.65/10.70 % (2364180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.65/10.70 % (2364180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.70 % (2364180)CaDiCaL version: 2.1.3
% 68.65/10.70 % (2364180)Termination reason: Instruction limit
% 68.65/10.70 % (2364180)Termination phase: Saturation
% 68.65/10.70 % (2364180)Time elapsed: 3.718 s
% 68.65/10.70 % (2364180)Peak memory usage: 159 MB
% 68.65/10.70 % (2364180)Instructions burned: 8329 (million)
% 68.65/10.70 % (2364225)------------------------------
% 68.65/10.70 % (2364225)------------------------------
% 68.65/10.70 % (2364222)First to succeed.
% 68.65/10.70 % (2364222)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2364059"
% 68.65/10.70 % (2364228)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=2178474022:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2907 on theBenchmark for (2907ds/2037Mi)
% 68.65/10.70 % (2364229)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=1261257460:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2907 on theBenchmark for (2907ds/2110Mi)
% 68.65/10.70 % (2364230)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=2371376584:i=2430:add=off:aac=none:nm=16_2906 on theBenchmark for (2906ds/2430Mi)
% 68.65/10.70 [W927 10:44:45.311566353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311610667 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311648244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311660224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311687107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311699097 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311725491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311747878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311775751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311786185 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311810728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 [W927 10:44:45.311821175 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 68.65/10.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.65/10.70 % SZS status Satisfiable for theBenchmark
% 68.65/10.70 % SZS output start Saturation.
% See solution above
% 68.65/10.70 % SZS output start Definitions and Model Updates.
% 68.65/10.70 for all inputs,
% 68.65/10.70 define surjection(X0) := $true
% 68.65/10.70 for all inputs,
% 68.65/10.70 define exact(X0,X1) := $true
% 68.65/10.70 for all inputs,
% 68.65/10.70 define injection(X0) := $true
% 68.65/10.70 for all inputs,
% 68.65/10.70 define commute(X0,X1,X2,X3) := $true
% 68.65/10.70 for all inputs,
% 68.65/10.70 define morphism(X0,X1,X2) := $false
% 68.65/10.70 % SZS output end Definitions and Model Updates.
% 68.65/10.70 % (2364222)------------------------------
% 68.65/10.70 % (2364222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.65/10.70 % (2364222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.65/10.70 % (2364222)CaDiCaL version: 2.1.3
% 68.65/10.70 % (2364222)Termination reason: Satisfiable
% 68.65/10.70 % (2364222)Time elapsed: 0.584 s
% 68.65/10.70 % (2364222)Peak memory usage: 127 MB
% 68.65/10.70 % (2364222)Instructions burned: 858 (million)
% 68.65/10.70 % (2364222)------------------------------
% 68.65/10.70 % (2364222)------------------------------
% 68.65/10.70 % (2364059)Success in time 9.661 s
% 68.65/10.70 % Vampire exiting
%------------------------------------------------------------------------------