%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT305+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:44 AM UTC 2026
% Result : Theorem 19.31s 6.59s
% Output : Refutation 20.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 16
% Syntax : Number of formulae : 114 ( 21 unt; 10 def)
% Number of atoms : 549 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 747 ( 312 ~; 353 |; 45 &)
% ( 16 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 10 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 92 ( 0 sgn 86 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21519,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))
=> ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t18_filter_0) ).
fof(f21520,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))
=> ( r2_hidden(X1,k2_filter_0(X0,X1))
& r2_hidden(k3_lattices(X0,X1,X2),k2_filter_0(X0,X1))
& r2_hidden(k3_lattices(X0,X2,X1),k2_filter_0(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_filter_0) ).
fof(f34642,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m2_filter_2(k18_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k18_filter_2) ).
fof(f34682,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] :
( m2_filter_2(X3,X0)
=> ( r2_hidden(X1,X3)
=> ( r2_hidden(k4_lattices(X0,X1,X2),X3)
& r2_hidden(k4_lattices(X0,X2,X1),X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t23_filter_2) ).
fof(f34690,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))
=> ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_filter_2) ).
fof(f34692,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))
=> ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_filter_2) ).
fof(f34693,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))
=> ( r2_hidden(X1,k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
& r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34692]) ).
fof(f34810,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f34642]) ).
fof(f34811,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f34810]) ).
fof(f34887,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X1,X2),X3)
& r2_hidden(k4_lattices(X0,X2,X1),X3) )
| ~ r2_hidden(X1,X3)
| ~ m2_filter_2(X3,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,[],[f34682]) ).
fof(f34888,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X1,X2),X3)
& r2_hidden(k4_lattices(X0,X2,X1),X3) )
| ~ r2_hidden(X1,X3)
| ~ m2_filter_2(X3,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,[],[f34887]) ).
fof(f34903,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ 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,[],[f34690]) ).
fof(f34904,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k18_filter_2(X0,X2))
<=> r3_lattices(X0,X1,X2) )
| ~ 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,[],[f34903]) ).
fof(f34907,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r2_hidden(X1,k18_filter_2(X0,X1))
| ~ r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
| ~ r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
& 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,[],[f34693]) ).
fof(f34908,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( ~ r2_hidden(X1,k18_filter_2(X0,X1))
| ~ r2_hidden(k4_lattices(X0,X1,X2),k18_filter_2(X0,X1))
| ~ r2_hidden(k4_lattices(X0,X2,X1),k18_filter_2(X0,X1)) )
& 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,[],[f34907]) ).
fof(f34979,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X1))
& r2_hidden(k3_lattices(X0,X1,X2),k2_filter_0(X0,X1))
& r2_hidden(k3_lattices(X0,X2,X1),k2_filter_0(X0,X1)) )
| ~ 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,[],[f21520]) ).
fof(f34980,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X1))
& r2_hidden(k3_lattices(X0,X1,X2),k2_filter_0(X0,X1))
& r2_hidden(k3_lattices(X0,X2,X1),k2_filter_0(X0,X1)) )
| ~ 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,[],[f34979]) ).
fof(f34981,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) )
| ~ 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,[],[f21519]) ).
fof(f34982,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X1,k2_filter_0(X0,X2))
<=> r3_lattices(X0,X2,X1) )
| ~ 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,[],[f34981]) ).
fof(f35388,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X1,k18_filter_2(X0,X2))
| ~ r3_lattices(X0,X1,X2) )
& ( r3_lattices(X0,X1,X2)
| ~ r2_hidden(X1,k18_filter_2(X0,X2)) ) )
| ~ 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(nnf_transformation,[],[f34904]) ).
fof(f35389,plain,
( ( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ r2_hidden(k4_lattices(sK18,sK19,sK20),k18_filter_2(sK18,sK19))
| ~ r2_hidden(k4_lattices(sK18,sK20,sK19),k18_filter_2(sK18,sK19)) )
& m1_subset_1(sK20,u1_struct_0(sK18))
& m1_subset_1(sK19,u1_struct_0(sK18))
& ~ v3_struct_0(sK18)
& v10_lattices(sK18)
& l3_lattices(sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20]),skolemize(X0,sK18),skolemize(X1,sK19),skolemize(X2,sK20)],[f34908]) ).
fof(f35427,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X1,k2_filter_0(X0,X2))
| ~ r3_lattices(X0,X2,X1) )
& ( r3_lattices(X0,X2,X1)
| ~ r2_hidden(X1,k2_filter_0(X0,X2)) ) )
| ~ 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(nnf_transformation,[],[f34982]) ).
fof(f35632,plain,
! [X0,X1] :
( m2_filter_2(k18_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f34811]) ).
fof(f35738,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k4_lattices(X0,X2,X1),X3)
| ~ r2_hidden(X1,X3)
| ~ m2_filter_2(X3,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,[],[f34888]) ).
fof(f35739,plain,
! [X2,X3,X0,X1] :
( r2_hidden(k4_lattices(X0,X1,X2),X3)
| ~ r2_hidden(X1,X3)
| ~ m2_filter_2(X3,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,[],[f34888]) ).
fof(f35749,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k18_filter_2(X0,X2))
| ~ r3_lattices(X0,X1,X2)
| ~ 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,[],[f35388]) ).
fof(f35752,plain,
l3_lattices(sK18),
inference(cnf_transformation,[],[f35389]) ).
fof(f35753,plain,
v10_lattices(sK18),
inference(cnf_transformation,[],[f35389]) ).
fof(f35754,plain,
~ v3_struct_0(sK18),
inference(cnf_transformation,[],[f35389]) ).
fof(f35755,plain,
m1_subset_1(sK19,u1_struct_0(sK18)),
inference(cnf_transformation,[],[f35389]) ).
fof(f35756,plain,
m1_subset_1(sK20,u1_struct_0(sK18)),
inference(cnf_transformation,[],[f35389]) ).
fof(f35757,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ r2_hidden(k4_lattices(sK18,sK19,sK20),k18_filter_2(sK18,sK19))
| ~ r2_hidden(k4_lattices(sK18,sK20,sK19),k18_filter_2(sK18,sK19)) ),
inference(cnf_transformation,[],[f35389]) ).
fof(f35870,plain,
! [X2,X0,X1] :
( r2_hidden(X1,k2_filter_0(X0,X1))
| ~ 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,[],[f34980]) ).
fof(f35871,plain,
! [X2,X0,X1] :
( r3_lattices(X0,X2,X1)
| ~ r2_hidden(X1,k2_filter_0(X0,X2))
| ~ 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,[],[f35427]) ).
fof(f36529,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| sP162(X0) ),
inference(cnf_transformation,[],[f36529_D]) ).
fof(f36529_D,definition,
! [X0] :
( ! [X2] : ~ m1_subset_1(X2,u1_struct_0(X0))
<=> ~ sP162(X0) ),
introduced(definition,[new_symbols(definition,[sP162])],[general_splitting_component_introduction]) ).
fof(f36530,plain,
! [X0,X1] :
( r2_hidden(X1,k2_filter_0(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ sP162(X0) ),
inference(general_splitting,[],[f35870,f36529_D]) ).
fof(f36560,definition,
( spl164_1
<=> v3_struct_0(sK18) ),
introduced(definition,[new_symbols(definition,[spl164_1])],[avatar_definition]) ).
fof(f36562,plain,
( ~ v3_struct_0(sK18)
| spl164_1 ),
inference(avatar_component_clause,[],[f36560]) ).
fof(f36563,plain,
~ spl164_1,
inference(avatar_split_clause,[],[f35754,f36560]) ).
fof(f36565,definition,
( spl164_2
<=> l3_lattices(sK18) ),
introduced(definition,[new_symbols(definition,[spl164_2])],[avatar_definition]) ).
fof(f36567,plain,
( l3_lattices(sK18)
| ~ spl164_2 ),
inference(avatar_component_clause,[],[f36565]) ).
fof(f36568,plain,
spl164_2,
inference(avatar_split_clause,[],[f35752,f36565]) ).
fof(f36570,definition,
( spl164_3
<=> v10_lattices(sK18) ),
introduced(definition,[new_symbols(definition,[spl164_3])],[avatar_definition]) ).
fof(f36572,plain,
( v10_lattices(sK18)
| ~ spl164_3 ),
inference(avatar_component_clause,[],[f36570]) ).
fof(f36573,plain,
spl164_3,
inference(avatar_split_clause,[],[f35753,f36570]) ).
fof(f37039,plain,
( ! [X0] :
( r2_hidden(X0,k2_filter_0(sK18,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK18))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ sP162(sK18) )
| spl164_1 ),
inference(resolution,[],[f36562,f36530]) ).
fof(f37105,plain,
( ! [X0] :
( r2_hidden(X0,k2_filter_0(sK18,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK18))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18) )
| spl164_1 ),
inference(forward_subsumption_resolution,[],[f37039,f36529]) ).
fof(f37600,plain,
( ! [X0] :
( r2_hidden(X0,k2_filter_0(sK18,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK18))
| ~ l3_lattices(sK18) )
| spl164_1
| ~ spl164_3 ),
inference(forward_subsumption_resolution,[],[f37105,f36572]) ).
fof(f37989,plain,
( ! [X0] :
( r2_hidden(X0,k2_filter_0(sK18,X0))
| ~ m1_subset_1(X0,u1_struct_0(sK18)) )
| spl164_1
| ~ spl164_2
| ~ spl164_3 ),
inference(forward_subsumption_resolution,[],[f37600,f36567]) ).
fof(f38101,definition,
( spl164_4
<=> m1_subset_1(sK19,u1_struct_0(sK18)) ),
introduced(definition,[new_symbols(definition,[spl164_4])],[avatar_definition]) ).
fof(f38103,plain,
( m1_subset_1(sK19,u1_struct_0(sK18))
| ~ spl164_4 ),
inference(avatar_component_clause,[],[f38101]) ).
fof(f38104,plain,
spl164_4,
inference(avatar_split_clause,[],[f35755,f38101]) ).
fof(f40673,definition,
( spl164_5
<=> m1_subset_1(sK20,u1_struct_0(sK18)) ),
introduced(definition,[new_symbols(definition,[spl164_5])],[avatar_definition]) ).
fof(f40675,plain,
( m1_subset_1(sK20,u1_struct_0(sK18))
| ~ spl164_5 ),
inference(avatar_component_clause,[],[f40673]) ).
fof(f40676,plain,
spl164_5,
inference(avatar_split_clause,[],[f35756,f40673]) ).
fof(f42103,definition,
( spl164_6
<=> r2_hidden(k4_lattices(sK18,sK20,sK19),k18_filter_2(sK18,sK19)) ),
introduced(definition,[new_symbols(definition,[spl164_6])],[avatar_definition]) ).
fof(f42105,plain,
( ~ r2_hidden(k4_lattices(sK18,sK20,sK19),k18_filter_2(sK18,sK19))
| spl164_6 ),
inference(avatar_component_clause,[],[f42103]) ).
fof(f42107,definition,
( spl164_7
<=> r2_hidden(k4_lattices(sK18,sK19,sK20),k18_filter_2(sK18,sK19)) ),
introduced(definition,[new_symbols(definition,[spl164_7])],[avatar_definition]) ).
fof(f42109,plain,
( ~ r2_hidden(k4_lattices(sK18,sK19,sK20),k18_filter_2(sK18,sK19))
| spl164_7 ),
inference(avatar_component_clause,[],[f42107]) ).
fof(f42111,definition,
( spl164_8
<=> r2_hidden(sK19,k18_filter_2(sK18,sK19)) ),
introduced(definition,[new_symbols(definition,[spl164_8])],[avatar_definition]) ).
fof(f42112,plain,
( r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ spl164_8 ),
inference(avatar_component_clause,[],[f42111]) ).
fof(f42113,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| spl164_8 ),
inference(avatar_component_clause,[],[f42111]) ).
fof(f42114,plain,
( ~ spl164_6
| ~ spl164_7
| ~ spl164_8 ),
inference(avatar_split_clause,[],[f35757,f42111,f42107,f42103]) ).
fof(f42118,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ m2_filter_2(k18_filter_2(sK18,sK19),sK18)
| ~ m1_subset_1(sK20,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_6 ),
inference(resolution,[],[f42105,f35738]) ).
fof(f42145,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ m1_subset_1(sK20,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_6 ),
inference(forward_subsumption_resolution,[],[f42118,f35632]) ).
fof(f42159,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl164_5
| spl164_6 ),
inference(forward_subsumption_resolution,[],[f42145,f40675]) ).
fof(f42168,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl164_4
| ~ spl164_5
| spl164_6 ),
inference(forward_subsumption_resolution,[],[f42159,f38103]) ).
fof(f42176,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_4
| ~ spl164_5
| spl164_6 ),
inference(forward_subsumption_resolution,[],[f42168,f36562]) ).
fof(f42183,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_6 ),
inference(forward_subsumption_resolution,[],[f42176,f36572]) ).
fof(f42188,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_6 ),
inference(forward_subsumption_resolution,[],[f42183,f36567]) ).
fof(f42197,plain,
( ~ spl164_8
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_6 ),
inference(avatar_split_clause,[],[f42188,f42103,f40673,f38101,f36570,f36565,f36560,f42111]) ).
fof(f42198,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_8 ),
inference(resolution,[],[f42113,f35749]) ).
fof(f42209,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_8 ),
inference(duplicate_literal_removal,[],[f42198]) ).
fof(f42218,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl164_4
| spl164_8 ),
inference(forward_subsumption_resolution,[],[f42209,f38103]) ).
fof(f42225,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_4
| spl164_8 ),
inference(forward_subsumption_resolution,[],[f42218,f36562]) ).
fof(f42227,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_3
| ~ spl164_4
| spl164_8 ),
inference(forward_subsumption_resolution,[],[f42225,f36572]) ).
fof(f42228,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_8 ),
inference(forward_subsumption_resolution,[],[f42227,f36567]) ).
fof(f42261,definition,
( spl164_10
<=> r3_lattices(sK18,sK19,sK19) ),
introduced(definition,[new_symbols(definition,[spl164_10])],[avatar_definition]) ).
fof(f42263,plain,
( ~ r3_lattices(sK18,sK19,sK19)
| spl164_10 ),
inference(avatar_component_clause,[],[f42261]) ).
fof(f42264,plain,
( ~ spl164_10
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_8 ),
inference(avatar_split_clause,[],[f42228,f42111,f38101,f36570,f36565,f36560,f42261]) ).
fof(f42271,plain,
( ~ r2_hidden(sK19,k2_filter_0(sK18,sK19))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_10 ),
inference(resolution,[],[f42263,f35871]) ).
fof(f42284,plain,
( ~ r2_hidden(sK19,k2_filter_0(sK18,sK19))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_10 ),
inference(duplicate_literal_removal,[],[f42271]) ).
fof(f42292,plain,
( ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_2
| ~ spl164_3
| spl164_10 ),
inference(forward_subsumption_resolution,[],[f42284,f37989]) ).
fof(f42299,plain,
( v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_10 ),
inference(forward_subsumption_resolution,[],[f42292,f38103]) ).
fof(f42306,plain,
( ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_10 ),
inference(forward_subsumption_resolution,[],[f42299,f36562]) ).
fof(f42312,plain,
( ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_10 ),
inference(forward_subsumption_resolution,[],[f42306,f36572]) ).
fof(f42315,plain,
( $false
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_10 ),
inference(forward_subsumption_resolution,[],[f42312,f36567]) ).
fof(f42316,plain,
( spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_10 ),
inference(avatar_contradiction_clause,[],[f42315]) ).
fof(f42322,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ m2_filter_2(k18_filter_2(sK18,sK19),sK18)
| ~ m1_subset_1(sK20,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_7 ),
inference(resolution,[],[f42109,f35739]) ).
fof(f42347,plain,
( ~ r2_hidden(sK19,k18_filter_2(sK18,sK19))
| ~ m1_subset_1(sK20,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_7 ),
inference(forward_subsumption_resolution,[],[f42322,f35632]) ).
fof(f42359,plain,
( ~ m1_subset_1(sK20,u1_struct_0(sK18))
| ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_7
| ~ spl164_8 ),
inference(forward_subsumption_resolution,[],[f42347,f42112]) ).
fof(f42364,plain,
( ~ m1_subset_1(sK19,u1_struct_0(sK18))
| v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(forward_subsumption_resolution,[],[f42359,f40675]) ).
fof(f42368,plain,
( v3_struct_0(sK18)
| ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| ~ spl164_4
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(forward_subsumption_resolution,[],[f42364,f38103]) ).
fof(f42371,plain,
( ~ v10_lattices(sK18)
| ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_4
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(forward_subsumption_resolution,[],[f42368,f36562]) ).
fof(f42373,plain,
( ~ l3_lattices(sK18)
| spl164_1
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(forward_subsumption_resolution,[],[f42371,f36572]) ).
fof(f42374,plain,
( $false
| spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(forward_subsumption_resolution,[],[f42373,f36567]) ).
fof(f42375,plain,
( spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(avatar_contradiction_clause,[],[f42374]) ).
cnf(s1,plain,
~ spl164_1,
inference(sat_conversion,[],[f36563]) ).
cnf(s2,plain,
spl164_2,
inference(sat_conversion,[],[f36568]) ).
cnf(s3,plain,
spl164_3,
inference(sat_conversion,[],[f36573]) ).
cnf(s4,plain,
spl164_4,
inference(sat_conversion,[],[f38104]) ).
cnf(s5,plain,
spl164_5,
inference(sat_conversion,[],[f40676]) ).
cnf(s6,plain,
( ~ spl164_6
| ~ spl164_7
| ~ spl164_8 ),
inference(sat_conversion,[],[f42114]) ).
cnf(s8,plain,
( spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_6
| ~ spl164_8 ),
inference(sat_conversion,[],[f42197]) ).
cnf(s9,plain,
( spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_8
| ~ spl164_10 ),
inference(sat_conversion,[],[f42264]) ).
cnf(s11,plain,
( spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| spl164_10 ),
inference(sat_conversion,[],[f42316]) ).
cnf(s12,plain,
( spl164_1
| ~ spl164_2
| ~ spl164_3
| ~ spl164_4
| ~ spl164_5
| spl164_7
| ~ spl164_8 ),
inference(sat_conversion,[],[f42375]) ).
cnf(s13,plain,
spl164_10,
inference(rat,[],[s11,s2,s4,s3,s1]) ).
cnf(s14,plain,
spl164_8,
inference(rat,[],[s9,s13,s2,s4,s3,s1]) ).
cnf(s15,plain,
spl164_6,
inference(rat,[],[s8,s14,s2,s5,s4,s3,s1]) ).
cnf(s16,plain,
spl164_7,
inference(rat,[],[s12,s1,s2,s5,s4,s3,s14]) ).
cnf(s17,plain,
$false,
inference(rat,[],[s6,s14,s16,s15]) ).
fof(f42376,plain,
$false,
inference(avatar_sat_refutation,[],[s17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT305+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.19/0.46 % Computer : n011.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 27 14:25:51 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.19/0.50 Running first-order theorem proving
% 0.23/0.50 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
% 19.31/6.59 % (2475130)Detected formulas, will run a generic FOF schedule.
% 19.31/6.59 % (2475136)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=2689556433:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2970 on theBenchmark for (2970ds/134677Mi)
% 19.31/6.59 % (2475140)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3730760619:s2a=on:i=139:gtg=position_2970 on theBenchmark for (2970ds/139Mi)
% 19.31/6.59 % (2475137)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=1862619398:i=141695:sd=1:nm=32:gsp=on:ss=included_2970 on theBenchmark for (2970ds/141695Mi)
% 19.31/6.59 % (2475135)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=3604279610:i=141193_2970 on theBenchmark for (2970ds/141193Mi)
% 19.31/6.59 % (2475141)dis-21_1_sil=8000:lcm=predicate:random_seed=3130523017:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2970 on theBenchmark for (2970ds/129Mi)
% 19.31/6.59 % (2475138)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2289711622:i=109:sd=1:ins=1:gsp=on:ss=axioms_2970 on theBenchmark for (2970ds/109Mi)
% 19.31/6.59 % (2475140)Instruction limit reached!
% 19.31/6.59 % (2475140)------------------------------
% 19.31/6.59 % (2475140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475140)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475140)Termination reason: Instruction limit
% 19.31/6.59 % (2475140)Termination phase: Property scanning
% 19.31/6.59 % (2475140)Time elapsed: 0.066 s
% 19.31/6.59 % (2475140)Peak memory usage: 137 MB
% 19.31/6.59 % (2475140)Instructions burned: 140 (million)
% 19.31/6.59 % (2475139)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1680540721:i=119:av=off:ss=axioms_2970 on theBenchmark for (2970ds/119Mi)
% 19.31/6.59 % (2475138)Instruction limit reached!
% 19.31/6.59 % (2475138)------------------------------
% 19.31/6.59 % (2475138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475138)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475138)Termination reason: Instruction limit
% 19.31/6.59 % (2475138)Termination phase: SInE selection
% 19.31/6.59 % (2475138)Time elapsed: 0.114 s
% 19.31/6.59 % (2475138)Peak memory usage: 136 MB
% 19.31/6.59 % (2475138)Instructions burned: 109 (million)
% 19.31/6.59 % (2475141)Instruction limit reached!
% 19.31/6.59 % (2475141)------------------------------
% 19.31/6.59 % (2475141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475141)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475141)Termination reason: Instruction limit
% 19.31/6.59 % (2475141)Termination phase: SInE selection
% 19.31/6.59 % (2475141)Time elapsed: 0.131 s
% 19.31/6.59 % (2475141)Peak memory usage: 136 MB
% 19.31/6.59 % (2475141)Instructions burned: 132 (million)
% 19.31/6.59 % (2475139)Instruction limit reached!
% 19.31/6.59 % (2475139)------------------------------
% 19.31/6.59 % (2475139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475139)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475139)Termination reason: Instruction limit
% 19.31/6.59 % (2475139)Termination phase: SInE selection
% 19.31/6.59 % (2475139)Time elapsed: 0.131 s
% 19.31/6.59 % (2475139)Peak memory usage: 136 MB
% 19.31/6.59 % (2475139)Instructions burned: 119 (million)
% 19.31/6.59 % (2475148)lrs+10_1_sil=8000:sp=occurrence:random_seed=2787754322:i=285:sd=3:ss=axioms:sgt=8_2967 on theBenchmark for (2967ds/285Mi)
% 19.31/6.59 % (2475151)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1181855809:i=325:sd=1:ss=axioms:sgt=32_2966 on theBenchmark for (2966ds/325Mi)
% 19.31/6.59 % (2475150)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2866827216:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2966 on theBenchmark for (2966ds/157Mi)
% 19.31/6.59 % (2475152)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=2525839679:s2a=on:i=248:s2at=1.23:gtg=position_2966 on theBenchmark for (2966ds/248Mi)
% 19.31/6.59 % (2475150)Instruction limit reached!
% 19.31/6.59 % (2475150)------------------------------
% 19.31/6.59 % (2475150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475150)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475150)Termination reason: Instruction limit
% 19.31/6.59 % (2475150)Termination phase: Property scanning
% 19.31/6.59 % (2475150)Time elapsed: 0.134 s
% 19.31/6.59 % (2475150)Peak memory usage: 136 MB
% 19.31/6.59 % (2475150)Instructions burned: 158 (million)
% 19.31/6.59 % (2475148)Instruction limit reached!
% 19.31/6.59 % (2475148)------------------------------
% 19.31/6.59 % (2475148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475148)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475148)Termination reason: Instruction limit
% 19.31/6.59 % (2475148)Termination phase: Saturation
% 19.31/6.59 % (2475148)Time elapsed: 0.335 s
% 19.31/6.59 % (2475148)Peak memory usage: 141 MB
% 19.31/6.59 % (2475148)Instructions burned: 288 (million)
% 19.31/6.59 % (2475151)Refutation not found, incomplete strategy
% 19.31/6.59 % (2475151)------------------------------
% 19.31/6.59 % (2475151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475151)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475151)Termination reason: Refutation not found, incomplete strategy
% 19.31/6.59 % (2475151)Time elapsed: 0.288 s
% 19.31/6.59 % (2475151)Peak memory usage: 142 MB
% 19.31/6.59 % (2475151)Instructions burned: 291 (million)
% 19.31/6.59 % (2475152)Instruction limit reached!
% 19.31/6.59 % (2475152)------------------------------
% 19.31/6.59 % (2475152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475152)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475152)Termination reason: Instruction limit
% 19.31/6.59 % (2475152)Termination phase: Property scanning
% 19.31/6.59 % (2475152)Time elapsed: 0.202 s
% 19.31/6.59 % (2475152)Peak memory usage: 136 MB
% 19.31/6.59 % (2475152)Instructions burned: 249 (million)
% 19.31/6.59 % (2475157)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=493107978:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2962 on theBenchmark for (2962ds/294Mi)
% 19.31/6.59 % (2475158)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1987137274:i=2350_2960 on theBenchmark for (2960ds/2350Mi)
% 19.31/6.59 % (2475159)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3246226813:cts=off:i=113:fsr=off:ss=included:sgt=4_2960 on theBenchmark for (2960ds/113Mi)
% 19.31/6.59 % (2475157)Instruction limit reached!
% 19.31/6.59 % (2475157)------------------------------
% 19.31/6.59 % (2475157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475157)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475157)Termination reason: Instruction limit
% 19.31/6.59 % (2475157)Termination phase: SInE selection
% 19.31/6.59 % (2475157)Time elapsed: 0.179 s
% 19.31/6.59 % (2475157)Peak memory usage: 136 MB
% 19.31/6.59 % (2475157)Instructions burned: 294 (million)
% 19.31/6.59 % (2475159)Instruction limit reached!
% 19.31/6.59 % (2475159)------------------------------
% 19.31/6.59 % (2475159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475159)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475159)Termination reason: Instruction limit
% 19.31/6.59 % (2475159)Termination phase: SInE selection
% 19.31/6.59 % (2475159)Time elapsed: 0.118 s
% 19.31/6.59 % (2475159)Peak memory usage: 136 MB
% 19.31/6.59 % (2475159)Instructions burned: 113 (million)
% 19.31/6.59 % (2475151)------------------------------
% 19.31/6.59 % (2475151)------------------------------
% 19.31/6.59 % (2475163)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3376059978:i=127:av=off:fsr=off:sup=off_2957 on theBenchmark for (2957ds/127Mi)
% 19.31/6.59 % (2475165)lrs+10_1_sil=8000:sp=occurrence:random_seed=3168155110:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2957 on theBenchmark for (2957ds/907Mi)
% 19.31/6.59 % (2475163)Instruction limit reached!
% 19.31/6.59 % (2475163)------------------------------
% 19.31/6.59 % (2475163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475163)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475163)Termination reason: Instruction limit
% 19.31/6.59 % (2475163)Termination phase: Preprocessing 1
% 19.31/6.59 % (2475163)Time elapsed: 0.096 s
% 19.31/6.59 % (2475163)Peak memory usage: 137 MB
% 19.31/6.59 % (2475163)Instructions burned: 127 (million)
% 19.31/6.59 % (2475164)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2235917680:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2957 on theBenchmark for (2957ds/114Mi)
% 19.31/6.59 % (2475164)Instruction limit reached!
% 19.31/6.59 % (2475164)------------------------------
% 19.31/6.59 % (2475164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475164)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475164)Termination reason: Instruction limit
% 19.31/6.59 % (2475164)Termination phase: Property scanning
% 19.31/6.59 % (2475164)Time elapsed: 0.100 s
% 19.31/6.59 % (2475164)Peak memory usage: 137 MB
% 19.31/6.59 % (2475164)Instructions burned: 114 (million)
% 19.31/6.59 % (2475169)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3984921812:i=437:sd=1:aac=none:ss=included_2955 on theBenchmark for (2955ds/437Mi)
% 19.31/6.59 % (2475170)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2157991068:i=5202:ss=axioms:sgt=16_2954 on theBenchmark for (2954ds/5202Mi)
% 19.31/6.59 % (2475169)Refutation not found, incomplete strategy
% 19.31/6.59 % (2475169)------------------------------
% 19.31/6.59 % (2475169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475169)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475169)Termination reason: Refutation not found, incomplete strategy
% 19.31/6.59 % (2475169)Time elapsed: 0.278 s
% 19.31/6.59 % (2475169)Peak memory usage: 143 MB
% 19.31/6.59 % (2475169)Instructions burned: 319 (million)
% 19.31/6.59 % (2475137)First to succeed.
% 19.31/6.59 % (2475137)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2475130"
% 19.31/6.59 % (2475165)Instruction limit reached!
% 19.31/6.59 % (2475165)------------------------------
% 19.31/6.59 % (2475165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.31/6.59 % (2475165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.31/6.59 % (2475165)CaDiCaL version: 2.1.3
% 19.31/6.59 % (2475165)Termination reason: Instruction limit
% 19.31/6.59 % (2475165)Termination phase: Property scanning
% 19.31/6.59 % (2475165)Time elapsed: 0.680 s
% 19.31/6.59 % (2475165)Peak memory usage: 156 MB
% 19.31/6.59 % (2475165)Instructions burned: 907 (million)
% 19.31/6.59 % (2475169)------------------------------
% 19.31/6.59 % (2475169)------------------------------
% 19.31/6.59 % (2475137)Refutation found. Thanks to Tanya!
% 19.31/6.59 % SZS status Theorem for theBenchmark
% 19.31/6.59 % SZS output start Proof for theBenchmark
% See solution above
% 20.12/6.83 % (2475137)------------------------------
% 20.12/6.83 % (2475137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.12/6.83 % (2475137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.12/6.83 % (2475137)CaDiCaL version: 2.1.3
% 20.12/6.83 % (2475137)Termination reason: Refutation
% 20.12/6.83 % (2475137)Time elapsed: 1.912 s
% 20.12/6.83 % (2475137)Peak memory usage: 209 MB
% 20.12/6.83 % (2475137)Instructions burned: 2726 (million)
% 20.12/6.83 % (2475137)------------------------------
% 20.12/6.83 % (2475137)------------------------------
% 20.12/6.83 % (2475130)Success in time 5.319 s
% 20.12/6.83 % Vampire exiting
%------------------------------------------------------------------------------