%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE173+1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:40:33 AM UTC 2026
% Result : Satisfiable 21.25s 4.07s
% Output : Saturation 21.25s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u101,axiom,
zero = c(one) ).
cnf(u105,axiom,
zero = sK0(one) ).
cnf(u114,axiom,
test(one) ).
cnf(u119,axiom,
complement(zero,one) ).
cnf(u135,axiom,
test(zero) ).
cnf(u140,axiom,
one = c(zero) ).
cnf(u350,axiom,
zero = one ).
cnf(u58,axiom,
( ~ test(X0)
| zero = multiplication(X0,sK0(X0)) ) ).
cnf(u37,axiom,
multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2) ).
cnf(u47,axiom,
( ~ complement(X1,X0)
| zero = multiplication(X1,X0) ) ).
cnf(u451,axiom,
complement(X0,zero) ).
cnf(u269,axiom,
multiplication(X0,multiplication(addition(one,X1),X1)) = multiplication(X0,multiplication(X1,addition(one,X1))) ).
cnf(u396,axiom,
X0 = X1 ).
cnf(u187,axiom,
( complement(X0,c(X0))
| zero = c(X0) ) ).
cnf(u164,axiom,
( multiplication(sK0(X0),addition(X0,X1)) = multiplication(sK0(X0),X1)
| zero = c(X0) ) ).
cnf(u45,axiom,
( ~ complement(X1,X0)
| test(X0) ) ).
cnf(u449,axiom,
complement(zero,X0) ).
cnf(u122,axiom,
( ~ test(sK0(X0))
| c(sK0(X0)) = X0
| zero = c(X0) ) ).
cnf(u55,axiom,
( complement(X0,c(X0))
| ~ test(X0) ) ).
cnf(u83,axiom,
( one != addition(X2,multiplication(X0,X1))
| zero != multiplication(X2,multiplication(X0,X1))
| complement(multiplication(X0,X1),X2)
| zero != multiplication(X0,multiplication(X1,X2)) ) ).
cnf(u57,axiom,
( ~ test(X0)
| zero = multiplication(X0,c(X0)) ) ).
cnf(u287,axiom,
( multiplication(c(X0),X1) = multiplication(c(X0),addition(X1,X0))
| zero = c(X0) ) ).
cnf(u289,axiom,
( zero = multiplication(c(X0),multiplication(X0,X1))
| zero = c(X0) ) ).
cnf(u296,axiom,
( c(c(X0)) = X0
| zero = c(X0) ) ).
cnf(u34,axiom,
addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0) ).
cnf(u355,axiom,
zero = c(zero) ).
cnf(u358,axiom,
( zero != X0
| complement(X0,zero) ) ).
cnf(u312,axiom,
( one != X0
| complement(zero,X0) ) ).
cnf(u220,axiom,
( one != X0
| complement(X0,zero) ) ).
cnf(u39,axiom,
multiplication(one,X0) = X0 ).
cnf(u366,axiom,
zero = X0 ).
cnf(u76,axiom,
( zero = multiplication(X0,sK0(X0))
| zero = c(X0) ) ).
cnf(u42,axiom,
zero = multiplication(X0,zero) ).
cnf(u60,axiom,
( ~ test(X0)
| one = addition(X0,sK0(X0)) ) ).
cnf(u88,axiom,
( zero = multiplication(X0,c(X0))
| zero = c(X0) ) ).
cnf(u177,axiom,
( zero = multiplication(X0,multiplication(X1,c(multiplication(X0,X1))))
| zero = c(multiplication(X0,X1)) ) ).
cnf(u263,axiom,
( multiplication(addition(X0,X1),c(X0)) = multiplication(X1,c(X0))
| zero = c(X0) ) ).
cnf(u163,axiom,
addition(X0,multiplication(X0,X1)) = multiplication(X0,addition(X1,one)) ).
cnf(u571,axiom,
test(X0) ).
cnf(u199,axiom,
( sK0(X0) = multiplication(sK0(X0),addition(one,X0))
| zero = c(X0) ) ).
cnf(u201,axiom,
( multiplication(X0,addition(one,c(X0))) = X0
| zero = c(X0) ) ).
cnf(u183,axiom,
( zero = multiplication(X0,multiplication(c(X0),X1))
| zero = c(X0) ) ).
cnf(u44,axiom,
( complement(sK0(X0),X0)
| ~ test(X0) ) ).
cnf(u185,axiom,
( multiplication(X0,X1) = multiplication(X0,addition(X1,c(X0)))
| zero = c(X0) ) ).
cnf(u286,axiom,
( multiplication(X0,X1) = multiplication(addition(X0,c(X1)),X1)
| zero = c(X1) ) ).
cnf(u239,axiom,
multiplication(addition(X3,multiplication(X0,X1)),X2) = addition(multiplication(X3,X2),multiplication(X0,multiplication(X1,X2))) ).
cnf(u41,axiom,
multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)) ).
cnf(u51,axiom,
( ~ complement(X0,X1)
| c(X0) = X1
| ~ test(X0) ) ).
cnf(u97,axiom,
( zero = multiplication(sK0(X0),multiplication(X0,X1))
| zero = c(X0) ) ).
cnf(u283,axiom,
( c(X0) = multiplication(c(X0),addition(one,X0))
| zero = c(X0) ) ).
cnf(u256,axiom,
( multiplication(X0,X1) = multiplication(addition(X0,sK0(X1)),X1)
| zero = c(X1) ) ).
cnf(u456,axiom,
complement(X0,X1) ).
cnf(u49,axiom,
( zero != multiplication(X1,X0)
| zero != multiplication(X0,X1)
| complement(X1,X0)
| addition(X0,X1) != one ) ).
cnf(u59,axiom,
( ~ test(X0)
| zero = multiplication(c(X0),X0) ) ).
cnf(u188,axiom,
( test(c(X0))
| zero = c(X0) ) ).
cnf(u70,axiom,
( one != addition(X0,one)
| complement(one,X0)
| zero != X0 ) ).
cnf(u159,axiom,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)) ).
cnf(u72,axiom,
( one != addition(one,X0)
| complement(X0,one)
| zero != X0 ) ).
cnf(u35,axiom,
addition(X0,zero) = X0 ).
cnf(u54,axiom,
( ~ test(X1)
| ~ test(X0)
| c(multiplication(X0,X1)) = addition(c(X0),c(X1)) ) ).
cnf(u56,axiom,
( ~ test(X0)
| zero = multiplication(sK0(X0),X0) ) ).
cnf(u259,axiom,
( multiplication(addition(X0,X1),c(X1)) = multiplication(X0,c(X1))
| zero = c(X1) ) ).
cnf(u222,axiom,
complement(one,zero) ).
cnf(u43,axiom,
zero = multiplication(zero,X0) ).
cnf(u360,axiom,
( zero != X0
| complement(zero,X0) ) ).
cnf(u73,axiom,
( ~ test(sK0(X0))
| c(sK0(X0)) = X0
| ~ test(X0) ) ).
cnf(u234,axiom,
multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)) ).
cnf(u52,axiom,
( test(X0)
| zero = c(X0) ) ).
cnf(u62,axiom,
( ~ test(X0)
| one = addition(X0,c(X0)) ) ).
cnf(u90,axiom,
( zero = multiplication(sK0(X0),X0)
| zero = c(X0) ) ).
cnf(u108,axiom,
( complement(sK0(X0),X0)
| zero = c(X0) ) ).
cnf(u38,axiom,
multiplication(X0,one) = X0 ).
cnf(u146,axiom,
multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)) ).
cnf(u257,axiom,
addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,one),X0) ).
cnf(u53,axiom,
( ~ test(X1)
| ~ test(X0)
| c(addition(X0,X1)) = multiplication(c(X0),c(X1)) ) ).
cnf(u439,axiom,
( complement(zero,X0)
| ~ test(X0) ) ).
cnf(u285,axiom,
( multiplication(X1,X0) = multiplication(addition(c(X0),X1),X0)
| zero = c(X0) ) ).
cnf(u434,axiom,
( complement(X0,zero)
| ~ test(X0) ) ).
cnf(u33,axiom,
addition(X0,X1) = addition(X1,X0) ).
cnf(u77,axiom,
( one = addition(X0,sK0(X0))
| zero = c(X0) ) ).
cnf(u233,axiom,
multiplication(addition(multiplication(X0,X1),X3),X2) = addition(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2)) ).
cnf(u290,axiom,
( complement(c(X0),X0)
| zero = c(X0) ) ).
cnf(u87,axiom,
( test(c(X0))
| ~ test(X0) ) ).
cnf(u356,axiom,
zero = sK0(zero) ).
cnf(u89,axiom,
( zero = multiplication(c(X0),X0)
| zero = c(X0) ) ).
cnf(u184,axiom,
( multiplication(X0,X1) = multiplication(X0,addition(c(X0),X1))
| zero = c(X0) ) ).
cnf(u145,axiom,
( one = addition(X0,c(X0))
| zero = c(X0) ) ).
cnf(u66,axiom,
addition(zero,X0) = X0 ).
cnf(u40,axiom,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)) ).
cnf(u353,axiom,
multiplication(X0,zero) = X0 ).
cnf(u160,axiom,
( multiplication(sK0(X0),X1) = multiplication(sK0(X0),addition(X1,X0))
| zero = c(X0) ) ).
cnf(u359,axiom,
complement(zero,zero) ).
cnf(u288,axiom,
( multiplication(c(X0),X1) = multiplication(c(X0),addition(X0,X1))
| zero = c(X0) ) ).
cnf(u261,axiom,
( multiplication(X1,X0) = multiplication(addition(sK0(X0),X1),X0)
| zero = c(X0) ) ).
cnf(u251,axiom,
multiplication(addition(X0,X1),X2) = addition(multiplication(X1,X2),multiplication(X0,X2)) ).
cnf(u354,axiom,
multiplication(zero,X0) = X0 ).
cnf(u36,axiom,
addition(X0,X0) = X0 ).
cnf(u46,axiom,
( ~ complement(X1,X0)
| addition(X0,X1) = one ) ).
cnf(u48,axiom,
( ~ complement(X1,X0)
| zero = multiplication(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE173+1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n016.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 13:19:57 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.39/1.71 % (2641180)Detected formulas, will run a generic FOF schedule.
% 5.39/1.71 % (2641201)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=836016032:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.39/1.71 % (2641201)Refutation not found, incomplete strategy
% 5.39/1.71 % (2641201)------------------------------
% 5.39/1.71 % (2641201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.71 % (2641201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.71 % (2641201)CaDiCaL version: 2.1.3
% 5.39/1.71 % (2641201)Termination reason: Refutation not found, incomplete strategy
% 5.39/1.71 % (2641201)Time elapsed: 0.0000 s
% 5.39/1.71 % (2641201)Peak memory usage: 86 MB
% 5.39/1.71 % (2641204)dis-21_1_sil=8000:lcm=predicate:random_seed=3886316328: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)
% 5.39/1.71 % (2641204)Refutation not found, incomplete strategy
% 5.39/1.71 % (2641204)------------------------------
% 5.39/1.71 % (2641204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.71 % (2641204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.71 % (2641204)CaDiCaL version: 2.1.3
% 5.39/1.71 % (2641204)Termination reason: Refutation not found, incomplete strategy
% 5.39/1.71 % (2641204)Time elapsed: 0.001 s
% 5.39/1.71 % (2641204)Peak memory usage: 86 MB
% 5.39/1.71 % (2641198)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=2287630478:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.39/1.71 % (2641200)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=480951519:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.39/1.71 % (2641199)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=2497346375:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.39/1.71 % (2641203)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3479876709:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.39/1.71 % (2641202)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1855524197:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.39/1.71 % (2641202)Refutation not found, incomplete strategy
% 5.39/1.71 % (2641202)------------------------------
% 5.39/1.71 % (2641202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.71 % (2641202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.71 % (2641202)CaDiCaL version: 2.1.3
% 5.39/1.71 % (2641202)Termination reason: Refutation not found, incomplete strategy
% 5.39/1.71 % (2641202)Time elapsed: 0.001 s
% 5.39/1.71 % (2641202)Peak memory usage: 86 MB
% 5.39/1.71 % (2641203)Refutation not found, incomplete strategy
% 5.39/1.71 % (2641203)------------------------------
% 5.39/1.71 % (2641203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.71 % (2641203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.71 % (2641203)CaDiCaL version: 2.1.3
% 5.39/1.71 % (2641203)Termination reason: Refutation not found, incomplete strategy
% 5.39/1.71 % (2641203)Time elapsed: 0.075 s
% 5.39/1.71 % (2641203)Peak memory usage: 89 MB
% 5.39/1.71 % (2641203)Instructions burned: 89 (million)
% 5.39/1.71 % (2641201)------------------------------
% 5.39/1.71 % (2641201)------------------------------
% 5.39/1.71 % (2641204)------------------------------
% 5.39/1.71 % (2641204)------------------------------
% 5.39/1.71 % (2641227)lrs+10_1_sil=8000:sp=occurrence:random_seed=2856750591:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 5.39/1.71 % (2641227)Refutation not found, incomplete strategy
% 5.39/1.71 % (2641227)------------------------------
% 5.39/1.71 % (2641227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.71 % (2641227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.71 % (2641227)CaDiCaL version: 2.1.3
% 5.39/1.71 % (2641227)Termination reason: Refutation not found, incomplete strategy
% 5.39/1.71 % (2641227)Time elapsed: 0.0000 s
% 5.39/1.71 % (2641227)Peak memory usage: 86 MB
% 5.39/1.71 % (2641202)------------------------------
% 8.45/2.38 % (2641202)------------------------------
% 8.45/2.38 % (2641203)------------------------------
% 8.45/2.38 % (2641203)------------------------------
% 8.45/2.38 [W927 13:19:58.329788578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329823345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329862038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329874182 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329898422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329909579 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329933482 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329944509 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329968472 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.329979485 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.330017562 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.330030345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.45/2.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.45/2.38 [W927 13:19:58.355559316 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355609906 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355669172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355766909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355827209 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355845953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355891196 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355909116 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355951956 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.355969999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.356023033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 [W927 13:19:58.356043400 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 11.84/2.87 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 11.84/2.87 % (2641227)------------------------------
% 11.84/2.87 % (2641227)------------------------------
% 11.84/2.87 % (2641230)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3749607678:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 11.84/2.87 % (2641230)Refutation not found, incomplete strategy
% 11.84/2.87 % (2641230)------------------------------
% 11.84/2.87 % (2641230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.84/2.87 % (2641230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.84/2.87 % (2641230)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641230)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.47 % (2641230)Time elapsed: 0.001 s
% 17.52/3.47 % (2641230)Peak memory usage: 87 MB
% 17.52/3.47 % (2641199)Refutation not found, incomplete strategy
% 17.52/3.47 % (2641199)------------------------------
% 17.52/3.47 % (2641199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.47 % (2641199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.47 % (2641199)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641199)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.47 % (2641199)Time elapsed: 0.746 s
% 17.52/3.47 % (2641199)Peak memory usage: 125 MB
% 17.52/3.47 % (2641199)Instructions burned: 826 (million)
% 17.52/3.47 % (2641234)lrs+1011_1_sil=32000:sp=occurrence:random_seed=468791329:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 17.52/3.47 % (2641234)Refutation not found, incomplete strategy
% 17.52/3.47 % (2641234)------------------------------
% 17.52/3.47 % (2641234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.47 % (2641234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.47 % (2641234)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641234)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.47 % (2641234)Time elapsed: 0.001 s
% 17.52/3.47 % (2641234)Peak memory usage: 86 MB
% 17.52/3.47 % (2641236)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=1406922594:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 17.52/3.47 % (2641200)Refutation not found, incomplete strategy
% 17.52/3.47 % (2641200)------------------------------
% 17.52/3.47 % (2641200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.47 % (2641200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.47 % (2641200)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641200)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.47 % (2641200)Time elapsed: 0.839 s
% 17.52/3.47 % (2641200)Peak memory usage: 125 MB
% 17.52/3.47 % (2641200)Instructions burned: 825 (million)
% 17.52/3.47 % (2641240)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2504538986:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 17.52/3.47 % (2641240)Refutation not found, incomplete strategy
% 17.52/3.47 % (2641240)------------------------------
% 17.52/3.47 % (2641240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.47 % (2641240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.47 % (2641240)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641240)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.47 % (2641240)Time elapsed: 0.0000 s
% 17.52/3.47 % (2641240)Peak memory usage: 86 MB
% 17.52/3.47 % (2641230)------------------------------
% 17.52/3.47 % (2641230)------------------------------
% 17.52/3.47 % (2641236)Instruction limit reached!
% 17.52/3.47 % (2641236)------------------------------
% 17.52/3.47 % (2641236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.47 % (2641236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.47 % (2641236)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641236)Termination reason: Instruction limit
% 17.52/3.47 % (2641236)Termination phase: Saturation
% 17.52/3.47 % (2641236)Time elapsed: 0.237 s
% 17.52/3.47 % (2641236)Peak memory usage: 91 MB
% 17.52/3.47 % (2641236)Instructions burned: 249 (million)
% 17.52/3.47 % (2641198)Refutation not found, incomplete strategy
% 17.52/3.47 % (2641198)------------------------------
% 17.52/3.47 % (2641198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.47 % (2641198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.47 % (2641198)CaDiCaL version: 2.1.3
% 17.52/3.47 % (2641198)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.47 % (2641198)Time elapsed: 1.071 s
% 17.52/3.47 % (2641198)Peak memory usage: 129 MB
% 17.52/3.47 % (2641198)Instructions burned: 1014 (million)
% 17.52/3.47 % (2641240)------------------------------
% 17.52/3.47 % (2641240)------------------------------
% 17.52/3.47 % (2641234)------------------------------
% 17.52/3.47 % (2641234)------------------------------
% 17.52/3.47 % (2641199)------------------------------
% 17.52/3.47 % (2641199)------------------------------
% 17.52/3.47 % (2641200)------------------------------
% 17.52/3.47 % (2641200)------------------------------
% 17.52/3.47 % (2641249)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3927858734:i=2350_2987 on theBenchmark for (2987ds/2350Mi)
% 18.30/3.59 % (2641252)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1512220975:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 18.30/3.59 % (2641251)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3019969130:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 18.30/3.59 % (2641252)Refutation not found, incomplete strategy
% 18.30/3.59 % (2641252)------------------------------
% 18.30/3.59 % (2641252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/3.59 % (2641252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/3.59 % (2641252)CaDiCaL version: 2.1.3
% 18.30/3.59 % (2641252)Termination reason: Refutation not found, incomplete strategy
% 18.30/3.59 % (2641252)Time elapsed: 0.001 s
% 18.30/3.59 % (2641252)Peak memory usage: 87 MB
% 18.30/3.59 % (2641251)Refutation not found, incomplete strategy
% 18.30/3.59 % (2641251)------------------------------
% 18.30/3.59 % (2641251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/3.59 % (2641251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/3.59 % (2641251)CaDiCaL version: 2.1.3
% 18.30/3.59 % (2641251)Termination reason: Refutation not found, incomplete strategy
% 18.30/3.59 % (2641251)Time elapsed: 0.001 s
% 18.30/3.59 % (2641251)Peak memory usage: 86 MB
% 18.30/3.59 % (2641256)lrs+10_1_sil=8000:sp=occurrence:random_seed=1169739060:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 18.30/3.59 % (2641253)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1357264472:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 18.30/3.59 % (2641256)Refutation not found, incomplete strategy
% 18.30/3.59 % (2641256)------------------------------
% 18.30/3.59 % (2641256)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/3.59 % (2641256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/3.59 % (2641256)CaDiCaL version: 2.1.3
% 18.30/3.59 % (2641256)Termination reason: Refutation not found, incomplete strategy
% 18.30/3.59 % (2641256)Time elapsed: 0.001 s
% 18.30/3.59 % (2641256)Peak memory usage: 86 MB
% 18.30/3.59 % (2641253)Refutation not found, incomplete strategy
% 18.30/3.59 % (2641253)------------------------------
% 18.30/3.59 % (2641253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/3.59 % (2641253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/3.59 % (2641253)CaDiCaL version: 2.1.3
% 18.30/3.59 % (2641253)Termination reason: Refutation not found, incomplete strategy
% 18.30/3.59 % (2641253)Time elapsed: 0.001 s
% 18.30/3.59 % (2641253)Peak memory usage: 87 MB
% 18.30/3.59 % (2641198)------------------------------
% 18.30/3.59 % (2641198)------------------------------
% 18.30/3.59 % (2641257)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1433844096:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 18.30/3.59 % (2641257)Refutation not found, incomplete strategy
% 18.30/3.59 % (2641257)------------------------------
% 18.30/3.59 % (2641257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/3.59 % (2641257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/3.59 % (2641257)CaDiCaL version: 2.1.3
% 18.30/3.59 % (2641257)Termination reason: Refutation not found, incomplete strategy
% 18.30/3.59 % (2641257)Time elapsed: 0.001 s
% 18.30/3.59 % (2641257)Peak memory usage: 86 MB
% 18.30/3.59 % (2641252)------------------------------
% 18.30/3.59 % (2641252)------------------------------
% 18.30/3.59 % (2641256)------------------------------
% 18.30/3.59 % (2641256)------------------------------
% 18.30/3.59 % (2641251)------------------------------
% 18.30/3.59 % (2641251)------------------------------
% 18.30/3.59 % (2641253)------------------------------
% 18.30/3.59 % (2641253)------------------------------
% 18.30/3.59 % (2641267)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=537194919:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 18.30/3.59 % (2641272)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2524158681:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 18.30/3.59 % (2641272)Refutation not found, incomplete strategy
% 19.39/3.72 % (2641272)------------------------------
% 19.39/3.72 % (2641272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.72 % (2641272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.72 % (2641272)CaDiCaL version: 2.1.3
% 19.39/3.72 % (2641272)Termination reason: Refutation not found, incomplete strategy
% 19.39/3.72 % (2641272)Time elapsed: 0.001 s
% 19.39/3.72 % (2641272)Peak memory usage: 86 MB
% 19.39/3.72 % (2641275)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3376651012:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 19.39/3.72 % (2641257)------------------------------
% 19.39/3.72 % (2641257)------------------------------
% 19.39/3.72 % (2641274)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=808981348:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 19.39/3.72 % (2641274)Refutation not found, incomplete strategy
% 19.39/3.72 % (2641274)------------------------------
% 19.39/3.72 % (2641274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.72 % (2641274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.72 % (2641274)CaDiCaL version: 2.1.3
% 19.39/3.72 % (2641274)Termination reason: Refutation not found, incomplete strategy
% 19.39/3.72 % (2641274)Time elapsed: 0.001 s
% 19.39/3.72 % (2641274)Peak memory usage: 86 MB
% 19.39/3.72 % (2641272)------------------------------
% 19.39/3.72 % (2641272)------------------------------
% 19.39/3.72 % (2641279)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=376132118:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 19.39/3.72 % (2641279)Refutation not found, incomplete strategy
% 19.39/3.72 % (2641279)------------------------------
% 19.39/3.72 % (2641279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.72 % (2641279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.72 % (2641279)CaDiCaL version: 2.1.3
% 19.39/3.72 % (2641279)Termination reason: Refutation not found, incomplete strategy
% 19.39/3.72 % (2641279)Time elapsed: 0.001 s
% 19.39/3.72 % (2641279)Peak memory usage: 87 MB
% 19.39/3.72 % (2641285)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1691979432:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 19.39/3.72 % (2641290)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3059661311:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 19.39/3.72 % (2641290)Refutation not found, incomplete strategy
% 19.39/3.72 % (2641290)------------------------------
% 19.39/3.72 % (2641290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.72 % (2641290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.72 % (2641290)CaDiCaL version: 2.1.3
% 19.39/3.72 % (2641290)Termination reason: Refutation not found, incomplete strategy
% 19.39/3.72 % (2641290)Time elapsed: 0.001 s
% 19.39/3.72 % (2641290)Peak memory usage: 86 MB
% 19.39/3.72 % (2641274)------------------------------
% 19.39/3.72 % (2641274)------------------------------
% 19.39/3.72 % (2641285)Instruction limit reached!
% 19.39/3.72 % (2641285)------------------------------
% 19.39/3.72 % (2641285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.39/3.72 % (2641285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.39/3.72 % (2641285)CaDiCaL version: 2.1.3
% 19.39/3.72 % (2641285)Termination reason: Instruction limit
% 19.39/3.72 % (2641285)Termination phase: Saturation
% 19.39/3.72 % (2641285)Time elapsed: 0.121 s
% 19.39/3.72 % (2641285)Peak memory usage: 88 MB
% 19.39/3.72 % (2641285)Instructions burned: 137 (million)
% 19.39/3.72 % (2641249)First to succeed.
% 19.39/3.72 % (2641249)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2641180"
% 19.39/3.72 [W927 13:20:00.157136901 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.39/3.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.39/3.72 [W927 13:20:00.157190168 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157251984 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157286704 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157334668 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157353091 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157397241 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157415281 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157460375 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157479091 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157523408 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.157541531 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 % (2641279)------------------------------
% 17.50/3.82 % (2641279)------------------------------
% 17.50/3.82 % (2641290)------------------------------
% 17.50/3.82 % (2641290)------------------------------
% 17.50/3.82 [W927 13:20:00.276928567 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277079374 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277158611 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277178731 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277224977 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277242211 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277287497 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277304631 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277347384 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277364584 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277407101 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 [W927 13:20:00.277424718 register_special_ops.cpp:225] Warning: Creating a tensor from 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.50/3.82 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 17.50/3.82 % (2641295)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1417539900:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 17.50/3.82 % (2641295)Refutation not found, incomplete strategy
% 17.50/3.82 % (2641295)------------------------------
% 17.50/3.82 % (2641295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.50/3.82 % (2641295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.50/3.82 % (2641295)CaDiCaL version: 2.1.3
% 17.50/3.82 % (2641295)Termination reason: Refutation not found, incomplete strategy
% 17.50/3.82 % (2641295)Time elapsed: 0.001 s
% 17.50/3.82 % (2641295)Peak memory usage: 86 MB
% 17.50/3.82 % (2641297)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=1710329811:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 17.50/3.82 % (2641299)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=721924554:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 21.25/4.07 % (2641267)Refutation not found, incomplete strategy
% 21.25/4.07 % (2641267)------------------------------
% 21.25/4.07 % (2641267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.25/4.07 % (2641267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.25/4.07 % (2641267)CaDiCaL version: 2.1.3
% 21.25/4.07 % (2641267)Termination reason: Refutation not found, incomplete strategy
% 21.25/4.07 % (2641267)Time elapsed: 0.901 s
% 21.25/4.07 % (2641267)Peak memory usage: 125 MB
% 21.25/4.07 % (2641267)Instructions burned: 826 (million)
% 21.25/4.07 % SZS status Satisfiable for theBenchmark
% 21.25/4.07 % SZS output start Saturation.
% See solution above
% 21.25/4.07 % SZS output start Definitions and Model Updates.
% 21.25/4.07 for all inputs,
% 21.25/4.07 define leq(X0,X1) := addition(X0,X1) = X1
% 21.25/4.07 for all inputs,
% 21.25/4.07 define ismeet(X2,X0,X1) := leq(X2,X0) & leq(X2,X1) & ! [X3] : ((leq(X3,X0) & leq(X3,X1)) => leq(X3,X2))
% 21.25/4.07 for all inputs,
% 21.25/4.07 define ismeetu(X2,X0,X1) := ! [X3] : ((leq(X3,X0) & leq(X3,X1)) <=> leq(X3,X2))
% 21.25/4.07 % SZS output end Definitions and Model Updates.
% 21.25/4.07 % (2641249)------------------------------
% 21.25/4.07 % (2641249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.25/4.07 % (2641249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.25/4.07 % (2641249)CaDiCaL version: 2.1.3
% 21.25/4.07 % (2641249)Termination reason: Satisfiable
% 21.25/4.07 % (2641249)Time elapsed: 1.025 s
% 21.25/4.07 % (2641249)Peak memory usage: 130 MB
% 21.25/4.07 % (2641249)Instructions burned: 1010 (million)
% 21.25/4.07 % (2641249)------------------------------
% 21.25/4.07 % (2641249)------------------------------
% 21.25/4.07 % (2641180)Success in time 2.945 s
% 21.25/4.07 % Vampire exiting
%------------------------------------------------------------------------------