%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT303+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 : n005.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 26.51s 6.59s
% Output : Refutation 27.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 27
% Syntax : Number of formulae : 173 ( 30 unt; 15 def)
% Number of atoms : 629 ( 22 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 746 ( 290 ~; 327 |; 84 &)
% ( 24 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 16 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(f2301,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(f21514,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(f21515,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(f21600,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(f22747,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(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/sandbox/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/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22827,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(f22852,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(f34606,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(f34675,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(f34685,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(f34686,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)],[f34685]) ).
fof(f34719,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,[],[f22752]) ).
fof(f34731,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,[],[f34606]) ).
fof(f34732,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,[],[f34731]) ).
fof(f34866,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,[],[f34675]) ).
fof(f34867,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,[],[f34866]) ).
fof(f34886,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,[],[f34686]) ).
fof(f34887,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,[],[f34886]) ).
fof(f34911,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,[],[f21600]) ).
fof(f34912,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,[],[f34911]) ).
fof(f34913,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21515]) ).
fof(f34914,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34913]) ).
fof(f34992,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f34999,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22827]) ).
fof(f35000,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34999]) ).
fof(f35009,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(f35010,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,[],[f35009]) ).
fof(f35012,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,[],[f34719]) ).
fof(f35013,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,[],[f35012]) ).
fof(f35014,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(f35015,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35014]) ).
fof(f35227,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,[],[f21514]) ).
fof(f35228,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,[],[f35227]) ).
fof(f35331,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f2301]) ).
fof(f35332,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f35331]) ).
fof(f35338,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,[],[f34732]) ).
fof(f35358,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,[],[f34867]) ).
fof(f35364,plain,
( ~ v13_lattices(sK17)
& m2_filter_2(k6_domain_1(u1_struct_0(sK17),sK18),sK17)
& m1_subset_1(sK18,u1_struct_0(sK17))
& ~ v3_struct_0(sK17)
& v10_lattices(sK17)
& l3_lattices(sK17) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18]),skolemize(X0,sK17),skolemize(X1,sK18)],[f34887]) ).
fof(f35410,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,[],[f35000]) ).
fof(f35563,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,[],[f35338]) ).
fof(f35676,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,[],[f35358]) ).
fof(f35715,plain,
l3_lattices(sK17),
inference(cnf_transformation,[],[f35364]) ).
fof(f35716,plain,
v10_lattices(sK17),
inference(cnf_transformation,[],[f35364]) ).
fof(f35717,plain,
~ v3_struct_0(sK17),
inference(cnf_transformation,[],[f35364]) ).
fof(f35718,plain,
m1_subset_1(sK18,u1_struct_0(sK17)),
inference(cnf_transformation,[],[f35364]) ).
fof(f35719,plain,
m2_filter_2(k6_domain_1(u1_struct_0(sK17),sK18),sK17),
inference(cnf_transformation,[],[f35364]) ).
fof(f35720,plain,
~ v13_lattices(sK17),
inference(cnf_transformation,[],[f35364]) ).
fof(f35749,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,[],[f34912]) ).
fof(f35750,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34914]) ).
fof(f35859,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34992]) ).
fof(f35874,plain,
! [X0] :
( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35410]) ).
fof(f35882,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35010]) ).
fof(f35884,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35013]) ).
fof(f35893,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35015]) ).
fof(f36180,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,[],[f35228]) ).
fof(f36357,plain,
! [X0,X1] :
( k1_tarski(X1) = k6_domain_1(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f35332]) ).
fof(f36522,definition,
( spl162_1
<=> v13_lattices(sK17) ),
introduced(definition,[new_symbols(definition,[spl162_1])],[avatar_definition]) ).
fof(f36524,plain,
( ~ v13_lattices(sK17)
| spl162_1 ),
inference(avatar_component_clause,[],[f36522]) ).
fof(f36525,plain,
~ spl162_1,
inference(avatar_split_clause,[],[f35720,f36522]) ).
fof(f36527,definition,
( spl162_2
<=> v3_struct_0(sK17) ),
introduced(definition,[new_symbols(definition,[spl162_2])],[avatar_definition]) ).
fof(f36529,plain,
( ~ v3_struct_0(sK17)
| spl162_2 ),
inference(avatar_component_clause,[],[f36527]) ).
fof(f36530,plain,
~ spl162_2,
inference(avatar_split_clause,[],[f35717,f36527]) ).
fof(f36535,plain,
( ~ v14_lattices(k1_lattice2(sK17))
| v3_struct_0(sK17)
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17)
| spl162_1 ),
inference(resolution,[],[f36524,f35874]) ).
fof(f36536,plain,
( ~ v14_lattices(k1_lattice2(sK17))
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17)
| spl162_1
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36535,f36529]) ).
fof(f36541,plain,
( ~ v14_lattices(k1_lattice2(sK17))
| ~ l3_lattices(sK17)
| spl162_1
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36536,f35716]) ).
fof(f36546,plain,
( ~ v14_lattices(k1_lattice2(sK17))
| spl162_1
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36541,f35715]) ).
fof(f36632,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK17))
| ~ m2_filter_2(X0,sK17)
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17) )
| spl162_2 ),
inference(resolution,[],[f36529,f35676]) ).
fof(f36688,plain,
( m1_filter_0(u1_struct_0(sK17),sK17)
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17)
| spl162_2 ),
inference(resolution,[],[f36529,f35750]) ).
fof(f36776,plain,
( u1_struct_0(sK17) = u1_struct_0(k1_lattice2(sK17))
| ~ l3_lattices(sK17)
| spl162_2 ),
inference(resolution,[],[f36529,f35882]) ).
fof(f36777,plain,
( v10_lattices(k1_lattice2(sK17))
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17)
| spl162_2 ),
inference(resolution,[],[f36529,f35884]) ).
fof(f36786,plain,
( ~ v3_struct_0(k1_lattice2(sK17))
| ~ l3_lattices(sK17)
| spl162_2 ),
inference(resolution,[],[f36529,f35893]) ).
fof(f37206,plain,
( ~ v3_struct_0(k1_lattice2(sK17))
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36786,f35715]) ).
fof(f37213,plain,
( v10_lattices(k1_lattice2(sK17))
| ~ l3_lattices(sK17)
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36777,f35716]) ).
fof(f37214,plain,
( u1_struct_0(sK17) = u1_struct_0(k1_lattice2(sK17))
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36776,f35715]) ).
fof(f37299,plain,
( m1_filter_0(u1_struct_0(sK17),sK17)
| ~ l3_lattices(sK17)
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36688,f35716]) ).
fof(f37353,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK17))
| ~ m2_filter_2(X0,sK17)
| ~ l3_lattices(sK17) )
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f36632,f35716]) ).
fof(f37557,plain,
( v10_lattices(k1_lattice2(sK17))
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f37213,f35715]) ).
fof(f37639,plain,
( m1_filter_0(u1_struct_0(sK17),sK17)
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f37299,f35715]) ).
fof(f37693,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK17))
| ~ m2_filter_2(X0,sK17) )
| spl162_2 ),
inference(forward_subsumption_resolution,[],[f37353,f35715]) ).
fof(f37890,definition,
( spl162_3
<=> v10_lattices(sK17) ),
introduced(definition,[new_symbols(definition,[spl162_3])],[avatar_definition]) ).
fof(f37892,plain,
( v10_lattices(sK17)
| ~ spl162_3 ),
inference(avatar_component_clause,[],[f37890]) ).
fof(f37893,plain,
spl162_3,
inference(avatar_split_clause,[],[f35716,f37890]) ).
fof(f37895,definition,
( spl162_4
<=> l3_lattices(sK17) ),
introduced(definition,[new_symbols(definition,[spl162_4])],[avatar_definition]) ).
fof(f37897,plain,
( l3_lattices(sK17)
| ~ spl162_4 ),
inference(avatar_component_clause,[],[f37895]) ).
fof(f37898,plain,
spl162_4,
inference(avatar_split_clause,[],[f35715,f37895]) ).
fof(f37900,definition,
( spl162_5
<=> m2_filter_2(k6_domain_1(u1_struct_0(sK17),sK18),sK17) ),
introduced(definition,[new_symbols(definition,[spl162_5])],[avatar_definition]) ).
fof(f37902,plain,
( m2_filter_2(k6_domain_1(u1_struct_0(sK17),sK18),sK17)
| ~ spl162_5 ),
inference(avatar_component_clause,[],[f37900]) ).
fof(f37903,plain,
spl162_5,
inference(avatar_split_clause,[],[f35719,f37900]) ).
fof(f37925,plain,
( m2_filter_2(k1_tarski(sK18),sK17)
| v1_xboole_0(u1_struct_0(sK17))
| ~ m1_subset_1(sK18,u1_struct_0(sK17))
| ~ spl162_5 ),
inference(superposition,[],[f37902,f36357]) ).
fof(f37926,plain,
( m2_filter_2(k1_tarski(sK18),sK17)
| v1_xboole_0(u1_struct_0(sK17))
| ~ spl162_5 ),
inference(forward_subsumption_resolution,[],[f37925,f35718]) ).
fof(f38496,definition,
( spl162_6
<=> m1_subset_1(sK18,u1_struct_0(sK17)) ),
introduced(definition,[new_symbols(definition,[spl162_6])],[avatar_definition]) ).
fof(f38498,plain,
( m1_subset_1(sK18,u1_struct_0(sK17))
| ~ spl162_6 ),
inference(avatar_component_clause,[],[f38496]) ).
fof(f38499,plain,
spl162_6,
inference(avatar_split_clause,[],[f35718,f38496]) ).
fof(f38934,plain,
( k6_domain_1(u1_struct_0(sK17),sK18) = k1_tarski(sK18)
| v1_xboole_0(u1_struct_0(sK17))
| ~ spl162_6 ),
inference(resolution,[],[f38498,f36357]) ).
fof(f39932,plain,
( l3_lattices(k1_lattice2(sK17))
| ~ spl162_4 ),
inference(resolution,[],[f37897,f35859]) ).
fof(f42869,definition,
( spl162_22
<=> u1_struct_0(sK17) = u1_struct_0(k1_lattice2(sK17)) ),
introduced(definition,[new_symbols(definition,[spl162_22])],[avatar_definition]) ).
fof(f42871,plain,
( u1_struct_0(sK17) = u1_struct_0(k1_lattice2(sK17))
| ~ spl162_22 ),
inference(avatar_component_clause,[],[f42869]) ).
fof(f42872,plain,
( spl162_22
| spl162_2 ),
inference(avatar_split_clause,[],[f37214,f36527,f42869]) ).
fof(f44402,definition,
( spl162_25
<=> m1_filter_0(u1_struct_0(sK17),sK17) ),
introduced(definition,[new_symbols(definition,[spl162_25])],[avatar_definition]) ).
fof(f44404,plain,
( m1_filter_0(u1_struct_0(sK17),sK17)
| ~ spl162_25 ),
inference(avatar_component_clause,[],[f44402]) ).
fof(f44405,plain,
( spl162_25
| spl162_2 ),
inference(avatar_split_clause,[],[f37639,f36527,f44402]) ).
fof(f44417,plain,
( ~ v1_xboole_0(u1_struct_0(sK17))
| v3_struct_0(sK17)
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17)
| ~ spl162_25 ),
inference(resolution,[],[f44404,f35749]) ).
fof(f44461,plain,
( ~ v1_xboole_0(u1_struct_0(sK17))
| ~ v10_lattices(sK17)
| ~ l3_lattices(sK17)
| spl162_2
| ~ spl162_25 ),
inference(forward_subsumption_resolution,[],[f44417,f36529]) ).
fof(f44490,plain,
( ~ v1_xboole_0(u1_struct_0(sK17))
| ~ l3_lattices(sK17)
| spl162_2
| ~ spl162_3
| ~ spl162_25 ),
inference(forward_subsumption_resolution,[],[f44461,f37892]) ).
fof(f44519,plain,
( ~ v1_xboole_0(u1_struct_0(sK17))
| spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_25 ),
inference(forward_subsumption_resolution,[],[f44490,f37897]) ).
fof(f44535,plain,
( m2_filter_2(k1_tarski(sK18),sK17)
| spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_25 ),
inference(backward_subsumption_resolution,[],[f37926,f44519]) ).
fof(f44589,plain,
( k6_domain_1(u1_struct_0(sK17),sK18) = k1_tarski(sK18)
| spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_6
| ~ spl162_25 ),
inference(backward_subsumption_resolution,[],[f38934,f44519]) ).
fof(f45050,definition,
( spl162_27
<=> m2_filter_2(k1_tarski(sK18),sK17) ),
introduced(definition,[new_symbols(definition,[spl162_27])],[avatar_definition]) ).
fof(f45052,plain,
( m2_filter_2(k1_tarski(sK18),sK17)
| ~ spl162_27 ),
inference(avatar_component_clause,[],[f45050]) ).
fof(f45053,plain,
( spl162_27
| spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_25 ),
inference(avatar_split_clause,[],[f44535,f44402,f37900,f37895,f37890,f36527,f45050]) ).
fof(f48559,definition,
( spl162_38
<=> l3_lattices(k1_lattice2(sK17)) ),
introduced(definition,[new_symbols(definition,[spl162_38])],[avatar_definition]) ).
fof(f48561,plain,
( l3_lattices(k1_lattice2(sK17))
| ~ spl162_38 ),
inference(avatar_component_clause,[],[f48559]) ).
fof(f48562,plain,
( spl162_38
| ~ spl162_4 ),
inference(avatar_split_clause,[],[f39932,f37895,f48559]) ).
fof(f48978,definition,
( spl162_45
<=> ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK17))
| ~ m2_filter_2(X0,sK17) ) ),
introduced(definition,[new_symbols(definition,[spl162_45])],[avatar_definition]) ).
fof(f48979,plain,
( ! [X0] :
( m1_filter_2(X0,k1_lattice2(sK17))
| ~ m2_filter_2(X0,sK17) )
| ~ spl162_45 ),
inference(avatar_component_clause,[],[f48978]) ).
fof(f48980,plain,
( spl162_45
| spl162_2 ),
inference(avatar_split_clause,[],[f37693,f36527,f48978]) ).
fof(f48983,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK17)
| m1_filter_0(X0,k1_lattice2(sK17))
| v3_struct_0(k1_lattice2(sK17))
| ~ v10_lattices(k1_lattice2(sK17))
| ~ l3_lattices(k1_lattice2(sK17)) )
| ~ spl162_45 ),
inference(resolution,[],[f48979,f35563]) ).
fof(f48991,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK17)
| m1_filter_0(X0,k1_lattice2(sK17))
| ~ v10_lattices(k1_lattice2(sK17))
| ~ l3_lattices(k1_lattice2(sK17)) )
| spl162_2
| ~ spl162_45 ),
inference(forward_subsumption_resolution,[],[f48983,f37206]) ).
fof(f48996,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK17)
| m1_filter_0(X0,k1_lattice2(sK17))
| ~ l3_lattices(k1_lattice2(sK17)) )
| spl162_2
| ~ spl162_45 ),
inference(forward_subsumption_resolution,[],[f48991,f37557]) ).
fof(f48999,plain,
( ! [X0] :
( ~ m2_filter_2(X0,sK17)
| m1_filter_0(X0,k1_lattice2(sK17)) )
| spl162_2
| ~ spl162_38
| ~ spl162_45 ),
inference(forward_subsumption_resolution,[],[f48996,f48561]) ).
fof(f49006,definition,
( spl162_46
<=> v14_lattices(k1_lattice2(sK17)) ),
introduced(definition,[new_symbols(definition,[spl162_46])],[avatar_definition]) ).
fof(f49008,plain,
( ~ v14_lattices(k1_lattice2(sK17))
| spl162_46 ),
inference(avatar_component_clause,[],[f49006]) ).
fof(f49009,plain,
( ~ spl162_46
| spl162_1
| spl162_2 ),
inference(avatar_split_clause,[],[f36546,f36527,f36522,f49006]) ).
fof(f51076,definition,
( spl162_53
<=> ! [X0] :
( ~ m2_filter_2(X0,sK17)
| m1_filter_0(X0,k1_lattice2(sK17)) ) ),
introduced(definition,[new_symbols(definition,[spl162_53])],[avatar_definition]) ).
fof(f51077,plain,
( ! [X0] :
( m1_filter_0(X0,k1_lattice2(sK17))
| ~ m2_filter_2(X0,sK17) )
| ~ spl162_53 ),
inference(avatar_component_clause,[],[f51076]) ).
fof(f51078,plain,
( spl162_53
| spl162_2
| ~ spl162_38
| ~ spl162_45 ),
inference(avatar_split_clause,[],[f48999,f48978,f48559,f36527,f51076]) ).
fof(f51118,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK17)),X0),sK17)
| v14_lattices(k1_lattice2(sK17))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK17)))
| v3_struct_0(k1_lattice2(sK17))
| ~ v10_lattices(k1_lattice2(sK17))
| ~ l3_lattices(k1_lattice2(sK17)) )
| ~ spl162_53 ),
inference(resolution,[],[f51077,f36180]) ).
fof(f51123,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK17)),X0),sK17)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK17)))
| v3_struct_0(k1_lattice2(sK17))
| ~ v10_lattices(k1_lattice2(sK17))
| ~ l3_lattices(k1_lattice2(sK17)) )
| spl162_46
| ~ spl162_53 ),
inference(forward_subsumption_resolution,[],[f51118,f49008]) ).
fof(f51161,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK17)),X0),sK17)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK17)))
| ~ v10_lattices(k1_lattice2(sK17))
| ~ l3_lattices(k1_lattice2(sK17)) )
| spl162_2
| spl162_46
| ~ spl162_53 ),
inference(forward_subsumption_resolution,[],[f51123,f37206]) ).
fof(f51197,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK17)),X0),sK17)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK17)))
| ~ l3_lattices(k1_lattice2(sK17)) )
| spl162_2
| spl162_46
| ~ spl162_53 ),
inference(forward_subsumption_resolution,[],[f51161,f37557]) ).
fof(f51233,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(k1_lattice2(sK17)),X0),sK17)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK17))) )
| spl162_2
| ~ spl162_38
| spl162_46
| ~ spl162_53 ),
inference(forward_subsumption_resolution,[],[f51197,f48561]) ).
fof(f51254,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(sK17),X0),sK17)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK17))) )
| spl162_2
| ~ spl162_22
| ~ spl162_38
| spl162_46
| ~ spl162_53 ),
inference(forward_demodulation,[],[f51233,f42871]) ).
fof(f51263,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK17))
| ~ m2_filter_2(k6_domain_1(u1_struct_0(sK17),X0),sK17) )
| spl162_2
| ~ spl162_22
| ~ spl162_38
| spl162_46
| ~ spl162_53 ),
inference(forward_demodulation,[],[f51254,f42871]) ).
fof(f51280,definition,
( spl162_54
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK17))
| ~ m2_filter_2(k6_domain_1(u1_struct_0(sK17),X0),sK17) ) ),
introduced(definition,[new_symbols(definition,[spl162_54])],[avatar_definition]) ).
fof(f51281,plain,
( ! [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(sK17),X0),sK17)
| ~ m1_subset_1(X0,u1_struct_0(sK17)) )
| ~ spl162_54 ),
inference(avatar_component_clause,[],[f51280]) ).
fof(f51282,plain,
( spl162_54
| spl162_2
| ~ spl162_22
| ~ spl162_38
| spl162_46
| ~ spl162_53 ),
inference(avatar_split_clause,[],[f51263,f51076,f49006,f48559,f42869,f36527,f51280]) ).
fof(f57252,definition,
( spl162_74
<=> k6_domain_1(u1_struct_0(sK17),sK18) = k1_tarski(sK18) ),
introduced(definition,[new_symbols(definition,[spl162_74])],[avatar_definition]) ).
fof(f57254,plain,
( k6_domain_1(u1_struct_0(sK17),sK18) = k1_tarski(sK18)
| ~ spl162_74 ),
inference(avatar_component_clause,[],[f57252]) ).
fof(f57255,plain,
( spl162_74
| spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_6
| ~ spl162_25 ),
inference(avatar_split_clause,[],[f44589,f44402,f38496,f37895,f37890,f36527,f57252]) ).
fof(f58262,plain,
( ~ m2_filter_2(k1_tarski(sK18),sK17)
| ~ m1_subset_1(sK18,u1_struct_0(sK17))
| ~ spl162_54
| ~ spl162_74 ),
inference(superposition,[],[f51281,f57254]) ).
fof(f58266,plain,
( ~ m1_subset_1(sK18,u1_struct_0(sK17))
| ~ spl162_27
| ~ spl162_54
| ~ spl162_74 ),
inference(forward_subsumption_resolution,[],[f58262,f45052]) ).
fof(f58303,plain,
( $false
| ~ spl162_6
| ~ spl162_27
| ~ spl162_54
| ~ spl162_74 ),
inference(forward_subsumption_resolution,[],[f58266,f38498]) ).
fof(f58304,plain,
( ~ spl162_6
| ~ spl162_27
| ~ spl162_54
| ~ spl162_74 ),
inference(avatar_contradiction_clause,[],[f58303]) ).
cnf(s1,plain,
~ spl162_1,
inference(sat_conversion,[],[f36525]) ).
cnf(s2,plain,
~ spl162_2,
inference(sat_conversion,[],[f36530]) ).
cnf(s3,plain,
spl162_3,
inference(sat_conversion,[],[f37893]) ).
cnf(s4,plain,
spl162_4,
inference(sat_conversion,[],[f37898]) ).
cnf(s5,plain,
spl162_5,
inference(sat_conversion,[],[f37903]) ).
cnf(s6,plain,
spl162_6,
inference(sat_conversion,[],[f38499]) ).
cnf(s22,plain,
( spl162_2
| spl162_22 ),
inference(sat_conversion,[],[f42872]) ).
cnf(s25,plain,
( spl162_2
| spl162_25 ),
inference(sat_conversion,[],[f44405]) ).
cnf(s27,plain,
( spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_5
| ~ spl162_25
| spl162_27 ),
inference(sat_conversion,[],[f45053]) ).
cnf(s37,plain,
( ~ spl162_4
| spl162_38 ),
inference(sat_conversion,[],[f48562]) ).
cnf(s44,plain,
( spl162_2
| spl162_45 ),
inference(sat_conversion,[],[f48980]) ).
cnf(s45,plain,
( spl162_1
| spl162_2
| ~ spl162_46 ),
inference(sat_conversion,[],[f49009]) ).
cnf(s84,plain,
( spl162_2
| ~ spl162_38
| ~ spl162_45
| spl162_53 ),
inference(sat_conversion,[],[f51078]) ).
cnf(s85,plain,
( spl162_2
| ~ spl162_22
| ~ spl162_38
| spl162_46
| ~ spl162_53
| spl162_54 ),
inference(sat_conversion,[],[f51282]) ).
cnf(s105,plain,
( spl162_2
| ~ spl162_3
| ~ spl162_4
| ~ spl162_6
| ~ spl162_25
| spl162_74 ),
inference(sat_conversion,[],[f57255]) ).
cnf(s110,plain,
( ~ spl162_6
| ~ spl162_27
| ~ spl162_54
| ~ spl162_74 ),
inference(sat_conversion,[],[f58304]) ).
cnf(s112,plain,
spl162_38,
inference(rat,[],[s37,s4]) ).
cnf(s118,plain,
spl162_45,
inference(rat,[],[s44,s2]) ).
cnf(s132,plain,
spl162_25,
inference(rat,[],[s25,s2]) ).
cnf(s135,plain,
spl162_22,
inference(rat,[],[s22,s2]) ).
cnf(s147,plain,
spl162_53,
inference(rat,[],[s84,s2,s112,s118]) ).
cnf(s148,plain,
spl162_74,
inference(rat,[],[s105,s2,s3,s6,s4,s132]) ).
cnf(s150,plain,
spl162_27,
inference(rat,[],[s27,s2,s3,s5,s4,s132]) ).
cnf(s170,plain,
~ spl162_54,
inference(rat,[],[s110,s148,s6,s150]) ).
cnf(s174,plain,
spl162_46,
inference(rat,[],[s85,s135,s147,s2,s112,s170]) ).
cnf(s176,plain,
spl162_1,
inference(rat,[],[s45,s2,s174]) ).
cnf(s177,plain,
$false,
inference(rat,[],[s1,s176]) ).
fof(f58390,plain,
$false,
inference(avatar_sat_refutation,[],[s177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT303+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n005.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 14:24:40 UTC 2026
% 0.11/0.40 % CPUTime :
% 0.11/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.28/4.99 % (4041437)Detected formulas, will run a generic FOF schedule.
% 14.28/4.99 % (4041445)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=482225855:i=109:sd=1:ins=1:gsp=on:ss=axioms_2978 on theBenchmark for (2978ds/109Mi)
% 14.28/4.99 % (4041444)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=282273791:i=141695:sd=1:nm=32:gsp=on:ss=included_2978 on theBenchmark for (2978ds/141695Mi)
% 14.28/4.99 % (4041442)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=2819673422:i=141193_2978 on theBenchmark for (2978ds/141193Mi)
% 14.28/4.99 % (4041443)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=1056964968:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2978 on theBenchmark for (2978ds/134677Mi)
% 14.28/4.99 % (4041445)Instruction limit reached!
% 14.28/4.99 % (4041445)------------------------------
% 14.28/4.99 % (4041445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.28/4.99 % (4041445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.28/4.99 % (4041445)CaDiCaL version: 2.1.3
% 14.28/4.99 % (4041445)Termination reason: Instruction limit
% 14.28/4.99 % (4041445)Termination phase: SInE selection
% 14.28/4.99 % (4041445)Time elapsed: 0.049 s
% 14.28/4.99 % (4041445)Peak memory usage: 136 MB
% 14.28/4.99 % (4041445)Instructions burned: 109 (million)
% 14.28/4.99 % (4041448)dis-21_1_sil=8000:lcm=predicate:random_seed=2296341327:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2978 on theBenchmark for (2978ds/129Mi)
% 14.28/4.99 % (4041447)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=400391690:s2a=on:i=139:gtg=position_2978 on theBenchmark for (2978ds/139Mi)
% 14.28/4.99 % (4041446)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2443089408:i=119:av=off:ss=axioms_2978 on theBenchmark for (2978ds/119Mi)
% 14.28/4.99 % (4041447)Instruction limit reached!
% 14.28/4.99 % (4041447)------------------------------
% 14.28/4.99 % (4041447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.28/4.99 % (4041447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.28/4.99 % (4041447)CaDiCaL version: 2.1.3
% 14.28/4.99 % (4041447)Termination reason: Instruction limit
% 14.28/4.99 % (4041447)Termination phase: Property scanning
% 14.28/4.99 % (4041447)Time elapsed: 0.064 s
% 14.28/4.99 % (4041447)Peak memory usage: 136 MB
% 14.28/4.99 % (4041447)Instructions burned: 139 (million)
% 14.28/4.99 % (4041446)Instruction limit reached!
% 14.28/4.99 % (4041446)------------------------------
% 14.28/4.99 % (4041446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.28/4.99 % (4041446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.28/4.99 % (4041446)CaDiCaL version: 2.1.3
% 14.28/4.99 % (4041446)Termination reason: Instruction limit
% 14.28/4.99 % (4041446)Termination phase: SInE selection
% 14.28/4.99 % (4041446)Time elapsed: 0.090 s
% 14.28/4.99 % (4041446)Peak memory usage: 136 MB
% 14.28/4.99 % (4041446)Instructions burned: 120 (million)
% 14.28/4.99 % (4041448)Instruction limit reached!
% 14.28/4.99 % (4041448)------------------------------
% 14.28/4.99 % (4041448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.28/4.99 % (4041448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.28/4.99 % (4041448)CaDiCaL version: 2.1.3
% 14.28/4.99 % (4041448)Termination reason: Instruction limit
% 14.28/4.99 % (4041448)Termination phase: SInE selection
% 14.28/4.99 % (4041448)Time elapsed: 0.093 s
% 14.28/4.99 % (4041448)Peak memory usage: 136 MB
% 14.28/4.99 % (4041448)Instructions burned: 131 (million)
% 14.28/4.99 % (4041456)lrs+10_1_sil=8000:sp=occurrence:random_seed=2418502579:i=285:sd=3:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/285Mi)
% 14.28/4.99 % (4041457)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1116303189:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/157Mi)
% 14.28/4.99 % (4041456)Instruction limit reached!
% 14.28/4.99 % (4041456)------------------------------
% 14.28/4.99 % (4041456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.28/4.99 % (4041456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.28/4.99 % (4041456)CaDiCaL version: 2.1.3
% 14.28/4.99 % (4041456)Termination reason: Instruction limit
% 23.57/6.12 % (4041456)Termination phase: Saturation
% 23.57/6.12 % (4041456)Time elapsed: 0.130 s
% 23.57/6.12 % (4041456)Peak memory usage: 142 MB
% 23.57/6.12 % (4041456)Instructions burned: 285 (million)
% 23.57/6.12 % (4041459)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=4213703500:s2a=on:i=248:s2at=1.23:gtg=position_2975 on theBenchmark for (2975ds/248Mi)
% 23.57/6.12 % (4041458)lrs+1011_1_sil=32000:sp=occurrence:random_seed=610225106:i=325:sd=1:ss=axioms:sgt=32_2975 on theBenchmark for (2975ds/325Mi)
% 23.57/6.12 % (4041457)Instruction limit reached!
% 23.57/6.12 % (4041457)------------------------------
% 23.57/6.12 % (4041457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.57/6.12 % (4041457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.57/6.12 % (4041457)CaDiCaL version: 2.1.3
% 23.57/6.12 % (4041457)Termination reason: Instruction limit
% 23.57/6.12 % (4041457)Termination phase: Property scanning
% 23.57/6.12 % (4041457)Time elapsed: 0.071 s
% 23.57/6.12 % (4041457)Peak memory usage: 136 MB
% 23.57/6.12 % (4041457)Instructions burned: 159 (million)
% 23.57/6.12 % (4041459)Instruction limit reached!
% 23.57/6.12 % (4041459)------------------------------
% 23.57/6.12 % (4041459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.57/6.12 % (4041459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.57/6.12 % (4041459)CaDiCaL version: 2.1.3
% 23.57/6.12 % (4041459)Termination reason: Instruction limit
% 23.57/6.12 % (4041459)Termination phase: Property scanning
% 23.57/6.12 % (4041459)Time elapsed: 0.110 s
% 23.57/6.12 % (4041459)Peak memory usage: 136 MB
% 23.57/6.12 % (4041459)Instructions burned: 249 (million)
% 23.57/6.12 % (4041463)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3145302409:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2973 on theBenchmark for (2973ds/294Mi)
% 23.57/6.12 % (4041458)Refutation not found, incomplete strategy
% 23.57/6.12 % (4041458)------------------------------
% 23.57/6.12 % (4041458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.57/6.12 % (4041458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.57/6.12 % (4041458)CaDiCaL version: 2.1.3
% 23.57/6.12 % (4041458)Termination reason: Refutation not found, incomplete strategy
% 23.57/6.12 % (4041458)Time elapsed: 0.207 s
% 23.57/6.12 % (4041458)Peak memory usage: 142 MB
% 23.57/6.12 % (4041458)Instructions burned: 248 (million)
% 23.57/6.12 % (4041465)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2113981611:i=2350_2973 on theBenchmark for (2973ds/2350Mi)
% 23.57/6.12 % (4041463)Instruction limit reached!
% 23.57/6.12 % (4041463)------------------------------
% 23.57/6.12 % (4041463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.57/6.12 % (4041463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.57/6.12 % (4041463)CaDiCaL version: 2.1.3
% 23.57/6.12 % (4041463)Termination reason: Instruction limit
% 23.57/6.12 % (4041463)Termination phase: SInE selection
% 23.57/6.12 % (4041463)Time elapsed: 0.104 s
% 23.57/6.12 % (4041463)Peak memory usage: 137 MB
% 23.57/6.12 % (4041463)Instructions burned: 294 (million)
% 23.57/6.12 % (4041466)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4080909548:cts=off:i=113:fsr=off:ss=included:sgt=4_2972 on theBenchmark for (2972ds/113Mi)
% 23.57/6.12 % (4041469)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=373012542:i=127:av=off:fsr=off:sup=off_2971 on theBenchmark for (2971ds/127Mi)
% 23.57/6.12 % (4041466)Instruction limit reached!
% 23.57/6.12 % (4041466)------------------------------
% 23.57/6.12 % (4041466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.57/6.12 % (4041466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.57/6.12 % (4041466)CaDiCaL version: 2.1.3
% 23.57/6.12 % (4041466)Termination reason: Instruction limit
% 23.57/6.12 % (4041466)Termination phase: SInE selection
% 23.57/6.12 % (4041466)Time elapsed: 0.089 s
% 23.57/6.12 % (4041466)Peak memory usage: 136 MB
% 23.57/6.12 % (4041466)Instructions burned: 113 (million)
% 23.57/6.12 % (4041469)Instruction limit reached!
% 23.57/6.12 % (4041469)------------------------------
% 23.57/6.12 % (4041469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.57/6.12 % (4041469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.57/6.12 % (4041469)CaDiCaL version: 2.1.3
% 23.57/6.12 % (4041469)Termination reason: Instruction limit
% 26.51/6.59 % (4041469)Termination phase: Preprocessing 1
% 26.51/6.59 % (4041469)Time elapsed: 0.056 s
% 26.51/6.59 % (4041469)Peak memory usage: 137 MB
% 26.51/6.59 % (4041469)Instructions burned: 128 (million)
% 26.51/6.59 % (4041458)------------------------------
% 26.51/6.59 % (4041458)------------------------------
% 26.51/6.59 % (4041472)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2274671245:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2969 on theBenchmark for (2969ds/114Mi)
% 26.51/6.59 % (4041473)lrs+10_1_sil=8000:sp=occurrence:random_seed=2297812897:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2969 on theBenchmark for (2969ds/907Mi)
% 26.51/6.59 % (4041472)Instruction limit reached!
% 26.51/6.59 % (4041472)------------------------------
% 26.51/6.59 % (4041472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041472)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041472)Termination reason: Instruction limit
% 26.51/6.59 % (4041472)Termination phase: Property scanning
% 26.51/6.59 % (4041472)Time elapsed: 0.052 s
% 26.51/6.59 % (4041472)Peak memory usage: 136 MB
% 26.51/6.59 % (4041472)Instructions burned: 115 (million)
% 26.51/6.59 % (4041474)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3862493508:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 26.51/6.59 % (4041477)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=610546906:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 26.51/6.59 % (4041473)Instruction limit reached!
% 26.51/6.59 % (4041473)------------------------------
% 26.51/6.59 % (4041473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041473)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041473)Termination reason: Instruction limit
% 26.51/6.59 % (4041473)Termination phase: Property scanning
% 26.51/6.59 % (4041473)Time elapsed: 0.334 s
% 26.51/6.59 % (4041473)Peak memory usage: 154 MB
% 26.51/6.59 % (4041473)Instructions burned: 909 (million)
% 26.51/6.59 % (4041474)Refutation not found, incomplete strategy
% 26.51/6.59 % (4041474)------------------------------
% 26.51/6.59 % (4041474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041474)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041474)Termination reason: Refutation not found, incomplete strategy
% 26.51/6.59 % (4041474)Time elapsed: 0.237 s
% 26.51/6.59 % (4041474)Peak memory usage: 142 MB
% 26.51/6.59 % (4041474)Instructions burned: 310 (million)
% 26.51/6.59 % (4041480)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2095437220:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 26.51/6.59 % (4041480)Instruction limit reached!
% 26.51/6.59 % (4041480)------------------------------
% 26.51/6.59 % (4041480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041480)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041480)Termination reason: Instruction limit
% 26.51/6.59 % (4041480)Termination phase: SInE selection
% 26.51/6.59 % (4041480)Time elapsed: 0.058 s
% 26.51/6.59 % (4041480)Peak memory usage: 136 MB
% 26.51/6.59 % (4041480)Instructions burned: 137 (million)
% 26.51/6.59 % (4041474)------------------------------
% 26.51/6.59 % (4041474)------------------------------
% 26.51/6.59 % (4041482)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1255332925:st=8:i=592:sd=3:ep=RST:ss=axioms_2962 on theBenchmark for (2962ds/592Mi)
% 26.51/6.59 % (4041484)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3307266251:st=3:i=13193:sd=3:ss=axioms_2961 on theBenchmark for (2961ds/13193Mi)
% 26.51/6.59 % (4041482)Instruction limit reached!
% 26.51/6.59 % (4041482)------------------------------
% 26.51/6.59 % (4041482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041482)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041482)Termination reason: Instruction limit
% 26.51/6.59 % (4041482)Termination phase: Preprocessing 2
% 26.51/6.59 % (4041482)Time elapsed: 0.265 s
% 26.51/6.59 % (4041482)Peak memory usage: 143 MB
% 26.51/6.59 % (4041482)Instructions burned: 592 (million)
% 26.51/6.59 % (4041486)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=3842900273:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2958 on theBenchmark for (2958ds/125Mi)
% 26.51/6.59 % (4041486)Instruction limit reached!
% 26.51/6.59 % (4041486)------------------------------
% 26.51/6.59 % (4041486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041486)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041486)Termination reason: Instruction limit
% 26.51/6.59 % (4041486)Termination phase: Property scanning
% 26.51/6.59 % (4041486)Time elapsed: 0.031 s
% 26.51/6.59 % (4041486)Peak memory usage: 136 MB
% 26.51/6.59 % (4041486)Instructions burned: 128 (million)
% 26.51/6.59 % (4041488)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3489133414:i=134:gtgl=5:slsql=off:gtg=exists_sym_2957 on theBenchmark for (2957ds/134Mi)
% 26.51/6.59 % (4041488)Instruction limit reached!
% 26.51/6.59 % (4041488)------------------------------
% 26.51/6.59 % (4041488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041488)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041488)Termination reason: Instruction limit
% 26.51/6.59 % (4041488)Termination phase: Property scanning
% 26.51/6.59 % (4041488)Time elapsed: 0.033 s
% 26.51/6.59 % (4041488)Peak memory usage: 136 MB
% 26.51/6.59 % (4041488)Instructions burned: 134 (million)
% 26.51/6.59 % (4041465)Instruction limit reached!
% 26.51/6.59 % (4041465)------------------------------
% 26.51/6.59 % (4041465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041465)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041465)Termination reason: Instruction limit
% 26.51/6.59 % (4041465)Termination phase: Property scanning
% 26.51/6.59 % (4041465)Time elapsed: 1.608 s
% 26.51/6.59 % (4041465)Peak memory usage: 233 MB
% 26.51/6.59 % (4041465)Instructions burned: 2353 (million)
% 26.51/6.59 % (4041490)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1785594772:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/141Mi)
% 26.51/6.59 % (4041490)Instruction limit reached!
% 26.51/6.59 % (4041490)------------------------------
% 26.51/6.59 % (4041490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041490)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041490)Termination reason: Instruction limit
% 26.51/6.59 % (4041490)Termination phase: SInE selection
% 26.51/6.59 % (4041490)Time elapsed: 0.060 s
% 26.51/6.59 % (4041490)Peak memory usage: 136 MB
% 26.51/6.59 % (4041490)Instructions burned: 142 (million)
% 26.51/6.59 % (4041491)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=780710581:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2955 on theBenchmark for (2955ds/431Mi)
% 26.51/6.59 % (4041493)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=1161513650:i=6060:aac=none:ins=25_2953 on theBenchmark for (2953ds/6060Mi)
% 26.51/6.59 % (4041491)Instruction limit reached!
% 26.51/6.59 % (4041491)------------------------------
% 26.51/6.59 % (4041491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041491)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041491)Termination reason: Instruction limit
% 26.51/6.59 % (4041491)Termination phase: Saturation
% 26.51/6.59 % (4041491)Time elapsed: 0.302 s
% 26.51/6.59 % (4041491)Peak memory usage: 143 MB
% 26.51/6.59 % (4041491)Instructions burned: 432 (million)
% 26.51/6.59 % (4041496)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=3945379979:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2950 on theBenchmark for (2950ds/150Mi)
% 26.51/6.59 % (4041496)Instruction limit reached!
% 26.51/6.59 % (4041496)------------------------------
% 26.51/6.59 % (4041496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.51/6.59 % (4041496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.51/6.59 % (4041496)CaDiCaL version: 2.1.3
% 26.51/6.59 % (4041496)Termination reason: Instruction limit
% 26.51/6.59 % (4041496)Termination phase: SInE selection
% 26.51/6.59 % (4041496)Time elapsed: 0.117 s
% 26.51/6.59 % (4041496)Peak memory usage: 136 MB
% 26.51/6.59 % (4041496)Instructions burned: 151 (million)
% 26.51/6.59 % (4041444)First to succeed.
% 26.51/6.59 % (4041444)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4041437"
% 26.51/6.59 % (4041498)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=488987749:i=14155:bd=all_2947 on theBenchmark for (2947ds/14155Mi)
% 26.51/6.59 % (4041444)Refutation found. Thanks to Tanya!
% 26.51/6.59 % SZS status Theorem for theBenchmark
% 26.51/6.59 % SZS output start Proof for theBenchmark
% See solution above
% 27.66/6.84 % (4041444)------------------------------
% 27.66/6.84 % (4041444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.66/6.84 % (4041444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.66/6.84 % (4041444)CaDiCaL version: 2.1.3
% 27.66/6.84 % (4041444)Termination reason: Refutation
% 27.66/6.84 % (4041444)Time elapsed: 3.025 s
% 27.66/6.84 % (4041444)Peak memory usage: 211 MB
% 27.66/6.84 % (4041444)Instructions burned: 4943 (million)
% 27.66/6.84 % (4041444)------------------------------
% 27.66/6.84 % (4041444)------------------------------
% 27.66/6.84 % (4041437)Success in time 5.706 s
% 27.66/6.84 % Vampire exiting
%------------------------------------------------------------------------------