%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT303+3 : 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 : n008.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:43 AM UTC 2026
% Result : Theorem 15.09s 3.68s
% Output : Refutation 16.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 26
% Syntax : Number of formulae : 168 ( 29 unt; 14 def)
% Number of atoms : 619 ( 22 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 738 ( 287 ~; 323 |; 84 &)
% ( 23 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 15 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-2 aty)
% Number of variables : 97 ( 0 sgn 93 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2212,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f8587,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
=> v14_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t14_filter_0) ).
fof(f8588,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f8673,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f9363,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/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,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/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f9438,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f13531,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f13610,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
=> v13_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t27_filter_2) ).
fof(f13611,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
=> v13_lattices(X0) ) ) ),
inference(negated_conjecture,[status(cth)],[f13610]) ).
fof(f13635,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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)) ) ),
inference(pure_predicate_removal,[],[f9363]) ).
fof(f13696,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13531]) ).
fof(f13697,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13696]) ).
fof(f13821,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13600]) ).
fof(f13822,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13821]) ).
fof(f13841,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(X0)
& m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13611]) ).
fof(f13842,plain,
? [X0] :
( ? [X1] :
( ~ v13_lattices(X0)
& m2_filter_2(k6_domain_1(u1_struct_0(X0),X1),X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13841]) ).
fof(f13867,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8673]) ).
fof(f13868,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13867]) ).
fof(f13869,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8588]) ).
fof(f13870,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13869]) ).
fof(f13949,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9438]) ).
fof(f13950,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13949]) ).
fof(f13957,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,[],[f9391]) ).
fof(f13958,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,[],[f13957]) ).
fof(f13970,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f13973,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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,[],[f13635]) ).
fof(f13974,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_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,[],[f13973]) ).
fof(f13975,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f13976,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13975]) ).
fof(f14079,plain,
! [X0] :
( ! [X1] :
( v14_lattices(X0)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8587]) ).
fof(f14080,plain,
! [X0] :
( ! [X1] :
( v14_lattices(X0)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14079]) ).
fof(f14173,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2212]) ).
fof(f14174,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f14173]) ).
fof(f14178,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13697]) ).
fof(f14198,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13822]) ).
fof(f14204,plain,
( ~ v13_lattices(sK16)
& m2_filter_2(k6_domain_1(u1_struct_0(sK16),sK17),sK16)
& m1_subset_1(sK17,u1_struct_0(sK16))
& ~ v3_struct_0(sK16)
& v10_lattices(sK16)
& l3_lattices(sK16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X0,sK16),skolemize(X1,sK17)],[f13842]) ).
fof(f14237,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13950]) ).
fof(f14311,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14178]) ).
fof(f14414,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14198]) ).
fof(f14453,plain,
l3_lattices(sK16),
inference(cnf_transformation,[],[f14204]) ).
fof(f14454,plain,
v10_lattices(sK16),
inference(cnf_transformation,[],[f14204]) ).
fof(f14455,plain,
~ v3_struct_0(sK16),
inference(cnf_transformation,[],[f14204]) ).
fof(f14456,plain,
m1_subset_1(sK17,u1_struct_0(sK16)),
inference(cnf_transformation,[],[f14204]) ).
fof(f14457,plain,
m2_filter_2(k6_domain_1(u1_struct_0(sK16),sK17),sK16),
inference(cnf_transformation,[],[f14204]) ).
fof(f14458,plain,
~ v13_lattices(sK16),
inference(cnf_transformation,[],[f14204]) ).
fof(f14492,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13868]) ).
fof(f14493,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13870]) ).
fof(f14569,plain,
! [X0] :
( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14237]) ).
fof(f14576,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13958]) ).
fof(f14596,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13970]) ).
fof(f14599,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13974]) ).
fof(f14608,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13976]) ).
fof(f14742,plain,
! [X0,X1] :
( v14_lattices(X0)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(X0),X1),X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14080]) ).
fof(f14929,plain,
! [X0,X1] :
( k1_tarski(X1) = k6_domain_1(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f14174]) ).
fof(f15049,definition,
( spl109_1
<=> v13_lattices(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_1])],[avatar_definition]) ).
fof(f15051,plain,
( ~ v13_lattices(sK16)
| spl109_1 ),
inference(avatar_component_clause,[],[f15049]) ).
fof(f15052,plain,
~ spl109_1,
inference(avatar_split_clause,[],[f14458,f15049]) ).
fof(f15054,definition,
( spl109_2
<=> v3_struct_0(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_2])],[avatar_definition]) ).
fof(f15056,plain,
( ~ v3_struct_0(sK16)
| spl109_2 ),
inference(avatar_component_clause,[],[f15054]) ).
fof(f15057,plain,
~ spl109_2,
inference(avatar_split_clause,[],[f14455,f15054]) ).
fof(f15062,plain,
( ~ v14_lattices(k1_lattice2(sK16))
| v3_struct_0(sK16)
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1 ),
inference(resolution,[],[f15051,f14569]) ).
fof(f15063,plain,
( ~ v14_lattices(k1_lattice2(sK16))
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_1
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15062,f15056]) ).
fof(f15068,plain,
( ~ v14_lattices(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_1
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15063,f14454]) ).
fof(f15073,plain,
( ~ v14_lattices(k1_lattice2(sK16))
| spl109_1
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15068,f14453]) ).
fof(f15159,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK16))
| ~ m2_filter_2(X0,sK16)
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16) )
| spl109_2 ),
inference(resolution,[],[f15056,f14414]) ).
fof(f15215,plain,
( m1_filter_0(u1_struct_0(sK16),sK16)
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_2 ),
inference(resolution,[],[f15056,f14493]) ).
fof(f15268,plain,
( u1_struct_0(sK16) = u1_struct_0(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_2 ),
inference(resolution,[],[f15056,f14576]) ).
fof(f15292,plain,
( v10_lattices(k1_lattice2(sK16))
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_2 ),
inference(resolution,[],[f15056,f14599]) ).
fof(f15301,plain,
( ~ v3_struct_0(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_2 ),
inference(resolution,[],[f15056,f14608]) ).
fof(f15725,plain,
( ~ v3_struct_0(k1_lattice2(sK16))
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15301,f14453]) ).
fof(f15732,plain,
( v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(sK16)
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15292,f14454]) ).
fof(f15756,plain,
( u1_struct_0(sK16) = u1_struct_0(k1_lattice2(sK16))
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15268,f14453]) ).
fof(f15806,plain,
( m1_filter_0(u1_struct_0(sK16),sK16)
| ~ l3_lattices(sK16)
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15215,f14454]) ).
fof(f15860,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK16))
| ~ m2_filter_2(X0,sK16)
| ~ l3_lattices(sK16) )
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15159,f14454]) ).
fof(f16062,plain,
( v10_lattices(k1_lattice2(sK16))
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15732,f14453]) ).
fof(f16132,plain,
( m1_filter_0(u1_struct_0(sK16),sK16)
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15806,f14453]) ).
fof(f16186,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK16))
| ~ m2_filter_2(X0,sK16) )
| spl109_2 ),
inference(forward_subsumption_resolution,[],[f15860,f14453]) ).
fof(f16383,definition,
( spl109_3
<=> l3_lattices(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_3])],[avatar_definition]) ).
fof(f16385,plain,
( l3_lattices(sK16)
| ~ spl109_3 ),
inference(avatar_component_clause,[],[f16383]) ).
fof(f16386,plain,
spl109_3,
inference(avatar_split_clause,[],[f14453,f16383]) ).
fof(f16388,definition,
( spl109_4
<=> v10_lattices(sK16) ),
introduced(definition,[new_symbols(definition,[spl109_4])],[avatar_definition]) ).
fof(f16390,plain,
( v10_lattices(sK16)
| ~ spl109_4 ),
inference(avatar_component_clause,[],[f16388]) ).
fof(f16391,plain,
spl109_4,
inference(avatar_split_clause,[],[f14454,f16388]) ).
fof(f16393,definition,
( spl109_5
<=> m2_filter_2(k6_domain_1(u1_struct_0(sK16),sK17),sK16) ),
introduced(definition,[new_symbols(definition,[spl109_5])],[avatar_definition]) ).
fof(f16395,plain,
( m2_filter_2(k6_domain_1(u1_struct_0(sK16),sK17),sK16)
| ~ spl109_5 ),
inference(avatar_component_clause,[],[f16393]) ).
fof(f16396,plain,
spl109_5,
inference(avatar_split_clause,[],[f14457,f16393]) ).
fof(f16418,plain,
( m2_filter_2(k1_tarski(sK17),sK16)
| v1_xboole_0(u1_struct_0(sK16))
| ~ m1_subset_1(sK17,u1_struct_0(sK16))
| ~ spl109_5 ),
inference(superposition,[],[f16395,f14929]) ).
fof(f16419,plain,
( m2_filter_2(k1_tarski(sK17),sK16)
| v1_xboole_0(u1_struct_0(sK16))
| ~ spl109_5 ),
inference(forward_subsumption_resolution,[],[f16418,f14456]) ).
fof(f16973,definition,
( spl109_6
<=> m1_subset_1(sK17,u1_struct_0(sK16)) ),
introduced(definition,[new_symbols(definition,[spl109_6])],[avatar_definition]) ).
fof(f16975,plain,
( m1_subset_1(sK17,u1_struct_0(sK16))
| ~ spl109_6 ),
inference(avatar_component_clause,[],[f16973]) ).
fof(f16976,plain,
spl109_6,
inference(avatar_split_clause,[],[f14456,f16973]) ).
fof(f17291,plain,
( k6_domain_1(u1_struct_0(sK16),sK17) = k1_tarski(sK17)
| v1_xboole_0(u1_struct_0(sK16))
| ~ spl109_6 ),
inference(resolution,[],[f16975,f14929]) ).
fof(f18235,plain,
( l3_lattices(k1_lattice2(sK16))
| ~ spl109_3 ),
inference(resolution,[],[f16385,f14596]) ).
fof(f21173,definition,
( spl109_25
<=> u1_struct_0(sK16) = u1_struct_0(k1_lattice2(sK16)) ),
introduced(definition,[new_symbols(definition,[spl109_25])],[avatar_definition]) ).
fof(f21175,plain,
( u1_struct_0(sK16) = u1_struct_0(k1_lattice2(sK16))
| ~ spl109_25 ),
inference(avatar_component_clause,[],[f21173]) ).
fof(f21176,plain,
( spl109_25
| spl109_2 ),
inference(avatar_split_clause,[],[f15756,f15054,f21173]) ).
fof(f21799,definition,
( spl109_30
<=> l3_lattices(k1_lattice2(sK16)) ),
introduced(definition,[new_symbols(definition,[spl109_30])],[avatar_definition]) ).
fof(f21801,plain,
( l3_lattices(k1_lattice2(sK16))
| ~ spl109_30 ),
inference(avatar_component_clause,[],[f21799]) ).
fof(f21802,plain,
( spl109_30
| ~ spl109_3 ),
inference(avatar_split_clause,[],[f18235,f16383,f21799]) ).
fof(f24834,definition,
( spl109_33
<=> m1_filter_0(u1_struct_0(sK16),sK16) ),
introduced(definition,[new_symbols(definition,[spl109_33])],[avatar_definition]) ).
fof(f24836,plain,
( m1_filter_0(u1_struct_0(sK16),sK16)
| ~ spl109_33 ),
inference(avatar_component_clause,[],[f24834]) ).
fof(f24837,plain,
( spl109_33
| spl109_2 ),
inference(avatar_split_clause,[],[f16132,f15054,f24834]) ).
fof(f24850,plain,
( ~ v1_xboole_0(u1_struct_0(sK16))
| v3_struct_0(sK16)
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| ~ spl109_33 ),
inference(resolution,[],[f24836,f14492]) ).
fof(f24894,plain,
( ~ v1_xboole_0(u1_struct_0(sK16))
| ~ v10_lattices(sK16)
| ~ l3_lattices(sK16)
| spl109_2
| ~ spl109_33 ),
inference(forward_subsumption_resolution,[],[f24850,f15056]) ).
fof(f24922,plain,
( ~ v1_xboole_0(u1_struct_0(sK16))
| ~ l3_lattices(sK16)
| spl109_2
| ~ spl109_4
| ~ spl109_33 ),
inference(forward_subsumption_resolution,[],[f24894,f16390]) ).
fof(f24950,plain,
( ~ v1_xboole_0(u1_struct_0(sK16))
| spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_33 ),
inference(forward_subsumption_resolution,[],[f24922,f16385]) ).
fof(f24965,plain,
( m2_filter_2(k1_tarski(sK17),sK16)
| spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_5
| ~ spl109_33 ),
inference(backward_subsumption_resolution,[],[f16419,f24950]) ).
fof(f24970,plain,
( k6_domain_1(u1_struct_0(sK16),sK17) = k1_tarski(sK17)
| spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_6
| ~ spl109_33 ),
inference(backward_subsumption_resolution,[],[f17291,f24950]) ).
fof(f24983,definition,
( spl109_34
<=> m2_filter_2(k1_tarski(sK17),sK16) ),
introduced(definition,[new_symbols(definition,[spl109_34])],[avatar_definition]) ).
fof(f24985,plain,
( m2_filter_2(k1_tarski(sK17),sK16)
| ~ spl109_34 ),
inference(avatar_component_clause,[],[f24983]) ).
fof(f24986,plain,
( spl109_34
| spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_5
| ~ spl109_33 ),
inference(avatar_split_clause,[],[f24965,f24834,f16393,f16388,f16383,f15054,f24983]) ).
fof(f25585,definition,
( spl109_40
<=> ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK16))
| ~ m2_filter_2(X0,sK16) ) ),
introduced(definition,[new_symbols(definition,[spl109_40])],[avatar_definition]) ).
fof(f25586,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK16))
| ~ m2_filter_2(X0,sK16) )
| ~ spl109_40 ),
inference(avatar_component_clause,[],[f25585]) ).
fof(f25587,plain,
( spl109_40
| spl109_2 ),
inference(avatar_split_clause,[],[f16186,f15054,f25585]) ).
fof(f25590,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK16)
| m1_filter_0(X0,k1_lattice2(sK16))
| v3_struct_0(k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| ~ spl109_40 ),
inference(resolution,[],[f25586,f14311]) ).
fof(f25598,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK16)
| m1_filter_0(X0,k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_2
| ~ spl109_40 ),
inference(forward_subsumption_resolution,[],[f25590,f15725]) ).
fof(f25603,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK16)
| m1_filter_0(X0,k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_2
| ~ spl109_40 ),
inference(forward_subsumption_resolution,[],[f25598,f16062]) ).
fof(f25606,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK16)
| m1_filter_0(X0,k1_lattice2(sK16)) )
| spl109_2
| ~ spl109_30
| ~ spl109_40 ),
inference(forward_subsumption_resolution,[],[f25603,f21801]) ).
fof(f25613,definition,
( spl109_41
<=> ! [X0] :
( ~ m2_filter_2(X0,sK16)
| m1_filter_0(X0,k1_lattice2(sK16)) ) ),
introduced(definition,[new_symbols(definition,[spl109_41])],[avatar_definition]) ).
fof(f25614,plain,
( ! [X0] :
( m1_filter_0(X0,k1_lattice2(sK16))
| ~ m2_filter_2(X0,sK16) )
| ~ spl109_41 ),
inference(avatar_component_clause,[],[f25613]) ).
fof(f25615,plain,
( spl109_41
| spl109_2
| ~ spl109_30
| ~ spl109_40 ),
inference(avatar_split_clause,[],[f25606,f25585,f21799,f15054,f25613]) ).
fof(f25655,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK16)),X0),sK16)
| v14_lattices(k1_lattice2(sK16))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK16)))
| v3_struct_0(k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| ~ spl109_41 ),
inference(resolution,[],[f25614,f14742]) ).
fof(f25660,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK16)),X0),sK16)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK16)))
| v3_struct_0(k1_lattice2(sK16))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_1
| spl109_2
| ~ spl109_41 ),
inference(forward_subsumption_resolution,[],[f25655,f15073]) ).
fof(f25698,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK16)),X0),sK16)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK16)))
| ~ v10_lattices(k1_lattice2(sK16))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_1
| spl109_2
| ~ spl109_41 ),
inference(forward_subsumption_resolution,[],[f25660,f15725]) ).
fof(f25734,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK16)),X0),sK16)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK16)))
| ~ l3_lattices(k1_lattice2(sK16)) )
| spl109_1
| spl109_2
| ~ spl109_41 ),
inference(forward_subsumption_resolution,[],[f25698,f16062]) ).
fof(f25770,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK16)),X0),sK16)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK16))) )
| spl109_1
| spl109_2
| ~ spl109_30
| ~ spl109_41 ),
inference(forward_subsumption_resolution,[],[f25734,f21801]) ).
fof(f25791,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(sK16),X0),sK16)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK16))) )
| spl109_1
| spl109_2
| ~ spl109_25
| ~ spl109_30
| ~ spl109_41 ),
inference(forward_demodulation,[],[f25770,f21175]) ).
fof(f25800,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK16))
| ~ m2_filter_2(k6_domain_1(u1_struct_0(sK16),X0),sK16) )
| spl109_1
| spl109_2
| ~ spl109_25
| ~ spl109_30
| ~ spl109_41 ),
inference(forward_demodulation,[],[f25791,f21175]) ).
fof(f32679,definition,
( spl109_62
<=> k6_domain_1(u1_struct_0(sK16),sK17) = k1_tarski(sK17) ),
introduced(definition,[new_symbols(definition,[spl109_62])],[avatar_definition]) ).
fof(f32681,plain,
( k6_domain_1(u1_struct_0(sK16),sK17) = k1_tarski(sK17)
| ~ spl109_62 ),
inference(avatar_component_clause,[],[f32679]) ).
fof(f32682,plain,
( spl109_62
| spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_6
| ~ spl109_33 ),
inference(avatar_split_clause,[],[f24970,f24834,f16973,f16388,f16383,f15054,f32679]) ).
fof(f33609,definition,
( spl109_73
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK16))
| ~ m2_filter_2(k6_domain_1(u1_struct_0(sK16),X0),sK16) ) ),
introduced(definition,[new_symbols(definition,[spl109_73])],[avatar_definition]) ).
fof(f33610,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(sK16),X0),sK16)
| ~ m1_subset_1(X0,u1_struct_0(sK16)) )
| ~ spl109_73 ),
inference(avatar_component_clause,[],[f33609]) ).
fof(f33611,plain,
( spl109_73
| spl109_1
| spl109_2
| ~ spl109_25
| ~ spl109_30
| ~ spl109_41 ),
inference(avatar_split_clause,[],[f25800,f25613,f21799,f21173,f15054,f15049,f33609]) ).
fof(f38381,plain,
( ~ m2_filter_2(k1_tarski(sK17),sK16)
| ~ m1_subset_1(sK17,u1_struct_0(sK16))
| ~ spl109_62
| ~ spl109_73 ),
inference(superposition,[],[f33610,f32681]) ).
fof(f38385,plain,
( ~ m1_subset_1(sK17,u1_struct_0(sK16))
| ~ spl109_34
| ~ spl109_62
| ~ spl109_73 ),
inference(forward_subsumption_resolution,[],[f38381,f24985]) ).
fof(f38422,plain,
( $false
| ~ spl109_6
| ~ spl109_34
| ~ spl109_62
| ~ spl109_73 ),
inference(forward_subsumption_resolution,[],[f38385,f16975]) ).
fof(f38423,plain,
( ~ spl109_6
| ~ spl109_34
| ~ spl109_62
| ~ spl109_73 ),
inference(avatar_contradiction_clause,[],[f38422]) ).
cnf(s1,plain,
~ spl109_1,
inference(sat_conversion,[],[f15052]) ).
cnf(s2,plain,
~ spl109_2,
inference(sat_conversion,[],[f15057]) ).
cnf(s3,plain,
spl109_3,
inference(sat_conversion,[],[f16386]) ).
cnf(s4,plain,
spl109_4,
inference(sat_conversion,[],[f16391]) ).
cnf(s5,plain,
spl109_5,
inference(sat_conversion,[],[f16396]) ).
cnf(s6,plain,
spl109_6,
inference(sat_conversion,[],[f16976]) ).
cnf(s25,plain,
( spl109_2
| spl109_25 ),
inference(sat_conversion,[],[f21176]) ).
cnf(s30,plain,
( ~ spl109_3
| spl109_30 ),
inference(sat_conversion,[],[f21802]) ).
cnf(s33,plain,
( spl109_2
| spl109_33 ),
inference(sat_conversion,[],[f24837]) ).
cnf(s34,plain,
( spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_5
| ~ spl109_33
| spl109_34 ),
inference(sat_conversion,[],[f24986]) ).
cnf(s40,plain,
( spl109_2
| spl109_40 ),
inference(sat_conversion,[],[f25587]) ).
cnf(s41,plain,
( spl109_2
| ~ spl109_30
| ~ spl109_40
| spl109_41 ),
inference(sat_conversion,[],[f25615]) ).
cnf(s92,plain,
( spl109_2
| ~ spl109_3
| ~ spl109_4
| ~ spl109_6
| ~ spl109_33
| spl109_62 ),
inference(sat_conversion,[],[f32682]) ).
cnf(s103,plain,
( spl109_1
| spl109_2
| ~ spl109_25
| ~ spl109_30
| ~ spl109_41
| spl109_73 ),
inference(sat_conversion,[],[f33611]) ).
cnf(s131,plain,
( ~ spl109_6
| ~ spl109_34
| ~ spl109_62
| ~ spl109_73 ),
inference(sat_conversion,[],[f38423]) ).
cnf(s132,plain,
spl109_30,
inference(rat,[],[s30,s3]) ).
cnf(s159,plain,
spl109_40,
inference(rat,[],[s40,s2]) ).
cnf(s162,plain,
spl109_33,
inference(rat,[],[s33,s2]) ).
cnf(s166,plain,
spl109_25,
inference(rat,[],[s25,s2]) ).
cnf(s182,plain,
spl109_41,
inference(rat,[],[s41,s2,s132,s159]) ).
cnf(s183,plain,
spl109_62,
inference(rat,[],[s92,s2,s3,s6,s4,s162]) ).
cnf(s185,plain,
spl109_34,
inference(rat,[],[s34,s2,s3,s5,s4,s162]) ).
cnf(s214,plain,
~ spl109_73,
inference(rat,[],[s131,s183,s6,s185]) ).
cnf(s221,plain,
spl109_1,
inference(rat,[],[s103,s166,s182,s132,s2,s214]) ).
cnf(s223,plain,
$false,
inference(rat,[],[s1,s221]) ).
fof(f38509,plain,
$false,
inference(avatar_sat_refutation,[],[s223]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT303+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 14:24:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 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
% 15.09/3.62 % (1273444)Detected formulas, will run a generic FOF schedule.
% 15.09/3.62 % (1273453)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4266923164:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 15.09/3.62 % (1273449)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=4246491968:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 15.09/3.62 % (1273454)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3442302713:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 15.09/3.62 % (1273452)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2908882838:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 15.09/3.62 % (1273450)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=4171334402:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 15.09/3.62 % (1273451)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=2785989530:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 15.09/3.62 % (1273455)dis-21_1_sil=8000:lcm=predicate:random_seed=2155052381:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 15.09/3.62 % (1273453)Instruction limit reached!
% 15.09/3.62 % (1273453)------------------------------
% 15.09/3.62 % (1273453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.62 % (1273453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.62 % (1273453)CaDiCaL version: 2.1.3
% 15.09/3.62 % (1273453)Termination reason: Instruction limit
% 15.09/3.62 % (1273453)Termination phase: Property scanning
% 15.09/3.62 % (1273453)Time elapsed: 0.055 s
% 15.09/3.62 % (1273453)Peak memory usage: 106 MB
% 15.09/3.62 % (1273453)Instructions burned: 121 (million)
% 15.09/3.62 % (1273454)Instruction limit reached!
% 15.09/3.62 % (1273454)------------------------------
% 15.09/3.62 % (1273454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.62 % (1273454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.62 % (1273454)CaDiCaL version: 2.1.3
% 15.09/3.62 % (1273454)Termination reason: Instruction limit
% 15.09/3.62 % (1273454)Termination phase: Property scanning
% 15.09/3.62 % (1273454)Time elapsed: 0.059 s
% 15.09/3.62 % (1273454)Peak memory usage: 102 MB
% 15.09/3.62 % (1273454)Instructions burned: 140 (million)
% 15.09/3.62 % (1273452)Refutation not found, incomplete strategy
% 15.09/3.62 % (1273452)------------------------------
% 15.09/3.62 % (1273452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.62 % (1273452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.62 % (1273452)CaDiCaL version: 2.1.3
% 15.09/3.62 % (1273452)Termination reason: Refutation not found, incomplete strategy
% 15.09/3.62 % (1273452)Time elapsed: 0.069 s
% 15.09/3.62 % (1273452)Peak memory usage: 107 MB
% 15.09/3.62 % (1273452)Instructions burned: 83 (million)
% 15.09/3.62 % (1273455)Instruction limit reached!
% 15.09/3.62 % (1273455)------------------------------
% 15.09/3.62 % (1273455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.62 % (1273455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.62 % (1273455)CaDiCaL version: 2.1.3
% 15.09/3.62 % (1273455)Termination reason: Instruction limit
% 15.09/3.62 % (1273455)Termination phase: Preprocessing 1
% 15.09/3.62 % (1273455)Time elapsed: 0.098 s
% 15.09/3.62 % (1273455)Peak memory usage: 104 MB
% 15.09/3.62 % (1273455)Instructions burned: 130 (million)
% 15.09/3.62 % (1273463)lrs+10_1_sil=8000:sp=occurrence:random_seed=1453890188:i=285:sd=3:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/285Mi)
% 15.09/3.62 % (1273464)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2745451423:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 15.09/3.62 % (1273463)Instruction limit reached!
% 15.09/3.62 % (1273463)------------------------------
% 15.09/3.62 % (1273463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.62 % (1273463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.62 % (1273463)CaDiCaL version: 2.1.3
% 15.09/3.62 % (1273463)Termination reason: Instruction limit
% 15.09/3.68 % (1273463)Termination phase: Saturation
% 15.09/3.68 % (1273463)Time elapsed: 0.112 s
% 15.09/3.68 % (1273463)Peak memory usage: 109 MB
% 15.09/3.68 % (1273463)Instructions burned: 287 (million)
% 15.09/3.68 % (1273465)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3917096267:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 15.09/3.68 % (1273464)Instruction limit reached!
% 15.09/3.68 % (1273464)------------------------------
% 15.09/3.68 % (1273464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273464)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273464)Termination reason: Instruction limit
% 15.09/3.68 % (1273464)Termination phase: Property scanning
% 15.09/3.68 % (1273464)Time elapsed: 0.070 s
% 15.09/3.68 % (1273464)Peak memory usage: 102 MB
% 15.09/3.68 % (1273464)Instructions burned: 159 (million)
% 15.09/3.68 % (1273452)------------------------------
% 15.09/3.68 % (1273452)------------------------------
% 15.09/3.68 % (1273465)Refutation not found, incomplete strategy
% 15.09/3.68 % (1273465)------------------------------
% 15.09/3.68 % (1273465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273465)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273465)Termination reason: Refutation not found, incomplete strategy
% 15.09/3.68 % (1273465)Time elapsed: 0.073 s
% 15.09/3.68 % (1273465)Peak memory usage: 107 MB
% 15.09/3.68 % (1273465)Instructions burned: 84 (million)
% 15.09/3.68 % (1273468)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=3094179697:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 15.09/3.68 % (1273470)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4068276400:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 15.09/3.68 % (1273468)Instruction limit reached!
% 15.09/3.68 % (1273468)------------------------------
% 15.09/3.68 % (1273468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273468)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273468)Termination reason: Instruction limit
% 15.09/3.68 % (1273468)Termination phase: SInE selection
% 15.09/3.68 % (1273468)Time elapsed: 0.071 s
% 15.09/3.68 % (1273468)Peak memory usage: 103 MB
% 15.09/3.68 % (1273468)Instructions burned: 249 (million)
% 15.09/3.68 % (1273471)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=218188087:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 15.09/3.68 % (1273465)------------------------------
% 15.09/3.68 % (1273465)------------------------------
% 15.09/3.68 % (1273470)Instruction limit reached!
% 15.09/3.68 % (1273470)------------------------------
% 15.09/3.68 % (1273470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273470)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273470)Termination reason: Instruction limit
% 15.09/3.68 % (1273470)Termination phase: Property scanning
% 15.09/3.68 % (1273470)Time elapsed: 0.179 s
% 15.09/3.68 % (1273470)Peak memory usage: 109 MB
% 15.09/3.68 % (1273470)Instructions burned: 295 (million)
% 15.09/3.68 % (1273474)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=213966568:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 15.09/3.68 % (1273474)Instruction limit reached!
% 15.09/3.68 % (1273474)------------------------------
% 15.09/3.68 % (1273474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273474)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273474)Termination reason: Instruction limit
% 15.09/3.68 % (1273474)Termination phase: Preprocessing 3
% 15.09/3.68 % (1273474)Time elapsed: 0.115 s
% 15.09/3.68 % (1273474)Peak memory usage: 105 MB
% 15.09/3.68 % (1273474)Instructions burned: 114 (million)
% 15.09/3.68 % (1273476)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1820393138:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 15.09/3.68 % (1273478)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3176029477:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 15.09/3.68 % (1273478)Instruction limit reached!
% 15.09/3.68 % (1273478)------------------------------
% 15.09/3.68 % (1273478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273478)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273478)Termination reason: Instruction limit
% 15.09/3.68 % (1273478)Termination phase: Property scanning
% 15.09/3.68 % (1273478)Time elapsed: 0.049 s
% 15.09/3.68 % (1273478)Peak memory usage: 102 MB
% 15.09/3.68 % (1273478)Instructions burned: 115 (million)
% 15.09/3.68 % (1273476)Instruction limit reached!
% 15.09/3.68 % (1273476)------------------------------
% 15.09/3.68 % (1273476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273476)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273476)Termination reason: Instruction limit
% 15.09/3.68 % (1273476)Termination phase: Preprocessing 2
% 15.09/3.68 % (1273476)Time elapsed: 0.099 s
% 15.09/3.68 % (1273476)Peak memory usage: 106 MB
% 15.09/3.68 % (1273476)Instructions burned: 127 (million)
% 15.09/3.68 % (1273480)lrs+10_1_sil=8000:sp=occurrence:random_seed=1338593502:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2984 on theBenchmark for (2984ds/907Mi)
% 15.09/3.68 % (1273482)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4289294716:i=437:sd=1:aac=none:ss=included_2983 on theBenchmark for (2983ds/437Mi)
% 15.09/3.68 % (1273483)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1046869361:i=5202:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/5202Mi)
% 15.09/3.68 % (1273482)Refutation not found, incomplete strategy
% 15.09/3.68 % (1273482)------------------------------
% 15.09/3.68 % (1273482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273482)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273482)Termination reason: Refutation not found, incomplete strategy
% 15.09/3.68 % (1273482)Time elapsed: 0.089 s
% 15.09/3.68 % (1273482)Peak memory usage: 108 MB
% 15.09/3.68 % (1273482)Instructions burned: 119 (million)
% 15.09/3.68 % (1273482)------------------------------
% 15.09/3.68 % (1273482)------------------------------
% 15.09/3.68 % (1273480)Instruction limit reached!
% 15.09/3.68 % (1273480)------------------------------
% 15.09/3.68 % (1273480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273480)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273480)Termination reason: Instruction limit
% 15.09/3.68 % (1273480)Termination phase: Saturation
% 15.09/3.68 % (1273480)Time elapsed: 0.586 s
% 15.09/3.68 % (1273480)Peak memory usage: 120 MB
% 15.09/3.68 % (1273480)Instructions burned: 907 (million)
% 15.09/3.68 % (1273487)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3355045080:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 15.09/3.68 % (1273487)Instruction limit reached!
% 15.09/3.68 % (1273487)------------------------------
% 15.09/3.68 % (1273487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273487)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273487)Termination reason: Instruction limit
% 15.09/3.68 % (1273487)Termination phase: Property scanning
% 15.09/3.68 % (1273487)Time elapsed: 0.097 s
% 15.09/3.68 % (1273487)Peak memory usage: 106 MB
% 15.09/3.68 % (1273487)Instructions burned: 136 (million)
% 15.09/3.68 % (1273489)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1932521075:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 15.09/3.68 % (1273490)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2875193070:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 15.09/3.68 % (1273451)First to succeed.
% 15.09/3.68 % (1273451)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1273444"
% 15.09/3.68 % (1273471)Instruction limit reached!
% 15.09/3.68 % (1273471)------------------------------
% 15.09/3.68 % (1273471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.09/3.68 % (1273471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.09/3.68 % (1273471)CaDiCaL version: 2.1.3
% 15.09/3.68 % (1273471)Termination reason: Instruction limit
% 15.09/3.68 % (1273471)Termination phase: Saturation
% 15.09/3.68 % (1273471)Time elapsed: 1.456 s
% 15.09/3.68 % (1273471)Peak memory usage: 240 MB
% 15.09/3.68 % (1273471)Instructions burned: 2351 (million)
% 15.09/3.68 % (1273451)Refutation found. Thanks to Tanya!
% 15.09/3.68 % SZS status Theorem for theBenchmark
% 15.09/3.68 % SZS output start Proof for theBenchmark
% See solution above
% 16.40/3.88 % (1273451)------------------------------
% 16.40/3.88 % (1273451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.40/3.88 % (1273451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.40/3.88 % (1273451)CaDiCaL version: 2.1.3
% 16.40/3.88 % (1273451)Termination reason: Refutation
% 16.40/3.88 % (1273451)Time elapsed: 1.788 s
% 16.40/3.88 % (1273451)Peak memory usage: 176 MB
% 16.40/3.88 % (1273451)Instructions burned: 4646 (million)
% 16.40/3.88 % (1273451)------------------------------
% 16.40/3.88 % (1273451)------------------------------
% 16.40/3.88 % (1273444)Success in time 2.843 s
% 16.40/3.88 % Vampire exiting
%------------------------------------------------------------------------------