%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRA075+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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 09:55:36 AM UTC 2026
% Result : Satisfiable 95.98s 14.55s
% Output : Saturation 95.98s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u60,axiom,
( ~ on_path(X3,X2)
| ~ path(X0,X1,X2)
| edge(X3) ) ).
cnf(u59,axiom,
( ~ on_path(X3,X2)
| ~ path(X0,X1,X2)
| in_path(head_of(X3),X2) ) ).
cnf(u46,axiom,
( vertex(head_of(X0))
| ~ edge(X0) ) ).
cnf(u85,axiom,
( ~ sequential(X3,X5)
| ~ on_path(X3,X0)
| precedes(X3,X4,X0)
| ~ precedes(X5,X4,X0)
| ~ path(X1,X2,X0) ) ).
cnf(u66,axiom,
( ~ sequential(X0,X1)
| edge(X1) ) ).
cnf(u53,axiom,
( path_cons(sK0(X0,X1,X2),empty) != X2
| path_cons(sK0(X0,X1,X2),X4) != X2
| head_of(sK0(X0,X1,X2)) != X1
| ~ path(head_of(sK0(X0,X1,X2)),X1,X4)
| ~ path(X0,X1,X2) ) ).
cnf(u50,axiom,
( ~ path(X0,X1,X2)
| head_of(sK0(X0,X1,X2)) = X1
| path_cons(sK0(X0,X1,X2),sK1(X0,X1,X2)) = X2 ) ).
cnf(u90,axiom,
( ~ edge(X0)
| path(tail_of(X0),head_of(X0),path_cons(X0,empty)) ) ).
cnf(u63,axiom,
( ~ in_path(X3,X2)
| ~ path(X0,X1,X2)
| vertex(X3) ) ).
cnf(u73,axiom,
( ~ sequential(X3,X4)
| ~ precedes(X5,X4,X0)
| ~ sequential(X3,X5)
| ~ precedes(X3,X4,X0)
| ~ path(X1,X2,X0) ) ).
cnf(u84,axiom,
~ sequential(X1,X1) ).
cnf(u58,axiom,
( ~ on_path(X3,X2)
| ~ path(X0,X1,X2)
| in_path(tail_of(X3),X2) ) ).
cnf(u52,axiom,
( ~ path(X0,X1,X2)
| head_of(sK0(X0,X1,X2)) = X1
| path(head_of(sK0(X0,X1,X2)),X1,sK1(X0,X1,X2)) ) ).
cnf(u49,axiom,
( ~ path(X0,X1,X2)
| path_cons(sK0(X0,X1,X2),empty) = X2
| path_cons(sK0(X0,X1,X2),sK1(X0,X1,X2)) = X2 ) ).
cnf(u70,axiom,
( ~ sequential(X3,X4)
| ~ on_path(X3,X0)
| ~ on_path(X4,X0)
| precedes(X3,X4,X0)
| ~ path(X1,X2,X0) ) ).
cnf(u77,axiom,
( ~ shortest_path(X0,X1,X4)
| ~ precedes(X3,X2,X4)
| ~ precedes(X2,X3,X4) ) ).
cnf(u51,axiom,
( ~ path(X0,X1,X2)
| path_cons(sK0(X0,X1,X2),empty) = X2
| path(head_of(sK0(X0,X1,X2)),X1,sK1(X0,X1,X2)) ) ).
cnf(u62,axiom,
( ~ in_path(X3,X2)
| ~ path(X0,X1,X2)
| on_path(sK2(X2,X3),X2) ) ).
cnf(u45,axiom,
( vertex(tail_of(X0))
| ~ edge(X0) ) ).
cnf(u72,axiom,
( ~ precedes(X3,X4,X0)
| sequential(X3,X4)
| sequential(X3,sK3(X0,X3,X4))
| ~ path(X1,X2,X0) ) ).
cnf(u87,axiom,
( ~ path(head_of(X3),X1,X4)
| ~ edge(X3)
| path(tail_of(X3),X1,path_cons(X3,X4)) ) ).
cnf(u91,axiom,
( ~ path(X0,X1,X2)
| path(tail_of(sK0(X0,X1,X2)),head_of(sK0(X0,X1,X2)),path_cons(sK0(X0,X1,X2),empty)) ) ).
cnf(u55,axiom,
( edge(sK0(X0,X1,X2))
| ~ path(X0,X1,X2) ) ).
cnf(u76,axiom,
( ~ path(X0,X1,X2)
| shortest_path(X0,X1,X2)
| X0 = X1
| path(X0,X1,sK4(X0,X1)) ) ).
cnf(u75,axiom,
( ~ precedes(X3,X4,X0)
| on_path(X3,X0)
| ~ path(X1,X2,X0) ) ).
cnf(u57,axiom,
( ~ path(X0,X1,X2)
| vertex(X0) ) ).
cnf(u44,axiom,
( head_of(X0) != tail_of(X0)
| ~ edge(X0) ) ).
cnf(u64,axiom,
( ~ sequential(X0,X1)
| head_of(X0) = tail_of(X1) ) ).
cnf(u54,axiom,
( ~ path(X0,X1,X2)
| tail_of(sK0(X0,X1,X2)) = X0 ) ).
cnf(u61,axiom,
( ~ in_path(X3,X2)
| tail_of(sK2(X2,X3)) = X3
| ~ path(X0,X1,X2)
| head_of(sK2(X2,X3)) = X3 ) ).
cnf(u71,axiom,
( ~ precedes(X3,X4,X0)
| sequential(X3,X4)
| precedes(sK3(X0,X3,X4),X4,X0)
| ~ path(X1,X2,X0) ) ).
cnf(u74,axiom,
( ~ precedes(X3,X4,X0)
| on_path(X4,X0)
| ~ path(X1,X2,X0) ) ).
cnf(u56,axiom,
( ~ path(X0,X1,X2)
| vertex(X1) ) ).
cnf(u81,axiom,
( ~ vertex(tail_of(X3))
| path(tail_of(X3),head_of(X3),path_cons(X3,empty))
| ~ vertex(head_of(X3))
| ~ edge(X3) ) ).
cnf(u68,axiom,
( head_of(X0) != tail_of(X1)
| ~ edge(X0)
| ~ edge(X1)
| X0 = X1
| sequential(X0,X1) ) ).
cnf(u67,axiom,
( ~ sequential(X0,X1)
| edge(X0) ) ).
cnf(u78,axiom,
( ~ shortest_path(X0,X1,X4)
| head_of(X3) != head_of(X5)
| tail_of(X2) != tail_of(X5)
| ~ precedes(X2,X3,X4) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA075+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 08:59:38 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.85/1.42 % (2046774)Detected formulas, will run a generic FOF schedule.
% 3.85/1.42 % (2046784)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3297914318:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.85/1.42 % (2046779)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=1218736512:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.85/1.42 % (2046781)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=3226026071:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.85/1.42 % (2046785)dis-21_1_sil=8000:lcm=predicate:random_seed=3652896837: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.85/1.42 % (2046780)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=3433494800:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.85/1.42 % (2046782)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=964938008:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.85/1.42 % (2046783)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=31983544:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.85/1.42 % (2046783)Refutation not found, incomplete strategy
% 3.85/1.42 % (2046783)------------------------------
% 3.85/1.42 % (2046783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.42 % (2046782)Refutation not found, incomplete strategy
% 3.85/1.42 % (2046782)------------------------------
% 3.85/1.42 % (2046782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.42 % (2046785)Refutation not found, incomplete strategy
% 3.85/1.42 % (2046785)------------------------------
% 3.85/1.42 % (2046785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.42 % (2046783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.42 % (2046782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.42 % (2046785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.42 % (2046783)CaDiCaL version: 2.1.3
% 3.85/1.42 % (2046782)CaDiCaL version: 2.1.3
% 3.85/1.42 % (2046785)CaDiCaL version: 2.1.3
% 3.85/1.42 % (2046783)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.42 % (2046783)Time elapsed: 0.0000 s
% 3.85/1.42 % (2046782)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.42 % (2046782)Time elapsed: 0.0000 s
% 3.85/1.42 % (2046785)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.42 % (2046785)Time elapsed: 0.0000 s
% 3.85/1.42 % (2046783)Peak memory usage: 86 MB
% 3.85/1.42 % (2046782)Peak memory usage: 86 MB
% 3.85/1.42 % (2046785)Peak memory usage: 86 MB
% 3.85/1.42 % (2046784)Instruction limit reached!
% 3.85/1.42 % (2046784)------------------------------
% 3.85/1.42 % (2046784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.42 % (2046784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.42 % (2046784)CaDiCaL version: 2.1.3
% 3.85/1.42 % (2046784)Termination reason: Instruction limit
% 3.85/1.42 % (2046784)Termination phase: Saturation
% 3.85/1.42 % (2046784)Time elapsed: 0.044 s
% 3.85/1.42 % (2046784)Peak memory usage: 89 MB
% 3.85/1.42 % (2046784)Instructions burned: 141 (million)
% 3.85/1.42 % (2046793)lrs+10_1_sil=8000:sp=occurrence:random_seed=3252142975:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.85/1.42 % (2046793)Refutation not found, incomplete strategy
% 3.85/1.42 % (2046793)------------------------------
% 3.85/1.42 % (2046793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.85/1.42 % (2046793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.85/1.42 % (2046793)CaDiCaL version: 2.1.3
% 3.85/1.42 % (2046793)Termination reason: Refutation not found, incomplete strategy
% 3.85/1.42 % (2046793)Time elapsed: 0.0000 s
% 3.85/1.42 % (2046793)Peak memory usage: 86 MB
% 3.85/1.42 % (2046782)------------------------------
% 3.85/1.42 % (2046782)------------------------------
% 3.85/1.42 % (2046785)------------------------------
% 3.85/1.42 % (2046785)------------------------------
% 3.85/1.42 % (2046783)------------------------------
% 6.51/1.83 % (2046783)------------------------------
% 6.51/1.83 % (2046793)------------------------------
% 6.51/1.83 % (2046793)------------------------------
% 6.51/1.83 [W927 08:59:39.999241942 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999281472 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999318749 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999331743 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999358260 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999370166 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999396847 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999408470 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999434440 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999446150 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999471097 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.999483294 register_special_ops.cpp:225] Warning: Creating a tensor from 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.51/1.83 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.51/1.83 [W927 08:59:39.000694130 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000735590 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000775374 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000786840 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000811894 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000822367 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000846998 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000872491 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000898248 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000908311 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000931972 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 [W927 08:59:39.000941902 register_special_ops.cpp:225] Warning: Creating a tensor from 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.55/2.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 9.55/2.24 % (2046796)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1102632498:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 9.55/2.24 % (2046797)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=507896103:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 9.55/2.24 % (2046795)lrs+10_1_sil=32000:urr=on:br=off:random_seed=888542566:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 9.55/2.24 % (2046796)Refutation not found, incomplete strategy
% 11.37/2.62 % (2046796)------------------------------
% 11.37/2.62 % (2046796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.62 % (2046796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.62 % (2046796)CaDiCaL version: 2.1.3
% 11.37/2.62 % (2046795)Refutation not found, incomplete strategy
% 11.37/2.62 % (2046795)------------------------------
% 11.37/2.62 % (2046795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.62 % (2046795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.62 % (2046796)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.62 % (2046796)Time elapsed: 0.001 s
% 11.37/2.62 % (2046796)Peak memory usage: 86 MB
% 11.37/2.62 % (2046795)CaDiCaL version: 2.1.3
% 11.37/2.62 % (2046795)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.62 % (2046795)Time elapsed: 0.001 s
% 11.37/2.62 % (2046795)Peak memory usage: 87 MB
% 11.37/2.62 % (2046797)Refutation not found, incomplete strategy
% 11.37/2.62 % (2046797)------------------------------
% 11.37/2.62 % (2046797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.62 % (2046797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.62 % (2046797)CaDiCaL version: 2.1.3
% 11.37/2.62 % (2046797)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.62 % (2046797)Time elapsed: 0.004 s
% 11.37/2.62 % (2046797)Peak memory usage: 88 MB
% 11.37/2.62 % (2046797)Instructions burned: 3 (million)
% 11.37/2.62 % (2046798)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3458803041:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 11.37/2.62 % (2046798)Refutation not found, incomplete strategy
% 11.37/2.62 % (2046798)------------------------------
% 11.37/2.62 % (2046798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.62 % (2046798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.62 % (2046798)CaDiCaL version: 2.1.3
% 11.37/2.62 % (2046798)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.62 % (2046798)Time elapsed: 0.0000 s
% 11.37/2.62 % (2046798)Peak memory usage: 86 MB
% 11.37/2.62 % (2046798)------------------------------
% 11.37/2.62 % (2046798)------------------------------
% 11.37/2.62 % (2046781)Refutation not found, incomplete strategy
% 11.37/2.62 % (2046781)------------------------------
% 11.37/2.62 % (2046781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.62 % (2046780)Refutation not found, incomplete strategy
% 11.37/2.62 % (2046780)------------------------------
% 11.37/2.62 % (2046780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.37/2.62 % (2046781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.62 % (2046780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.37/2.62 % (2046781)CaDiCaL version: 2.1.3
% 11.37/2.62 % (2046781)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.62 % (2046781)Time elapsed: 0.561 s
% 11.37/2.62 % (2046780)CaDiCaL version: 2.1.3
% 11.37/2.62 % (2046781)Peak memory usage: 123 MB
% 11.37/2.62 % (2046781)Instructions burned: 826 (million)
% 11.37/2.62 % (2046780)Termination reason: Refutation not found, incomplete strategy
% 11.37/2.62 % (2046780)Time elapsed: 0.561 s
% 11.37/2.62 % (2046780)Peak memory usage: 122 MB
% 11.37/2.62 % (2046780)Instructions burned: 825 (million)
% 11.37/2.62 % (2046797)------------------------------
% 11.37/2.62 % (2046797)------------------------------
% 11.37/2.62 % (2046796)------------------------------
% 11.37/2.62 % (2046796)------------------------------
% 11.37/2.62 % (2046795)------------------------------
% 11.37/2.62 % (2046795)------------------------------
% 11.37/2.62 % (2046803)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3631193814:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 11.37/2.62 % (2046804)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3372474233:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 11.37/2.62 % (2046805)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2076947635:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 11.37/2.62 % (2046806)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1456850182:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 11.37/2.62 % (2046804)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046804)------------------------------
% 11.93/2.79 % (2046804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.79 % (2046804)CaDiCaL version: 2.1.3
% 11.93/2.79 % (2046804)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.79 % (2046804)Time elapsed: 0.001 s
% 11.93/2.79 % (2046804)Peak memory usage: 86 MB
% 11.93/2.79 % (2046806)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046806)------------------------------
% 11.93/2.79 % (2046806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.79 % (2046806)CaDiCaL version: 2.1.3
% 11.93/2.79 % (2046806)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.79 % (2046806)Time elapsed: 0.001 s
% 11.93/2.79 % (2046806)Peak memory usage: 87 MB
% 11.93/2.79 % (2046805)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046805)------------------------------
% 11.93/2.79 % (2046805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.79 % (2046805)CaDiCaL version: 2.1.3
% 11.93/2.79 % (2046805)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.79 % (2046805)Time elapsed: 0.002 s
% 11.93/2.79 % (2046805)Peak memory usage: 87 MB
% 11.93/2.79 % (2046805)Instructions burned: 2 (million)
% 11.93/2.79 % (2046780)------------------------------
% 11.93/2.79 % (2046780)------------------------------
% 11.93/2.79 % (2046781)------------------------------
% 11.93/2.79 % (2046781)------------------------------
% 11.93/2.79 % (2046811)lrs+10_1_sil=8000:sp=occurrence:random_seed=1129822629:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 11.93/2.79 % (2046812)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1511931194:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 11.93/2.79 % (2046811)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046811)------------------------------
% 11.93/2.79 % (2046811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046812)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046812)------------------------------
% 11.93/2.79 % (2046812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.79 % (2046812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.79 % (2046812)CaDiCaL version: 2.1.3
% 11.93/2.79 % (2046811)CaDiCaL version: 2.1.3
% 11.93/2.79 % (2046812)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.79 % (2046812)Time elapsed: 0.001 s
% 11.93/2.79 % (2046811)Termination reason: Refutation not found, incomplete strategy
% 11.93/2.79 % (2046811)Time elapsed: 0.001 s
% 11.93/2.79 % (2046811)Peak memory usage: 86 MB
% 11.93/2.79 % (2046812)Peak memory usage: 86 MB
% 11.93/2.79 % (2046806)------------------------------
% 11.93/2.79 % (2046806)------------------------------
% 11.93/2.79 % (2046805)------------------------------
% 11.93/2.79 % (2046805)------------------------------
% 11.93/2.79 % (2046804)------------------------------
% 11.93/2.79 % (2046804)------------------------------
% 11.93/2.79 % (2046816)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3776410431:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 11.93/2.79 % (2046815)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2889407836:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 11.93/2.79 % (2046817)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4108535042:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 11.93/2.79 % (2046816)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046816)------------------------------
% 11.93/2.79 % (2046816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046817)Refutation not found, incomplete strategy
% 11.93/2.79 % (2046817)------------------------------
% 11.93/2.79 % (2046817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.93/2.79 % (2046816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.93/2.79 % (2046817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.26/2.83 % (2046817)CaDiCaL version: 2.1.3
% 12.26/2.83 % (2046816)CaDiCaL version: 2.1.3
% 12.26/2.83 % (2046817)Termination reason: Refutation not found, incomplete strategy
% 12.26/2.83 % (2046817)Time elapsed: 0.001 s
% 12.26/2.83 % (2046816)Termination reason: Refutation not found, incomplete strategy
% 12.26/2.83 % (2046816)Time elapsed: 0.001 s
% 12.26/2.83 % (2046817)Peak memory usage: 86 MB
% 12.26/2.83 % (2046816)Peak memory usage: 86 MB
% 12.26/2.83 % (2046812)------------------------------
% 12.26/2.83 % (2046812)------------------------------
% 12.26/2.83 % (2046811)------------------------------
% 12.26/2.83 % (2046811)------------------------------
% 12.26/2.83 % (2046821)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=277077636:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 12.26/2.83 % (2046822)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=2952458210:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 12.26/2.83 % (2046822)Refutation not found, incomplete strategy
% 12.26/2.84 % (2046822)------------------------------
% 12.26/2.84 % (2046822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.26/2.84 % (2046822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.26/2.84 % (2046822)CaDiCaL version: 2.1.3
% 12.26/2.84 % (2046822)Termination reason: Refutation not found, incomplete strategy
% 12.26/2.84 % (2046822)Time elapsed: 0.001 s
% 12.26/2.84 % (2046822)Peak memory usage: 87 MB
% 12.26/2.84 % (2046817)------------------------------
% 12.26/2.84 % (2046817)------------------------------
% 12.26/2.84 % (2046816)------------------------------
% 12.26/2.84 % (2046816)------------------------------
% 12.26/2.84 [W927 08:59:40.206148955 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206185695 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206222072 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206234866 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206261943 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206274013 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206300270 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 12.26/2.84 [W927 08:59:40.206312306 register_special_ops.cpp:225] Warning: Creating a tensor from 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.26/2.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.11/3.31 [W927 08:59:40.206337700 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.11/3.31 [W927 08:59:40.206348727 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.11/3.31 [W927 08:59:40.206372867 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.11/3.31 [W927 08:59:40.206384104 register_special_ops.cpp:225] Warning: Creating a tensor from 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.11/3.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.11/3.31 % (2046803)Instruction limit reached!
% 17.11/3.31 % (2046803)------------------------------
% 17.11/3.31 % (2046803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.11/3.31 % (2046803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.11/3.31 % (2046803)CaDiCaL version: 2.1.3
% 17.11/3.31 % (2046803)Termination reason: Instruction limit
% 17.11/3.31 % (2046803)Termination phase: Saturation
% 17.11/3.31 % (2046803)Time elapsed: 0.928 s
% 17.11/3.31 % (2046803)Peak memory usage: 138 MB
% 17.11/3.31 % (2046803)Instructions burned: 2351 (million)
% 17.11/3.31 % (2046825)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2869252594:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 17.11/3.31 % (2046826)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=972157124:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 17.11/3.31 % (2046826)Refutation not found, incomplete strategy
% 17.11/3.31 % (2046826)------------------------------
% 17.11/3.31 % (2046826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.11/3.31 % (2046826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.11/3.31 % (2046826)CaDiCaL version: 2.1.3
% 17.11/3.31 % (2046826)Termination reason: Refutation not found, incomplete strategy
% 17.11/3.31 % (2046826)Time elapsed: 0.0000 s
% 17.11/3.31 % (2046826)Peak memory usage: 86 MB
% 17.11/3.31 % (2046822)------------------------------
% 17.11/3.31 % (2046822)------------------------------
% 17.11/3.31 % (2046825)Instruction limit reached!
% 17.11/3.31 % (2046825)------------------------------
% 17.11/3.31 % (2046825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.11/3.31 % (2046825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.11/3.31 % (2046825)CaDiCaL version: 2.1.3
% 17.11/3.31 % (2046825)Termination reason: Instruction limit
% 17.11/3.31 % (2046825)Termination phase: Saturation
% 17.11/3.31 % (2046825)Time elapsed: 0.063 s
% 17.11/3.31 % (2046825)Peak memory usage: 89 MB
% 17.11/3.31 % (2046825)Instructions burned: 136 (million)
% 17.11/3.31 % (2046829)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1635120596:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2982 on theBenchmark for (2982ds/431Mi)
% 17.11/3.31 % (2046829)Refutation not found, incomplete strategy
% 17.11/3.31 % (2046829)------------------------------
% 17.11/3.31 % (2046829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.11/3.31 % (2046829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.11/3.31 % (2046829)CaDiCaL version: 2.1.3
% 17.11/3.31 % (2046829)Termination reason: Refutation not found, incomplete strategy
% 17.11/3.31 % (2046829)Time elapsed: 0.0000 s
% 17.11/3.31 % (2046829)Peak memory usage: 86 MB
% 17.11/3.31 % (2046815)Refutation not found, incomplete strategy
% 17.11/3.31 % (2046815)------------------------------
% 17.11/3.31 % (2046815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.11/3.31 % (2046815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.80 % (2046815)CaDiCaL version: 2.1.3
% 20.25/3.80 % (2046815)Termination reason: Refutation not found, incomplete strategy
% 20.25/3.80 % (2046815)Time elapsed: 0.554 s
% 20.25/3.80 % (2046815)Peak memory usage: 125 MB
% 20.25/3.80 % (2046815)Instructions burned: 826 (million)
% 20.25/3.80 [W927 08:59:40.399524700 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399573101 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399611474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399625094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399651051 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399663128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399689318 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399701398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399726945 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399738858 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399764775 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 [W927 08:59:40.399776812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.25/3.80 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.25/3.80 % (2046830)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=874808582:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 22.77/4.08 % (2046831)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=2133938342:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2981 on theBenchmark for (2981ds/150Mi)
% 22.77/4.08 % (2046831)Refutation not found, incomplete strategy
% 22.77/4.08 % (2046831)------------------------------
% 22.77/4.08 % (2046831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.77/4.08 % (2046831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.77/4.08 % (2046831)CaDiCaL version: 2.1.3
% 22.77/4.08 % (2046831)Termination reason: Refutation not found, incomplete strategy
% 22.77/4.08 % (2046831)Time elapsed: 0.007 s
% 22.77/4.08 % (2046831)Peak memory usage: 89 MB
% 22.77/4.08 % (2046831)Instructions burned: 8 (million)
% 22.77/4.08 % (2046826)------------------------------
% 22.77/4.08 % (2046826)------------------------------
% 22.77/4.08 % (2046829)------------------------------
% 22.77/4.08 % (2046829)------------------------------
% 22.77/4.08 % (2046821)Refutation not found, incomplete strategy
% 22.77/4.08 % (2046821)------------------------------
% 22.77/4.08 % (2046821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.77/4.08 % (2046821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.77/4.08 % (2046821)CaDiCaL version: 2.1.3
% 22.77/4.08 % (2046821)Termination reason: Refutation not found, incomplete strategy
% 22.77/4.08 % (2046821)Time elapsed: 0.557 s
% 22.77/4.08 % (2046821)Peak memory usage: 125 MB
% 22.77/4.08 % (2046821)Instructions burned: 822 (million)
% 22.77/4.08 % (2046815)------------------------------
% 22.77/4.08 % (2046815)------------------------------
% 22.77/4.08 % (2046836)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1137415674:i=667:av=off:fsr=off_2979 on theBenchmark for (2979ds/667Mi)
% 22.77/4.08 % (2046836)Refutation not found, incomplete strategy
% 22.77/4.08 % (2046836)------------------------------
% 22.77/4.08 % (2046836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.77/4.08 % (2046836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.77/4.08 % (2046836)CaDiCaL version: 2.1.3
% 22.77/4.08 % (2046836)Termination reason: Refutation not found, incomplete strategy
% 22.77/4.08 % (2046836)Time elapsed: 0.001 s
% 22.77/4.08 % (2046836)Peak memory usage: 88 MB
% 22.77/4.08 % (2046836)Instructions burned: 1 (million)
% 22.77/4.08 % (2046835)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=304504316:i=14155:bd=all_2979 on theBenchmark for (2979ds/14155Mi)
% 22.77/4.08 % (2046831)------------------------------
% 22.77/4.08 % (2046831)------------------------------
% 22.77/4.08 % (2046836)------------------------------
% 22.77/4.08 % (2046836)------------------------------
% 22.77/4.08 % (2046839)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=1799904546:s2a=on:i=185:s2at=1.8:fdi=4_2978 on theBenchmark for (2978ds/185Mi)
% 22.77/4.08 % (2046821)------------------------------
% 22.77/4.08 % (2046821)------------------------------
% 22.77/4.08 % (2046840)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3574701983:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2977 on theBenchmark for (2977ds/193Mi)
% 22.77/4.08 % (2046840)Refutation not found, incomplete strategy
% 22.77/4.08 % (2046840)------------------------------
% 22.77/4.08 % (2046840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.77/4.08 % (2046840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.77/4.08 % (2046840)CaDiCaL version: 2.1.3
% 22.77/4.08 % (2046840)Termination reason: Refutation not found, incomplete strategy
% 22.77/4.08 % (2046840)Time elapsed: 0.001 s
% 22.77/4.08 % (2046840)Peak memory usage: 86 MB
% 22.77/4.08 % (2046841)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=430664183:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2976 on theBenchmark for (2976ds/4850Mi)
% 22.77/4.08 % (2046841)Refutation not found, incomplete strategy
% 22.77/4.08 % (2046841)------------------------------
% 22.77/4.08 % (2046841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/4.25 % (2046841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/4.25 % (2046841)CaDiCaL version: 2.1.3
% 23.89/4.25 % (2046841)Termination reason: Refutation not found, incomplete strategy
% 23.89/4.25 % (2046841)Time elapsed: 0.0000 s
% 23.89/4.25 % (2046841)Peak memory usage: 86 MB
% 23.89/4.25 % (2046839)Instruction limit reached!
% 23.89/4.25 % (2046839)------------------------------
% 23.89/4.25 % (2046839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/4.25 % (2046839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/4.25 % (2046839)CaDiCaL version: 2.1.3
% 23.89/4.25 % (2046839)Termination reason: Instruction limit
% 23.89/4.25 % (2046839)Termination phase: Saturation
% 23.89/4.25 % (2046839)Time elapsed: 0.107 s
% 23.89/4.25 % (2046839)Peak memory usage: 91 MB
% 23.89/4.25 % (2046839)Instructions burned: 185 (million)
% 23.89/4.25 % (2046843)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2550214428:i=12111:sd=1:ss=included_2976 on theBenchmark for (2976ds/12111Mi)
% 23.89/4.25 % (2046841)------------------------------
% 23.89/4.25 % (2046841)------------------------------
% 23.89/4.25 % (2046846)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1324430530:i=319:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/319Mi)
% 23.89/4.25 % (2046840)------------------------------
% 23.89/4.25 % (2046840)------------------------------
% 23.89/4.25 % (2046848)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1721479113:i=2064:ep=RST_2973 on theBenchmark for (2973ds/2064Mi)
% 23.89/4.25 % (2046848)Refutation not found, incomplete strategy
% 23.89/4.25 % (2046848)------------------------------
% 23.89/4.25 % (2046848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/4.25 % (2046848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/4.25 % (2046848)CaDiCaL version: 2.1.3
% 23.89/4.25 % (2046848)Termination reason: Refutation not found, incomplete strategy
% 23.89/4.25 % (2046848)Time elapsed: 0.001 s
% 23.89/4.25 % (2046848)Peak memory usage: 88 MB
% 23.89/4.25 % (2046848)Instructions burned: 2 (million)
% 23.89/4.25 % (2046846)Instruction limit reached!
% 23.89/4.25 % (2046846)------------------------------
% 23.89/4.25 % (2046846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/4.25 % (2046846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/4.25 % (2046846)CaDiCaL version: 2.1.3
% 23.89/4.25 % (2046846)Termination reason: Instruction limit
% 23.89/4.25 % (2046846)Termination phase: Saturation
% 23.89/4.25 % (2046846)Time elapsed: 0.183 s
% 23.89/4.25 % (2046846)Peak memory usage: 90 MB
% 23.89/4.25 % (2046846)Instructions burned: 321 (million)
% 23.89/4.25 % (2046850)dis-1011_128_sil=32000:random_seed=2903639782:i=3706:ep=RST:av=off_2973 on theBenchmark for (2973ds/3706Mi)
% 23.89/4.25 % (2046848)------------------------------
% 23.89/4.25 % (2046848)------------------------------
% 23.89/4.25 [W927 08:59:41.393940770 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 23.89/4.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 23.89/4.25 [W927 08:59:41.393989094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 23.89/4.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 23.89/4.25 [W927 08:59:41.394039831 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 23.89/4.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 23.89/4.25 [W927 08:59:41.394052478 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 23.89/4.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 23.89/4.25 [W927 08:59:41.394079575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394122598 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394154225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394165355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394188782 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394199786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394224389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 [W927 08:59:41.394235636 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 27.62/4.94 % (2046852)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1122943803:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2971 on theBenchmark for (2971ds/757Mi)
% 27.62/4.94 % (2046852)Refutation not found, incomplete strategy
% 27.62/4.94 % (2046852)------------------------------
% 27.62/4.94 % (2046852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.62/4.94 % (2046852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.62/4.94 % (2046852)CaDiCaL version: 2.1.3
% 27.62/4.94 % (2046852)Termination reason: Refutation not found, incomplete strategy
% 27.62/4.94 % (2046852)Time elapsed: 0.001 s
% 27.62/4.94 % (2046852)Peak memory usage: 86 MB
% 27.62/4.94 % (2046854)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2856680382:i=13913:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/13913Mi)
% 27.62/4.94 % (2046843)Refutation not found, incomplete strategy
% 27.62/4.94 % (2046843)------------------------------
% 27.62/4.94 % (2046843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.62/4.94 % (2046843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.62/4.94 % (2046843)CaDiCaL version: 2.1.3
% 27.62/4.94 % (2046843)Termination reason: Refutation not found, incomplete strategy
% 27.62/4.94 % (2046843)Time elapsed: 0.563 s
% 27.62/4.94 % (2046843)Peak memory usage: 125 MB
% 27.62/4.94 % (2046843)Instructions burned: 825 (million)
% 27.62/4.94 % (2046852)------------------------------
% 27.62/4.94 % (2046852)------------------------------
% 27.62/4.94 [W927 08:59:42.674184136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 27.62/4.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674208822 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674242200 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674248498 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674261955 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674273398 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674287475 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674292896 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674305692 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674311074 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674323978 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 [W927 08:59:42.674329480 register_special_ops.cpp:225] Warning: Creating a tensor from 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.91/5.23 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.91/5.23 % (2046854)Refutation not found, incomplete strategy
% 30.91/5.23 % (2046854)------------------------------
% 30.91/5.23 % (2046854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.91/5.23 % (2046854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.91/5.23 % (2046854)CaDiCaL version: 2.1.3
% 30.91/5.23 % (2046854)Termination reason: Refutation not found, incomplete strategy
% 30.91/5.23 % (2046854)Time elapsed: 0.312 s
% 30.91/5.23 % (2046854)Peak memory usage: 125 MB
% 30.91/5.23 % (2046854)Instructions burned: 825 (million)
% 30.91/5.23 % (2046843)------------------------------
% 30.91/5.23 % (2046843)------------------------------
% 30.91/5.23 % (2046857)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2331424127:i=9925:aac=none_2967 on theBenchmark for (2967ds/9925Mi)
% 41.95/7.02 % (2046854)------------------------------
% 41.95/7.02 % (2046854)------------------------------
% 41.95/7.02 % (2046858)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3756672491:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/2479Mi)
% 41.95/7.02 % (2046858)Refutation not found, incomplete strategy
% 41.95/7.02 % (2046858)------------------------------
% 41.95/7.02 % (2046858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.95/7.02 % (2046858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.95/7.02 % (2046858)CaDiCaL version: 2.1.3
% 41.95/7.02 % (2046858)Termination reason: Refutation not found, incomplete strategy
% 41.95/7.02 % (2046858)Time elapsed: 0.001 s
% 41.95/7.02 % (2046858)Peak memory usage: 86 MB
% 41.95/7.02 % (2046860)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=116221488:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2964 on theBenchmark for (2964ds/440Mi)
% 41.95/7.02 % (2046860)Instruction limit reached!
% 41.95/7.02 % (2046860)------------------------------
% 41.95/7.02 % (2046860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.95/7.02 % (2046860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.95/7.02 % (2046860)CaDiCaL version: 2.1.3
% 41.95/7.02 % (2046860)Termination reason: Instruction limit
% 41.95/7.02 % (2046860)Termination phase: Saturation
% 41.95/7.02 % (2046860)Time elapsed: 0.141 s
% 41.95/7.02 % (2046860)Peak memory usage: 93 MB
% 41.95/7.02 % (2046860)Instructions burned: 442 (million)
% 41.95/7.02 % (2046858)------------------------------
% 41.95/7.02 % (2046858)------------------------------
% 41.95/7.02 % (2046863)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3640933146:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2962 on theBenchmark for (2962ds/11145Mi)
% 41.95/7.02 % (2046864)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=1141529291:cts=off:i=3034:av=off:er=known:fsd=on_2962 on theBenchmark for (2962ds/3034Mi)
% 41.95/7.02 % (2046857)Refutation not found, incomplete strategy
% 41.95/7.02 % (2046857)------------------------------
% 41.95/7.02 % (2046857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.95/7.02 % (2046857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.95/7.02 % (2046857)CaDiCaL version: 2.1.3
% 41.95/7.02 % (2046857)Termination reason: Refutation not found, incomplete strategy
% 41.95/7.02 % (2046857)Time elapsed: 0.560 s
% 41.95/7.02 % (2046857)Peak memory usage: 127 MB
% 41.95/7.02 % (2046857)Instructions burned: 830 (million)
% 41.95/7.02 [W927 08:59:43.528494470 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 41.95/7.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 41.95/7.02 [W927 08:59:43.528518932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 41.95/7.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 41.95/7.02 [W927 08:59:43.528539725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 41.95/7.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 41.95/7.02 [W927 08:59:43.528545767 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 41.95/7.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 41.95/7.02 [W927 08:59:43.528558672 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528565068 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528590733 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528596070 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528609153 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528620753 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528634382 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 [W927 08:59:43.528639713 register_special_ops.cpp:225] Warning: Creating a tensor from 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.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 44.06/7.07 % (2046863)Refutation not found, incomplete strategy
% 44.06/7.07 % (2046863)------------------------------
% 44.06/7.07 % (2046863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.07 % (2046863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.07 % (2046863)CaDiCaL version: 2.1.3
% 44.06/7.07 % (2046863)Termination reason: Refutation not found, incomplete strategy
% 44.06/7.07 % (2046863)Time elapsed: 0.298 s
% 44.06/7.07 % (2046863)Peak memory usage: 125 MB
% 44.06/7.07 % (2046863)Instructions burned: 822 (million)
% 44.06/7.07 % (2046857)------------------------------
% 44.06/7.07 % (2046857)------------------------------
% 44.06/7.07 % (2046850)Instruction limit reached!
% 44.06/7.07 % (2046850)------------------------------
% 44.06/7.07 % (2046850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.07 % (2046850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.07 % (2046850)CaDiCaL version: 2.1.3
% 44.06/7.07 % (2046850)Termination reason: Instruction limit
% 44.06/7.07 % (2046850)Termination phase: Saturation
% 44.06/7.07 % (2046850)Time elapsed: 1.398 s
% 44.06/7.07 % (2046850)Peak memory usage: 89 MB
% 44.06/7.07 % (2046850)Instructions burned: 3706 (million)
% 44.06/7.07 % (2046863)------------------------------
% 44.06/7.07 % (2046863)------------------------------
% 44.06/7.07 % (2046867)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1449002802:st=2:s2a=on:i=524:s2at=2:ss=axioms_2957 on theBenchmark for (2957ds/524Mi)
% 44.06/7.07 % (2046867)Refutation not found, incomplete strategy
% 44.06/7.07 % (2046867)------------------------------
% 44.06/7.07 % (2046867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.06/7.07 % (2046867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.06/7.07 % (2046867)CaDiCaL version: 2.1.3
% 44.06/7.07 % (2046867)Termination reason: Refutation not found, incomplete strategy
% 44.06/7.07 % (2046867)Time elapsed: 0.001 s
% 45.24/7.24 % (2046867)Peak memory usage: 87 MB
% 45.24/7.24 % (2046868)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=948295031:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2957 on theBenchmark for (2957ds/1016Mi)
% 45.24/7.24 % (2046868)Refutation not found, incomplete strategy
% 45.24/7.24 % (2046868)------------------------------
% 45.24/7.24 % (2046868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.24 % (2046868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.24 % (2046868)CaDiCaL version: 2.1.3
% 45.24/7.24 % (2046868)Termination reason: Refutation not found, incomplete strategy
% 45.24/7.24 % (2046868)Time elapsed: 0.001 s
% 45.24/7.24 % (2046868)Peak memory usage: 87 MB
% 45.24/7.24 % (2046869)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2389608922:i=14123:bd=preordered:ins=4_2956 on theBenchmark for (2956ds/14123Mi)
% 45.24/7.24 % (2046867)------------------------------
% 45.24/7.24 % (2046867)------------------------------
% 45.24/7.24 % (2046868)------------------------------
% 45.24/7.24 % (2046868)------------------------------
% 45.24/7.24 % (2046873)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2445891657:i=5781:kws=precedence:bd=all:rawr=on_2953 on theBenchmark for (2953ds/5781Mi)
% 45.24/7.24 % (2046874)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=28268608:i=2448:gtgl=5:bd=preordered:gtg=all_2953 on theBenchmark for (2953ds/2448Mi)
% 45.24/7.24 % (2046874)Refutation not found, incomplete strategy
% 45.24/7.24 % (2046874)------------------------------
% 45.24/7.24 % (2046874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.24 % (2046874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.24 % (2046874)CaDiCaL version: 2.1.3
% 45.24/7.24 % (2046874)Termination reason: Refutation not found, incomplete strategy
% 45.24/7.24 % (2046874)Time elapsed: 0.596 s
% 45.24/7.24 % (2046874)Peak memory usage: 129 MB
% 45.24/7.24 % (2046874)Instructions burned: 911 (million)
% 45.24/7.24 % (2046864)Instruction limit reached!
% 45.24/7.24 % (2046864)------------------------------
% 45.24/7.24 % (2046864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.24 % (2046864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.24 % (2046864)CaDiCaL version: 2.1.3
% 45.24/7.24 % (2046864)Termination reason: Instruction limit
% 45.24/7.24 % (2046864)Termination phase: Saturation
% 45.24/7.24 % (2046864)Time elapsed: 1.660 s
% 45.24/7.24 % (2046864)Peak memory usage: 130 MB
% 45.24/7.24 % (2046864)Instructions burned: 3036 (million)
% 45.24/7.24 % (2046830)Instruction limit reached!
% 45.24/7.24 % (2046830)------------------------------
% 45.24/7.24 % (2046830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.24/7.24 % (2046830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/7.24 % (2046830)CaDiCaL version: 2.1.3
% 45.24/7.24 % (2046830)Termination reason: Instruction limit
% 45.24/7.24 % (2046830)Termination phase: Saturation
% 45.24/7.24 % (2046830)Time elapsed: 3.659 s
% 45.24/7.24 % (2046830)Peak memory usage: 152 MB
% 45.24/7.24 % (2046830)Instructions burned: 6060 (million)
% 45.24/7.24 % (2046874)------------------------------
% 45.24/7.24 % (2046874)------------------------------
% 45.24/7.24 % (2046877)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2905668244:i=3223:kws=precedence:fgj=on:av=off_2944 on theBenchmark for (2944ds/3223Mi)
% 45.24/7.24 % (2046878)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2596262327:st=5.6:i=2033:sd=3:ss=axioms_2943 on theBenchmark for (2943ds/2033Mi)
% 45.24/7.24 % (2046879)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2423624792:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2943 on theBenchmark for (2943ds/2055Mi)
% 45.24/7.24 [W927 08:59:45.611020828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.24/7.24 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.24/7.24 [W927 08:59:45.611064655 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611102646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611113863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611138693 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611149523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611174096 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611184926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611209987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611220840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611244840 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.611255650 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.657936497 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.657977114 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 49.75/7.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 49.75/7.98 [W927 08:59:45.658024631 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658036758 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658072048 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658082828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658108615 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658118735 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658142679 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658152729 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658176986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 [W927 08:59:45.658187039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 52.69/8.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 52.69/8.43 % (2046878)Refutation not found, incomplete strategy
% 52.69/8.43 % (2046878)------------------------------
% 52.69/8.43 % (2046878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.69/8.43 % (2046878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.69/8.43 % (2046878)CaDiCaL version: 2.1.3
% 52.69/8.43 % (2046878)Termination reason: Refutation not found, incomplete strategy
% 52.69/8.43 % (2046878)Time elapsed: 0.541 s
% 52.69/8.43 % (2046878)Peak memory usage: 125 MB
% 52.69/8.43 % (2046878)Instructions burned: 821 (million)
% 52.69/8.43 % (2046877)Refutation not found, incomplete strategy
% 52.69/8.43 % (2046877)------------------------------
% 52.69/8.43 % (2046877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.69/8.43 % (2046877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.69/8.43 % (2046877)CaDiCaL version: 2.1.3
% 52.69/8.43 % (2046877)Termination reason: Refutation not found, incomplete strategy
% 52.69/8.43 % (2046877)Time elapsed: 0.601 s
% 52.69/8.43 % (2046877)Peak memory usage: 128 MB
% 52.69/8.43 % (2046877)Instructions burned: 908 (million)
% 52.69/8.43 % (2046879)Refutation not found, incomplete strategy
% 52.69/8.43 % (2046879)------------------------------
% 58.22/9.12 % (2046879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.22/9.12 % (2046879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.22/9.12 % (2046879)CaDiCaL version: 2.1.3
% 58.22/9.12 % (2046879)Termination reason: Refutation not found, incomplete strategy
% 58.22/9.12 % (2046879)Time elapsed: 0.545 s
% 58.22/9.12 % (2046879)Peak memory usage: 125 MB
% 58.22/9.12 % (2046879)Instructions burned: 825 (million)
% 58.22/9.12 % (2046878)------------------------------
% 58.22/9.12 % (2046878)------------------------------
% 58.22/9.12 % (2046877)------------------------------
% 58.22/9.12 % (2046877)------------------------------
% 58.22/9.12 % (2046879)------------------------------
% 58.22/9.12 % (2046879)------------------------------
% 58.22/9.12 % (2046883)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=2119662925:i=21611:sd=3:ss=axioms_2934 on theBenchmark for (2934ds/21611Mi)
% 58.22/9.12 % (2046884)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3630782508:i=4835:sd=13:ss=axioms:sgt=23_2933 on theBenchmark for (2933ds/4835Mi)
% 58.22/9.12 % (2046884)Refutation not found, incomplete strategy
% 58.22/9.12 % (2046884)------------------------------
% 58.22/9.12 % (2046884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.22/9.12 % (2046884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.22/9.12 % (2046884)CaDiCaL version: 2.1.3
% 58.22/9.12 % (2046884)Termination reason: Refutation not found, incomplete strategy
% 58.22/9.12 % (2046884)Time elapsed: 0.001 s
% 58.22/9.12 % (2046884)Peak memory usage: 86 MB
% 58.22/9.12 % (2046885)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=43226117:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2933 on theBenchmark for (2933ds/797Mi)
% 58.22/9.12 % (2046885)Refutation not found, incomplete strategy
% 58.22/9.12 % (2046885)------------------------------
% 58.22/9.12 % (2046885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.22/9.12 % (2046885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.22/9.12 % (2046885)CaDiCaL version: 2.1.3
% 58.22/9.12 % (2046885)Termination reason: Refutation not found, incomplete strategy
% 58.22/9.12 % (2046885)Time elapsed: 0.001 s
% 58.22/9.12 % (2046885)Peak memory usage: 86 MB
% 58.22/9.12 % (2046884)------------------------------
% 58.22/9.12 % (2046884)------------------------------
% 58.22/9.12 % (2046885)------------------------------
% 58.22/9.12 % (2046885)------------------------------
% 58.22/9.12 [W927 08:59:46.572397818 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.22/9.12 [W927 08:59:46.572434475 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.22/9.12 [W927 08:59:46.572473152 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.22/9.12 [W927 08:59:46.572485909 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.22/9.12 [W927 08:59:46.572513082 register_special_ops.cpp:225] Warning: Creating a tensor from 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.22/9.12 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 58.22/9.12 [W927 08:59:46.572524473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 [W927 08:59:46.572550553 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 [W927 08:59:46.572560966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 [W927 08:59:46.572585663 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 [W927 08:59:46.572595996 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 [W927 08:59:46.572619887 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 [W927 08:59:46.572629997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 62.19/9.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 62.19/9.77 % (2046889)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3395923784:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2929 on theBenchmark for (2929ds/2326Mi)
% 62.19/9.77 % (2046889)Refutation not found, incomplete strategy
% 62.19/9.77 % (2046889)------------------------------
% 62.19/9.77 % (2046889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.19/9.77 % (2046889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.19/9.77 % (2046889)CaDiCaL version: 2.1.3
% 62.19/9.77 % (2046889)Termination reason: Refutation not found, incomplete strategy
% 62.19/9.77 % (2046889)Time elapsed: 0.002 s
% 62.19/9.77 % (2046889)Peak memory usage: 88 MB
% 62.19/9.77 % (2046889)Instructions burned: 2 (million)
% 62.19/9.77 % (2046890)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=4223436727:i=6038:nm=6_2929 on theBenchmark for (2929ds/6038Mi)
% 62.19/9.77 % (2046883)Refutation not found, incomplete strategy
% 62.19/9.77 % (2046883)------------------------------
% 62.19/9.77 % (2046883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.19/9.77 % (2046883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.19/9.77 % (2046883)CaDiCaL version: 2.1.3
% 62.19/9.77 % (2046883)Termination reason: Refutation not found, incomplete strategy
% 62.19/9.77 % (2046883)Time elapsed: 0.556 s
% 62.19/9.77 % (2046883)Peak memory usage: 125 MB
% 62.19/9.77 % (2046883)Instructions burned: 826 (million)
% 62.19/9.77 % (2046889)------------------------------
% 62.19/9.77 % (2046889)------------------------------
% 62.19/9.77 % (2046883)------------------------------
% 62.19/9.77 % (2046883)------------------------------
% 62.19/9.77 % (2046893)lrs+10_1_sil=32000:sp=occurrence:random_seed=3870875698:st=2:i=33334:sd=3:ss=included:sgt=32_2926 on theBenchmark for (2926ds/33334Mi)
% 62.19/9.77 % (2046893)Refutation not found, incomplete strategy
% 62.19/9.77 % (2046893)------------------------------
% 62.19/9.77 % (2046893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.19/9.77 % (2046893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.29/10.07 % (2046893)CaDiCaL version: 2.1.3
% 65.29/10.07 % (2046893)Termination reason: Refutation not found, incomplete strategy
% 65.29/10.07 % (2046893)Time elapsed: 0.001 s
% 65.29/10.07 % (2046893)Peak memory usage: 86 MB
% 65.29/10.07 % (2046894)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1636121473:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2924 on theBenchmark for (2924ds/1008Mi)
% 65.29/10.07 % (2046894)Refutation not found, incomplete strategy
% 65.29/10.07 % (2046894)------------------------------
% 65.29/10.07 % (2046894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.29/10.07 % (2046894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.29/10.07 % (2046894)CaDiCaL version: 2.1.3
% 65.29/10.07 % (2046894)Termination reason: Refutation not found, incomplete strategy
% 65.29/10.07 % (2046894)Time elapsed: 0.001 s
% 65.29/10.07 % (2046894)Peak memory usage: 86 MB
% 65.29/10.07 % (2046890)Refutation not found, incomplete strategy
% 65.29/10.07 % (2046890)------------------------------
% 65.29/10.07 % (2046890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.29/10.07 % (2046890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.29/10.07 % (2046890)CaDiCaL version: 2.1.3
% 65.29/10.07 % (2046890)Termination reason: Refutation not found, incomplete strategy
% 65.29/10.07 % (2046890)Time elapsed: 0.559 s
% 65.29/10.07 % (2046890)Peak memory usage: 128 MB
% 65.29/10.07 % (2046890)Instructions burned: 834 (million)
% 65.29/10.07 % (2046893)------------------------------
% 65.29/10.07 % (2046893)------------------------------
% 65.29/10.07 % (2046873)Instruction limit reached!
% 65.29/10.07 % (2046873)------------------------------
% 65.29/10.07 % (2046873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.29/10.07 % (2046873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.29/10.07 % (2046873)CaDiCaL version: 2.1.3
% 65.29/10.07 % (2046873)Termination reason: Instruction limit
% 65.29/10.07 % (2046873)Termination phase: Saturation
% 65.29/10.07 % (2046873)Time elapsed: 3.063 s
% 65.29/10.07 % (2046873)Peak memory usage: 127 MB
% 65.29/10.07 % (2046873)Instructions burned: 5782 (million)
% 65.29/10.07 % (2046894)------------------------------
% 65.29/10.07 % (2046894)------------------------------
% 65.29/10.07 % (2046897)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=2215310174:i=8327:s2at=5:bd=preordered_2921 on theBenchmark for (2921ds/8327Mi)
% 65.29/10.07 % (2046890)------------------------------
% 65.29/10.07 % (2046890)------------------------------
% 65.29/10.07 % (2046898)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=1276254501:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2921 on theBenchmark for (2921ds/1083Mi)
% 65.29/10.07 % (2046898)Refutation not found, incomplete strategy
% 65.29/10.07 % (2046898)------------------------------
% 65.29/10.07 % (2046898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.29/10.07 % (2046898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.29/10.07 % (2046898)CaDiCaL version: 2.1.3
% 65.29/10.07 % (2046898)Termination reason: Refutation not found, incomplete strategy
% 65.29/10.07 % (2046898)Time elapsed: 0.004 s
% 65.29/10.07 % (2046898)Peak memory usage: 88 MB
% 65.29/10.07 % (2046898)Instructions burned: 4 (million)
% 65.29/10.07 % (2046900)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2487489946:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2920 on theBenchmark for (2920ds/1084Mi)
% 65.29/10.07 % (2046900)Refutation not found, incomplete strategy
% 65.29/10.07 % (2046900)------------------------------
% 65.29/10.07 % (2046900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.29/10.07 % (2046900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.29/10.07 % (2046900)CaDiCaL version: 2.1.3
% 65.29/10.07 % (2046900)Termination reason: Refutation not found, incomplete strategy
% 65.29/10.07 % (2046900)Time elapsed: 0.0000 s
% 65.29/10.07 % (2046900)Peak memory usage: 86 MB
% 65.29/10.07 % (2046901)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2495869724:i=6995:s2at=5:gtg=all_2920 on theBenchmark for (2920ds/6995Mi)
% 65.29/10.07 % (2046898)------------------------------
% 68.82/10.71 % (2046898)------------------------------
% 68.82/10.71 % (2046900)------------------------------
% 68.82/10.71 % (2046900)------------------------------
% 68.82/10.71 % (2046905)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1046918129:st=2:i=6225:sd=15:ss=axioms_2917 on theBenchmark for (2917ds/6225Mi)
% 68.82/10.71 % (2046905)Refutation not found, incomplete strategy
% 68.82/10.71 % (2046905)------------------------------
% 68.82/10.71 % (2046905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.82/10.71 % (2046905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.82/10.71 % (2046905)CaDiCaL version: 2.1.3
% 68.82/10.71 % (2046905)Termination reason: Refutation not found, incomplete strategy
% 68.82/10.71 % (2046905)Time elapsed: 0.001 s
% 68.82/10.71 % (2046905)Peak memory usage: 86 MB
% 68.82/10.71 % (2046906)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3445913533:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2916 on theBenchmark for (2916ds/3372Mi)
% 68.82/10.71 % (2046905)------------------------------
% 68.82/10.71 % (2046905)------------------------------
% 68.82/10.71 % (2046869)Instruction limit reached!
% 68.82/10.71 % (2046869)------------------------------
% 68.82/10.71 % (2046869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.82/10.71 % (2046869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.82/10.71 % (2046869)CaDiCaL version: 2.1.3
% 68.82/10.71 % (2046869)Termination reason: Instruction limit
% 68.82/10.71 % (2046869)Termination phase: Saturation
% 68.82/10.71 % (2046869)Time elapsed: 4.221 s
% 68.82/10.71 % (2046869)Peak memory usage: 179 MB
% 68.82/10.71 % (2046869)Instructions burned: 14128 (million)
% 68.82/10.71 % (2046910)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=724506461:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2913 on theBenchmark for (2913ds/13494Mi)
% 68.82/10.71 % (2046909)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=3836696275:st=2.3:i=26457:sd=10:ss=included:sgt=8_2913 on theBenchmark for (2913ds/26457Mi)
% 68.82/10.71 [W927 08:59:47.363976047 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.71 [W927 08:59:47.364020654 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.71 [W927 08:59:47.364057341 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.71 [W927 08:59:47.364069708 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.71 [W927 08:59:47.364095325 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.71 [W927 08:59:47.364107462 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.71 [W927 08:59:47.364133299 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:47.364145555 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:47.364176416 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:47.364198122 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:47.364222943 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:47.364234183 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 % (2046906)Refutation not found, incomplete strategy
% 68.82/10.72 % (2046906)------------------------------
% 68.82/10.72 % (2046906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.82/10.72 % (2046906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.82/10.72 % (2046906)CaDiCaL version: 2.1.3
% 68.82/10.72 % (2046906)Termination reason: Refutation not found, incomplete strategy
% 68.82/10.72 % (2046906)Time elapsed: 0.543 s
% 68.82/10.72 % (2046906)Peak memory usage: 126 MB
% 68.82/10.72 % (2046906)Instructions burned: 822 (million)
% 68.82/10.72 [W927 08:59:48.661740016 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:48.661778063 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:48.661814520 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:48.661827610 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:48.661853697 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:48.661865777 register_special_ops.cpp:225] Warning: Creating a tensor from 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.82/10.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 68.82/10.72 [W927 08:59:48.661891191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 [W927 08:59:48.661902451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 [W927 08:59:48.661933471 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 [W927 08:59:48.661954368 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 [W927 08:59:48.661980445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 [W927 08:59:48.661990808 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 % (2046835)Instruction limit reached!
% 72.36/11.04 % (2046835)------------------------------
% 72.36/11.04 % (2046835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.36/11.04 % (2046835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.36/11.04 % (2046835)CaDiCaL version: 2.1.3
% 72.36/11.04 % (2046835)Termination reason: Instruction limit
% 72.36/11.04 % (2046835)Termination phase: Saturation
% 72.36/11.04 % (2046835)Time elapsed: 7.127 s
% 72.36/11.04 % (2046835)Peak memory usage: 169 MB
% 72.36/11.04 % (2046835)Instructions burned: 14155 (million)
% 72.36/11.04 % (2046906)------------------------------
% 72.36/11.04 % (2046906)------------------------------
% 72.36/11.04 % (2046909)Refutation not found, incomplete strategy
% 72.36/11.04 % (2046909)------------------------------
% 72.36/11.04 % (2046909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.36/11.04 % (2046909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.36/11.04 % (2046909)CaDiCaL version: 2.1.3
% 72.36/11.04 % (2046909)Termination reason: Refutation not found, incomplete strategy
% 72.36/11.04 % (2046909)Time elapsed: 0.549 s
% 72.36/11.04 % (2046909)Peak memory usage: 125 MB
% 72.36/11.04 % (2046909)Instructions burned: 825 (million)
% 72.36/11.04 % (2046913)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=2372887641:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2906 on theBenchmark for (2906ds/2503Mi)
% 72.36/11.04 % (2046914)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=405899813:i=2559:sd=1:ep=RSTC:ss=axioms_2906 on theBenchmark for (2906ds/2559Mi)
% 72.36/11.04 % (2046909)------------------------------
% 72.36/11.04 % (2046909)------------------------------
% 72.36/11.04 % (2046917)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2823051558:i=30753:av=off:ss=included_2903 on theBenchmark for (2903ds/30753Mi)
% 72.36/11.04 [W927 08:59:48.297543550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 72.36/11.04 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.36/11.04 [W927 08:59:48.297577260 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297614414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297626407 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297651717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297672841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297699011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297709151 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297733511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297743618 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297772095 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.297782445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.307946522 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.307974279 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.44/11.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.44/11.21 [W927 08:59:48.308022696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308036283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308063249 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308083343 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308108950 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308119667 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308143977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308154487 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308178307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 [W927 08:59:48.308188717 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 76.97/11.99 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 76.97/11.99 % (2046913)Refutation not found, incomplete strategy
% 76.97/11.99 % (2046913)------------------------------
% 76.97/11.99 % (2046913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.97/11.99 % (2046913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.97/11.99 % (2046913)CaDiCaL version: 2.1.3
% 76.97/11.99 % (2046913)Termination reason: Refutation not found, incomplete strategy
% 76.97/11.99 % (2046913)Time elapsed: 0.541 s
% 76.97/11.99 % (2046913)Peak memory usage: 125 MB
% 76.97/11.99 % (2046913)Instructions burned: 825 (million)
% 76.97/11.99 % (2046914)Refutation not found, incomplete strategy
% 76.97/11.99 % (2046914)------------------------------
% 76.97/11.99 % (2046914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.97/11.99 % (2046914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.97/11.99 % (2046914)CaDiCaL version: 2.1.3
% 76.97/11.99 % (2046914)Termination reason: Refutation not found, incomplete strategy
% 76.97/11.99 % (2046914)Time elapsed: 0.544 s
% 76.97/11.99 % (2046914)Peak memory usage: 125 MB
% 76.97/11.99 % (2046914)Instructions burned: 825 (million)
% 76.97/11.99 [W927 08:59:49.627512296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627550640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627587387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627600024 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627625627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627636867 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627666567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627677877 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627703181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627714318 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627738145 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 [W927 08:59:49.627749095 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 79.45/12.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 79.45/12.03 % (2046913)------------------------------
% 79.45/12.03 % (2046913)------------------------------
% 79.45/12.03 % (2046914)------------------------------
% 79.45/12.03 % (2046914)------------------------------
% 79.45/12.03 % (2046917)Refutation not found, incomplete strategy
% 79.45/12.03 % (2046917)------------------------------
% 79.45/12.03 % (2046917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.45/12.03 % (2046917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.04/12.57 % (2046917)CaDiCaL version: 2.1.3
% 82.04/12.57 % (2046917)Termination reason: Refutation not found, incomplete strategy
% 82.04/12.57 % (2046917)Time elapsed: 0.543 s
% 82.04/12.57 % (2046917)Peak memory usage: 125 MB
% 82.04/12.57 % (2046917)Instructions burned: 826 (million)
% 82.04/12.57 % (2046919)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=186735456:i=26473:ep=RSTC_2897 on theBenchmark for (2897ds/26473Mi)
% 82.04/12.57 % (2046919)Refutation not found, incomplete strategy
% 82.04/12.57 % (2046919)------------------------------
% 82.04/12.57 % (2046919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.04/12.57 % (2046919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.04/12.57 % (2046919)CaDiCaL version: 2.1.3
% 82.04/12.57 % (2046919)Termination reason: Refutation not found, incomplete strategy
% 82.04/12.57 % (2046919)Time elapsed: 0.004 s
% 82.04/12.57 % (2046919)Peak memory usage: 88 MB
% 82.04/12.57 % (2046919)Instructions burned: 4 (million)
% 82.04/12.57 % (2046920)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=130511122:cts=off:i=2759:kws=inv_arity:fgj=on_2897 on theBenchmark for (2897ds/2759Mi)
% 82.04/12.57 % (2046917)------------------------------
% 82.04/12.57 % (2046917)------------------------------
% 82.04/12.57 % (2046919)------------------------------
% 82.04/12.57 % (2046919)------------------------------
% 82.04/12.57 % (2046923)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=2743955691:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2894 on theBenchmark for (2894ds/5665Mi)
% 82.04/12.57 % (2046924)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=3289196092:i=1532:ep=RS:ss=axioms_2893 on theBenchmark for (2893ds/1532Mi)
% 82.04/12.57 % (2046920)Refutation not found, incomplete strategy
% 82.04/12.57 % (2046920)------------------------------
% 82.04/12.57 % (2046920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.04/12.57 % (2046920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.04/12.57 % (2046920)CaDiCaL version: 2.1.3
% 82.04/12.57 % (2046920)Termination reason: Refutation not found, incomplete strategy
% 82.04/12.57 % (2046920)Time elapsed: 0.551 s
% 82.04/12.57 % (2046920)Peak memory usage: 127 MB
% 82.04/12.57 % (2046920)Instructions burned: 829 (million)
% 82.04/12.57 [W927 08:59:50.579237310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.04/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.04/12.57 [W927 08:59:50.579274190 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.04/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.04/12.57 [W927 08:59:50.579309993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.04/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.04/12.57 [W927 08:59:50.579322447 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.04/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.04/12.57 [W927 08:59:50.579348687 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.04/12.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.04/12.57 [W927 08:59:50.579360490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.579385484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.579395707 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.579419194 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.579429664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.579452974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.579463271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624210907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624244064 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624280961 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624293398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624319634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624330948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 82.66/12.79 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.66/12.79 [W927 08:59:50.624355981 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.25/12.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.25/12.94 [W927 08:59:50.624367091 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.25/12.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.25/12.94 [W927 08:59:50.624391115 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.25/12.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.25/12.94 [W927 08:59:50.624401252 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.25/12.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.25/12.94 [W927 08:59:50.624425572 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.25/12.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.25/12.94 [W927 08:59:50.624435565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 83.25/12.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 83.25/12.94 % (2046920)------------------------------
% 83.25/12.94 % (2046920)------------------------------
% 83.25/12.94 % (2046923)Refutation not found, incomplete strategy
% 83.25/12.94 % (2046923)------------------------------
% 83.25/12.94 % (2046923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.25/12.94 % (2046923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.25/12.94 % (2046923)CaDiCaL version: 2.1.3
% 83.25/12.94 % (2046923)Termination reason: Refutation not found, incomplete strategy
% 83.25/12.94 % (2046923)Time elapsed: 0.543 s
% 83.25/12.94 % (2046923)Peak memory usage: 125 MB
% 83.25/12.94 % (2046923)Instructions burned: 825 (million)
% 83.25/12.94 % (2046924)Refutation not found, incomplete strategy
% 83.25/12.94 % (2046924)------------------------------
% 83.25/12.94 % (2046924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.25/12.94 % (2046924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.25/12.94 % (2046924)CaDiCaL version: 2.1.3
% 83.25/12.94 % (2046924)Termination reason: Refutation not found, incomplete strategy
% 83.25/12.94 % (2046924)Time elapsed: 0.541 s
% 83.25/12.94 % (2046924)Peak memory usage: 125 MB
% 83.25/12.94 % (2046924)Instructions burned: 825 (million)
% 83.25/12.94 % (2046927)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3009622666:i=1565:sd=2:ss=axioms:sgt=32_2887 on theBenchmark for (2887ds/1565Mi)
% 83.25/12.94 % (2046901)Instruction limit reached!
% 83.25/12.94 % (2046901)------------------------------
% 83.25/12.94 % (2046901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.25/12.94 % (2046901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.25/12.94 % (2046901)CaDiCaL version: 2.1.3
% 83.25/12.94 % (2046901)Termination reason: Instruction limit
% 83.25/12.94 % (2046901)Termination phase: Saturation
% 83.25/12.94 % (2046901)Time elapsed: 3.258 s
% 83.25/12.94 % (2046901)Peak memory usage: 148 MB
% 83.25/12.94 % (2046901)Instructions burned: 6996 (million)
% 83.25/12.94 % (2046923)------------------------------
% 83.25/12.94 % (2046923)------------------------------
% 83.25/12.94 % (2046924)------------------------------
% 83.25/12.94 % (2046924)------------------------------
% 83.25/12.94 % (2046929)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=4030375180:i=1572:fgj=on:gsp=on_2885 on theBenchmark for (2885ds/1572Mi)
% 83.25/12.94 % (2046930)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=819883234:i=6052:sd=4:ss=axioms:sgt=24_2884 on theBenchmark for (2884ds/6052Mi)
% 86.55/13.07 % (2046932)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=1671891560:i=3500:sd=1:bd=preordered:sup=off:ss=included_2884 on theBenchmark for (2884ds/3500Mi)
% 86.55/13.07 [W927 08:59:50.216655048 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216699512 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216736562 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216747792 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216773979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216784713 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216830820 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216841730 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216865140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216875507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216899787 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 [W927 08:59:50.216910577 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 86.55/13.07 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 86.55/13.07 % (2046927)Refutation not found, incomplete strategy
% 86.55/13.07 % (2046927)------------------------------
% 86.55/13.07 % (2046927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.32/13.60 % (2046927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.32/13.60 % (2046927)CaDiCaL version: 2.1.3
% 89.32/13.60 % (2046927)Termination reason: Refutation not found, incomplete strategy
% 89.32/13.60 % (2046927)Time elapsed: 0.547 s
% 89.32/13.60 % (2046927)Peak memory usage: 125 MB
% 89.32/13.60 % (2046927)Instructions burned: 822 (million)
% 89.32/13.60 [W927 08:59:51.530667691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530702228 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530739131 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530751951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530778248 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530789728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530815522 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530826725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530851225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530862465 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530887149 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 89.32/13.60 [W927 08:59:51.530898162 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 89.32/13.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.566924212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.566961552 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567000019 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567022169 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567049106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567061766 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567090127 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567101567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567126670 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567137937 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567163157 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 [W927 08:59:51.567174344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 90.26/13.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 90.26/13.90 % (2046927)------------------------------
% 90.26/13.90 % (2046927)------------------------------
% 90.26/13.90 % (2046929)Refutation not found, incomplete strategy
% 90.26/13.90 % (2046929)------------------------------
% 90.26/13.90 % (2046929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.20/14.35 % (2046929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.20/14.35 % (2046929)CaDiCaL version: 2.1.3
% 95.20/14.35 % (2046929)Termination reason: Refutation not found, incomplete strategy
% 95.20/14.35 % (2046929)Time elapsed: 0.621 s
% 95.20/14.35 % (2046929)Peak memory usage: 129 MB
% 95.20/14.35 % (2046929)Instructions burned: 936 (million)
% 95.20/14.35 % (2046930)Refutation not found, incomplete strategy
% 95.20/14.35 % (2046930)------------------------------
% 95.20/14.35 % (2046930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.20/14.35 % (2046930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.20/14.35 % (2046930)CaDiCaL version: 2.1.3
% 95.20/14.35 % (2046930)Termination reason: Refutation not found, incomplete strategy
% 95.20/14.35 % (2046930)Time elapsed: 0.548 s
% 95.20/14.35 % (2046930)Peak memory usage: 125 MB
% 95.20/14.35 % (2046930)Instructions burned: 825 (million)
% 95.20/14.35 % (2046932)Refutation not found, incomplete strategy
% 95.20/14.35 % (2046932)------------------------------
% 95.20/14.35 % (2046932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.20/14.35 % (2046932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.20/14.35 % (2046932)CaDiCaL version: 2.1.3
% 95.20/14.35 % (2046932)Termination reason: Refutation not found, incomplete strategy
% 95.20/14.35 % (2046932)Time elapsed: 0.541 s
% 95.20/14.35 % (2046932)Peak memory usage: 125 MB
% 95.20/14.35 % (2046932)Instructions burned: 822 (million)
% 95.20/14.35 % (2046935)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=2206260966:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2877 on theBenchmark for (2877ds/1842Mi)
% 95.20/14.35 % (2046929)------------------------------
% 95.20/14.35 % (2046929)------------------------------
% 95.20/14.35 % (2046930)------------------------------
% 95.20/14.35 % (2046930)------------------------------
% 95.20/14.35 % (2046932)------------------------------
% 95.20/14.35 % (2046932)------------------------------
% 95.20/14.35 % (2046937)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=3937547610:i=66096:add=on_2875 on theBenchmark for (2875ds/66096Mi)
% 95.20/14.35 % (2046938)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=2970918646:i=1884:sd=1:nm=60:ss=axioms_2874 on theBenchmark for (2874ds/1884Mi)
% 95.20/14.35 % (2046939)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1509563271:cts=off:i=5469:bs=on:fsr=off_2874 on theBenchmark for (2874ds/5469Mi)
% 95.20/14.35 [W927 08:59:51.194408952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.20/14.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.20/14.35 [W927 08:59:51.194441982 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.20/14.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.20/14.35 [W927 08:59:51.194479919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.20/14.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.20/14.35 [W927 08:59:51.194493056 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.20/14.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.20/14.35 [W927 08:59:51.194519266 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.20/14.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.20/14.35 [W927 08:59:51.194530833 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:51.194556307 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:51.194617377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:51.194650907 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:51.194662251 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:51.194687028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:51.194697871 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 % (2046935)Refutation not found, incomplete strategy
% 95.98/14.55 % (2046935)------------------------------
% 95.98/14.55 % (2046935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.55 % (2046935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.55 % (2046935)CaDiCaL version: 2.1.3
% 95.98/14.55 % (2046935)Termination reason: Refutation not found, incomplete strategy
% 95.98/14.55 % (2046935)Time elapsed: 0.543 s
% 95.98/14.55 % (2046935)Peak memory usage: 125 MB
% 95.98/14.55 % (2046935)Instructions burned: 826 (million)
% 95.98/14.55 [W927 08:59:52.490123626 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490160076 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490195866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490208353 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490235357 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490246640 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490270354 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490289864 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490314947 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490325107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490348431 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 [W927 08:59:52.490358651 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 95.98/14.55 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 95.98/14.55 % (2046935)------------------------------
% 95.98/14.55 % (2046935)------------------------------
% 95.98/14.55 % (2046938)Refutation not found, incomplete strategy
% 95.98/14.55 % (2046938)------------------------------
% 95.98/14.55 % (2046938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.55 % (2046938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.55 % (2046938)CaDiCaL version: 2.1.3
% 95.98/14.55 % (2046938)Termination reason: Refutation not found, incomplete strategy
% 95.98/14.55 % (2046938)Time elapsed: 0.541 s
% 95.98/14.55 % (2046938)Peak memory usage: 125 MB
% 95.98/14.55 % (2046938)Instructions burned: 823 (million)
% 95.98/14.55 % (2046937)First to succeed.
% 95.98/14.55 % (2046937)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2046774"
% 95.98/14.55 % (2046948)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=451300848:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2868 on theBenchmark for (2868ds/2037Mi)
% 95.98/14.55 % (2046938)------------------------------
% 95.98/14.55 % (2046938)------------------------------
% 95.98/14.55 % SZS status Satisfiable for theBenchmark
% 95.98/14.55 % SZS output start Saturation.
% See solution above
% 95.98/14.55 % SZS output start Definitions and Model Updates.
% 95.98/14.55 for all inputs,
% 95.98/14.55 define complete := $false
% 95.98/14.55 for all inputs,
% 95.98/14.55 define less_or_equal(X0,X1) := $false
% 95.98/14.55 for all groundings,
% 95.98/14.55 whenever path(X0,X1,X2) & X0 != X1 & ! [X3] : (path(X0,X1,X3) => less_or_equal(length_of(X2),length_of(X3))) is false, set ~shortest_path(X0,X1,X2) to true
% 95.98/14.55 % SZS output end Definitions and Model Updates.
% 95.98/14.55 % (2046937)------------------------------
% 95.98/14.55 % (2046937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.98/14.55 % (2046937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.98/14.55 % (2046937)CaDiCaL version: 2.1.3
% 95.98/14.55 % (2046937)Termination reason: Satisfiable
% 95.98/14.55 % (2046937)Time elapsed: 0.607 s
% 95.98/14.55 % (2046937)Peak memory usage: 128 MB
% 95.98/14.55 % (2046937)Instructions burned: 911 (million)
% 95.98/14.55 % (2046937)------------------------------
% 95.98/14.55 % (2046937)------------------------------
% 95.98/14.55 % (2046774)Success in time 13.497 s
% 95.98/14.55 % Vampire exiting
%------------------------------------------------------------------------------