%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT055-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:45:55 AM UTC 2026
% Result : Satisfiable 142.81s 21.48s
% Output : Saturation 143.83s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2271,axiom,
join(n1,n0,X1) ).
cnf(absorbtion1,axiom,
( ~ meet(X0,X1,X2)
| join(X0,X2,X0) ) ).
cnf(u58,axiom,
( ~ meet(X2,X0,X3)
| ~ meet(X0,X1,X2)
| meet(X3,X1,X2) ) ).
cnf(join_total_function_1,axiom,
join(X0,X1,join_of(X0,X1)) ).
cnf(u104,axiom,
( ~ meet(X0,X3,X0)
| ~ meet(X1,X3,X4)
| ~ join(X0,X1,X2)
| join(X0,X4,meet_of(X3,X2)) ) ).
cnf(u413,axiom,
( join(X0,meet_of(X2,X1),X2)
| ~ join(X0,X1,X2) ) ).
cnf(u65,axiom,
join(X0,meet_of(X1,X0),X0) ).
cnf(u47,axiom,
( ~ meet(X0,n1,X1)
| X0 = X1 ) ).
cnf(u523,axiom,
( join(n0,X2,join_of(X0,X1))
| ~ join(X0,X1,X2) ) ).
cnf(u391,axiom,
meet(meet_of(X0,X1),X1,meet_of(X0,X1)) ).
cnf(u479,axiom,
( meet(X0,X2,meet_of(X0,X1))
| ~ meet(X0,X1,X2) ) ).
cnf(u409,axiom,
( ~ join(X0,n1,X1)
| join(X0,X1,X1) ) ).
cnf(u24,axiom,
meet(X0,X1,meet_of(X1,X0)) ).
cnf(u205,axiom,
meet_of(X0,join_of(X0,X1)) = X0 ).
cnf(associativity_of_meet2,axiom,
( ~ meet(X2,X3,X5)
| ~ meet(X1,X3,X4)
| ~ meet(X0,X1,X2)
| meet(X0,X4,X5) ) ).
cnf(u134,axiom,
n0 = meet_of(n0,X0) ).
cnf(u189,axiom,
join_of(X0,n0) = X0 ).
cnf(u110,axiom,
( ~ meet(X1,X2,X3)
| ~ join(X0,X1,X2)
| join(X0,X3,X2) ) ).
cnf(u27,axiom,
join(X0,n0,X0) ).
cnf(u446,axiom,
( ~ join(n0,X0,X1)
| meet(n1,X1,X0) ) ).
cnf(u1811,axiom,
( ~ meet(n1,n1,X1)
| meet(X0,X1,X0) ) ).
cnf(u45,axiom,
( ~ meet(n1,X0,X1)
| X0 = X1 ) ).
cnf(u412,axiom,
( join(X0,meet_of(X1,X2),X2)
| ~ join(X0,X1,X2) ) ).
cnf(u55,axiom,
( ~ join(X0,n1,X1)
| n1 = X1 ) ).
cnf(u219,axiom,
join_of(X0,meet_of(X1,X0)) = X0 ).
cnf(u57,axiom,
( ~ meet(n0,X0,X3)
| ~ meet(X0,X1,X2)
| meet(X3,X1,n0) ) ).
cnf(u101,axiom,
( ~ meet(X0,n0,X0)
| ~ meet(X1,n0,X3)
| ~ join(X0,X1,X2)
| join(X0,X3,n0) ) ).
cnf(u2299,axiom,
X0 = X1 ).
cnf(u178,axiom,
join_of(X0,X0) = X0 ).
cnf(join_total_function_2,axiom,
( ~ join(X0,X1,X3)
| ~ join(X0,X1,X2)
| X2 = X3 ) ).
cnf(u68,axiom,
( ~ meet(X3,X0,X1)
| ~ meet(X0,X1,X2)
| meet(X3,X2,X1) ) ).
cnf(u1744,axiom,
( ~ meet(X1,n0,X0)
| meet(n1,X0,n0) ) ).
cnf(u2274,axiom,
join(X0,X1,n1) ).
cnf(u1655,axiom,
( ~ meet(n0,X1,n1)
| meet(n0,X1,X0) ) ).
cnf(u2277,axiom,
n1 = X0 ).
cnf(u272,axiom,
( ~ meet(X0,X0,X1)
| meet(n1,X1,X0) ) ).
cnf(u283,axiom,
( ~ meet(n1,X0,X1)
| meet(n1,X1,X0) ) ).
cnf(u304,axiom,
( join(join_of(X0,X2),X1,X2)
| ~ join(X0,X1,X2) ) ).
cnf(u1702,axiom,
( ~ meet(X0,n0,X1)
| meet(X0,X1,n0) ) ).
cnf(u1607,axiom,
( ~ meet(n1,X1,n0)
| meet(X0,X1,n0) ) ).
cnf(u507,axiom,
( join(n1,X0,join_of(X2,X1))
| ~ join(n1,X0,X1) ) ).
cnf(u335,axiom,
( ~ join(meet_of(X0,X1),X0,X2)
| join(X0,X2,X0) ) ).
cnf(u215,axiom,
join_of(X0,X1) = join_of(X1,X0) ).
cnf(u91,axiom,
( ~ join(X3,X0,X4)
| ~ join(X0,X1,X2)
| join(X3,X2,join_of(X4,X1)) ) ).
cnf(u135,axiom,
n0 = meet_of(X0,n0) ).
cnf(u500,axiom,
( join(X0,X1,join_of(X0,X2))
| ~ join(X0,X1,X2) ) ).
cnf(u109,axiom,
( ~ meet(X1,n1,X3)
| ~ join(X0,X1,X2)
| join(X0,X3,X2) ) ).
cnf(u275,axiom,
( ~ meet(n1,X0,X1)
| meet(X0,X1,X0) ) ).
cnf(u119,axiom,
( ~ meet(X0,X3,X0)
| ~ meet(X1,X3,X4)
| ~ join(X0,X1,X2)
| meet(X3,X2,join_of(X0,X4)) ) ).
cnf(u147,axiom,
meet_of(X0,X0) = X0 ).
cnf(u2301,axiom,
join(X0,X1,X0) ).
cnf(join_0_and_x,axiom,
join(n0,X0,X0) ).
cnf(u60,axiom,
( ~ meet(X3,X0,X4)
| ~ meet(X0,X1,X2)
| meet(X4,X1,meet_of(X3,X2)) ) ).
cnf(u88,axiom,
( ~ join(X3,X0,n1)
| ~ join(X0,X1,X2)
| join(X3,X2,n1) ) ).
cnf(u21,axiom,
meet(X0,n0,n0) ).
cnf(u3013,axiom,
( ~ meet(X0,X1,n1)
| meet(n1,X1,X2) ) ).
cnf(u59,axiom,
( ~ meet(n1,X0,X3)
| ~ meet(X0,X1,X2)
| meet(X3,X1,X2) ) ).
cnf(u508,axiom,
( join(X2,X0,join_of(X2,X1))
| ~ join(n0,X0,X1) ) ).
cnf(u306,axiom,
( ~ join(n0,X0,X1)
| join(X1,X0,X1) ) ).
cnf(u263,axiom,
( ~ meet(n0,X0,X1)
| meet(X2,X1,n0) ) ).
cnf(u419,axiom,
join(join_of(X0,X1),X1,join_of(X0,X1)) ).
cnf(u2304,axiom,
join(X1,X0,X0) ).
cnf(u2281,axiom,
meet(n1,X0,n1) ).
cnf(u271,axiom,
( ~ meet(X0,X0,X1)
| meet(X0,X1,X0) ) ).
cnf(u444,axiom,
( meet(X2,X1,meet_of(X2,X0))
| ~ join(n0,X0,X1) ) ).
cnf(u1701,axiom,
( ~ meet(X0,n1,X1)
| meet(X0,X1,X0) ) ).
cnf(u238,axiom,
( meet(meet_of(X0,X2),X1,X2)
| ~ meet(X0,X1,X2) ) ).
cnf(u1812,axiom,
( ~ meet(n1,n0,X1)
| meet(X0,X1,n0) ) ).
cnf(u448,axiom,
( meet(join_of(X0,X2),X1,X0)
| ~ join(n0,X0,X1) ) ).
cnf(associativity_of_meet1,axiom,
( ~ meet(X0,X4,X5)
| ~ meet(X1,X3,X4)
| ~ meet(X0,X1,X2)
| meet(X2,X3,X5) ) ).
cnf(u1743,axiom,
( ~ meet(X0,n1,X1)
| meet(n1,X1,X0) ) ).
cnf(u1959,axiom,
( ~ join(n1,X1,n0)
| join(n1,X1,X0) ) ).
cnf(u415,axiom,
( ~ join(X0,X1,n0)
| join(X0,n0,n0) ) ).
cnf(u67,axiom,
( ~ meet(X3,X0,n0)
| ~ meet(X0,X1,X2)
| meet(X3,X2,n0) ) ).
cnf(u239,axiom,
( ~ meet(n1,X0,X1)
| meet(X1,X0,X1) ) ).
cnf(u3024,axiom,
( ~ meet(X0,X1,n1)
| meet(X2,X1,n1)
| ~ join(n1,X2,X0) ) ).
cnf(u85,axiom,
( ~ join(X0,meet_of(X0,X1),X2)
| X0 = X2 ) ).
cnf(meet_1_and_x,axiom,
meet(n1,X0,X0) ).
cnf(u51,axiom,
( ~ join(n1,X0,X1)
| n1 = X1 ) ).
cnf(u1888,axiom,
( ~ join(X0,X1,n0)
| join(X0,X1,X0) ) ).
cnf(commutativity_of_join,axiom,
( ~ join(X0,X1,X2)
| join(X1,X0,X2) ) ).
cnf(meet_total_function_2,axiom,
( ~ meet(X0,X1,X3)
| ~ meet(X0,X1,X2)
| X2 = X3 ) ).
cnf(u3203,axiom,
meet(X1,X0,X2) ).
cnf(u329,axiom,
( ~ join(X0,X0,X1)
| join(X0,X1,X0) ) ).
cnf(u353,axiom,
( ~ join(n0,X0,X1)
| join(n0,X1,X0) ) ).
cnf(modularity2,axiom,
( ~ join(X0,X4,X5)
| ~ join(X0,X2,X3)
| ~ meet(X2,X1,X4)
| ~ meet(X0,X1,X0)
| meet(X1,X3,X5) ) ).
cnf(u3128,axiom,
meet(X1,X0,n1) ).
cnf(u1546,axiom,
( ~ meet(X0,X1,n1)
| meet(X0,X1,X0) ) ).
cnf(u334,axiom,
( ~ join(n0,X0,X1)
| join(X0,X1,X0) ) ).
cnf(u466,axiom,
( meet(n0,X0,meet_of(X2,X1))
| ~ meet(n0,X0,X1) ) ).
cnf(u440,axiom,
( ~ join(n0,n1,X0)
| meet(X1,X0,X1) ) ).
cnf(u237,axiom,
( meet(meet_of(X2,X0),X1,X2)
| ~ meet(X0,X1,X2) ) ).
cnf(u158,axiom,
meet_of(X0,n1) = X0 ).
cnf(u75,axiom,
meet(X0,join_of(X1,X0),X0) ).
cnf(meet_0_and_x,axiom,
meet(n0,X0,n0) ).
cnf(u2844,axiom,
join(n1,n1,X0) ).
cnf(associativity_of_join2,axiom,
( ~ join(X2,X3,X5)
| ~ join(X1,X3,X4)
| ~ join(X0,X1,X2)
| join(X0,X4,X5) ) ).
cnf(u170,axiom,
n1 = join_of(X0,n1) ).
cnf(u338,axiom,
meet(meet_of(X0,X1),X0,meet_of(X0,X1)) ).
cnf(u131,axiom,
meet(join_of(X0,X1),X1,X1) ).
cnf(u188,axiom,
join_of(n0,X0) = X0 ).
cnf(u3046,axiom,
meet(X0,X1,X0) ).
cnf(u70,axiom,
( ~ meet(X3,X0,X4)
| ~ meet(X0,X1,X2)
| meet(X3,X2,meet_of(X4,X1)) ) ).
cnf(u115,axiom,
join(meet_of(X0,X1),X1,X1) ).
cnf(u44,axiom,
( ~ meet(X0,X0,X1)
| X0 = X1 ) ).
cnf(meet_x_and_x,axiom,
meet(X0,X0,X0) ).
cnf(u54,axiom,
( ~ join(X0,X1,X2)
| join_of(X0,X1) = X2 ) ).
cnf(u458,axiom,
( meet(X0,X1,meet_of(X0,X2))
| ~ meet(X0,X1,X2) ) ).
cnf(modularity1,axiom,
( ~ meet(X1,X3,X5)
| ~ join(X0,X2,X3)
| ~ meet(X2,X1,X4)
| ~ meet(X0,X1,X0)
| join(X0,X4,X5) ) ).
cnf(u56,axiom,
( ~ join(X0,n0,X1)
| X0 = X1 ) ).
cnf(u3580,axiom,
join(X0,X2,X3) ).
cnf(meet_total_function_1,axiom,
meet(X0,X1,meet_of(X0,X1)) ).
cnf(u521,axiom,
( join(X0,X2,join_of(X0,X1))
| ~ join(X0,X1,X2) ) ).
cnf(u330,axiom,
( ~ join(X0,X0,X1)
| join(n0,X1,X0) ) ).
cnf(u202,axiom,
meet_of(X0,X1) = meet_of(X1,X0) ).
cnf(u241,axiom,
( ~ meet(join_of(X0,X1),X2,X0)
| meet(X0,X2,X0) ) ).
cnf(u277,axiom,
( ~ meet(join_of(X0,X1),X0,X2)
| meet(X0,X2,X0) ) ).
cnf(u324,axiom,
( ~ join(n1,X0,X1)
| join(X2,X1,n1) ) ).
cnf(u157,axiom,
meet_of(n1,X0) = X0 ).
cnf(u78,axiom,
( ~ join(X2,X0,X3)
| ~ join(X0,X1,X2)
| join(X3,X1,X2) ) ).
cnf(u52,axiom,
( ~ join(X0,X0,X1)
| X0 = X1 ) ).
cnf(u80,axiom,
( ~ join(X3,X0,X4)
| ~ join(X0,X1,X2)
| join(X4,X1,join_of(X3,X2)) ) ).
cnf(associativity_of_join1,axiom,
( ~ join(X0,X4,X5)
| ~ join(X1,X3,X4)
| ~ join(X0,X1,X2)
| join(X2,X3,X5) ) ).
cnf(u90,axiom,
( ~ join(X3,X0,n0)
| ~ join(X0,X1,X2)
| join(X3,X2,X1) ) ).
cnf(u23,axiom,
meet(X0,n1,X0) ).
cnf(u25,axiom,
join(X0,n1,n1) ).
cnf(u69,axiom,
( ~ meet(X3,X0,n1)
| ~ meet(X0,X1,X2)
| meet(X3,X2,X1) ) ).
cnf(u1399,axiom,
( ~ join(n0,X0,X1)
| meet(X1,X0,X1) ) ).
cnf(u79,axiom,
( ~ join(n0,X0,X3)
| ~ join(X0,X1,X2)
| join(X3,X1,X2) ) ).
cnf(u3058,axiom,
( ~ join(X0,n1,X1)
| join(X0,X2,X1) ) ).
cnf(u53,axiom,
( ~ join(n0,X0,X1)
| X0 = X1 ) ).
cnf(u3045,axiom,
meet(n1,X0,X1) ).
cnf(join_x_and_x,axiom,
join(X0,X0,X0) ).
cnf(u439,axiom,
( ~ join(n0,X0,X1)
| meet(X0,X1,X0) ) ).
cnf(u3028,axiom,
meet(n1,n1,X0) ).
cnf(u441,axiom,
( ~ join(n0,n0,X0)
| meet(X1,X0,n0) ) ).
cnf(u323,axiom,
( ~ join(n1,X0,X1)
| join(n0,X1,n1) ) ).
cnf(u307,axiom,
( ~ join(meet_of(X0,X1),X2,X0)
| join(X0,X2,X0) ) ).
cnf(u529,axiom,
( join(X2,X1,join_of(X2,X0))
| ~ join(n0,X0,X1) ) ).
cnf(u443,axiom,
( meet(X2,X1,meet_of(X0,X2))
| ~ join(n0,X0,X1) ) ).
cnf(u116,axiom,
( ~ meet(n1,X2,n1)
| ~ meet(X0,X2,X3)
| ~ join(n1,X0,X1)
| meet(X2,X1,n1) ) ).
cnf(u33,axiom,
join(X0,meet_of(X0,X1),X0) ).
cnf(u77,axiom,
( ~ join(n1,X0,X3)
| ~ join(X0,X1,X2)
| join(X3,X1,n1) ) ).
cnf(u480,axiom,
( meet(n1,X2,meet_of(X0,X1))
| ~ meet(X0,X1,X2) ) ).
cnf(u43,axiom,
( ~ meet(n0,X0,X1)
| n0 = X1 ) ).
cnf(u87,axiom,
join(meet_of(X0,X1),X0,X0) ).
cnf(u61,axiom,
( ~ meet(X2,X0,X3)
| ~ meet(X0,X1,n1)
| meet(X3,X1,X2) ) ).
cnf(u89,axiom,
( ~ join(X3,X0,X1)
| ~ join(X0,X1,X2)
| join(X3,X2,X1) ) ).
cnf(absorbtion2,axiom,
( ~ join(X0,X1,X2)
| meet(X0,X2,X0) ) ).
cnf(u1606,axiom,
( ~ meet(n1,X1,n1)
| meet(X0,X1,X0) ) ).
cnf(u28,axiom,
join(X0,X1,join_of(X1,X0)) ).
cnf(u363,axiom,
join(join_of(X0,X1),X0,join_of(X0,X1)) ).
cnf(u117,axiom,
( ~ meet(X0,X3,X0)
| ~ meet(X1,X3,X0)
| ~ join(X0,X1,X2)
| meet(X3,X2,X0) ) ).
cnf(u303,axiom,
( join(join_of(X2,X0),X1,X2)
| ~ join(X0,X1,X2) ) ).
cnf(u40,axiom,
meet(X0,join_of(X0,X1),X0) ).
cnf(join_1_and_x,axiom,
join(n1,X0,n1) ).
cnf(u261,axiom,
( ~ meet(n0,X0,X1)
| meet(n1,X1,n0) ) ).
cnf(u100,axiom,
meet(join_of(X0,X1),X0,X0) ).
cnf(u3008,axiom,
( ~ meet(X3,X0,X2)
| ~ meet(X0,X1,n1)
| meet(X2,X1,n1) ) ).
cnf(u1400,axiom,
( ~ join(n0,X0,X1)
| meet(n1,X0,X1) ) ).
cnf(u486,axiom,
( meet(X2,X1,meet_of(X2,X0))
| ~ meet(n1,X0,X1) ) ).
cnf(u98,axiom,
( ~ meet(X0,join_of(X0,X1),X2)
| X0 = X2 ) ).
cnf(u206,axiom,
meet_of(X0,join_of(X1,X0)) = X0 ).
cnf(u161,axiom,
n1 = join_of(n1,X0) ).
cnf(u3161,axiom,
meet(X0,n1,X1) ).
cnf(u218,axiom,
join_of(X0,meet_of(X0,X1)) = X0 ).
cnf(u64,axiom,
( ~ meet(X0,X1,X2)
| meet_of(X1,X0) = X2 ) ).
cnf(u125,axiom,
( ~ meet(X0,X2,X3)
| ~ join(n0,X0,X1)
| meet(X2,X1,X3) ) ).
cnf(u46,axiom,
( ~ meet(X0,X1,X2)
| meet_of(X0,X1) = X2 ) ).
cnf(u74,axiom,
( ~ join(X0,X1,X2)
| join_of(X1,X0) = X2 ) ).
cnf(commutativity_of_meet,axiom,
( ~ meet(X0,X1,X2)
| meet(X1,X0,X2) ) ).
cnf(u48,axiom,
( ~ meet(X0,n0,X1)
| n0 = X1 ) ).
cnf(u465,axiom,
( meet(X2,X0,meet_of(X2,X1))
| ~ meet(n1,X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT055-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.49 % Computer : n017.cluster.edu
% 0.21/0.49 % Model : x86_64 x86_64
% 0.21/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.49 % Memory : 8046.5625MB
% 0.21/0.49 % OS : Linux 6.8.0-71-generic
% 0.21/0.49 % CPULimit : 300
% 0.21/0.49 % WCLimit : 300
% 0.21/0.49 % DateTime : Sun Sep 27 13:53:50 UTC 2026
% 0.21/0.49 % CPUTime :
% 0.21/0.49 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.55 Running first-order theorem proving
% 0.25/0.55 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
% 14.75/3.39 % (2568755)Input is clausal, will run a generic CNF schedule.
% 14.75/3.39 % (2568771)lrs+10_1_sil=8000:sp=occurrence:random_seed=2464514681:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 14.75/3.39 % (2568771)Refutation not found, incomplete strategy
% 14.75/3.39 % (2568771)------------------------------
% 14.75/3.39 % (2568771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.75/3.39 % (2568771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/3.39 % (2568771)CaDiCaL version: 2.1.3
% 14.75/3.39 % (2568771)Termination reason: Refutation not found, incomplete strategy
% 14.75/3.39 % (2568771)Time elapsed: 0.0000 s
% 14.75/3.39 % (2568771)Peak memory usage: 86 MB
% 14.75/3.39 % (2568769)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4194897562:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 14.75/3.39 % (2568770)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=988293261:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 14.75/3.39 % (2568768)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=877263961:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 14.75/3.39 % (2568772)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=591297801:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 14.75/3.39 % (2568774)dis-21_1_sil=8000:lcm=predicate:random_seed=1846872774:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 14.75/3.39 % (2568773)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=200120694:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 14.75/3.39 % (2568774)Refutation not found, incomplete strategy
% 14.75/3.39 % (2568774)------------------------------
% 14.75/3.39 % (2568774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.75/3.39 % (2568772)Refutation not found, incomplete strategy
% 14.75/3.39 % (2568772)------------------------------
% 14.75/3.39 % (2568772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.75/3.39 % (2568772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/3.39 % (2568774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/3.39 % (2568774)CaDiCaL version: 2.1.3
% 14.75/3.39 % (2568772)CaDiCaL version: 2.1.3
% 14.75/3.39 % (2568772)Termination reason: Refutation not found, incomplete strategy
% 14.75/3.39 % (2568772)Time elapsed: 0.001 s
% 14.75/3.39 % (2568772)Peak memory usage: 86 MB
% 14.75/3.39 % (2568774)Termination reason: Refutation not found, incomplete strategy
% 14.75/3.39 % (2568774)Time elapsed: 0.001 s
% 14.75/3.39 % (2568774)Peak memory usage: 86 MB
% 14.75/3.39 % (2568771)------------------------------
% 14.75/3.39 % (2568771)------------------------------
% 14.75/3.39 % (2568773)Instruction limit reached!
% 14.75/3.39 % (2568773)------------------------------
% 14.75/3.39 % (2568773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.75/3.39 % (2568773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/3.39 % (2568773)CaDiCaL version: 2.1.3
% 14.75/3.39 % (2568773)Termination reason: Instruction limit
% 14.75/3.39 % (2568773)Termination phase: Saturation
% 14.75/3.39 % (2568773)Time elapsed: 0.172 s
% 14.75/3.39 % (2568773)Peak memory usage: 88 MB
% 14.75/3.39 % (2568773)Instructions burned: 180 (million)
% 14.75/3.39 % (2568772)------------------------------
% 14.75/3.39 % (2568772)------------------------------
% 14.75/3.39 % (2568774)------------------------------
% 14.75/3.39 % (2568774)------------------------------
% 14.75/3.39 % (2568784)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=664819254:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 14.75/3.39 % (2568784)Refutation not found, incomplete strategy
% 14.75/3.39 % (2568784)------------------------------
% 14.75/3.39 % (2568784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.75/3.39 % (2568784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.75/3.39 % (2568784)CaDiCaL version: 2.1.3
% 14.75/3.39 % (2568784)Termination reason: Refutation not found, incomplete strategy
% 14.75/3.39 % (2568784)Time elapsed: 0.0000 s
% 21.48/4.40 % (2568784)Peak memory usage: 86 MB
% 21.48/4.40 % (2568783)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=247973184:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 21.48/4.40 % (2568783)Refutation not found, incomplete strategy
% 21.48/4.40 % (2568783)------------------------------
% 21.48/4.40 % (2568783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.48/4.40 % (2568783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.48/4.40 % (2568783)CaDiCaL version: 2.1.3
% 21.48/4.40 % (2568783)Termination reason: Refutation not found, incomplete strategy
% 21.48/4.40 % (2568783)Time elapsed: 0.001 s
% 21.48/4.40 % (2568783)Peak memory usage: 86 MB
% 21.48/4.40 % (2568784)------------------------------
% 21.48/4.40 % (2568784)------------------------------
% 21.48/4.40 % (2568786)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3827578623:st=4:i=219:sd=3:ss=axioms_2992 on theBenchmark for (2992ds/219Mi)
% 21.48/4.40 % (2568788)lrs+10_64_to=lpo:sil=8000:random_seed=2206316371:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 21.48/4.40 % (2568786)Refutation not found, incomplete strategy
% 21.48/4.40 % (2568786)------------------------------
% 21.48/4.40 % (2568786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.48/4.40 % (2568786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.48/4.40 % (2568786)CaDiCaL version: 2.1.3
% 21.48/4.40 % (2568786)Termination reason: Refutation not found, incomplete strategy
% 21.48/4.40 % (2568786)Time elapsed: 0.001 s
% 21.48/4.40 % (2568786)Peak memory usage: 86 MB
% 21.48/4.40 % (2568783)------------------------------
% 21.48/4.40 % (2568783)------------------------------
% 21.48/4.40 % (2568788)Instruction limit reached!
% 21.48/4.40 % (2568788)------------------------------
% 21.48/4.40 % (2568788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.48/4.40 % (2568788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.48/4.40 % (2568788)CaDiCaL version: 2.1.3
% 21.48/4.40 % (2568788)Termination reason: Instruction limit
% 21.48/4.40 % (2568788)Termination phase: Saturation
% 21.48/4.40 % (2568788)Time elapsed: 0.129 s
% 21.48/4.40 % (2568788)Peak memory usage: 88 MB
% 21.48/4.40 % (2568788)Instructions burned: 126 (million)
% 21.48/4.40 % (2568789)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3065498800:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 21.48/4.40 % (2568789)Instruction limit reached!
% 21.48/4.40 % (2568789)------------------------------
% 21.48/4.40 % (2568789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.48/4.40 % (2568789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.48/4.40 % (2568789)CaDiCaL version: 2.1.3
% 21.48/4.40 % (2568789)Termination reason: Instruction limit
% 21.48/4.40 % (2568789)Termination phase: Saturation
% 21.48/4.40 % (2568789)Time elapsed: 0.093 s
% 21.48/4.40 % (2568789)Peak memory usage: 88 MB
% 21.48/4.40 % (2568789)Instructions burned: 195 (million)
% 21.48/4.40 % (2568786)------------------------------
% 21.48/4.40 % (2568786)------------------------------
% 21.48/4.40 % (2568792)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=501170332:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 21.48/4.40 % (2568793)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1922856125:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 21.48/4.40 % (2568792)Instruction limit reached!
% 21.48/4.40 % (2568792)------------------------------
% 21.48/4.40 % (2568792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.48/4.40 % (2568792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.48/4.40 % (2568792)CaDiCaL version: 2.1.3
% 21.48/4.40 % (2568792)Termination reason: Instruction limit
% 21.48/4.40 % (2568792)Termination phase: Saturation
% 21.48/4.40 % (2568792)Time elapsed: 0.161 s
% 21.48/4.40 % (2568792)Peak memory usage: 88 MB
% 21.48/4.40 % (2568792)Instructions burned: 158 (million)
% 21.48/4.40 % (2568795)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1927452779:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2986 on theBenchmark for (2986ds/106Mi)
% 21.48/4.40 % (2568795)Refutation not found, incomplete strategy
% 21.48/4.40 % (2568795)------------------------------
% 32.03/6.00 % (2568795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.03/6.00 % (2568795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.03/6.00 % (2568795)CaDiCaL version: 2.1.3
% 32.03/6.00 % (2568795)Termination reason: Refutation not found, incomplete strategy
% 32.03/6.00 % (2568795)Time elapsed: 0.001 s
% 32.03/6.00 % (2568795)Peak memory usage: 86 MB
% 32.03/6.00 % (2568797)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2885082163:i=107_2985 on theBenchmark for (2985ds/107Mi)
% 32.03/6.00 % (2568797)Refutation not found, incomplete strategy
% 32.03/6.00 % (2568797)------------------------------
% 32.03/6.00 % (2568797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.03/6.00 % (2568797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.03/6.00 % (2568797)CaDiCaL version: 2.1.3
% 32.03/6.00 % (2568797)Termination reason: Refutation not found, incomplete strategy
% 32.03/6.00 % (2568797)Time elapsed: 0.002 s
% 32.03/6.00 % (2568797)Peak memory usage: 87 MB
% 32.03/6.00 % (2568799)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3503104327:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 32.03/6.00 % (2568799)Refutation not found, incomplete strategy
% 32.03/6.00 % (2568799)------------------------------
% 32.03/6.00 % (2568799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.03/6.00 % (2568799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.03/6.00 % (2568799)CaDiCaL version: 2.1.3
% 32.03/6.00 % (2568799)Termination reason: Refutation not found, incomplete strategy
% 32.03/6.00 % (2568799)Time elapsed: 0.001 s
% 32.03/6.00 % (2568799)Peak memory usage: 86 MB
% 32.03/6.00 % (2568795)------------------------------
% 32.03/6.00 % (2568795)------------------------------
% 32.03/6.00 [W927 13:53:53.199244088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199294052 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199355296 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199376209 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199425440 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199445313 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199491020 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.03/6.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.03/6.00 [W927 13:53:53.199509760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.53/9.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.53/9.25 [W927 13:53:53.199559987 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.53/9.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.53/9.25 [W927 13:53:53.199577444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.53/9.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.53/9.25 [W927 13:53:53.199702422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.53/9.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.53/9.25 [W927 13:53:53.199731025 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.53/9.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.53/9.25 % (2568797)------------------------------
% 56.53/9.25 % (2568797)------------------------------
% 56.53/9.25 % (2568799)------------------------------
% 56.53/9.25 % (2568799)------------------------------
% 56.53/9.25 % (2568805)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2018124457:cond=fast:i=5208:av=off_2979 on theBenchmark for (2979ds/5208Mi)
% 56.53/9.25 % (2568793)Refutation not found, incomplete strategy
% 56.53/9.25 % (2568793)------------------------------
% 56.53/9.25 % (2568793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.53/9.25 % (2568793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.53/9.25 % (2568793)CaDiCaL version: 2.1.3
% 56.53/9.25 % (2568793)Termination reason: Refutation not found, incomplete strategy
% 56.53/9.25 % (2568793)Time elapsed: 0.927 s
% 56.53/9.25 % (2568793)Peak memory usage: 125 MB
% 56.53/9.25 % (2568793)Instructions burned: 826 (million)
% 56.53/9.25 % (2568806)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3881470493:i=134:sd=2:doe=on:ss=axioms:sgt=14_2979 on theBenchmark for (2979ds/134Mi)
% 56.53/9.25 % (2568806)Refutation not found, incomplete strategy
% 56.53/9.25 % (2568806)------------------------------
% 56.53/9.25 % (2568806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.53/9.25 % (2568806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.53/9.25 % (2568806)CaDiCaL version: 2.1.3
% 56.53/9.25 % (2568806)Termination reason: Refutation not found, incomplete strategy
% 56.53/9.25 % (2568806)Time elapsed: 0.001 s
% 56.53/9.25 % (2568806)Peak memory usage: 86 MB
% 56.53/9.25 % (2568807)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1843059668:i=499:bd=all_2977 on theBenchmark for (2977ds/499Mi)
% 56.53/9.25 % (2568793)------------------------------
% 56.53/9.25 % (2568793)------------------------------
% 56.53/9.25 % (2568806)------------------------------
% 56.53/9.25 % (2568806)------------------------------
% 56.53/9.25 % (2568807)Instruction limit reached!
% 56.53/9.25 % (2568807)------------------------------
% 56.53/9.25 % (2568807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.53/9.25 % (2568807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.53/9.25 % (2568807)CaDiCaL version: 2.1.3
% 56.53/9.25 % (2568807)Termination reason: Instruction limit
% 56.53/9.25 % (2568807)Termination phase: Saturation
% 56.53/9.25 % (2568807)Time elapsed: 0.455 s
% 56.53/9.25 % (2568807)Peak memory usage: 90 MB
% 56.53/9.25 % (2568807)Instructions burned: 500 (million)
% 56.53/9.25 % (2568811)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2739477597:i=191:fgj=on:bd=all_2972 on theBenchmark for (2972ds/191Mi)
% 56.53/9.25 % (2568812)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1197452829:i=264:kws=precedence:fsr=off_2972 on theBenchmark for (2972ds/264Mi)
% 58.99/9.64 % (2568811)Instruction limit reached!
% 58.99/9.64 % (2568811)------------------------------
% 58.99/9.64 % (2568811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.99/9.64 % (2568811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.99/9.64 % (2568811)CaDiCaL version: 2.1.3
% 58.99/9.64 % (2568811)Termination reason: Instruction limit
% 58.99/9.64 % (2568811)Termination phase: Saturation
% 58.99/9.64 % (2568811)Time elapsed: 0.213 s
% 58.99/9.64 % (2568811)Peak memory usage: 90 MB
% 58.99/9.64 % (2568811)Instructions burned: 192 (million)
% 58.99/9.64 % (2568812)Instruction limit reached!
% 58.99/9.64 % (2568812)------------------------------
% 58.99/9.64 % (2568812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.99/9.64 % (2568812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.99/9.64 % (2568812)CaDiCaL version: 2.1.3
% 58.99/9.64 % (2568812)Termination reason: Instruction limit
% 58.99/9.64 % (2568812)Termination phase: Saturation
% 58.99/9.64 % (2568812)Time elapsed: 0.245 s
% 58.99/9.64 % (2568812)Peak memory usage: 90 MB
% 58.99/9.64 % (2568812)Instructions burned: 265 (million)
% 58.99/9.64 % (2568813)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=698727126:cond=on:i=156:bs=on:gtg=exists_all:er=known_2969 on theBenchmark for (2969ds/156Mi)
% 58.99/9.64 % (2568813)Instruction limit reached!
% 58.99/9.64 % (2568813)------------------------------
% 58.99/9.64 % (2568813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.99/9.64 % (2568813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.99/9.64 % (2568813)CaDiCaL version: 2.1.3
% 58.99/9.64 % (2568813)Termination reason: Instruction limit
% 58.99/9.64 % (2568813)Termination phase: Saturation
% 58.99/9.64 % (2568813)Time elapsed: 0.158 s
% 58.99/9.64 % (2568813)Peak memory usage: 88 MB
% 58.99/9.64 % (2568813)Instructions burned: 156 (million)
% 58.99/9.64 % (2568816)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1135979207:i=3256:kws=precedence:bd=preordered:av=off_2967 on theBenchmark for (2967ds/3256Mi)
% 58.99/9.64 % (2568817)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2073488507:i=537:av=off:ss=included_2966 on theBenchmark for (2966ds/537Mi)
% 58.99/9.64 % (2568817)Refutation not found, incomplete strategy
% 58.99/9.64 % (2568817)------------------------------
% 58.99/9.64 % (2568817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.99/9.64 % (2568817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.99/9.64 % (2568817)CaDiCaL version: 2.1.3
% 58.99/9.64 % (2568817)Termination reason: Refutation not found, incomplete strategy
% 58.99/9.64 % (2568817)Time elapsed: 0.001 s
% 58.99/9.64 % (2568817)Peak memory usage: 86 MB
% 58.99/9.64 % (2568819)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=660748145:i=180:bd=preordered:av=off_2964 on theBenchmark for (2964ds/180Mi)
% 58.99/9.64 % (2568819)Instruction limit reached!
% 58.99/9.64 % (2568819)------------------------------
% 58.99/9.64 % (2568819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.99/9.64 % (2568819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.99/9.64 % (2568819)CaDiCaL version: 2.1.3
% 58.99/9.64 % (2568819)Termination reason: Instruction limit
% 58.99/9.64 % (2568819)Termination phase: Saturation
% 58.99/9.64 % (2568819)Time elapsed: 0.166 s
% 58.99/9.64 % (2568819)Peak memory usage: 88 MB
% 58.99/9.64 % (2568819)Instructions burned: 181 (million)
% 58.99/9.64 % (2568817)------------------------------
% 58.99/9.64 % (2568817)------------------------------
% 58.99/9.64 % (2568823)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=177468877:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2960 on theBenchmark for (2960ds/10307Mi)
% 58.99/9.64 % (2568824)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4053490578:i=412:gtgl=4:gtg=exists_all_2959 on theBenchmark for (2959ds/412Mi)
% 58.99/9.64 % (2568824)Instruction limit reached!
% 58.99/9.64 % (2568824)------------------------------
% 58.99/9.64 % (2568824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.99/9.64 % (2568824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/11.34 % (2568824)CaDiCaL version: 2.1.3
% 71.53/11.34 % (2568824)Termination reason: Instruction limit
% 71.53/11.34 % (2568824)Termination phase: Saturation
% 71.53/11.34 % (2568824)Time elapsed: 0.380 s
% 71.53/11.34 % (2568824)Peak memory usage: 89 MB
% 71.53/11.34 % (2568824)Instructions burned: 413 (million)
% 71.53/11.34 % (2568827)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1011963255:s2pl=no:i=8478:s2at=4:nm=6_2953 on theBenchmark for (2953ds/8478Mi)
% 71.53/11.34 % (2568816)Instruction limit reached!
% 71.53/11.34 % (2568816)------------------------------
% 71.53/11.34 % (2568816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.53/11.34 % (2568816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/11.34 % (2568816)CaDiCaL version: 2.1.3
% 71.53/11.34 % (2568816)Termination reason: Instruction limit
% 71.53/11.34 % (2568816)Termination phase: Saturation
% 71.53/11.34 % (2568816)Time elapsed: 3.193 s
% 71.53/11.34 % (2568816)Peak memory usage: 141 MB
% 71.53/11.34 % (2568816)Instructions burned: 3256 (million)
% 71.53/11.34 % (2568829)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3670033655:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2932 on theBenchmark for (2932ds/303Mi)
% 71.53/11.34 % (2568829)Refutation not found, incomplete strategy
% 71.53/11.34 % (2568829)------------------------------
% 71.53/11.34 % (2568829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.53/11.34 % (2568829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/11.34 % (2568829)CaDiCaL version: 2.1.3
% 71.53/11.34 % (2568829)Termination reason: Refutation not found, incomplete strategy
% 71.53/11.34 % (2568829)Time elapsed: 0.001 s
% 71.53/11.34 % (2568829)Peak memory usage: 86 MB
% 71.53/11.34 % (2568829)------------------------------
% 71.53/11.34 % (2568829)------------------------------
% 71.53/11.34 % (2568935)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2892356204:st=4:i=720:sd=3:fsr=off:ss=axioms_2928 on theBenchmark for (2928ds/720Mi)
% 71.53/11.34 % (2568935)Refutation not found, incomplete strategy
% 71.53/11.34 % (2568935)------------------------------
% 71.53/11.34 % (2568935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.53/11.34 % (2568935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/11.34 % (2568935)CaDiCaL version: 2.1.3
% 71.53/11.34 % (2568935)Termination reason: Refutation not found, incomplete strategy
% 71.53/11.34 % (2568935)Time elapsed: 0.001 s
% 71.53/11.34 % (2568935)Peak memory usage: 86 MB
% 71.53/11.34 % (2568805)Instruction limit reached!
% 71.53/11.34 % (2568805)------------------------------
% 71.53/11.34 % (2568805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.53/11.34 % (2568805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/11.34 % (2568805)CaDiCaL version: 2.1.3
% 71.53/11.34 % (2568805)Termination reason: Instruction limit
% 71.53/11.34 % (2568805)Termination phase: Saturation
% 71.53/11.34 % (2568805)Time elapsed: 5.017 s
% 71.53/11.34 % (2568805)Peak memory usage: 150 MB
% 71.53/11.34 % (2568805)Instructions burned: 5209 (million)
% 71.53/11.34 % (2568986)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2285589014:i=598:bs=on:bd=preordered:av=off:ss=axioms_2926 on theBenchmark for (2926ds/598Mi)
% 71.53/11.34 % (2568986)Refutation not found, incomplete strategy
% 71.53/11.34 % (2568986)------------------------------
% 71.53/11.34 % (2568986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.53/11.34 % (2568986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.53/11.34 % (2568986)CaDiCaL version: 2.1.3
% 71.53/11.34 % (2568986)Termination reason: Refutation not found, incomplete strategy
% 71.53/11.34 % (2568986)Time elapsed: 0.0000 s
% 71.53/11.34 % (2568986)Peak memory usage: 86 MB
% 71.53/11.34 % (2568935)------------------------------
% 71.53/11.34 % (2568935)------------------------------
% 71.53/11.34 % (2568986)------------------------------
% 71.53/11.34 % (2568986)------------------------------
% 71.53/11.34 % (2568988)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=51391223:i=2989:sd=3:ss=axioms:sgt=60_2924 on theBenchmark for (2924ds/2989Mi)
% 71.53/11.34 % (2568989)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1839812599:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2922 on theBenchmark for (2922ds/1997Mi)
% 72.80/11.58 [W927 13:53:59.277828825 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277870622 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277907566 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277918799 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277946173 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277958003 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277983506 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.277994663 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.278030923 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.278051837 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.278076857 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 [W927 13:53:59.278098597 register_special_ops.cpp:225] Warning: Creating a tensor from 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.80/11.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 72.80/11.58 % (2568988)Refutation not found, incomplete strategy
% 72.80/11.58 % (2568988)------------------------------
% 72.80/11.58 % (2568988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.73/12.12 % (2568988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.73/12.12 % (2568988)CaDiCaL version: 2.1.3
% 76.73/12.12 % (2568988)Termination reason: Refutation not found, incomplete strategy
% 76.73/12.12 % (2568988)Time elapsed: 0.552 s
% 76.73/12.12 % (2568988)Peak memory usage: 125 MB
% 76.73/12.12 % (2568988)Instructions burned: 826 (million)
% 76.73/12.12 % (2568988)------------------------------
% 76.73/12.12 % (2568988)------------------------------
% 76.73/12.12 % (2568992)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1592201831:i=2088:bd=preordered:av=off_2914 on theBenchmark for (2914ds/2088Mi)
% 76.73/12.12 % (2568823)Instruction limit reached!
% 76.73/12.12 % (2568823)------------------------------
% 76.73/12.12 % (2568823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.73/12.12 % (2568823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.73/12.12 % (2568823)CaDiCaL version: 2.1.3
% 76.73/12.12 % (2568823)Termination reason: Instruction limit
% 76.73/12.12 % (2568823)Termination phase: Saturation
% 76.73/12.12 % (2568823)Time elapsed: 4.586 s
% 76.73/12.12 % (2568823)Peak memory usage: 159 MB
% 76.73/12.12 % (2568823)Instructions burned: 10308 (million)
% 76.73/12.12 % (2568994)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2702641946:i=1098:nicw=on_2911 on theBenchmark for (2911ds/1098Mi)
% 76.73/12.12 % (2568989)Instruction limit reached!
% 76.73/12.12 % (2568989)------------------------------
% 76.73/12.12 % (2568989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.73/12.12 % (2568989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.73/12.12 % (2568989)CaDiCaL version: 2.1.3
% 76.73/12.12 % (2568989)Termination reason: Instruction limit
% 76.73/12.12 % (2568989)Termination phase: Saturation
% 76.73/12.12 % (2568989)Time elapsed: 1.204 s
% 76.73/12.12 % (2568989)Peak memory usage: 138 MB
% 76.73/12.12 % (2568989)Instructions burned: 1999 (million)
% 76.73/12.12 % (2568996)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1982416676:i=433:bd=preordered_2908 on theBenchmark for (2908ds/433Mi)
% 76.73/12.12 % (2568996)Refutation not found, incomplete strategy
% 76.73/12.12 % (2568996)------------------------------
% 76.73/12.12 % (2568996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.73/12.12 % (2568996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.73/12.12 % (2568996)CaDiCaL version: 2.1.3
% 76.73/12.12 % (2568996)Termination reason: Refutation not found, incomplete strategy
% 76.73/12.12 % (2568996)Time elapsed: 0.001 s
% 76.73/12.12 % (2568996)Peak memory usage: 87 MB
% 76.73/12.12 % (2568994)Instruction limit reached!
% 76.73/12.12 % (2568994)------------------------------
% 76.73/12.12 % (2568994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.73/12.12 % (2568994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.73/12.12 % (2568994)CaDiCaL version: 2.1.3
% 76.73/12.12 % (2568994)Termination reason: Instruction limit
% 76.73/12.12 % (2568994)Termination phase: Saturation
% 76.73/12.12 % (2568994)Time elapsed: 0.327 s
% 76.73/12.12 % (2568994)Peak memory usage: 106 MB
% 76.73/12.12 % (2568994)Instructions burned: 1102 (million)
% 76.73/12.12 % (2568998)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4031132737:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2906 on theBenchmark for (2906ds/2942Mi)
% 76.73/12.12 % (2568996)------------------------------
% 76.73/12.12 % (2568996)------------------------------
% 76.73/12.12 % (2569000)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3813752573:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2904 on theBenchmark for (2904ds/6922Mi)
% 76.73/12.12 % (2568992)Instruction limit reached!
% 76.73/12.12 % (2568992)------------------------------
% 76.73/12.12 % (2568992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.73/12.12 % (2568992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.73/12.12 % (2568992)CaDiCaL version: 2.1.3
% 76.73/12.12 % (2568992)Termination reason: Instruction limit
% 76.73/12.12 % (2568992)Termination phase: Saturation
% 76.73/12.12 % (2568992)Time elapsed: 1.282 s
% 76.73/12.12 % (2568992)Peak memory usage: 133 MB
% 76.73/12.12 % (2568992)Instructions burned: 2089 (million)
% 78.62/12.37 [W927 13:54:01.215489773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215524390 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215561301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215574301 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215600094 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215611528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215637158 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215661278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215687281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215697355 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215720718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 [W927 13:54:01.215730702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 78.62/12.37 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.62/12.37 % (2569002)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1525736708:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2899 on theBenchmark for (2899ds/596Mi)
% 78.62/12.37 % (2569000)Refutation not found, incomplete strategy
% 78.62/12.37 % (2569000)------------------------------
% 82.23/13.02 % (2569000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.23/13.02 % (2569000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/13.02 % (2569000)CaDiCaL version: 2.1.3
% 82.23/13.02 % (2569000)Termination reason: Refutation not found, incomplete strategy
% 82.23/13.02 % (2569000)Time elapsed: 0.545 s
% 82.23/13.02 % (2569000)Peak memory usage: 125 MB
% 82.23/13.02 % (2569000)Instructions burned: 826 (million)
% 82.23/13.02 % (2568827)Instruction limit reached!
% 82.23/13.02 % (2568827)------------------------------
% 82.23/13.02 % (2568827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.23/13.02 % (2568827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/13.02 % (2568827)CaDiCaL version: 2.1.3
% 82.23/13.02 % (2568827)Termination reason: Instruction limit
% 82.23/13.02 % (2568827)Termination phase: Saturation
% 82.23/13.02 % (2568827)Time elapsed: 5.364 s
% 82.23/13.02 % (2568827)Peak memory usage: 160 MB
% 82.23/13.02 % (2568827)Instructions burned: 8479 (million)
% 82.23/13.02 % (2569002)Instruction limit reached!
% 82.23/13.02 % (2569002)------------------------------
% 82.23/13.02 % (2569002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.23/13.02 % (2569002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/13.02 % (2569002)CaDiCaL version: 2.1.3
% 82.23/13.02 % (2569002)Termination reason: Instruction limit
% 82.23/13.02 % (2569002)Termination phase: Saturation
% 82.23/13.02 % (2569002)Time elapsed: 0.291 s
% 82.23/13.02 % (2569002)Peak memory usage: 93 MB
% 82.23/13.02 % (2569002)Instructions burned: 597 (million)
% 82.23/13.02 % (2568998)Instruction limit reached!
% 82.23/13.02 % (2568998)------------------------------
% 82.23/13.02 % (2568998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.23/13.02 % (2568998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.23/13.02 % (2568998)CaDiCaL version: 2.1.3
% 82.23/13.02 % (2568998)Termination reason: Instruction limit
% 82.23/13.02 % (2568998)Termination phase: Saturation
% 82.23/13.02 % (2568998)Time elapsed: 1.026 s
% 82.23/13.02 % (2568998)Peak memory usage: 134 MB
% 82.23/13.02 % (2568998)Instructions burned: 2944 (million)
% 82.23/13.02 % (2569000)------------------------------
% 82.23/13.02 % (2569000)------------------------------
% 82.23/13.02 % (2569004)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=513900925:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2896 on theBenchmark for (2896ds/4123Mi)
% 82.23/13.02 % (2569005)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3442604955:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2895 on theBenchmark for (2895ds/16411Mi)
% 82.23/13.02 % (2569006)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3226551241:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2895 on theBenchmark for (2895ds/1670Mi)
% 82.23/13.02 % (2569007)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3159583746:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2894 on theBenchmark for (2894ds/1722Mi)
% 82.23/13.02 [W927 13:54:01.928794621 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.23/13.02 [W927 13:54:01.928833735 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.23/13.02 [W927 13:54:01.928855243 register_special_ops.cpp:225] Warning: Creating a tensor from 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.23/13.02 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 82.23/13.02 [W927 13:54:01.928861264 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928874853 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928891736 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928904812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928910656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928923146 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928928942 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928941569 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:01.928947420 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 % (2569005)Refutation not found, incomplete strategy
% 85.40/13.33 % (2569005)------------------------------
% 85.40/13.33 % (2569005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.40/13.33 % (2569005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.40/13.33 % (2569005)CaDiCaL version: 2.1.3
% 85.40/13.33 % (2569005)Termination reason: Refutation not found, incomplete strategy
% 85.40/13.33 % (2569005)Time elapsed: 0.302 s
% 85.40/13.33 % (2569005)Peak memory usage: 125 MB
% 85.40/13.33 % (2569005)Instructions burned: 825 (million)
% 85.40/13.33 % (2569005)------------------------------
% 85.40/13.33 % (2569005)------------------------------
% 85.40/13.33 [W927 13:54:02.180685966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:02.180718780 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 85.40/13.33 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 85.40/13.33 [W927 13:54:02.180759580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180772837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180803704 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180814081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180838484 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180848511 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180872601 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180882728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180906525 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 [W927 13:54:02.180916731 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 100.79/15.54 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 100.79/15.54 % (2569012)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2270385823:cts=off:cond=on:i=9530:bs=on:fsd=on_2889 on theBenchmark for (2889ds/9530Mi)
% 100.79/15.54 % (2569007)Refutation not found, incomplete strategy
% 100.79/15.54 % (2569007)------------------------------
% 100.79/15.54 % (2569007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.79/15.54 % (2569007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.79/15.54 % (2569007)CaDiCaL version: 2.1.3
% 100.79/15.54 % (2569007)Termination reason: Refutation not found, incomplete strategy
% 100.79/15.54 % (2569007)Time elapsed: 0.553 s
% 100.79/15.54 % (2569007)Peak memory usage: 125 MB
% 100.79/15.54 % (2569007)Instructions burned: 826 (million)
% 100.79/15.54 % (2569007)------------------------------
% 100.79/15.54 % (2569007)------------------------------
% 100.79/15.54 % (2569014)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1479417878:st=2:i=4495:sd=10:ss=included_2885 on theBenchmark for (2885ds/4495Mi)
% 100.79/15.54 % (2569006)Instruction limit reached!
% 100.79/15.54 % (2569006)------------------------------
% 100.79/15.54 % (2569006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.26/15.81 % (2569006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.26/15.81 % (2569006)CaDiCaL version: 2.1.3
% 102.26/15.81 % (2569006)Termination reason: Instruction limit
% 102.26/15.81 % (2569006)Termination phase: Saturation
% 102.26/15.81 % (2569006)Time elapsed: 1.061 s
% 102.26/15.81 % (2569006)Peak memory usage: 135 MB
% 102.26/15.81 % (2569006)Instructions burned: 1670 (million)
% 102.26/15.81 % (2569016)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=294323115:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2882 on theBenchmark for (2882ds/4920Mi)
% 102.26/15.81 [W927 13:54:03.134383959 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134417693 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134454756 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134467723 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134493223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134505837 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134532593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134544740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134569224 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134580740 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.26/15.81 [W927 13:54:03.134606541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.26/15.81 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.67/16.00 [W927 13:54:03.134618277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 102.67/16.00 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 102.67/16.00 % (2569014)Refutation not found, incomplete strategy
% 102.67/16.00 % (2569014)------------------------------
% 102.67/16.00 % (2569014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.67/16.00 % (2569014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.67/16.00 % (2569014)CaDiCaL version: 2.1.3
% 102.67/16.00 % (2569014)Termination reason: Refutation not found, incomplete strategy
% 102.67/16.00 % (2569014)Time elapsed: 0.547 s
% 102.67/16.00 % (2569014)Peak memory usage: 125 MB
% 102.67/16.00 % (2569014)Instructions burned: 826 (million)
% 102.67/16.00 % (2569014)------------------------------
% 102.67/16.00 % (2569014)------------------------------
% 102.67/16.00 % (2569018)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1944637426:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2875 on theBenchmark for (2875ds/2083Mi)
% 102.67/16.00 % (2569004)Instruction limit reached!
% 102.67/16.00 % (2569004)------------------------------
% 102.67/16.00 % (2569004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.67/16.00 % (2569004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.67/16.00 % (2569004)CaDiCaL version: 2.1.3
% 102.67/16.00 % (2569004)Termination reason: Instruction limit
% 102.67/16.00 % (2569004)Termination phase: Saturation
% 102.67/16.00 % (2569004)Time elapsed: 2.456 s
% 102.67/16.00 % (2569004)Peak memory usage: 150 MB
% 102.67/16.00 % (2569004)Instructions burned: 4123 (million)
% 102.67/16.00 % (2569085)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2738536191:i=4629:av=off:gsp=on_2870 on theBenchmark for (2870ds/4629Mi)
% 102.67/16.00 % (2569085)Refutation not found, incomplete strategy
% 102.67/16.00 % (2569085)------------------------------
% 102.67/16.00 % (2569085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.67/16.00 % (2569085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.67/16.00 % (2569085)CaDiCaL version: 2.1.3
% 102.67/16.00 % (2569085)Termination reason: Refutation not found, incomplete strategy
% 102.67/16.00 % (2569085)Time elapsed: 0.553 s
% 102.67/16.00 % (2569085)Peak memory usage: 127 MB
% 102.67/16.00 % (2569085)Instructions burned: 826 (million)
% 102.67/16.00 % (2569018)Instruction limit reached!
% 102.67/16.00 % (2569018)------------------------------
% 102.67/16.00 % (2569018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.67/16.00 % (2569018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.67/16.00 % (2569018)CaDiCaL version: 2.1.3
% 102.67/16.00 % (2569018)Termination reason: Instruction limit
% 102.67/16.00 % (2569018)Termination phase: Saturation
% 102.67/16.00 % (2569018)Time elapsed: 1.326 s
% 102.67/16.00 % (2569018)Peak memory usage: 135 MB
% 102.67/16.00 % (2569018)Instructions burned: 2085 (million)
% 102.67/16.00 % (2569085)------------------------------
% 102.67/16.00 % (2569085)------------------------------
% 102.67/16.00 % (2569299)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=305488586:i=1258:av=off_2860 on theBenchmark for (2860ds/1258Mi)
% 102.67/16.00 % (2569012)Instruction limit reached!
% 102.67/16.00 % (2569012)------------------------------
% 102.67/16.00 % (2569012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 102.67/16.00 % (2569012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.67/16.00 % (2569012)CaDiCaL version: 2.1.3
% 102.67/16.00 % (2569012)Termination reason: Instruction limit
% 102.67/16.00 % (2569012)Termination phase: Saturation
% 102.67/16.00 % (2569012)Time elapsed: 2.923 s
% 102.67/16.00 % (2569012)Peak memory usage: 154 MB
% 102.67/16.00 % (2569012)Instructions burned: 9532 (million)
% 102.67/16.00 % (2569301)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=103974733:i=7343:av=off:ss=included_2860 on theBenchmark for (2860ds/7343Mi)
% 102.67/16.00 % (2569360)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3791636601:i=1325:sd=2:ss=axioms:sgt=16_2858 on theBenchmark for (2858ds/1325Mi)
% 102.67/16.00 % (2569360)Refutation not found, incomplete strategy
% 102.67/16.00 % (2569360)------------------------------
% 107.45/16.65 % (2569360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.45/16.65 % (2569360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.45/16.65 % (2569360)CaDiCaL version: 2.1.3
% 107.45/16.65 % (2569360)Termination reason: Refutation not found, incomplete strategy
% 107.45/16.65 % (2569360)Time elapsed: 0.0000 s
% 107.45/16.65 % (2569360)Peak memory usage: 86 MB
% 107.45/16.65 % (2569360)------------------------------
% 107.45/16.65 % (2569360)------------------------------
% 107.45/16.65 % (2569456)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2518028927:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2856 on theBenchmark for (2856ds/2646Mi)
% 107.45/16.65 [W927 13:54:05.622369697 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622410201 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622447481 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622459191 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622483278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622495382 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622529125 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622553729 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622579242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622589966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.45/16.65 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.45/16.65 [W927 13:54:05.622614136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.622624819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 % (2569301)Refutation not found, incomplete strategy
% 112.12/17.09 % (2569301)------------------------------
% 112.12/17.09 % (2569301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.12/17.09 % (2569301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.12/17.09 % (2569301)CaDiCaL version: 2.1.3
% 112.12/17.09 % (2569301)Termination reason: Refutation not found, incomplete strategy
% 112.12/17.09 % (2569301)Time elapsed: 0.553 s
% 112.12/17.09 % (2569301)Peak memory usage: 125 MB
% 112.12/17.09 % (2569301)Instructions burned: 825 (million)
% 112.12/17.09 [W927 13:54:05.807323948 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807352108 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807373045 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807379268 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807392930 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807398533 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807411851 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807417753 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807431830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807437436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 112.12/17.09 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 112.12/17.09 [W927 13:54:05.807449953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 114.43/17.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 114.43/17.41 [W927 13:54:05.807455416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 114.43/17.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 114.43/17.41 % (2569299)Instruction limit reached!
% 114.43/17.41 % (2569299)------------------------------
% 114.43/17.41 % (2569299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.43/17.41 % (2569299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.43/17.41 % (2569299)CaDiCaL version: 2.1.3
% 114.43/17.41 % (2569299)Termination reason: Instruction limit
% 114.43/17.41 % (2569299)Termination phase: Saturation
% 114.43/17.41 % (2569299)Time elapsed: 0.695 s
% 114.43/17.41 % (2569299)Peak memory usage: 92 MB
% 114.43/17.41 % (2569299)Instructions burned: 1258 (million)
% 114.43/17.41 % (2569016)Instruction limit reached!
% 114.43/17.41 % (2569016)------------------------------
% 114.43/17.41 % (2569016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.43/17.41 % (2569016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.43/17.41 % (2569016)CaDiCaL version: 2.1.3
% 114.43/17.41 % (2569016)Termination reason: Instruction limit
% 114.43/17.41 % (2569016)Termination phase: Saturation
% 114.43/17.41 % (2569016)Time elapsed: 2.913 s
% 114.43/17.41 % (2569016)Peak memory usage: 143 MB
% 114.43/17.41 % (2569016)Instructions burned: 4920 (million)
% 114.43/17.41 % (2569456)Refutation not found, incomplete strategy
% 114.43/17.41 % (2569456)------------------------------
% 114.43/17.41 % (2569456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.43/17.41 % (2569456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.43/17.41 % (2569456)CaDiCaL version: 2.1.3
% 114.43/17.41 % (2569456)Termination reason: Refutation not found, incomplete strategy
% 114.43/17.41 % (2569456)Time elapsed: 0.315 s
% 114.43/17.41 % (2569456)Peak memory usage: 125 MB
% 114.43/17.41 % (2569456)Instructions burned: 826 (million)
% 114.43/17.41 % (2569301)------------------------------
% 114.43/17.41 % (2569301)------------------------------
% 114.43/17.41 % (2569459)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2993386711:i=1489:sd=2:ep=R:ss=axioms_2852 on theBenchmark for (2852ds/1489Mi)
% 114.43/17.41 % (2569460)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2654197120:i=1503_2852 on theBenchmark for (2852ds/1503Mi)
% 114.43/17.41 % (2569456)------------------------------
% 114.43/17.41 % (2569456)------------------------------
% 114.43/17.41 % (2569461)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1861786025:i=13942:kws=frequency_2850 on theBenchmark for (2850ds/13942Mi)
% 114.43/17.41 % (2569464)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=716579740:i=3604:fsr=off:er=filter_2850 on theBenchmark for (2850ds/3604Mi)
% 114.43/17.41 [W927 13:54:06.457518166 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 114.43/17.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 114.43/17.41 [W927 13:54:06.457560693 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 114.43/17.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 114.43/17.41 [W927 13:54:06.457598593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 114.43/17.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457609846 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457633807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457644140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457667744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457689367 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457714720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457724791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457749181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 [W927 13:54:06.457759237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 115.58/17.63 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 115.58/17.63 % (2569460)Refutation not found, incomplete strategy
% 115.58/17.63 % (2569460)------------------------------
% 115.58/17.63 % (2569460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.58/17.63 % (2569460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.58/17.63 % (2569460)CaDiCaL version: 2.1.3
% 115.58/17.63 % (2569460)Termination reason: Refutation not found, incomplete strategy
% 115.58/17.63 % (2569460)Time elapsed: 0.533 s
% 115.58/17.63 % (2569460)Peak memory usage: 126 MB
% 115.58/17.63 % (2569460)Instructions burned: 825 (million)
% 115.58/17.63 % (2569459)Refutation not found, incomplete strategy
% 115.58/17.63 % (2569459)------------------------------
% 115.58/17.63 % (2569459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.58/17.63 % (2569459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.58/17.63 % (2569459)CaDiCaL version: 2.1.3
% 115.58/17.63 % (2569459)Termination reason: Refutation not found, incomplete strategy
% 115.58/17.63 % (2569459)Time elapsed: 0.557 s
% 115.58/17.63 % (2569459)Peak memory usage: 125 MB
% 115.58/17.63 % (2569459)Instructions burned: 826 (million)
% 115.58/17.63 % (2569460)------------------------------
% 115.58/17.63 % (2569460)------------------------------
% 115.58/17.63 % (2569459)------------------------------
% 115.58/17.63 % (2569459)------------------------------
% 115.58/17.63 % (2569467)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=5279517:i=1876:sd=1:ss=included:sgt=32_2843 on theBenchmark for (2843ds/1876Mi)
% 121.63/18.58 % (2569468)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1812115514:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2842 on theBenchmark for (2842ds/1932Mi)
% 121.63/18.58 [W927 13:54:06.106582057 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106610868 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106633571 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106640218 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106654374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106659949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106673412 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106678976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106691919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106697507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106710376 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 [W927 13:54:06.106715859 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 121.63/18.58 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 121.63/18.58 % (2569467)Refutation not found, incomplete strategy
% 135.98/20.44 % (2569467)------------------------------
% 135.98/20.44 % (2569467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 135.98/20.44 % (2569467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 135.98/20.44 % (2569467)CaDiCaL version: 2.1.3
% 135.98/20.44 % (2569467)Termination reason: Refutation not found, incomplete strategy
% 135.98/20.44 % (2569467)Time elapsed: 0.314 s
% 135.98/20.44 % (2569467)Peak memory usage: 125 MB
% 135.98/20.44 % (2569467)Instructions burned: 827 (million)
% 135.98/20.44 % (2569467)------------------------------
% 135.98/20.44 % (2569467)------------------------------
% 135.98/20.44 [W927 13:54:07.438116429 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438151909 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438191726 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438205313 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438233183 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438244946 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438271980 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438283536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438309283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438320977 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438347137 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 135.98/20.44 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 135.98/20.44 [W927 13:54:07.438358824 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.22/20.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.22/20.86 % (2569471)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=1932105663:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2837 on theBenchmark for (2837ds/1980Mi)
% 138.22/20.86 % (2569468)Refutation not found, incomplete strategy
% 138.22/20.86 % (2569468)------------------------------
% 138.22/20.86 % (2569468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.22/20.86 % (2569468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.22/20.86 % (2569468)CaDiCaL version: 2.1.3
% 138.22/20.86 % (2569468)Termination reason: Refutation not found, incomplete strategy
% 138.22/20.86 % (2569468)Time elapsed: 0.555 s
% 138.22/20.86 % (2569468)Peak memory usage: 125 MB
% 138.22/20.86 % (2569468)Instructions burned: 825 (million)
% 138.22/20.86 % (2569468)------------------------------
% 138.22/20.86 % (2569468)------------------------------
% 138.22/20.86 % (2569464)Instruction limit reached!
% 138.22/20.86 % (2569464)------------------------------
% 138.22/20.86 % (2569464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.22/20.86 % (2569464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.22/20.86 % (2569464)CaDiCaL version: 2.1.3
% 138.22/20.86 % (2569464)Termination reason: Instruction limit
% 138.22/20.86 % (2569464)Termination phase: Saturation
% 138.22/20.86 % (2569464)Time elapsed: 1.742 s
% 138.22/20.86 % (2569464)Peak memory usage: 137 MB
% 138.22/20.86 % (2569464)Instructions burned: 3604 (million)
% 138.22/20.86 % (2569473)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=286836935:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2832 on theBenchmark for (2832ds/3902Mi)
% 138.22/20.86 % (2569474)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=744827507:avsq=on:i=3916:aac=none:amm=off_2831 on theBenchmark for (2831ds/3916Mi)
% 138.22/20.86 % (2569471)Instruction limit reached!
% 138.22/20.86 % (2569471)------------------------------
% 138.22/20.86 % (2569471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.22/20.86 % (2569471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.22/20.86 % (2569471)CaDiCaL version: 2.1.3
% 138.22/20.86 % (2569471)Termination reason: Instruction limit
% 138.22/20.86 % (2569471)Termination phase: Saturation
% 138.22/20.86 % (2569471)Time elapsed: 0.689 s
% 138.22/20.86 % (2569471)Peak memory usage: 134 MB
% 138.22/20.86 % (2569471)Instructions burned: 1981 (million)
% 138.22/20.86 % (2569477)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=982426651:cond=on:i=3940:av=off:er=known_2829 on theBenchmark for (2829ds/3940Mi)
% 138.22/20.86 [W927 13:54:08.391627793 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.22/20.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.22/20.86 [W927 13:54:08.391676827 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.22/20.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.22/20.86 [W927 13:54:08.391714891 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.22/20.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.22/20.86 [W927 13:54:08.391726491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.22/20.86 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.22/20.86 [W927 13:54:08.391751118 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391761464 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391795291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391857068 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391891409 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391901705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391925115 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:08.391935039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 % (2569473)Refutation not found, incomplete strategy
% 142.81/21.48 % (2569473)------------------------------
% 142.81/21.48 % (2569473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.81/21.48 % (2569473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.81/21.48 % (2569473)CaDiCaL version: 2.1.3
% 142.81/21.48 % (2569473)Termination reason: Refutation not found, incomplete strategy
% 142.81/21.48 % (2569473)Time elapsed: 0.549 s
% 142.81/21.48 % (2569473)Peak memory usage: 125 MB
% 142.81/21.48 % (2569473)Instructions burned: 826 (million)
% 142.81/21.48 % (2569473)------------------------------
% 142.81/21.48 % (2569473)------------------------------
% 142.81/21.48 % (2569479)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=311548833:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2823 on theBenchmark for (2823ds/3980Mi)
% 142.81/21.48 % (2569477)Instruction limit reached!
% 142.81/21.48 % (2569477)------------------------------
% 142.81/21.48 % (2569477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.81/21.48 % (2569477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.81/21.48 % (2569477)CaDiCaL version: 2.1.3
% 142.81/21.48 % (2569477)Termination reason: Instruction limit
% 142.81/21.48 % (2569477)Termination phase: Saturation
% 142.81/21.48 % (2569477)Time elapsed: 1.186 s
% 142.81/21.48 % (2569477)Peak memory usage: 156 MB
% 142.81/21.48 % (2569477)Instructions burned: 3941 (million)
% 142.81/21.48 % (2569481)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2881075001:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2816 on theBenchmark for (2816ds/2087Mi)
% 142.81/21.48 % (2569474)Instruction limit reached!
% 142.81/21.48 % (2569474)------------------------------
% 142.81/21.48 % (2569474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.81/21.48 % (2569474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.81/21.48 % (2569474)CaDiCaL version: 2.1.3
% 142.81/21.48 % (2569474)Termination reason: Instruction limit
% 142.81/21.48 % (2569474)Termination phase: Saturation
% 142.81/21.48 % (2569474)Time elapsed: 2.125 s
% 142.81/21.48 % (2569474)Peak memory usage: 98 MB
% 142.81/21.48 % (2569474)Instructions burned: 3917 (million)
% 142.81/21.48 % (2569481)Instruction limit reached!
% 142.81/21.48 % (2569481)------------------------------
% 142.81/21.48 % (2569481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.81/21.48 % (2569481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.81/21.48 % (2569481)CaDiCaL version: 2.1.3
% 142.81/21.48 % (2569481)Termination reason: Instruction limit
% 142.81/21.48 % (2569481)Termination phase: Saturation
% 142.81/21.48 % (2569481)Time elapsed: 0.716 s
% 142.81/21.48 % (2569481)Peak memory usage: 138 MB
% 142.81/21.48 % (2569481)Instructions burned: 2091 (million)
% 142.81/21.48 % (2569483)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2538191088:cts=off:cond=on:i=4272:bs=on:fsd=on_2808 on theBenchmark for (2808ds/4272Mi)
% 142.81/21.48 % (2569484)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=856897941:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2807 on theBenchmark for (2807ds/2197Mi)
% 142.81/21.48 [W927 13:54:10.672236469 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672258509 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672279819 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672286235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672300480 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672307080 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672319953 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672326130 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672338838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672345197 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672369424 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 [W927 13:54:10.672375023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 142.81/21.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 142.81/21.48 % (2569484)Refutation not found, incomplete strategy
% 142.81/21.48 % (2569484)------------------------------
% 142.81/21.48 % (2569484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.81/21.48 % (2569484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.81/21.48 % (2569484)CaDiCaL version: 2.1.3
% 142.81/21.48 % (2569484)Termination reason: Refutation not found, incomplete strategy
% 142.81/21.48 % (2569484)Time elapsed: 0.313 s
% 142.81/21.48 % (2569484)Peak memory usage: 125 MB
% 142.81/21.48 % (2569484)Instructions burned: 826 (million)
% 142.81/21.48 % (2569484)------------------------------
% 142.81/21.48 % (2569484)------------------------------
% 142.81/21.48 % (2569487)dis+21_1_sil=8000:spb=goal_then_units:random_seed=2340924913:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2801 on theBenchmark for (2801ds/6508Mi)
% 142.81/21.48 % (2569487)First to succeed.
% 142.81/21.48 % (2569487)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2568755"
% 142.81/21.48 % SZS status Satisfiable for theBenchmark
% 142.81/21.48 % SZS output start Saturation.
% See solution above
% 143.83/21.72 % SZS output start Definitions and Model Updates.
% 143.83/21.72 % SZS output end Definitions and Model Updates.
% 143.83/21.72 % (2569487)------------------------------
% 143.83/21.72 % (2569487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.83/21.72 % (2569487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.83/21.72 % (2569487)CaDiCaL version: 2.1.3
% 143.83/21.72 % (2569487)Termination reason: Satisfiable
% 143.83/21.72 % (2569487)Time elapsed: 0.035 s
% 143.83/21.72 % (2569487)Peak memory usage: 89 MB
% 143.83/21.72 % (2569487)Instructions burned: 112 (million)
% 143.83/21.72 % (2569487)------------------------------
% 143.83/21.72 % (2569487)------------------------------
% 143.83/21.72 % (2568755)Success in time 20.161 s
% 143.83/21.72 % Vampire exiting
%------------------------------------------------------------------------------