%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT308+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:46:46 AM UTC 2026
% Result : Theorem 26.00s 9.82s
% Output : Refutation 50.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 17
% Syntax : Number of formulae : 134 ( 25 unt; 7 def)
% Number of atoms : 531 ( 100 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 652 ( 255 ~; 265 |; 103 &)
% ( 6 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 7 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-3 aty)
% Number of variables : 121 ( 0 sgn 115 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21525,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( ~ ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k4_lattices(X0,X1,X2) = X1 )
& k2_filter_0(X0,X1) = u1_struct_0(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_filter_0) ).
fof(f22747,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f22752,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22852,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f34616,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f34671,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f34674,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
=> ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
& k4_lattices(k1_lattice2(X0),X3,X4) = k3_lattices(X0,k6_filter_2(X0,X3),k6_filter_2(X0,X4))
& k3_lattices(k1_lattice2(X0),X3,X4) = k4_lattices(X0,k6_filter_2(X0,X3),k6_filter_2(X0,X4)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t19_filter_2) ).
fof(f34691,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f34697,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( ~ ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k3_lattices(X0,X1,X2) = X1 )
& k18_filter_2(X0,X1) = u1_struct_0(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t35_filter_2) ).
fof(f34698,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ~ ( ~ ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k3_lattices(X0,X1,X2) = X1 )
& k18_filter_2(X0,X1) = u1_struct_0(X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f34697]) ).
fof(f34848,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k3_lattices(X0,X1,X2) != X1
& m1_subset_1(X2,u1_struct_0(X0)) )
& k18_filter_2(X0,X1) = u1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34698]) ).
fof(f34849,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( k3_lattices(X0,X1,X2) != X1
& m1_subset_1(X2,u1_struct_0(X0)) )
& k18_filter_2(X0,X1) = u1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34848]) ).
fof(f34942,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34691]) ).
fof(f34943,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34942]) ).
fof(f35203,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35210,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22780]) ).
fof(f35211,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35210]) ).
fof(f35213,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22752]) ).
fof(f35214,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35213]) ).
fof(f35215,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f35216,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35215]) ).
fof(f35284,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34616]) ).
fof(f35285,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f35284]) ).
fof(f35290,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
& k4_lattices(k1_lattice2(X0),X3,X4) = k3_lattices(X0,k6_filter_2(X0,X3),k6_filter_2(X0,X4))
& k3_lattices(k1_lattice2(X0),X3,X4) = k4_lattices(X0,k6_filter_2(X0,X3),k6_filter_2(X0,X4)) )
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34674]) ).
fof(f35291,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
& k4_lattices(k1_lattice2(X0),X3,X4) = k3_lattices(X0,k6_filter_2(X0,X3),k6_filter_2(X0,X4))
& k3_lattices(k1_lattice2(X0),X3,X4) = k4_lattices(X0,k6_filter_2(X0,X3),k6_filter_2(X0,X4)) )
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35290]) ).
fof(f35294,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34671]) ).
fof(f35295,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35294]) ).
fof(f37045,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k4_lattices(X0,X1,X2) = X1
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| u1_struct_0(X0) != k2_filter_0(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21525]) ).
fof(f37046,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k4_lattices(X0,X1,X2) = X1
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| u1_struct_0(X0) != k2_filter_0(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f37045]) ).
fof(f37114,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP4(X0) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f37115,plain,
! [X0] :
( sP4(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f35214,f37114]) ).
fof(f37208,plain,
( sK61 != k3_lattices(sK60,sK61,sK62)
& m1_subset_1(sK62,u1_struct_0(sK60))
& u1_struct_0(sK60) = k18_filter_2(sK60,sK61)
& m1_subset_1(sK61,u1_struct_0(sK60))
& ~ v3_struct_0(sK60)
& v10_lattices(sK60)
& l3_lattices(sK60) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60,sK61,sK62]),skolemize(X0,sK60),skolemize(X1,sK61),skolemize(X2,sK62)],[f34849]) ).
fof(f37312,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| ~ sP4(X0) ),
inference(nnf_transformation,[],[f37114]) ).
fof(f38038,plain,
l3_lattices(sK60),
inference(cnf_transformation,[],[f37208]) ).
fof(f38039,plain,
v10_lattices(sK60),
inference(cnf_transformation,[],[f37208]) ).
fof(f38040,plain,
~ v3_struct_0(sK60),
inference(cnf_transformation,[],[f37208]) ).
fof(f38041,plain,
m1_subset_1(sK61,u1_struct_0(sK60)),
inference(cnf_transformation,[],[f37208]) ).
fof(f38042,plain,
u1_struct_0(sK60) = k18_filter_2(sK60,sK61),
inference(cnf_transformation,[],[f37208]) ).
fof(f38043,plain,
m1_subset_1(sK62,u1_struct_0(sK60)),
inference(cnf_transformation,[],[f37208]) ).
fof(f38044,plain,
sK61 != k3_lattices(sK60,sK61,sK62),
inference(cnf_transformation,[],[f37208]) ).
fof(f38133,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34943]) ).
fof(f38439,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35203]) ).
fof(f38448,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f35211]) ).
fof(f38450,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f37312]) ).
fof(f38459,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP4(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37115]) ).
fof(f38461,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35216]) ).
fof(f38624,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f35285]) ).
fof(f38632,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),k5_filter_2(X0,X1),k5_filter_2(X0,X2))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35291]) ).
fof(f38636,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35295]) ).
fof(f41425,plain,
! [X2,X0,X1] :
( u1_struct_0(X0) != k2_filter_0(X0,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k4_lattices(X0,X1,X2) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f37046]) ).
fof(f42730,plain,
( k18_filter_2(sK60,sK61) = k2_filter_2(k1_lattice2(sK60),k5_filter_2(sK60,sK61))
| v3_struct_0(sK60)
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(resolution,[],[f38133,f38041]) ).
fof(f42731,plain,
( k18_filter_2(sK60,sK61) = k2_filter_2(k1_lattice2(sK60),k5_filter_2(sK60,sK61))
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f42730,f38040]) ).
fof(f42733,plain,
( k18_filter_2(sK60,sK61) = k2_filter_2(k1_lattice2(sK60),k5_filter_2(sK60,sK61))
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f42731,f38039]) ).
fof(f42735,plain,
k18_filter_2(sK60,sK61) = k2_filter_2(k1_lattice2(sK60),k5_filter_2(sK60,sK61)),
inference(forward_subsumption_resolution,[],[f42733,f38038]) ).
fof(f42737,plain,
u1_struct_0(sK60) = k2_filter_2(k1_lattice2(sK60),k5_filter_2(sK60,sK61)),
inference(forward_demodulation,[],[f42735,f38042]) ).
fof(f42773,plain,
( v3_struct_0(sK60)
| u1_struct_0(sK60) = u1_struct_0(k1_lattice2(sK60)) ),
inference(resolution,[],[f38448,f38038]) ).
fof(f42775,plain,
u1_struct_0(sK60) = u1_struct_0(k1_lattice2(sK60)),
inference(forward_subsumption_resolution,[],[f42773,f38040]) ).
fof(f42778,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| v3_struct_0(k1_lattice2(sK60))
| ~ v10_lattices(k1_lattice2(sK60))
| ~ l3_lattices(k1_lattice2(sK60))
| k2_filter_0(k1_lattice2(sK60),X0) = k2_filter_2(k1_lattice2(sK60),X0) ),
inference(superposition,[],[f38624,f42775]) ).
fof(f42782,definition,
( spl555_11
<=> l3_lattices(k1_lattice2(sK60)) ),
introduced(definition,[new_symbols(definition,[spl555_11])],[avatar_definition]) ).
fof(f42783,plain,
( l3_lattices(k1_lattice2(sK60))
| ~ spl555_11 ),
inference(avatar_component_clause,[],[f42782]) ).
fof(f42784,plain,
( ~ l3_lattices(k1_lattice2(sK60))
| spl555_11 ),
inference(avatar_component_clause,[],[f42782]) ).
fof(f42786,definition,
( spl555_12
<=> v10_lattices(k1_lattice2(sK60)) ),
introduced(definition,[new_symbols(definition,[spl555_12])],[avatar_definition]) ).
fof(f42787,plain,
( v10_lattices(k1_lattice2(sK60))
| ~ spl555_12 ),
inference(avatar_component_clause,[],[f42786]) ).
fof(f42788,plain,
( ~ v10_lattices(k1_lattice2(sK60))
| spl555_12 ),
inference(avatar_component_clause,[],[f42786]) ).
fof(f42790,definition,
( spl555_13
<=> v3_struct_0(k1_lattice2(sK60)) ),
introduced(definition,[new_symbols(definition,[spl555_13])],[avatar_definition]) ).
fof(f42791,plain,
( ~ v3_struct_0(k1_lattice2(sK60))
| spl555_13 ),
inference(avatar_component_clause,[],[f42790]) ).
fof(f42792,plain,
( v3_struct_0(k1_lattice2(sK60))
| ~ spl555_13 ),
inference(avatar_component_clause,[],[f42790]) ).
fof(f42797,definition,
( spl555_15
<=> ! [X0] : ~ m1_subset_1(X0,u1_struct_0(sK60)) ),
introduced(definition,[new_symbols(definition,[spl555_15])],[avatar_definition]) ).
fof(f42798,plain,
( ! [X0] : ~ m1_subset_1(X0,u1_struct_0(sK60))
| ~ spl555_15 ),
inference(avatar_component_clause,[],[f42797]) ).
fof(f42805,definition,
( spl555_17
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k2_filter_0(k1_lattice2(sK60),X0) = k2_filter_2(k1_lattice2(sK60),X0) ) ),
introduced(definition,[new_symbols(definition,[spl555_17])],[avatar_definition]) ).
fof(f42806,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k2_filter_0(k1_lattice2(sK60),X0) = k2_filter_2(k1_lattice2(sK60),X0) )
| ~ spl555_17 ),
inference(avatar_component_clause,[],[f42805]) ).
fof(f42807,plain,
( ~ spl555_11
| ~ spl555_12
| spl555_13
| spl555_17 ),
inference(avatar_split_clause,[],[f42778,f42805,f42790,f42786,f42782]) ).
fof(f42816,plain,
( ~ l3_lattices(sK60)
| spl555_11 ),
inference(resolution,[],[f42784,f38439]) ).
fof(f42817,plain,
( $false
| spl555_11 ),
inference(forward_subsumption_resolution,[],[f42816,f38038]) ).
fof(f42818,plain,
spl555_11,
inference(avatar_contradiction_clause,[],[f42817]) ).
fof(f42826,plain,
( v3_struct_0(sK60)
| ~ l3_lattices(sK60)
| ~ spl555_13 ),
inference(resolution,[],[f42792,f38461]) ).
fof(f42827,plain,
( ~ l3_lattices(sK60)
| ~ spl555_13 ),
inference(forward_subsumption_resolution,[],[f42826,f38040]) ).
fof(f42828,plain,
( $false
| ~ spl555_13 ),
inference(forward_subsumption_resolution,[],[f42827,f38038]) ).
fof(f42829,plain,
~ spl555_13,
inference(avatar_contradiction_clause,[],[f42828]) ).
fof(f42841,plain,
( ~ sP4(sK60)
| spl555_12 ),
inference(resolution,[],[f38450,f42788]) ).
fof(f42873,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k3_lattices(sK60,X1,X2) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X1),k5_filter_2(sK60,X2))
| ~ m1_subset_1(X3,u1_struct_0(sK60))
| ~ m1_subset_1(X2,u1_struct_0(sK60))
| ~ m1_subset_1(X1,u1_struct_0(sK60))
| v3_struct_0(sK60)
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(superposition,[],[f38632,f42775]) ).
fof(f42874,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k3_lattices(sK60,X1,X2) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X1),k5_filter_2(sK60,X2))
| ~ m1_subset_1(X3,u1_struct_0(sK60))
| ~ m1_subset_1(X2,u1_struct_0(sK60))
| ~ m1_subset_1(X1,u1_struct_0(sK60))
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f42873,f38040]) ).
fof(f42875,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k3_lattices(sK60,X1,X2) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X1),k5_filter_2(sK60,X2))
| ~ m1_subset_1(X3,u1_struct_0(sK60))
| ~ m1_subset_1(X2,u1_struct_0(sK60))
| ~ m1_subset_1(X1,u1_struct_0(sK60))
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f42874,f38039]) ).
fof(f42876,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k3_lattices(sK60,X1,X2) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X1),k5_filter_2(sK60,X2))
| ~ m1_subset_1(X3,u1_struct_0(sK60))
| ~ m1_subset_1(X2,u1_struct_0(sK60))
| ~ m1_subset_1(X1,u1_struct_0(sK60)) ),
inference(forward_subsumption_resolution,[],[f42875,f38038]) ).
fof(f42878,definition,
( spl555_24
<=> ! [X2,X1] :
( k3_lattices(sK60,X1,X2) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X1),k5_filter_2(sK60,X2))
| ~ m1_subset_1(X1,u1_struct_0(sK60))
| ~ m1_subset_1(X2,u1_struct_0(sK60)) ) ),
introduced(definition,[new_symbols(definition,[spl555_24])],[avatar_definition]) ).
fof(f42879,plain,
( ! [X2,X1] :
( ~ m1_subset_1(X2,u1_struct_0(sK60))
| ~ m1_subset_1(X1,u1_struct_0(sK60))
| k3_lattices(sK60,X1,X2) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X1),k5_filter_2(sK60,X2)) )
| ~ spl555_24 ),
inference(avatar_component_clause,[],[f42878]) ).
fof(f42880,plain,
( spl555_15
| spl555_24
| spl555_15 ),
inference(avatar_split_clause,[],[f42876,f42797,f42878,f42797]) ).
fof(f42881,plain,
( $false
| ~ spl555_15 ),
inference(resolution,[],[f42798,f38043]) ).
fof(f42884,plain,
~ spl555_15,
inference(avatar_contradiction_clause,[],[f42881]) ).
fof(f42885,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| k3_lattices(sK60,X0,sK62) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,X0),k5_filter_2(sK60,sK62)) )
| ~ spl555_24 ),
inference(resolution,[],[f42879,f38043]) ).
fof(f42890,plain,
( k3_lattices(sK60,sK61,sK62) = k4_lattices(k1_lattice2(sK60),k5_filter_2(sK60,sK61),k5_filter_2(sK60,sK62))
| ~ spl555_24 ),
inference(resolution,[],[f42885,f38041]) ).
fof(f42906,plain,
( v3_struct_0(sK60)
| sP4(sK60)
| ~ l3_lattices(sK60) ),
inference(resolution,[],[f38459,f38039]) ).
fof(f42909,plain,
( sP4(sK60)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f42906,f38040]) ).
fof(f42910,plain,
( ~ l3_lattices(sK60)
| spl555_12 ),
inference(forward_subsumption_resolution,[],[f42909,f42841]) ).
fof(f42911,plain,
( $false
| spl555_12 ),
inference(forward_subsumption_resolution,[],[f42910,f38038]) ).
fof(f42912,plain,
spl555_12,
inference(avatar_contradiction_clause,[],[f42911]) ).
fof(f43045,plain,
( sK62 = k5_filter_2(sK60,sK62)
| v3_struct_0(sK60)
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(resolution,[],[f38636,f38043]) ).
fof(f43046,plain,
( sK61 = k5_filter_2(sK60,sK61)
| v3_struct_0(sK60)
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(resolution,[],[f38636,f38041]) ).
fof(f43049,plain,
( sK61 = k5_filter_2(sK60,sK61)
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f43046,f38040]) ).
fof(f43050,plain,
( sK62 = k5_filter_2(sK60,sK62)
| ~ v10_lattices(sK60)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f43045,f38040]) ).
fof(f43052,plain,
( sK61 = k5_filter_2(sK60,sK61)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f43049,f38039]) ).
fof(f43053,plain,
( sK62 = k5_filter_2(sK60,sK62)
| ~ l3_lattices(sK60) ),
inference(forward_subsumption_resolution,[],[f43050,f38039]) ).
fof(f43055,plain,
sK61 = k5_filter_2(sK60,sK61),
inference(forward_subsumption_resolution,[],[f43052,f38038]) ).
fof(f43056,plain,
sK62 = k5_filter_2(sK60,sK62),
inference(forward_subsumption_resolution,[],[f43053,f38038]) ).
fof(f43058,plain,
( k3_lattices(sK60,sK61,sK62) = k4_lattices(k1_lattice2(sK60),sK61,k5_filter_2(sK60,sK62))
| ~ spl555_24 ),
inference(superposition,[],[f42890,f43055]) ).
fof(f43061,plain,
u1_struct_0(sK60) = k2_filter_2(k1_lattice2(sK60),sK61),
inference(superposition,[],[f42737,f43055]) ).
fof(f43064,plain,
( k3_lattices(sK60,sK61,sK62) = k4_lattices(k1_lattice2(sK60),sK61,sK62)
| ~ spl555_24 ),
inference(forward_demodulation,[],[f43058,f43056]) ).
fof(f43925,plain,
( k2_filter_2(k1_lattice2(sK60),sK61) = k2_filter_0(k1_lattice2(sK60),sK61)
| ~ spl555_17 ),
inference(resolution,[],[f42806,f38041]) ).
fof(f43927,plain,
( u1_struct_0(sK60) = k2_filter_0(k1_lattice2(sK60),sK61)
| ~ spl555_17 ),
inference(forward_demodulation,[],[f43925,f43061]) ).
fof(f44596,plain,
( ! [X0] :
( u1_struct_0(sK60) != u1_struct_0(k1_lattice2(sK60))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK60)))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0)
| ~ m1_subset_1(sK61,u1_struct_0(k1_lattice2(sK60)))
| v3_struct_0(k1_lattice2(sK60))
| ~ v10_lattices(k1_lattice2(sK60))
| ~ l3_lattices(k1_lattice2(sK60)) )
| ~ spl555_17 ),
inference(superposition,[],[f41425,f43927]) ).
fof(f44597,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK60)))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0)
| ~ m1_subset_1(sK61,u1_struct_0(k1_lattice2(sK60)))
| v3_struct_0(k1_lattice2(sK60))
| ~ v10_lattices(k1_lattice2(sK60))
| ~ l3_lattices(k1_lattice2(sK60)) )
| ~ spl555_17 ),
inference(forward_subsumption_resolution,[],[f44596,f42775]) ).
fof(f44599,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK60)))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0)
| ~ m1_subset_1(sK61,u1_struct_0(k1_lattice2(sK60)))
| ~ v10_lattices(k1_lattice2(sK60))
| ~ l3_lattices(k1_lattice2(sK60)) )
| spl555_13
| ~ spl555_17 ),
inference(forward_subsumption_resolution,[],[f44597,f42791]) ).
fof(f44601,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK60)))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0)
| ~ m1_subset_1(sK61,u1_struct_0(k1_lattice2(sK60)))
| ~ l3_lattices(k1_lattice2(sK60)) )
| ~ spl555_12
| spl555_13
| ~ spl555_17 ),
inference(forward_subsumption_resolution,[],[f44599,f42787]) ).
fof(f44603,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK60)))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0)
| ~ m1_subset_1(sK61,u1_struct_0(k1_lattice2(sK60))) )
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17 ),
inference(forward_subsumption_resolution,[],[f44601,f42783]) ).
fof(f44605,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0)
| ~ m1_subset_1(sK61,u1_struct_0(k1_lattice2(sK60))) )
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17 ),
inference(forward_demodulation,[],[f44603,f42775]) ).
fof(f44606,plain,
( ! [X0] :
( ~ m1_subset_1(sK61,u1_struct_0(sK60))
| ~ m1_subset_1(X0,u1_struct_0(sK60))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0) )
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17 ),
inference(forward_demodulation,[],[f44605,f42775]) ).
fof(f44607,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK60))
| sK61 = k4_lattices(k1_lattice2(sK60),sK61,X0) )
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17 ),
inference(forward_subsumption_resolution,[],[f44606,f38041]) ).
fof(f44608,plain,
( sK61 = k4_lattices(k1_lattice2(sK60),sK61,sK62)
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17 ),
inference(resolution,[],[f44607,f38043]) ).
fof(f44616,plain,
( sK61 = k3_lattices(sK60,sK61,sK62)
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17
| ~ spl555_24 ),
inference(superposition,[],[f44608,f43064]) ).
fof(f44623,plain,
( $false
| ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17
| ~ spl555_24 ),
inference(forward_subsumption_resolution,[],[f44616,f38044]) ).
fof(f44624,plain,
( ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17
| ~ spl555_24 ),
inference(avatar_contradiction_clause,[],[f44623]) ).
cnf(s9,plain,
( ~ spl555_11
| ~ spl555_12
| spl555_13
| spl555_17 ),
inference(sat_conversion,[],[f42807]) ).
cnf(s12,plain,
spl555_11,
inference(sat_conversion,[],[f42818]) ).
cnf(s14,plain,
~ spl555_13,
inference(sat_conversion,[],[f42829]) ).
cnf(s17,plain,
( spl555_15
| spl555_15
| spl555_24 ),
inference(sat_conversion,[],[f42880]) ).
cnf(s18,plain,
( spl555_15
| spl555_24 ),
inference(rat,[],[s17]) ).
cnf(s20,plain,
~ spl555_15,
inference(sat_conversion,[],[f42884]) ).
cnf(s21,plain,
spl555_12,
inference(sat_conversion,[],[f42912]) ).
cnf(s80,plain,
( ~ spl555_11
| ~ spl555_12
| spl555_13
| ~ spl555_17
| ~ spl555_24 ),
inference(sat_conversion,[],[f44624]) ).
cnf(s88,plain,
spl555_24,
inference(rat,[],[s18,s20]) ).
cnf(s90,plain,
~ spl555_17,
inference(rat,[],[s80,s88,s14,s21,s12]) ).
cnf(s99,plain,
$false,
inference(rat,[],[s9,s90,s14,s21,s12]) ).
fof(f44632,plain,
$false,
inference(avatar_sat_refutation,[],[s99]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT308+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n004.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:27:44 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.97/6.03 % (3574842)Detected formulas, will run a generic FOF schedule.
% 21.97/6.03 % (3574933)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3723359123:i=109:sd=1:ins=1:gsp=on:ss=axioms_2977 on theBenchmark for (2977ds/109Mi)
% 21.97/6.03 % (3574935)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3835505159:s2a=on:i=139:gtg=position_2977 on theBenchmark for (2977ds/139Mi)
% 21.97/6.03 % (3574930)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=2816864014:i=141193_2977 on theBenchmark for (2977ds/141193Mi)
% 21.97/6.03 % (3574931)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1037988458:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2977 on theBenchmark for (2977ds/134677Mi)
% 21.97/6.03 % (3574932)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1439718541:i=141695:sd=1:nm=32:gsp=on:ss=included_2977 on theBenchmark for (2977ds/141695Mi)
% 21.97/6.03 % (3574934)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1789020252:i=119:av=off:ss=axioms_2977 on theBenchmark for (2977ds/119Mi)
% 21.97/6.03 % (3574933)Instruction limit reached!
% 21.97/6.03 % (3574933)------------------------------
% 21.97/6.03 % (3574933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.97/6.03 % (3574933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.97/6.03 % (3574933)CaDiCaL version: 2.1.3
% 21.97/6.03 % (3574933)Termination reason: Instruction limit
% 21.97/6.03 % (3574933)Termination phase: SInE selection
% 21.97/6.03 % (3574933)Time elapsed: 0.074 s
% 21.97/6.03 % (3574933)Peak memory usage: 136 MB
% 21.97/6.03 % (3574933)Instructions burned: 110 (million)
% 21.97/6.03 % (3574936)dis-21_1_sil=8000:lcm=predicate:random_seed=3155480067:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2977 on theBenchmark for (2977ds/129Mi)
% 21.97/6.03 % (3574935)Instruction limit reached!
% 21.97/6.03 % (3574935)------------------------------
% 21.97/6.03 % (3574935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.97/6.03 % (3574935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.97/6.03 % (3574935)CaDiCaL version: 2.1.3
% 21.97/6.03 % (3574935)Termination reason: Instruction limit
% 21.97/6.03 % (3574935)Termination phase: Property scanning
% 21.97/6.03 % (3574935)Time elapsed: 0.119 s
% 21.97/6.03 % (3574935)Peak memory usage: 136 MB
% 21.97/6.03 % (3574935)Instructions burned: 140 (million)
% 21.97/6.03 % (3574936)Instruction limit reached!
% 21.97/6.03 % (3574936)------------------------------
% 21.97/6.03 % (3574936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.97/6.03 % (3574936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.97/6.03 % (3574936)CaDiCaL version: 2.1.3
% 21.97/6.03 % (3574936)Termination reason: Instruction limit
% 21.97/6.03 % (3574936)Termination phase: SInE selection
% 21.97/6.03 % (3574936)Time elapsed: 0.083 s
% 21.97/6.03 % (3574936)Peak memory usage: 136 MB
% 21.97/6.03 % (3574936)Instructions burned: 131 (million)
% 21.97/6.03 % (3574934)Instruction limit reached!
% 21.97/6.03 % (3574934)------------------------------
% 21.97/6.03 % (3574934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.97/6.03 % (3574934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.97/6.03 % (3574934)CaDiCaL version: 2.1.3
% 21.97/6.03 % (3574934)Termination reason: Instruction limit
% 21.97/6.03 % (3574934)Termination phase: SInE selection
% 21.97/6.03 % (3574934)Time elapsed: 0.134 s
% 21.97/6.03 % (3574934)Peak memory usage: 136 MB
% 21.97/6.03 % (3574934)Instructions burned: 120 (million)
% 21.97/6.03 % (3574943)lrs+10_1_sil=8000:sp=occurrence:random_seed=2732326674:i=285:sd=3:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/285Mi)
% 21.97/6.03 % (3574945)lrs+10_1_sil=32000:urr=on:br=off:random_seed=730411477:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/157Mi)
% 21.97/6.03 % (3574946)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4134608707:i=325:sd=1:ss=axioms:sgt=32_2973 on theBenchmark for (2973ds/325Mi)
% 21.97/6.03 % (3574947)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3433196393:s2a=on:i=248:s2at=1.23:gtg=position_2973 on theBenchmark for (2973ds/248Mi)
% 21.97/6.03 % (3574945)Instruction limit reached!
% 34.80/7.70 % (3574945)------------------------------
% 34.80/7.70 % (3574945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.80/7.70 % (3574945)CaDiCaL version: 2.1.3
% 34.80/7.70 % (3574945)Termination reason: Instruction limit
% 34.80/7.70 % (3574945)Termination phase: Property scanning
% 34.80/7.70 % (3574945)Time elapsed: 0.112 s
% 34.80/7.70 % (3574945)Peak memory usage: 136 MB
% 34.80/7.70 % (3574945)Instructions burned: 158 (million)
% 34.80/7.70 % (3574946)Refutation not found, incomplete strategy
% 34.80/7.70 % (3574946)------------------------------
% 34.80/7.70 % (3574946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.80/7.70 % (3574946)CaDiCaL version: 2.1.3
% 34.80/7.70 % (3574946)Termination reason: Refutation not found, incomplete strategy
% 34.80/7.70 % (3574946)Time elapsed: 0.166 s
% 34.80/7.70 % (3574946)Peak memory usage: 142 MB
% 34.80/7.70 % (3574946)Instructions burned: 244 (million)
% 34.80/7.70 % (3574943)Instruction limit reached!
% 34.80/7.70 % (3574943)------------------------------
% 34.80/7.70 % (3574943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.80/7.70 % (3574943)CaDiCaL version: 2.1.3
% 34.80/7.70 % (3574943)Termination reason: Instruction limit
% 34.80/7.70 % (3574943)Termination phase: Saturation
% 34.80/7.70 % (3574943)Time elapsed: 0.330 s
% 34.80/7.70 % (3574943)Peak memory usage: 142 MB
% 34.80/7.70 % (3574943)Instructions burned: 285 (million)
% 34.80/7.70 % (3574947)Instruction limit reached!
% 34.80/7.70 % (3574947)------------------------------
% 34.80/7.70 % (3574947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.80/7.70 % (3574947)CaDiCaL version: 2.1.3
% 34.80/7.70 % (3574947)Termination reason: Instruction limit
% 34.80/7.70 % (3574947)Termination phase: Property scanning
% 34.80/7.70 % (3574947)Time elapsed: 0.195 s
% 34.80/7.70 % (3574947)Peak memory usage: 136 MB
% 34.80/7.70 % (3574947)Instructions burned: 249 (million)
% 34.80/7.70 % (3574958)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2628599891:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2970 on theBenchmark for (2970ds/294Mi)
% 34.80/7.70 % (3574946)------------------------------
% 34.80/7.70 % (3574946)------------------------------
% 34.80/7.70 % (3574959)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4141498078:i=2350_2968 on theBenchmark for (2968ds/2350Mi)
% 34.80/7.70 % (3574960)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2164120743:cts=off:i=113:fsr=off:ss=included:sgt=4_2968 on theBenchmark for (2968ds/113Mi)
% 34.80/7.70 % (3574958)Instruction limit reached!
% 34.80/7.70 % (3574958)------------------------------
% 34.80/7.70 % (3574958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.80/7.70 % (3574958)CaDiCaL version: 2.1.3
% 34.80/7.70 % (3574958)Termination reason: Instruction limit
% 34.80/7.70 % (3574958)Termination phase: SInE selection
% 34.80/7.70 % (3574958)Time elapsed: 0.280 s
% 34.80/7.70 % (3574958)Peak memory usage: 137 MB
% 34.80/7.70 % (3574958)Instructions burned: 295 (million)
% 34.80/7.70 % (3574964)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1618794544:i=127:av=off:fsr=off:sup=off_2967 on theBenchmark for (2967ds/127Mi)
% 34.80/7.70 % (3574964)Instruction limit reached!
% 34.80/7.70 % (3574964)------------------------------
% 34.80/7.70 % (3574964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.80/7.70 % (3574964)CaDiCaL version: 2.1.3
% 34.80/7.70 % (3574964)Termination reason: Instruction limit
% 34.80/7.70 % (3574964)Termination phase: Preprocessing 1
% 34.80/7.70 % (3574964)Time elapsed: 0.085 s
% 34.80/7.70 % (3574964)Peak memory usage: 137 MB
% 34.80/7.70 % (3574964)Instructions burned: 128 (million)
% 34.80/7.70 % (3574960)Instruction limit reached!
% 34.80/7.70 % (3574960)------------------------------
% 34.80/7.70 % (3574960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.80/7.70 % (3574960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574960)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574960)Termination reason: Instruction limit
% 26.00/9.82 % (3574960)Termination phase: SInE selection
% 26.00/9.82 % (3574960)Time elapsed: 0.127 s
% 26.00/9.82 % (3574960)Peak memory usage: 136 MB
% 26.00/9.82 % (3574960)Instructions burned: 113 (million)
% 26.00/9.82 % (3574968)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1028496922:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2965 on theBenchmark for (2965ds/114Mi)
% 26.00/9.82 % (3574968)Instruction limit reached!
% 26.00/9.82 % (3574968)------------------------------
% 26.00/9.82 % (3574968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574968)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574968)Termination reason: Instruction limit
% 26.00/9.82 % (3574968)Termination phase: Property scanning
% 26.00/9.82 % (3574968)Time elapsed: 0.057 s
% 26.00/9.82 % (3574968)Peak memory usage: 136 MB
% 26.00/9.82 % (3574968)Instructions burned: 115 (million)
% 26.00/9.82 % (3574969)lrs+10_1_sil=8000:sp=occurrence:random_seed=2114658791:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2964 on theBenchmark for (2964ds/907Mi)
% 26.00/9.82 % (3574970)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2697338549:i=437:sd=1:aac=none:ss=included_2964 on theBenchmark for (2964ds/437Mi)
% 26.00/9.82 % (3574974)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3167384945:i=5202:ss=axioms:sgt=16_2962 on theBenchmark for (2962ds/5202Mi)
% 26.00/9.82 % (3574970)Instruction limit reached!
% 26.00/9.82 % (3574970)------------------------------
% 26.00/9.82 % (3574970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574970)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574970)Termination reason: Instruction limit
% 26.00/9.82 % (3574970)Termination phase: Saturation
% 26.00/9.82 % (3574970)Time elapsed: 0.464 s
% 26.00/9.82 % (3574970)Peak memory usage: 143 MB
% 26.00/9.82 % (3574970)Instructions burned: 438 (million)
% 26.00/9.82 % (3574969)Instruction limit reached!
% 26.00/9.82 % (3574969)------------------------------
% 26.00/9.82 % (3574969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574969)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574969)Termination reason: Instruction limit
% 26.00/9.82 % (3574969)Termination phase: Property scanning
% 26.00/9.82 % (3574969)Time elapsed: 0.538 s
% 26.00/9.82 % (3574969)Peak memory usage: 157 MB
% 26.00/9.82 % (3574969)Instructions burned: 908 (million)
% 26.00/9.82 % (3574985)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4151864384:st=8:i=592:sd=3:ep=RST:ss=axioms_2956 on theBenchmark for (2956ds/592Mi)
% 26.00/9.82 % (3574984)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4109930078:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2956 on theBenchmark for (2956ds/134Mi)
% 26.00/9.82 % (3574984)Instruction limit reached!
% 26.00/9.82 % (3574984)------------------------------
% 26.00/9.82 % (3574984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574984)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574984)Termination reason: Instruction limit
% 26.00/9.82 % (3574984)Termination phase: SInE selection
% 26.00/9.82 % (3574984)Time elapsed: 0.129 s
% 26.00/9.82 % (3574984)Peak memory usage: 136 MB
% 26.00/9.82 % (3574984)Instructions burned: 134 (million)
% 26.00/9.82 % (3574988)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2467819214:st=3:i=13193:sd=3:ss=axioms_2953 on theBenchmark for (2953ds/13193Mi)
% 26.00/9.82 % (3574985)Instruction limit reached!
% 26.00/9.82 % (3574985)------------------------------
% 26.00/9.82 % (3574985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574985)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574985)Termination reason: Instruction limit
% 26.00/9.82 % (3574985)Termination phase: Naming
% 26.00/9.82 % (3574985)Time elapsed: 0.379 s
% 26.00/9.82 % (3574985)Peak memory usage: 152 MB
% 26.00/9.82 % (3574985)Instructions burned: 594 (million)
% 26.00/9.82 % (3574990)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=151850322:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2951 on theBenchmark for (2951ds/125Mi)
% 26.00/9.82 % (3574990)Instruction limit reached!
% 26.00/9.82 % (3574990)------------------------------
% 26.00/9.82 % (3574990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574990)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574990)Termination reason: Instruction limit
% 26.00/9.82 % (3574990)Termination phase: Property scanning
% 26.00/9.82 % (3574990)Time elapsed: 0.058 s
% 26.00/9.82 % (3574990)Peak memory usage: 136 MB
% 26.00/9.82 % (3574990)Instructions burned: 125 (million)
% 26.00/9.82 % (3574994)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3968230819:i=134:gtgl=5:slsql=off:gtg=exists_sym_2947 on theBenchmark for (2947ds/134Mi)
% 26.00/9.82 % (3574994)Instruction limit reached!
% 26.00/9.82 % (3574994)------------------------------
% 26.00/9.82 % (3574994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574994)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574994)Termination reason: Instruction limit
% 26.00/9.82 % (3574994)Termination phase: Property scanning
% 26.00/9.82 % (3574994)Time elapsed: 0.067 s
% 26.00/9.82 % (3574994)Peak memory usage: 137 MB
% 26.00/9.82 % (3574994)Instructions burned: 135 (million)
% 26.00/9.82 % (3574996)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2275568973:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2945 on theBenchmark for (2945ds/141Mi)
% 26.00/9.82 % (3574996)Instruction limit reached!
% 26.00/9.82 % (3574996)------------------------------
% 26.00/9.82 % (3574996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574996)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574996)Termination reason: Instruction limit
% 26.00/9.82 % (3574996)Termination phase: SInE selection
% 26.00/9.82 % (3574996)Time elapsed: 0.096 s
% 26.00/9.82 % (3574996)Peak memory usage: 136 MB
% 26.00/9.82 % (3574996)Instructions burned: 142 (million)
% 26.00/9.82 % (3574959)Instruction limit reached!
% 26.00/9.82 % (3574959)------------------------------
% 26.00/9.82 % (3574959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574959)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574959)Termination reason: Instruction limit
% 26.00/9.82 % (3574959)Termination phase: Property scanning
% 26.00/9.82 % (3574959)Time elapsed: 2.448 s
% 26.00/9.82 % (3574959)Peak memory usage: 233 MB
% 26.00/9.82 % (3574959)Instructions burned: 2350 (million)
% 26.00/9.82 % (3574998)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3726171295:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2941 on theBenchmark for (2941ds/431Mi)
% 26.00/9.82 % (3574999)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2776537427:i=6060:aac=none:ins=25_2941 on theBenchmark for (2941ds/6060Mi)
% 26.00/9.82 % (3574998)Refutation not found, incomplete strategy
% 26.00/9.82 % (3574998)------------------------------
% 26.00/9.82 % (3574998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3574998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3574998)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3574998)Termination reason: Refutation not found, incomplete strategy
% 26.00/9.82 % (3574998)Time elapsed: 0.174 s
% 26.00/9.82 % (3574998)Peak memory usage: 142 MB
% 26.00/9.82 % (3574998)Instructions burned: 241 (million)
% 26.00/9.82 % (3574998)------------------------------
% 26.00/9.82 % (3574998)------------------------------
% 26.00/9.82 % (3575002)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=906130872:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2934 on theBenchmark for (2934ds/150Mi)
% 26.00/9.82 % (3575002)Instruction limit reached!
% 26.00/9.82 % (3575002)------------------------------
% 26.00/9.82 % (3575002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.00/9.82 % (3575002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.00/9.82 % (3575002)CaDiCaL version: 2.1.3
% 26.00/9.82 % (3575002)Termination reason: Instruction limit
% 26.00/9.82 % (3575002)Termination phase: SInE selection
% 26.00/9.82 % (3575002)Time elapsed: 0.106 s
% 26.00/9.82 % (3575002)Peak memory usage: 136 MB
% 26.00/9.82 % (3575002)Instructions burned: 150 (million)
% 26.00/9.82 % (3575006)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3509450914:i=14155:bd=all_2931 on theBenchmark for (2931ds/14155Mi)
% 26.00/9.82 % (3574988)First to succeed.
% 26.00/9.82 % (3574988)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3574842"
% 26.00/9.82 % (3574988)Refutation found. Thanks to Tanya!
% 26.00/9.82 % SZS status Theorem for theBenchmark
% 26.00/9.82 % SZS output start Proof for theBenchmark
% See solution above
% 50.02/10.01 % (3574988)------------------------------
% 50.02/10.01 % (3574988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.02/10.01 % (3574988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.02/10.01 % (3574988)CaDiCaL version: 2.1.3
% 50.02/10.01 % (3574988)Termination reason: Refutation
% 50.02/10.01 % (3574988)Time elapsed: 3.547 s
% 50.02/10.01 % (3574988)Peak memory usage: 217 MB
% 50.02/10.01 % (3574988)Instructions burned: 3538 (million)
% 50.02/10.01 % (3574988)------------------------------
% 50.02/10.01 % (3574988)------------------------------
% 50.02/10.01 % (3574842)Success in time 8.946 s
% 50.02/10.01 % Vampire exiting
%------------------------------------------------------------------------------