%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT298+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:39 AM UTC 2026
% Result : Theorem 129.44s 24.71s
% Output : Refutation 160.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 48
% Syntax : Number of formulae : 319 ( 64 unt; 38 def)
% Number of atoms : 1805 ( 118 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 2528 (1042 ~;1267 |; 130 &)
% ( 44 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 30 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 11 con; 0-3 aty)
% Number of variables : 332 ( 0 sgn 314 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f21507,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( m1_filter_0(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_filter_0) ).
fof(f21509,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( m1_filter_0(X1,X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r3_lattices(X0,X2,X3) )
=> r2_hidden(X3,X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_filter_0) ).
fof(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22816,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
=> ( ( X1 = X3
& X2 = X4 )
=> ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t52_lattice2) ).
fof(f31938,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> m2_lattice4(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_lattice4) ).
fof(f31985,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f34604,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_2) ).
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/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f34656,axiom,
! [X0] :
( l3_lattices(X0)
=> ! [X1] :
( l3_lattices(X1)
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> k1_lattice2(X0) = k1_lattice2(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_filter_2) ).
fof(f34668,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_filter_2(X2,X0)
=> m1_filter_2(X2,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_filter_2) ).
fof(f34669,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
=> ! [X2] :
( m1_filter_2(X2,X0)
=> m1_filter_2(X2,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34668]) ).
fof(f34670,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( m1_filter_0(X1,X0)
<=> ( ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) )
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X0))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X0))
=> ( ( r2_hidden(X4,X1)
& r3_lattices(X0,X4,X5) )
=> r2_hidden(X5,X1) ) ) ) ) ) ) ),
inference(rectify,[],[f21509]) ).
fof(f34788,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m1_filter_2(X2,X1)
& m1_filter_2(X2,X0) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f34669]) ).
fof(f34789,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m1_filter_2(X2,X1)
& m1_filter_2(X2,X0) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f34788]) ).
fof(f34790,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(f34791,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,[],[f34790]) ).
fof(f34794,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34604]) ).
fof(f34795,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34794]) ).
fof(f34810,plain,
! [X0] :
( ! [X1] :
( k1_lattice2(X0) = k1_lattice2(X1)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34656]) ).
fof(f34811,plain,
! [X0] :
( ! [X1] :
( k1_lattice2(X0) = k1_lattice2(X1)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1) )
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34810]) ).
fof(f34834,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(f34835,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,[],[f34834]) ).
fof(f34861,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ( ! [X2] :
( ! [X3] :
( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r3_lattices(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34670]) ).
fof(f34862,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ( ! [X2] :
( ! [X3] :
( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r3_lattices(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34861]) ).
fof(f34863,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21507]) ).
fof(f34864,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34863]) ).
fof(f34886,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31985]) ).
fof(f34887,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34886]) ).
fof(f34888,plain,
! [X0] :
( ! [X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f31938]) ).
fof(f34889,plain,
! [X0] :
( ! [X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f34888]) ).
fof(f35000,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22816]) ).
fof(f35001,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
& k3_lattices(X0,X1,X2) = k4_lattices(k1_lattice2(X0),X3,X4) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35000]) ).
fof(f36006,definition,
! [X1,X0] :
( sP0(X1,X0)
<=> ! [X4] :
( ! [X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(X4,X1)
| ~ r3_lattices(X0,X4,X5)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f36007,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ( ! [X2] :
( ! [X3] :
( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& sP0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f34862,f36006]) ).
fof(f36050,plain,
( ~ m1_filter_2(sK29,sK28)
& m1_filter_2(sK29,sK27)
& g3_lattices(u1_struct_0(sK27),u2_lattices(sK27),u1_lattices(sK27)) = g3_lattices(u1_struct_0(sK28),u2_lattices(sK28),u1_lattices(sK28))
& ~ v3_struct_0(sK28)
& v10_lattices(sK28)
& l3_lattices(sK28)
& ~ v3_struct_0(sK27)
& v10_lattices(sK27)
& l3_lattices(sK27) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29]),skolemize(X0,sK27),skolemize(X1,sK28),skolemize(X2,sK29)],[f34789]) ).
fof(f36052,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,[],[f34791]) ).
fof(f36061,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ sP0(X1,X0) )
& ( ( ! [X2] :
( ! [X3] :
( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& sP0(X1,X0) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f36007]) ).
fof(f36062,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ sP0(X1,X0) )
& ( ( ! [X2] :
( ! [X3] :
( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
& sP0(X1,X0) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36061]) ).
fof(f36063,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
& r2_hidden(X2,X1)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ sP0(X1,X0) )
& ( ( ! [X4] :
( ! [X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
& sP0(X1,X0) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f36062]) ).
fof(f36064,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ( ~ r2_hidden(k4_lattices(X0,sK38(X0,X1),sK39(X0,X1)),X1)
& r2_hidden(sK38(X0,X1),X1)
& r2_hidden(sK39(X0,X1),X1)
& m1_subset_1(sK39(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK38(X0,X1),u1_struct_0(X0)) )
| ~ sP0(X1,X0) )
& ( ( ! [X4] :
( ! [X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
& sP0(X1,X0) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38,sK39]),skolemize(X2,sK38(X0,X1)),skolemize(X3,sK39(X0,X1))],[f36063]) ).
fof(f36065,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f34864]) ).
fof(f36066,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f36065]) ).
fof(f36067,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f36066]) ).
fof(f36068,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ( ( ~ r2_hidden(k4_lattices(X0,sK40(X0,X1),sK41(X0,X1)),X1)
| ~ r2_hidden(sK40(X0,X1),X1)
| ~ r2_hidden(sK41(X0,X1),X1) )
& ( r2_hidden(k4_lattices(X0,sK40(X0,X1),sK41(X0,X1)),X1)
| ( r2_hidden(sK40(X0,X1),X1)
& r2_hidden(sK41(X0,X1),X1) ) )
& m1_subset_1(sK41(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK40(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40,sK41]),skolemize(X2,sK40(X0,X1)),skolemize(X3,sK41(X0,X1))],[f36067]) ).
fof(f36544,plain,
l3_lattices(sK27),
inference(cnf_transformation,[],[f36050]) ).
fof(f36545,plain,
v10_lattices(sK27),
inference(cnf_transformation,[],[f36050]) ).
fof(f36546,plain,
~ v3_struct_0(sK27),
inference(cnf_transformation,[],[f36050]) ).
fof(f36547,plain,
l3_lattices(sK28),
inference(cnf_transformation,[],[f36050]) ).
fof(f36548,plain,
v10_lattices(sK28),
inference(cnf_transformation,[],[f36050]) ).
fof(f36549,plain,
~ v3_struct_0(sK28),
inference(cnf_transformation,[],[f36050]) ).
fof(f36550,plain,
g3_lattices(u1_struct_0(sK27),u2_lattices(sK27),u1_lattices(sK27)) = g3_lattices(u1_struct_0(sK28),u2_lattices(sK28),u1_lattices(sK28)),
inference(cnf_transformation,[],[f36050]) ).
fof(f36551,plain,
m1_filter_2(sK29,sK27),
inference(cnf_transformation,[],[f36050]) ).
fof(f36552,plain,
~ m1_filter_2(sK29,sK28),
inference(cnf_transformation,[],[f36050]) ).
fof(f36554,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,[],[f36052]) ).
fof(f36555,plain,
! [X0,X1] :
( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36052]) ).
fof(f36558,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34795]) ).
fof(f36570,plain,
! [X0,X1] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| k1_lattice2(X0) = k1_lattice2(X1)
| ~ l3_lattices(X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34811]) ).
fof(f36585,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34835]) ).
fof(f36610,plain,
! [X0,X1,X4,X5] :
( v1_xboole_0(X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36064]) ).
fof(f36617,plain,
! [X0,X1,X4,X5] :
( v1_xboole_0(X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| r2_hidden(X5,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36618,plain,
! [X0,X1,X4,X5] :
( v1_xboole_0(X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| r2_hidden(X4,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36619,plain,
! [X0,X1] :
( m1_subset_1(sK40(X0,X1),u1_struct_0(X0))
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36620,plain,
! [X0,X1] :
( m1_subset_1(sK41(X0,X1),u1_struct_0(X0))
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36621,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| r2_hidden(k4_lattices(X0,sK40(X0,X1),sK41(X0,X1)),X1)
| r2_hidden(sK41(X0,X1),X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36622,plain,
! [X0,X1] :
( r2_hidden(sK40(X0,X1),X1)
| r2_hidden(k4_lattices(X0,sK40(X0,X1),sK41(X0,X1)),X1)
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36623,plain,
! [X0,X1] :
( ~ r2_hidden(sK41(X0,X1),X1)
| ~ r2_hidden(k4_lattices(X0,sK40(X0,X1),sK41(X0,X1)),X1)
| ~ r2_hidden(sK40(X0,X1),X1)
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f36068]) ).
fof(f36657,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34887]) ).
fof(f36658,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f34889]) ).
fof(f36853,plain,
! [X2,X3,X0,X1,X4] :
( X2 != X4
| X1 != X3
| k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X3,X4)
| ~ m1_subset_1(X4,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35001]) ).
fof(f38759,definition,
sF394 = u1_struct_0(sK27),
introduced(definition,[new_symbols(definition,[sF394])],[function_definition]) ).
fof(f38760,plain,
u1_struct_0(sK27) = sF394,
inference(reorient_equations,[],[f38759]) ).
fof(f38761,definition,
sF395 = u2_lattices(sK27),
introduced(definition,[new_symbols(definition,[sF395])],[function_definition]) ).
fof(f38762,plain,
u2_lattices(sK27) = sF395,
inference(reorient_equations,[],[f38761]) ).
fof(f38763,definition,
sF396 = u1_lattices(sK27),
introduced(definition,[new_symbols(definition,[sF396])],[function_definition]) ).
fof(f38764,plain,
u1_lattices(sK27) = sF396,
inference(reorient_equations,[],[f38763]) ).
fof(f38765,definition,
sF397 = g3_lattices(sF394,sF395,sF396),
introduced(definition,[new_symbols(definition,[sF397])],[function_definition]) ).
fof(f38766,plain,
g3_lattices(sF394,sF395,sF396) = sF397,
inference(reorient_equations,[],[f38765]) ).
fof(f38767,definition,
sF398 = u1_struct_0(sK28),
introduced(definition,[new_symbols(definition,[sF398])],[function_definition]) ).
fof(f38768,plain,
u1_struct_0(sK28) = sF398,
inference(reorient_equations,[],[f38767]) ).
fof(f38769,definition,
sF399 = u2_lattices(sK28),
introduced(definition,[new_symbols(definition,[sF399])],[function_definition]) ).
fof(f38770,plain,
u2_lattices(sK28) = sF399,
inference(reorient_equations,[],[f38769]) ).
fof(f38771,definition,
sF400 = u1_lattices(sK28),
introduced(definition,[new_symbols(definition,[sF400])],[function_definition]) ).
fof(f38772,plain,
u1_lattices(sK28) = sF400,
inference(reorient_equations,[],[f38771]) ).
fof(f38773,definition,
sF401 = g3_lattices(sF398,sF399,sF400),
introduced(definition,[new_symbols(definition,[sF401])],[function_definition]) ).
fof(f38774,plain,
g3_lattices(sF398,sF399,sF400) = sF401,
inference(reorient_equations,[],[f38773]) ).
fof(f38775,plain,
sF397 = sF401,
inference(definition_folding,[],[f36550,f38774,f38772,f38770,f38768,f38766,f38764,f38762,f38760]) ).
fof(f38798,definition,
( spl402_1
<=> l3_lattices(sK27) ),
introduced(definition,[new_symbols(definition,[spl402_1])],[avatar_definition]) ).
fof(f38815,definition,
( spl402_4
<=> l3_lattices(sK28) ),
introduced(definition,[new_symbols(definition,[spl402_4])],[avatar_definition]) ).
fof(f38846,plain,
spl402_1,
inference(avatar_split_clause,[],[f36544,f38798]) ).
fof(f38852,plain,
spl402_4,
inference(avatar_split_clause,[],[f36547,f38815]) ).
fof(f38858,plain,
( ~ m1_filter_0(sK29,sK28)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) ),
inference(resolution,[],[f36555,f36552]) ).
fof(f38860,definition,
( spl402_9
<=> v10_lattices(sK28) ),
introduced(definition,[new_symbols(definition,[spl402_9])],[avatar_definition]) ).
fof(f38864,definition,
( spl402_10
<=> v3_struct_0(sK28) ),
introduced(definition,[new_symbols(definition,[spl402_10])],[avatar_definition]) ).
fof(f38868,definition,
( spl402_11
<=> m1_filter_0(sK29,sK28) ),
introduced(definition,[new_symbols(definition,[spl402_11])],[avatar_definition]) ).
fof(f38870,plain,
( ~ m1_filter_0(sK29,sK28)
| spl402_11 ),
inference(avatar_component_clause,[],[f38868]) ).
fof(f38871,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| ~ spl402_11 ),
inference(avatar_split_clause,[],[f38858,f38868,f38864,f38860,f38815]) ).
fof(f38951,definition,
( spl402_16
<=> v10_lattices(sK27) ),
introduced(definition,[new_symbols(definition,[spl402_16])],[avatar_definition]) ).
fof(f38955,definition,
( spl402_17
<=> v3_struct_0(sK27) ),
introduced(definition,[new_symbols(definition,[spl402_17])],[avatar_definition]) ).
fof(f38976,plain,
spl402_16,
inference(avatar_split_clause,[],[f36545,f38951]) ).
fof(f38979,plain,
~ spl402_17,
inference(avatar_split_clause,[],[f36546,f38955]) ).
fof(f38982,plain,
spl402_9,
inference(avatar_split_clause,[],[f36548,f38860]) ).
fof(f39006,plain,
~ spl402_10,
inference(avatar_split_clause,[],[f36549,f38864]) ).
fof(f39008,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(sF398,u2_lattices(sK28),u1_lattices(sK28))
| k1_lattice2(X0) = k1_lattice2(sK28)
| ~ l3_lattices(X0)
| ~ l3_lattices(sK28) ),
inference(superposition,[],[f36570,f38768]) ).
fof(f39039,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(sF398,u2_lattices(sK28),sF400)
| k1_lattice2(X0) = k1_lattice2(sK28)
| ~ l3_lattices(X0)
| ~ l3_lattices(sK28) ),
inference(forward_demodulation,[],[f39008,f38772]) ).
fof(f39051,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(sF398,sF399,sF400)
| k1_lattice2(X0) = k1_lattice2(sK28)
| ~ l3_lattices(X0)
| ~ l3_lattices(sK28) ),
inference(forward_demodulation,[],[f39039,f38770]) ).
fof(f39063,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != sF401
| k1_lattice2(X0) = k1_lattice2(sK28)
| ~ l3_lattices(X0)
| ~ l3_lattices(sK28) ),
inference(forward_demodulation,[],[f39051,f38774]) ).
fof(f39078,plain,
! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != sF397
| k1_lattice2(X0) = k1_lattice2(sK28)
| ~ l3_lattices(X0)
| ~ l3_lattices(sK28) ),
inference(forward_demodulation,[],[f39063,f38775]) ).
fof(f39081,definition,
( spl402_23
<=> ! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != sF397
| ~ l3_lattices(X0)
| k1_lattice2(X0) = k1_lattice2(sK28) ) ),
introduced(definition,[new_symbols(definition,[spl402_23])],[avatar_definition]) ).
fof(f39082,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != sF397
| ~ l3_lattices(X0)
| k1_lattice2(X0) = k1_lattice2(sK28) )
| ~ spl402_23 ),
inference(avatar_component_clause,[],[f39081]) ).
fof(f39088,plain,
( ~ spl402_4
| spl402_23 ),
inference(avatar_split_clause,[],[f39078,f39081,f38815]) ).
fof(f39109,plain,
( ~ v1_xboole_0(sK29)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) ),
inference(resolution,[],[f36558,f36551]) ).
fof(f39113,definition,
( spl402_26
<=> v1_xboole_0(sK29) ),
introduced(definition,[new_symbols(definition,[spl402_26])],[avatar_definition]) ).
fof(f39115,plain,
( ~ v1_xboole_0(sK29)
| spl402_26 ),
inference(avatar_component_clause,[],[f39113]) ).
fof(f39116,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_26 ),
inference(avatar_split_clause,[],[f39109,f39113,f38955,f38951,f38798]) ).
fof(f39117,plain,
( sF397 != g3_lattices(sF394,u2_lattices(sK27),u1_lattices(sK27))
| ~ l3_lattices(sK27)
| k1_lattice2(sK27) = k1_lattice2(sK28)
| ~ spl402_23 ),
inference(superposition,[],[f39082,f38760]) ).
fof(f39126,plain,
( sF397 != g3_lattices(sF394,u2_lattices(sK27),sF396)
| ~ l3_lattices(sK27)
| k1_lattice2(sK27) = k1_lattice2(sK28)
| ~ spl402_23 ),
inference(forward_demodulation,[],[f39117,f38764]) ).
fof(f39129,plain,
( g3_lattices(sF394,sF395,sF396) != sF397
| ~ l3_lattices(sK27)
| k1_lattice2(sK27) = k1_lattice2(sK28)
| ~ spl402_23 ),
inference(forward_demodulation,[],[f39126,f38762]) ).
fof(f39134,plain,
( sF397 != sF397
| ~ l3_lattices(sK27)
| k1_lattice2(sK27) = k1_lattice2(sK28)
| ~ spl402_23 ),
inference(forward_demodulation,[],[f39129,f38766]) ).
fof(f39135,plain,
( ~ l3_lattices(sK27)
| k1_lattice2(sK27) = k1_lattice2(sK28)
| ~ spl402_23 ),
inference(trivial_inequality_removal,[],[f39134]) ).
fof(f39137,definition,
( spl402_27
<=> k1_lattice2(sK27) = k1_lattice2(sK28) ),
introduced(definition,[new_symbols(definition,[spl402_27])],[avatar_definition]) ).
fof(f39139,plain,
( k1_lattice2(sK27) = k1_lattice2(sK28)
| ~ spl402_27 ),
inference(avatar_component_clause,[],[f39137]) ).
fof(f39142,plain,
( spl402_27
| ~ spl402_1
| ~ spl402_23 ),
inference(avatar_split_clause,[],[f39135,f39081,f38798,f39137]) ).
fof(f39146,plain,
( u1_struct_0(sK28) = u1_struct_0(k1_lattice2(sK27))
| v3_struct_0(sK28)
| ~ l3_lattices(sK28)
| ~ spl402_27 ),
inference(superposition,[],[f36585,f39139]) ).
fof(f39156,plain,
( sF398 = u1_struct_0(k1_lattice2(sK27))
| v3_struct_0(sK28)
| ~ l3_lattices(sK28)
| ~ spl402_27 ),
inference(forward_demodulation,[],[f39146,f38768]) ).
fof(f39172,definition,
( spl402_31
<=> sF398 = u1_struct_0(k1_lattice2(sK27)) ),
introduced(definition,[new_symbols(definition,[spl402_31])],[avatar_definition]) ).
fof(f39174,plain,
( sF398 = u1_struct_0(k1_lattice2(sK27))
| ~ spl402_31 ),
inference(avatar_component_clause,[],[f39172]) ).
fof(f39175,plain,
( ~ spl402_4
| spl402_10
| spl402_31
| ~ spl402_27 ),
inference(avatar_split_clause,[],[f39156,f39137,f39172,f38864,f38815]) ).
fof(f39179,plain,
( u1_struct_0(sK27) = sF398
| v3_struct_0(sK27)
| ~ l3_lattices(sK27)
| ~ spl402_31 ),
inference(superposition,[],[f39174,f36585]) ).
fof(f39218,plain,
( sF394 = sF398
| v3_struct_0(sK27)
| ~ l3_lattices(sK27)
| ~ spl402_31 ),
inference(forward_demodulation,[],[f39179,f38760]) ).
fof(f39236,definition,
( spl402_40
<=> sF394 = sF398 ),
introduced(definition,[new_symbols(definition,[spl402_40])],[avatar_definition]) ).
fof(f39238,plain,
( sF394 = sF398
| ~ spl402_40 ),
inference(avatar_component_clause,[],[f39236]) ).
fof(f39240,plain,
( ~ spl402_1
| spl402_17
| spl402_40
| ~ spl402_31 ),
inference(avatar_split_clause,[],[f39218,f39172,f39236,f38955,f38798]) ).
fof(f39517,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF394))
| ~ m2_lattice4(X0,sK27)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) ),
inference(superposition,[],[f36657,f38760]) ).
fof(f39523,definition,
( spl402_61
<=> ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF394))
| ~ m2_lattice4(X0,sK27) ) ),
introduced(definition,[new_symbols(definition,[spl402_61])],[avatar_definition]) ).
fof(f39524,plain,
( ! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF394))
| ~ m2_lattice4(X0,sK27) )
| ~ spl402_61 ),
inference(avatar_component_clause,[],[f39523]) ).
fof(f39525,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_61 ),
inference(avatar_split_clause,[],[f39517,f39523,f38955,f38951,f38798]) ).
fof(f40236,plain,
! [X0] :
( m1_subset_1(sK40(sK28,X0),sF398)
| m1_filter_0(X0,sK28)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF398))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) ),
inference(superposition,[],[f36619,f38768]) ).
fof(f40238,plain,
( ! [X0] :
( m1_subset_1(sK40(sK28,X0),sF394)
| m1_filter_0(X0,sK28)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF398))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40236,f39238]) ).
fof(f40244,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF394))
| m1_subset_1(sK40(sK28,X0),sF394)
| m1_filter_0(X0,sK28)
| v1_xboole_0(X0)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40238,f39238]) ).
fof(f40247,definition,
( spl402_112
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF394))
| v1_xboole_0(X0)
| m1_filter_0(X0,sK28)
| m1_subset_1(sK40(sK28,X0),sF394) ) ),
introduced(definition,[new_symbols(definition,[spl402_112])],[avatar_definition]) ).
fof(f40248,plain,
( ! [X0] :
( m1_subset_1(sK40(sK28,X0),sF394)
| v1_xboole_0(X0)
| m1_filter_0(X0,sK28)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF394)) )
| ~ spl402_112 ),
inference(avatar_component_clause,[],[f40247]) ).
fof(f40249,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_112
| ~ spl402_40 ),
inference(avatar_split_clause,[],[f40244,f39236,f40247,f38864,f38860,f38815]) ).
fof(f40262,plain,
! [X0] :
( m1_subset_1(sK41(sK28,X0),sF398)
| m1_filter_0(X0,sK28)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF398))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) ),
inference(superposition,[],[f36620,f38768]) ).
fof(f40264,plain,
( ! [X0] :
( m1_subset_1(sK41(sK28,X0),sF394)
| m1_filter_0(X0,sK28)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF398))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40262,f39238]) ).
fof(f40270,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF394))
| m1_subset_1(sK41(sK28,X0),sF394)
| m1_filter_0(X0,sK28)
| v1_xboole_0(X0)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40264,f39238]) ).
fof(f40273,definition,
( spl402_115
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF394))
| v1_xboole_0(X0)
| m1_filter_0(X0,sK28)
| m1_subset_1(sK41(sK28,X0),sF394) ) ),
introduced(definition,[new_symbols(definition,[spl402_115])],[avatar_definition]) ).
fof(f40274,plain,
( ! [X0] :
( m1_subset_1(sK41(sK28,X0),sF394)
| v1_xboole_0(X0)
| m1_filter_0(X0,sK28)
| ~ m1_subset_1(X0,k1_zfmisc_1(sF394)) )
| ~ spl402_115 ),
inference(avatar_component_clause,[],[f40273]) ).
fof(f40275,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_115
| ~ spl402_40 ),
inference(avatar_split_clause,[],[f40270,f39236,f40273,f38864,f38860,f38815]) ).
fof(f40281,plain,
! [X2,X3,X0,X1] :
( X0 != X1
| k4_lattices(X2,X0,X3) = k3_lattices(k1_lattice2(X2),X1,X3)
| ~ m1_subset_1(X3,u1_struct_0(k1_lattice2(X2)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X2)))
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X0,u1_struct_0(X2))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) ),
inference(equality_resolution,[],[f36853]) ).
fof(f40282,plain,
! [X2,X0,X1] :
( k4_lattices(X0,X1,X2) = k3_lattices(k1_lattice2(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f40281]) ).
fof(f40286,plain,
( ! [X0,X1] :
( k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK28))
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27 ),
inference(superposition,[],[f40282,f39139]) ).
fof(f40288,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF398)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK28))
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31 ),
inference(forward_demodulation,[],[f40286,f39174]) ).
fof(f40291,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK28))
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40288,f39238]) ).
fof(f40294,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF398)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK28))
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40291,f39174]) ).
fof(f40297,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK28))
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40294,f39238]) ).
fof(f40301,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF398)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40297,f38768]) ).
fof(f40304,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40301,f39238]) ).
fof(f40305,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK28))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(duplicate_literal_removal,[],[f40304]) ).
fof(f40310,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF398)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40305,f38768]) ).
fof(f40316,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(forward_demodulation,[],[f40310,f39238]) ).
fof(f40317,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28) )
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(duplicate_literal_removal,[],[f40316]) ).
fof(f40320,definition,
( spl402_118
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X1,sF394) ) ),
introduced(definition,[new_symbols(definition,[spl402_118])],[avatar_definition]) ).
fof(f40321,plain,
( ! [X0,X1] :
( k4_lattices(sK28,X0,X1) = k3_lattices(k1_lattice2(sK27),X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394) )
| ~ spl402_118 ),
inference(avatar_component_clause,[],[f40320]) ).
fof(f40322,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_118
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40 ),
inference(avatar_split_clause,[],[f40317,f39236,f39172,f39137,f40320,f38864,f38860,f38815]) ).
fof(f40329,plain,
( ! [X0,X1] :
( k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_118 ),
inference(superposition,[],[f40321,f40282]) ).
fof(f40332,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF398)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_118 ),
inference(forward_demodulation,[],[f40329,f39174]) ).
fof(f40335,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(forward_demodulation,[],[f40332,f39238]) ).
fof(f40336,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK27)))
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(duplicate_literal_removal,[],[f40335]) ).
fof(f40338,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF398)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(forward_demodulation,[],[f40336,f39174]) ).
fof(f40341,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(forward_demodulation,[],[f40338,f39238]) ).
fof(f40342,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(duplicate_literal_removal,[],[f40341]) ).
fof(f40345,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(forward_demodulation,[],[f40342,f38760]) ).
fof(f40346,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK27))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(duplicate_literal_removal,[],[f40345]) ).
fof(f40349,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(forward_demodulation,[],[f40346,f38760]) ).
fof(f40350,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(duplicate_literal_removal,[],[f40349]) ).
fof(f40352,definition,
( spl402_119
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X1,sF394) ) ),
introduced(definition,[new_symbols(definition,[spl402_119])],[avatar_definition]) ).
fof(f40353,plain,
( ! [X0,X1] :
( k4_lattices(sK28,X0,X1) = k4_lattices(sK27,X0,X1)
| ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,sF394) )
| ~ spl402_119 ),
inference(avatar_component_clause,[],[f40352]) ).
fof(f40355,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_119
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118 ),
inference(avatar_split_clause,[],[f40350,f40320,f39236,f39172,f40352,f38955,f38951,f38798]) ).
fof(f41171,plain,
( r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| r2_hidden(sK41(sK28,sK29),sK29)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28)))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| spl402_11 ),
inference(resolution,[],[f36621,f38870]) ).
fof(f41174,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF398))
| r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| r2_hidden(sK41(sK28,sK29),sK29)
| v1_xboole_0(sK29)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| spl402_11 ),
inference(forward_demodulation,[],[f41171,f38768]) ).
fof(f41175,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| r2_hidden(sK41(sK28,sK29),sK29)
| v1_xboole_0(sK29)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| spl402_11
| ~ spl402_40 ),
inference(forward_demodulation,[],[f41174,f39238]) ).
fof(f41177,definition,
( spl402_170
<=> r2_hidden(sK41(sK28,sK29),sK29) ),
introduced(definition,[new_symbols(definition,[spl402_170])],[avatar_definition]) ).
fof(f41179,plain,
( r2_hidden(sK41(sK28,sK29),sK29)
| ~ spl402_170 ),
inference(avatar_component_clause,[],[f41177]) ).
fof(f41181,definition,
( spl402_171
<=> r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29) ),
introduced(definition,[new_symbols(definition,[spl402_171])],[avatar_definition]) ).
fof(f41182,plain,
( ~ r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| spl402_171 ),
inference(avatar_component_clause,[],[f41181]) ).
fof(f41183,plain,
( r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ spl402_171 ),
inference(avatar_component_clause,[],[f41181]) ).
fof(f41185,definition,
( spl402_172
<=> m1_subset_1(sK29,k1_zfmisc_1(sF394)) ),
introduced(definition,[new_symbols(definition,[spl402_172])],[avatar_definition]) ).
fof(f41187,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| spl402_172 ),
inference(avatar_component_clause,[],[f41185]) ).
fof(f41188,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_26
| spl402_170
| spl402_171
| ~ spl402_172
| spl402_11
| ~ spl402_40 ),
inference(avatar_split_clause,[],[f41175,f39236,f38868,f41185,f41181,f41177,f39113,f38864,f38860,f38815]) ).
fof(f41189,plain,
( ~ m2_lattice4(sK29,sK27)
| ~ spl402_61
| spl402_172 ),
inference(resolution,[],[f41187,f39524]) ).
fof(f41200,plain,
( ~ m1_filter_0(sK29,sK27)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ spl402_61
| spl402_172 ),
inference(resolution,[],[f41189,f36658]) ).
fof(f41203,definition,
( spl402_173
<=> m1_filter_2(sK29,sK27) ),
introduced(definition,[new_symbols(definition,[spl402_173])],[avatar_definition]) ).
fof(f41204,plain,
( m1_filter_2(sK29,sK27)
| ~ spl402_173 ),
inference(avatar_component_clause,[],[f41203]) ).
fof(f41208,definition,
( spl402_174
<=> m1_filter_0(sK29,sK27) ),
introduced(definition,[new_symbols(definition,[spl402_174])],[avatar_definition]) ).
fof(f41210,plain,
( ~ m1_filter_0(sK29,sK27)
| spl402_174 ),
inference(avatar_component_clause,[],[f41208]) ).
fof(f41211,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_174
| ~ spl402_61
| spl402_172 ),
inference(avatar_split_clause,[],[f41200,f41185,f39523,f41208,f38955,f38951,f38798]) ).
fof(f41225,plain,
( ~ m1_filter_2(sK29,sK27)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| spl402_174 ),
inference(resolution,[],[f41210,f36554]) ).
fof(f41226,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_173
| spl402_174 ),
inference(avatar_split_clause,[],[f41225,f41208,f41203,f38955,f38951,f38798]) ).
fof(f41232,plain,
spl402_173,
inference(avatar_split_clause,[],[f36551,f41203]) ).
fof(f41233,plain,
( ~ r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ r2_hidden(sK40(sK28,sK29),sK29)
| m1_filter_0(sK29,sK28)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28)))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| ~ spl402_170 ),
inference(resolution,[],[f41179,f36623]) ).
fof(f41235,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF398))
| ~ r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ r2_hidden(sK40(sK28,sK29),sK29)
| m1_filter_0(sK29,sK28)
| v1_xboole_0(sK29)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| ~ spl402_170 ),
inference(forward_demodulation,[],[f41233,f38768]) ).
fof(f41236,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ r2_hidden(sK40(sK28,sK29),sK29)
| m1_filter_0(sK29,sK28)
| v1_xboole_0(sK29)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| ~ spl402_40
| ~ spl402_170 ),
inference(forward_demodulation,[],[f41235,f39238]) ).
fof(f41238,definition,
( spl402_177
<=> r2_hidden(sK40(sK28,sK29),sK29) ),
introduced(definition,[new_symbols(definition,[spl402_177])],[avatar_definition]) ).
fof(f41240,plain,
( ~ r2_hidden(sK40(sK28,sK29),sK29)
| spl402_177 ),
inference(avatar_component_clause,[],[f41238]) ).
fof(f41241,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_26
| spl402_11
| ~ spl402_177
| ~ spl402_171
| ~ spl402_172
| ~ spl402_40
| ~ spl402_170 ),
inference(avatar_split_clause,[],[f41236,f41177,f39236,f41185,f41181,f41238,f38868,f39113,f38864,f38860,f38815]) ).
fof(f41245,plain,
( ~ r2_hidden(k4_lattices(sK27,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ m1_subset_1(sK40(sK28,sK29),sF394)
| ~ m1_subset_1(sK41(sK28,sK29),sF394)
| ~ spl402_119
| spl402_171 ),
inference(superposition,[],[f41182,f40353]) ).
fof(f41247,definition,
( spl402_178
<=> m1_subset_1(sK41(sK28,sK29),sF394) ),
introduced(definition,[new_symbols(definition,[spl402_178])],[avatar_definition]) ).
fof(f41249,plain,
( ~ m1_subset_1(sK41(sK28,sK29),sF394)
| spl402_178 ),
inference(avatar_component_clause,[],[f41247]) ).
fof(f41251,definition,
( spl402_179
<=> m1_subset_1(sK40(sK28,sK29),sF394) ),
introduced(definition,[new_symbols(definition,[spl402_179])],[avatar_definition]) ).
fof(f41253,plain,
( ~ m1_subset_1(sK40(sK28,sK29),sF394)
| spl402_179 ),
inference(avatar_component_clause,[],[f41251]) ).
fof(f41255,definition,
( spl402_180
<=> r2_hidden(k4_lattices(sK27,sK40(sK28,sK29),sK41(sK28,sK29)),sK29) ),
introduced(definition,[new_symbols(definition,[spl402_180])],[avatar_definition]) ).
fof(f41256,plain,
( r2_hidden(k4_lattices(sK27,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ spl402_180 ),
inference(avatar_component_clause,[],[f41255]) ).
fof(f41257,plain,
( ~ r2_hidden(k4_lattices(sK27,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| spl402_180 ),
inference(avatar_component_clause,[],[f41255]) ).
fof(f41258,plain,
( ~ spl402_178
| ~ spl402_179
| ~ spl402_180
| ~ spl402_119
| spl402_171 ),
inference(avatar_split_clause,[],[f41245,f41181,f40352,f41255,f41251,f41247]) ).
fof(f41265,plain,
( v1_xboole_0(sK29)
| m1_filter_0(sK29,sK28)
| ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ spl402_115
| spl402_178 ),
inference(resolution,[],[f41249,f40274]) ).
fof(f41274,plain,
( ~ spl402_172
| spl402_11
| spl402_26
| ~ spl402_115
| spl402_178 ),
inference(avatar_split_clause,[],[f41265,f41247,f40273,f39113,f38868,f41185]) ).
fof(f41275,plain,
( v1_xboole_0(sK29)
| m1_filter_0(sK29,sK28)
| ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ spl402_112
| spl402_179 ),
inference(resolution,[],[f41253,f40248]) ).
fof(f41284,plain,
( ~ spl402_172
| spl402_11
| spl402_26
| ~ spl402_112
| spl402_179 ),
inference(avatar_split_clause,[],[f41275,f41251,f40247,f39113,f38868,f41185]) ).
fof(f41752,plain,
( ! [X2,X0,X1] :
( ~ m1_filter_0(sK29,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r2_hidden(k4_lattices(X0,X1,X2),sK29)
| r2_hidden(X1,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl402_26 ),
inference(resolution,[],[f36618,f39115]) ).
fof(f41757,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r2_hidden(k4_lattices(X1,X2,X0),sK29)
| r2_hidden(X2,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_filter_2(sK29,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| spl402_26 ),
inference(resolution,[],[f41752,f36554]) ).
fof(f41758,plain,
( ! [X2,X0,X1] :
( ~ m1_filter_2(sK29,X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r2_hidden(k4_lattices(X1,X2,X0),sK29)
| r2_hidden(X2,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1)) )
| spl402_26 ),
inference(duplicate_literal_removal,[],[f41757]) ).
fof(f41772,definition,
( spl402_220
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| r2_hidden(X1,sK29)
| ~ r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ m1_subset_1(X0,sF394) ) ),
introduced(definition,[new_symbols(definition,[spl402_220])],[avatar_definition]) ).
fof(f41773,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| r2_hidden(X1,sK29)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394) )
| ~ spl402_220 ),
inference(avatar_component_clause,[],[f41772]) ).
fof(f41781,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK27))
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X0,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ m1_subset_1(X1,u1_struct_0(sK27)) )
| spl402_26
| ~ spl402_173 ),
inference(resolution,[],[f41758,f41204]) ).
fof(f41786,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X0,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ m1_subset_1(X1,u1_struct_0(sK27)) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f41781,f38760]) ).
fof(f41788,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X0,sK29)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ m1_subset_1(X1,u1_struct_0(sK27)) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f41786,f38760]) ).
fof(f41790,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X0,sK29)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f41788,f38760]) ).
fof(f41792,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_172
| spl402_220
| spl402_26
| ~ spl402_173 ),
inference(avatar_split_clause,[],[f41790,f41203,f39113,f41772,f41185,f38955,f38951,f38798]) ).
fof(f42058,plain,
( ! [X2,X0,X1] :
( ~ m1_filter_0(sK29,X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r2_hidden(k4_lattices(X0,X1,X2),sK29)
| r2_hidden(X2,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl402_26 ),
inference(resolution,[],[f36617,f39115]) ).
fof(f42063,plain,
( ! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r2_hidden(k4_lattices(X1,X2,X0),sK29)
| r2_hidden(X0,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_filter_2(sK29,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| spl402_26 ),
inference(resolution,[],[f42058,f36554]) ).
fof(f42064,plain,
( ! [X2,X0,X1] :
( ~ m1_filter_2(sK29,X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r2_hidden(k4_lattices(X1,X2,X0),sK29)
| r2_hidden(X0,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1)) )
| spl402_26 ),
inference(duplicate_literal_removal,[],[f42063]) ).
fof(f42078,definition,
( spl402_243
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| r2_hidden(X0,sK29)
| ~ r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ m1_subset_1(X0,sF394) ) ),
introduced(definition,[new_symbols(definition,[spl402_243])],[avatar_definition]) ).
fof(f42079,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| r2_hidden(X0,sK29)
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394) )
| ~ spl402_243 ),
inference(avatar_component_clause,[],[f42078]) ).
fof(f42087,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK27))
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X1,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ m1_subset_1(X1,u1_struct_0(sK27)) )
| spl402_26
| ~ spl402_173 ),
inference(resolution,[],[f42064,f41204]) ).
fof(f42092,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X1,sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ m1_subset_1(X1,u1_struct_0(sK27)) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f42087,f38760]) ).
fof(f42094,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X1,sK29)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ m1_subset_1(X1,u1_struct_0(sK27)) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f42092,f38760]) ).
fof(f42096,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(k4_lattices(sK27,X0,X1),sK29)
| r2_hidden(X1,sK29)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f42094,f38760]) ).
fof(f42098,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_172
| spl402_243
| spl402_26
| ~ spl402_173 ),
inference(avatar_split_clause,[],[f42096,f41203,f39113,f42078,f41185,f38955,f38951,f38798]) ).
fof(f42715,plain,
( ! [X2,X0,X1] :
( ~ m1_filter_0(sK29,X2)
| ~ r2_hidden(X1,sK29)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ r2_hidden(X0,sK29)
| r2_hidden(k4_lattices(X2,X0,X1),sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X2)))
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2) )
| spl402_26 ),
inference(resolution,[],[f36610,f39115]) ).
fof(f42720,plain,
( ! [X2,X0,X1] :
( ~ r2_hidden(X0,sK29)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r2_hidden(X2,sK29)
| r2_hidden(k4_lattices(X1,X2,X0),sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_filter_2(sK29,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| spl402_26 ),
inference(resolution,[],[f42715,f36554]) ).
fof(f42721,plain,
( ! [X2,X0,X1] :
( ~ m1_filter_2(sK29,X1)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r2_hidden(X2,sK29)
| r2_hidden(k4_lattices(X1,X2,X0),sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r2_hidden(X0,sK29) )
| spl402_26 ),
inference(duplicate_literal_removal,[],[f42720]) ).
fof(f42735,definition,
( spl402_297
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ r2_hidden(X1,sK29)
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(X0,sK29) ) ),
introduced(definition,[new_symbols(definition,[spl402_297])],[avatar_definition]) ).
fof(f42736,plain,
( ! [X0,X1] :
( r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ m1_subset_1(X1,sF394)
| ~ r2_hidden(X1,sK29)
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(X0,sK29) )
| ~ spl402_297 ),
inference(avatar_component_clause,[],[f42735]) ).
fof(f42744,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK27))
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ r2_hidden(X1,sK29)
| r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ r2_hidden(X0,sK29) )
| spl402_26
| ~ spl402_173 ),
inference(resolution,[],[f42721,f41204]) ).
fof(f42749,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF394)
| ~ m1_subset_1(X1,u1_struct_0(sK27))
| ~ r2_hidden(X1,sK29)
| r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ r2_hidden(X0,sK29) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f42744,f38760]) ).
fof(f42751,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(X1,sK29)
| r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK27)))
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ r2_hidden(X0,sK29) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f42749,f38760]) ).
fof(f42753,plain,
( ! [X0,X1] :
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| ~ m1_subset_1(X1,sF394)
| ~ m1_subset_1(X0,sF394)
| ~ r2_hidden(X1,sK29)
| r2_hidden(k4_lattices(sK27,X1,X0),sK29)
| v3_struct_0(sK27)
| ~ v10_lattices(sK27)
| ~ l3_lattices(sK27)
| ~ r2_hidden(X0,sK29) )
| spl402_26
| ~ spl402_173 ),
inference(forward_demodulation,[],[f42751,f38760]) ).
fof(f42755,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_297
| ~ spl402_172
| spl402_26
| ~ spl402_173 ),
inference(avatar_split_clause,[],[f42753,f41203,f39113,f41185,f42735,f38955,f38951,f38798]) ).
fof(f42759,plain,
( ~ m1_subset_1(sK40(sK28,sK29),sF394)
| ~ r2_hidden(sK40(sK28,sK29),sK29)
| ~ m1_subset_1(sK41(sK28,sK29),sF394)
| ~ r2_hidden(sK41(sK28,sK29),sK29)
| spl402_180
| ~ spl402_297 ),
inference(resolution,[],[f42736,f41257]) ).
fof(f42767,plain,
( ~ spl402_170
| ~ spl402_178
| ~ spl402_177
| ~ spl402_179
| spl402_180
| ~ spl402_297 ),
inference(avatar_split_clause,[],[f42759,f42735,f41255,f41251,f41238,f41247,f41177]) ).
fof(f42768,plain,
( r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| m1_filter_0(sK29,sK28)
| v1_xboole_0(sK29)
| ~ m1_subset_1(sK29,k1_zfmisc_1(u1_struct_0(sK28)))
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| spl402_177 ),
inference(resolution,[],[f41240,f36622]) ).
fof(f42777,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF398))
| r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| m1_filter_0(sK29,sK28)
| v1_xboole_0(sK29)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| spl402_177 ),
inference(forward_demodulation,[],[f42768,f38768]) ).
fof(f42778,plain,
( ~ m1_subset_1(sK29,k1_zfmisc_1(sF394))
| r2_hidden(k4_lattices(sK28,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| m1_filter_0(sK29,sK28)
| v1_xboole_0(sK29)
| v3_struct_0(sK28)
| ~ v10_lattices(sK28)
| ~ l3_lattices(sK28)
| ~ spl402_40
| spl402_177 ),
inference(forward_demodulation,[],[f42777,f39238]) ).
fof(f42779,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_26
| spl402_11
| spl402_171
| ~ spl402_172
| ~ spl402_40
| spl402_177 ),
inference(avatar_split_clause,[],[f42778,f41238,f39236,f41185,f41181,f38868,f39113,f38864,f38860,f38815]) ).
fof(f42812,plain,
( r2_hidden(k4_lattices(sK27,sK40(sK28,sK29),sK41(sK28,sK29)),sK29)
| ~ m1_subset_1(sK40(sK28,sK29),sF394)
| ~ m1_subset_1(sK41(sK28,sK29),sF394)
| ~ spl402_119
| ~ spl402_171 ),
inference(superposition,[],[f41183,f40353]) ).
fof(f42813,plain,
( ~ spl402_178
| ~ spl402_179
| spl402_180
| ~ spl402_119
| ~ spl402_171 ),
inference(avatar_split_clause,[],[f42812,f41181,f40352,f41255,f41251,f41247]) ).
fof(f42815,plain,
( r2_hidden(sK41(sK28,sK29),sK29)
| ~ m1_subset_1(sK40(sK28,sK29),sF394)
| ~ m1_subset_1(sK41(sK28,sK29),sF394)
| ~ spl402_180
| ~ spl402_243 ),
inference(resolution,[],[f41256,f42079]) ).
fof(f42816,plain,
( r2_hidden(sK40(sK28,sK29),sK29)
| ~ m1_subset_1(sK40(sK28,sK29),sF394)
| ~ m1_subset_1(sK41(sK28,sK29),sF394)
| ~ spl402_180
| ~ spl402_220 ),
inference(resolution,[],[f41256,f41773]) ).
fof(f42818,plain,
( ~ spl402_178
| ~ spl402_179
| spl402_177
| ~ spl402_180
| ~ spl402_220 ),
inference(avatar_split_clause,[],[f42816,f41772,f41255,f41238,f41251,f41247]) ).
fof(f42819,plain,
( ~ spl402_178
| ~ spl402_179
| spl402_170
| ~ spl402_180
| ~ spl402_243 ),
inference(avatar_split_clause,[],[f42815,f42078,f41255,f41177,f41251,f41247]) ).
cnf(s7,plain,
spl402_1,
inference(sat_conversion,[],[f38846]) ).
cnf(s10,plain,
spl402_4,
inference(sat_conversion,[],[f38852]) ).
cnf(s13,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| ~ spl402_11 ),
inference(sat_conversion,[],[f38871]) ).
cnf(s27,plain,
spl402_16,
inference(sat_conversion,[],[f38976]) ).
cnf(s29,plain,
~ spl402_17,
inference(sat_conversion,[],[f38979]) ).
cnf(s31,plain,
spl402_9,
inference(sat_conversion,[],[f38982]) ).
cnf(s37,plain,
~ spl402_10,
inference(sat_conversion,[],[f39006]) ).
cnf(s49,plain,
( ~ spl402_4
| spl402_23 ),
inference(sat_conversion,[],[f39088]) ).
cnf(s54,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_26 ),
inference(sat_conversion,[],[f39116]) ).
cnf(s57,plain,
( ~ spl402_1
| ~ spl402_23
| spl402_27 ),
inference(sat_conversion,[],[f39142]) ).
cnf(s59,plain,
( ~ spl402_4
| spl402_10
| ~ spl402_27
| spl402_31 ),
inference(sat_conversion,[],[f39175]) ).
cnf(s69,plain,
( ~ spl402_1
| spl402_17
| ~ spl402_31
| spl402_40 ),
inference(sat_conversion,[],[f39240]) ).
cnf(s100,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_61 ),
inference(sat_conversion,[],[f39525]) ).
cnf(s200,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| ~ spl402_40
| spl402_112 ),
inference(sat_conversion,[],[f40249]) ).
cnf(s203,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| ~ spl402_40
| spl402_115 ),
inference(sat_conversion,[],[f40275]) ).
cnf(s206,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| ~ spl402_27
| ~ spl402_31
| ~ spl402_40
| spl402_118 ),
inference(sat_conversion,[],[f40322]) ).
cnf(s209,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_31
| ~ spl402_40
| ~ spl402_118
| spl402_119 ),
inference(sat_conversion,[],[f40355]) ).
cnf(s279,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_11
| spl402_26
| ~ spl402_40
| spl402_170
| spl402_171
| ~ spl402_172 ),
inference(sat_conversion,[],[f41188]) ).
cnf(s281,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_61
| spl402_172
| ~ spl402_174 ),
inference(sat_conversion,[],[f41211]) ).
cnf(s284,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| ~ spl402_173
| spl402_174 ),
inference(sat_conversion,[],[f41226]) ).
cnf(s287,plain,
spl402_173,
inference(sat_conversion,[],[f41232]) ).
cnf(s288,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_11
| spl402_26
| ~ spl402_40
| ~ spl402_170
| ~ spl402_171
| ~ spl402_172
| ~ spl402_177 ),
inference(sat_conversion,[],[f41241]) ).
cnf(s289,plain,
( ~ spl402_119
| spl402_171
| ~ spl402_178
| ~ spl402_179
| ~ spl402_180 ),
inference(sat_conversion,[],[f41258]) ).
cnf(s291,plain,
( spl402_11
| spl402_26
| ~ spl402_115
| ~ spl402_172
| spl402_178 ),
inference(sat_conversion,[],[f41274]) ).
cnf(s292,plain,
( spl402_11
| spl402_26
| ~ spl402_112
| ~ spl402_172
| spl402_179 ),
inference(sat_conversion,[],[f41284]) ).
cnf(s346,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_26
| ~ spl402_172
| ~ spl402_173
| spl402_220 ),
inference(sat_conversion,[],[f41792]) ).
cnf(s379,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_26
| ~ spl402_172
| ~ spl402_173
| spl402_243 ),
inference(sat_conversion,[],[f42098]) ).
cnf(s443,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_26
| ~ spl402_172
| ~ spl402_173
| spl402_297 ),
inference(sat_conversion,[],[f42755]) ).
cnf(s445,plain,
( ~ spl402_170
| ~ spl402_177
| ~ spl402_178
| ~ spl402_179
| spl402_180
| ~ spl402_297 ),
inference(sat_conversion,[],[f42767]) ).
cnf(s447,plain,
( ~ spl402_4
| ~ spl402_9
| spl402_10
| spl402_11
| spl402_26
| ~ spl402_40
| spl402_171
| ~ spl402_172
| spl402_177 ),
inference(sat_conversion,[],[f42779]) ).
cnf(s452,plain,
( ~ spl402_119
| ~ spl402_171
| ~ spl402_178
| ~ spl402_179
| spl402_180 ),
inference(sat_conversion,[],[f42813]) ).
cnf(s454,plain,
( spl402_177
| ~ spl402_178
| ~ spl402_179
| ~ spl402_180
| ~ spl402_220 ),
inference(sat_conversion,[],[f42818]) ).
cnf(s455,plain,
( spl402_170
| ~ spl402_178
| ~ spl402_179
| ~ spl402_180
| ~ spl402_243 ),
inference(sat_conversion,[],[f42819]) ).
cnf(s456,plain,
( ~ spl402_1
| ~ spl402_16
| spl402_17
| spl402_174 ),
inference(rat,[],[s284,s287]) ).
cnf(s466,plain,
( ~ spl402_4
| ~ spl402_11 ),
inference(rat,[],[s13,s37,s31]) ).
cnf(s469,plain,
spl402_23,
inference(rat,[],[s49,s10]) ).
cnf(s472,plain,
~ spl402_11,
inference(rat,[],[s466,s10]) ).
cnf(s481,plain,
spl402_174,
inference(rat,[],[s456,s27,s29,s7]) ).
cnf(s499,plain,
spl402_61,
inference(rat,[],[s100,s27,s29,s7]) ).
cnf(s502,plain,
spl402_27,
inference(rat,[],[s57,s469,s7]) ).
cnf(s503,plain,
~ spl402_26,
inference(rat,[],[s54,s27,s29,s7]) ).
cnf(s510,plain,
spl402_172,
inference(rat,[],[s281,s481,s7,s27,s29,s499]) ).
cnf(s519,plain,
spl402_31,
inference(rat,[],[s59,s10,s37,s502]) ).
cnf(s526,plain,
spl402_297,
inference(rat,[],[s443,s503,s287,s7,s27,s29,s510]) ).
cnf(s527,plain,
spl402_243,
inference(rat,[],[s379,s503,s287,s7,s27,s29,s510]) ).
cnf(s528,plain,
spl402_220,
inference(rat,[],[s346,s503,s287,s7,s27,s29,s510]) ).
cnf(s533,plain,
spl402_40,
inference(rat,[],[s69,s7,s29,s519]) ).
cnf(s558,plain,
spl402_115,
inference(rat,[],[s203,s10,s31,s37,s533]) ).
cnf(s559,plain,
spl402_112,
inference(rat,[],[s200,s10,s31,s37,s533]) ).
cnf(s588,plain,
spl402_118,
inference(rat,[],[s206,s519,s502,s10,s31,s37,s533]) ).
cnf(s647,plain,
spl402_178,
inference(rat,[],[s291,s503,s510,s472,s558]) ).
cnf(s648,plain,
spl402_179,
inference(rat,[],[s292,s503,s510,s472,s559]) ).
cnf(s656,plain,
spl402_119,
inference(rat,[],[s209,s533,s519,s7,s27,s29,s588]) ).
cnf(s668,plain,
spl402_170,
inference(rat,[],[s452,s279,s455,s647,s648,s656,s37,s31,s10,s472,s503,s533,s510,s527]) ).
cnf(s669,plain,
~ spl402_171,
inference(rat,[],[s454,s288,s452,s648,s647,s528,s37,s31,s10,s472,s503,s533,s510,s668,s656]) ).
cnf(s671,plain,
~ spl402_180,
inference(rat,[],[s289,s656,s648,s647,s669]) ).
cnf(s672,plain,
spl402_177,
inference(rat,[],[s447,s533,s510,s503,s472,s10,s31,s37,s669]) ).
cnf(s674,plain,
$false,
inference(rat,[],[s445,s526,s668,s648,s647,s671,s672]) ).
fof(f42820,plain,
$false,
inference(avatar_sat_refutation,[],[s674]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT298+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 % Computer : n026.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 14:24:45 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.46 Running first-order theorem proving
% 0.15/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.70/4.67 % (2893237)Detected formulas, will run a generic FOF schedule.
% 18.70/4.67 % (2893250)dis-21_1_sil=8000:lcm=predicate:random_seed=2562188160:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2987 on theBenchmark for (2987ds/129Mi)
% 18.70/4.67 % (2893250)Instruction limit reached!
% 18.70/4.67 % (2893250)------------------------------
% 18.70/4.67 % (2893250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/4.67 % (2893250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/4.67 % (2893250)CaDiCaL version: 2.1.3
% 18.70/4.67 % (2893250)Termination reason: Instruction limit
% 18.70/4.67 % (2893250)Termination phase: SInE selection
% 18.70/4.67 % (2893250)Time elapsed: 0.057 s
% 18.70/4.67 % (2893250)Peak memory usage: 136 MB
% 18.70/4.67 % (2893250)Instructions burned: 131 (million)
% 18.70/4.67 % (2893247)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3717706793:i=109:sd=1:ins=1:gsp=on:ss=axioms_2987 on theBenchmark for (2987ds/109Mi)
% 18.70/4.67 % (2893248)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3521109015:i=119:av=off:ss=axioms_2987 on theBenchmark for (2987ds/119Mi)
% 18.70/4.67 % (2893244)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=2571752609:i=141193_2987 on theBenchmark for (2987ds/141193Mi)
% 18.70/4.67 % (2893245)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=2634423510:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2987 on theBenchmark for (2987ds/134677Mi)
% 18.70/4.67 % (2893246)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=2877036551:i=141695:sd=1:nm=32:gsp=on:ss=included_2987 on theBenchmark for (2987ds/141695Mi)
% 18.70/4.67 % (2893249)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3857424543:s2a=on:i=139:gtg=position_2987 on theBenchmark for (2987ds/139Mi)
% 18.70/4.67 % (2893252)lrs+10_1_sil=8000:sp=occurrence:random_seed=854392346:i=285:sd=3:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/285Mi)
% 18.70/4.67 % (2893247)Instruction limit reached!
% 18.70/4.67 % (2893247)------------------------------
% 18.70/4.67 % (2893247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/4.67 % (2893247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/4.67 % (2893247)CaDiCaL version: 2.1.3
% 18.70/4.67 % (2893247)Termination reason: Instruction limit
% 18.70/4.67 % (2893247)Termination phase: SInE selection
% 18.70/4.67 % (2893247)Time elapsed: 0.098 s
% 18.70/4.67 % (2893247)Peak memory usage: 136 MB
% 18.70/4.67 % (2893247)Instructions burned: 110 (million)
% 18.70/4.67 % (2893249)Instruction limit reached!
% 18.70/4.67 % (2893249)------------------------------
% 18.70/4.67 % (2893249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/4.67 % (2893249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/4.67 % (2893249)CaDiCaL version: 2.1.3
% 18.70/4.67 % (2893249)Termination reason: Instruction limit
% 18.70/4.67 % (2893249)Termination phase: Property scanning
% 18.70/4.67 % (2893249)Time elapsed: 0.114 s
% 18.70/4.67 % (2893249)Peak memory usage: 136 MB
% 18.70/4.67 % (2893249)Instructions burned: 139 (million)
% 18.70/4.67 % (2893248)Instruction limit reached!
% 18.70/4.67 % (2893248)------------------------------
% 18.70/4.67 % (2893248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/4.67 % (2893248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/4.67 % (2893248)CaDiCaL version: 2.1.3
% 18.70/4.67 % (2893248)Termination reason: Instruction limit
% 18.70/4.67 % (2893248)Termination phase: SInE selection
% 18.70/4.67 % (2893248)Time elapsed: 0.123 s
% 18.70/4.67 % (2893248)Peak memory usage: 136 MB
% 18.70/4.67 % (2893248)Instructions burned: 119 (million)
% 18.70/4.67 % (2893252)Instruction limit reached!
% 18.70/4.67 % (2893252)------------------------------
% 18.70/4.67 % (2893252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.70/4.67 % (2893252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.70/4.67 % (2893252)CaDiCaL version: 2.1.3
% 18.70/4.67 % (2893252)Termination reason: Instruction limit
% 18.70/4.67 % (2893252)Termination phase: Saturation
% 18.70/4.67 % (2893252)Time elapsed: 0.186 s
% 18.70/4.67 % (2893252)Peak memory usage: 142 MB
% 18.70/4.67 % (2893252)Instructions burned: 285 (million)
% 26.53/5.79 % (2893262)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=567279658:s2a=on:i=248:s2at=1.23:gtg=position_2983 on theBenchmark for (2983ds/248Mi)
% 26.53/5.79 % (2893260)lrs+10_1_sil=32000:urr=on:br=off:random_seed=273233496:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/157Mi)
% 26.53/5.79 % (2893261)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2210604141:i=325:sd=1:ss=axioms:sgt=32_2983 on theBenchmark for (2983ds/325Mi)
% 26.53/5.79 % (2893262)Instruction limit reached!
% 26.53/5.79 % (2893262)------------------------------
% 26.53/5.79 % (2893262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/5.79 % (2893262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/5.79 % (2893262)CaDiCaL version: 2.1.3
% 26.53/5.79 % (2893262)Termination reason: Instruction limit
% 26.53/5.79 % (2893262)Termination phase: Property scanning
% 26.53/5.79 % (2893262)Time elapsed: 0.122 s
% 26.53/5.79 % (2893262)Peak memory usage: 137 MB
% 26.53/5.79 % (2893262)Instructions burned: 250 (million)
% 26.53/5.79 % (2893260)Instruction limit reached!
% 26.53/5.79 % (2893260)------------------------------
% 26.53/5.79 % (2893260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/5.79 % (2893260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/5.79 % (2893260)CaDiCaL version: 2.1.3
% 26.53/5.79 % (2893260)Termination reason: Instruction limit
% 26.53/5.79 % (2893260)Termination phase: Property scanning
% 26.53/5.79 % (2893260)Time elapsed: 0.137 s
% 26.53/5.79 % (2893260)Peak memory usage: 136 MB
% 26.53/5.79 % (2893260)Instructions burned: 158 (million)
% 26.53/5.79 % (2893264)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2245262751:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2982 on theBenchmark for (2982ds/294Mi)
% 26.53/5.79 % (2893267)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2089381669:i=2350_2981 on theBenchmark for (2981ds/2350Mi)
% 26.53/5.79 % (2893261)Refutation not found, incomplete strategy
% 26.53/5.79 % (2893261)------------------------------
% 26.53/5.79 % (2893261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/5.79 % (2893261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/5.79 % (2893261)CaDiCaL version: 2.1.3
% 26.53/5.79 % (2893261)Termination reason: Refutation not found, incomplete strategy
% 26.53/5.79 % (2893261)Time elapsed: 0.276 s
% 26.53/5.79 % (2893261)Peak memory usage: 142 MB
% 26.53/5.79 % (2893261)Instructions burned: 240 (million)
% 26.53/5.79 % (2893268)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1831840713:cts=off:i=113:fsr=off:ss=included:sgt=4_2980 on theBenchmark for (2980ds/113Mi)
% 26.53/5.79 % (2893268)Instruction limit reached!
% 26.53/5.79 % (2893268)------------------------------
% 26.53/5.79 % (2893268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/5.79 % (2893268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/5.79 % (2893268)CaDiCaL version: 2.1.3
% 26.53/5.79 % (2893268)Termination reason: Instruction limit
% 26.53/5.79 % (2893268)Termination phase: SInE selection
% 26.53/5.79 % (2893268)Time elapsed: 0.121 s
% 26.53/5.79 % (2893268)Peak memory usage: 136 MB
% 26.53/5.79 % (2893268)Instructions burned: 114 (million)
% 26.53/5.79 % (2893264)Instruction limit reached!
% 26.53/5.79 % (2893264)------------------------------
% 26.53/5.79 % (2893264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.53/5.79 % (2893264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.53/5.79 % (2893264)CaDiCaL version: 2.1.3
% 26.53/5.79 % (2893264)Termination reason: Instruction limit
% 26.53/5.79 % (2893264)Termination phase: SInE selection
% 26.53/5.79 % (2893264)Time elapsed: 0.289 s
% 26.53/5.79 % (2893264)Peak memory usage: 137 MB
% 26.53/5.79 % (2893264)Instructions burned: 294 (million)
% 26.53/5.79 % (2893272)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1326731222:i=127:av=off:fsr=off:sup=off_2977 on theBenchmark for (2977ds/127Mi)
% 26.53/5.79 % (2893273)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1565506437:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2977 on theBenchmark for (2977ds/114Mi)
% 26.53/5.79 % (2893261)------------------------------
% 26.53/5.79 % (2893261)------------------------------
% 26.53/5.79 % (2893273)Instruction limit reached!
% 26.53/5.79 % (2893273)------------------------------
% 69.27/11.76 % (2893273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.27/11.76 % (2893273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.27/11.76 % (2893273)CaDiCaL version: 2.1.3
% 69.27/11.76 % (2893273)Termination reason: Instruction limit
% 69.27/11.76 % (2893273)Termination phase: Property scanning
% 69.27/11.76 % (2893273)Time elapsed: 0.099 s
% 69.27/11.76 % (2893273)Peak memory usage: 136 MB
% 69.27/11.76 % (2893273)Instructions burned: 114 (million)
% 69.27/11.76 % (2893272)Instruction limit reached!
% 69.27/11.76 % (2893272)------------------------------
% 69.27/11.76 % (2893272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.27/11.76 % (2893272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.27/11.76 % (2893272)CaDiCaL version: 2.1.3
% 69.27/11.76 % (2893272)Termination reason: Instruction limit
% 69.27/11.76 % (2893272)Termination phase: Preprocessing 1
% 69.27/11.76 % (2893272)Time elapsed: 0.152 s
% 69.27/11.76 % (2893272)Peak memory usage: 137 MB
% 69.27/11.76 % (2893272)Instructions burned: 127 (million)
% 69.27/11.76 % (2893276)lrs+10_1_sil=8000:sp=occurrence:random_seed=1761998076:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 69.27/11.76 % (2893278)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=897375637:i=5202:ss=axioms:sgt=16_2973 on theBenchmark for (2973ds/5202Mi)
% 69.27/11.76 % (2893277)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1389289915:i=437:sd=1:aac=none:ss=included_2974 on theBenchmark for (2974ds/437Mi)
% 69.27/11.76 % (2893277)Instruction limit reached!
% 69.27/11.76 % (2893277)------------------------------
% 69.27/11.76 % (2893277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.27/11.76 % (2893277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.27/11.76 % (2893277)CaDiCaL version: 2.1.3
% 69.27/11.76 % (2893277)Termination reason: Instruction limit
% 69.27/11.76 % (2893277)Termination phase: Saturation
% 69.27/11.76 % (2893277)Time elapsed: 0.452 s
% 69.27/11.76 % (2893277)Peak memory usage: 143 MB
% 69.27/11.76 % (2893277)Instructions burned: 438 (million)
% 69.27/11.76 % (2893267)Instruction limit reached!
% 69.27/11.76 % (2893267)------------------------------
% 69.27/11.76 % (2893267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.27/11.76 % (2893267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.27/11.76 % (2893267)CaDiCaL version: 2.1.3
% 69.27/11.76 % (2893267)Termination reason: Instruction limit
% 69.27/11.76 % (2893267)Termination phase: Property scanning
% 69.27/11.76 % (2893267)Time elapsed: 1.348 s
% 69.27/11.76 % (2893267)Peak memory usage: 233 MB
% 69.27/11.76 % (2893267)Instructions burned: 2352 (million)
% 69.27/11.76 % (2893282)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3635218591:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2967 on theBenchmark for (2967ds/134Mi)
% 69.27/11.76 % (2893283)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1230652514:st=8:i=592:sd=3:ep=RST:ss=axioms_2966 on theBenchmark for (2966ds/592Mi)
% 69.27/11.76 % (2893276)Instruction limit reached!
% 69.27/11.76 % (2893276)------------------------------
% 69.27/11.76 % (2893276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.27/11.76 % (2893276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.27/11.76 % (2893276)CaDiCaL version: 2.1.3
% 69.27/11.76 % (2893276)Termination reason: Instruction limit
% 69.27/11.76 % (2893276)Termination phase: Property scanning
% 69.27/11.76 % (2893276)Time elapsed: 0.948 s
% 69.27/11.76 % (2893276)Peak memory usage: 157 MB
% 69.27/11.76 % (2893276)Instructions burned: 907 (million)
% 69.27/11.76 % (2893282)Instruction limit reached!
% 69.27/11.76 % (2893282)------------------------------
% 69.27/11.76 % (2893282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.27/11.76 % (2893282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.27/11.76 % (2893282)CaDiCaL version: 2.1.3
% 69.27/11.76 % (2893282)Termination reason: Instruction limit
% 69.27/11.76 % (2893282)Termination phase: SInE selection
% 69.27/11.76 % (2893282)Time elapsed: 0.150 s
% 69.27/11.76 % (2893282)Peak memory usage: 136 MB
% 69.27/11.76 % (2893282)Instructions burned: 134 (million)
% 69.27/11.76 % (2893286)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1577093465:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 69.27/11.76 % (2893287)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=3152044277:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/125Mi)
% 117.97/18.52 % (2893283)Instruction limit reached!
% 117.97/18.52 % (2893283)------------------------------
% 117.97/18.52 % (2893283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.97/18.52 % (2893283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.97/18.52 % (2893283)CaDiCaL version: 2.1.3
% 117.97/18.52 % (2893283)Termination reason: Instruction limit
% 117.97/18.52 % (2893283)Termination phase: Naming
% 117.97/18.52 % (2893283)Time elapsed: 0.400 s
% 117.97/18.52 % (2893283)Peak memory usage: 154 MB
% 117.97/18.52 % (2893283)Instructions burned: 592 (million)
% 117.97/18.52 % (2893287)Instruction limit reached!
% 117.97/18.52 % (2893287)------------------------------
% 117.97/18.52 % (2893287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.97/18.52 % (2893287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.97/18.52 % (2893287)CaDiCaL version: 2.1.3
% 117.97/18.52 % (2893287)Termination reason: Instruction limit
% 117.97/18.52 % (2893287)Termination phase: Property scanning
% 117.97/18.52 % (2893287)Time elapsed: 0.109 s
% 117.97/18.52 % (2893287)Peak memory usage: 136 MB
% 117.97/18.52 % (2893287)Instructions burned: 125 (million)
% 117.97/18.52 % (2893290)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=674202004:i=134:gtgl=5:slsql=off:gtg=exists_sym_2960 on theBenchmark for (2960ds/134Mi)
% 117.97/18.52 % (2893290)Instruction limit reached!
% 117.97/18.52 % (2893290)------------------------------
% 117.97/18.52 % (2893290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.97/18.52 % (2893290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.97/18.52 % (2893290)CaDiCaL version: 2.1.3
% 117.97/18.52 % (2893290)Termination reason: Instruction limit
% 117.97/18.52 % (2893290)Termination phase: Property scanning
% 117.97/18.52 % (2893290)Time elapsed: 0.063 s
% 117.97/18.52 % (2893290)Peak memory usage: 136 MB
% 117.97/18.52 % (2893290)Instructions burned: 135 (million)
% 117.97/18.52 % (2893291)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3543874098:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/141Mi)
% 117.97/18.52 % (2893293)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1216283096:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2958 on theBenchmark for (2958ds/431Mi)
% 117.97/18.52 % (2893291)Instruction limit reached!
% 117.97/18.52 % (2893291)------------------------------
% 117.97/18.52 % (2893291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.97/18.52 % (2893291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.97/18.52 % (2893291)CaDiCaL version: 2.1.3
% 117.97/18.52 % (2893291)Termination reason: Instruction limit
% 117.97/18.52 % (2893291)Termination phase: SInE selection
% 117.97/18.52 % (2893291)Time elapsed: 0.160 s
% 117.97/18.52 % (2893291)Peak memory usage: 136 MB
% 117.97/18.52 % (2893291)Instructions burned: 141 (million)
% 117.97/18.52 % (2893293)Refutation not found, incomplete strategy
% 117.97/18.52 % (2893293)------------------------------
% 117.97/18.52 % (2893293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.97/18.52 % (2893293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.97/18.52 % (2893293)CaDiCaL version: 2.1.3
% 117.97/18.52 % (2893293)Termination reason: Refutation not found, incomplete strategy
% 117.97/18.52 % (2893293)Time elapsed: 0.167 s
% 117.97/18.52 % (2893293)Peak memory usage: 142 MB
% 117.97/18.52 % (2893293)Instructions burned: 246 (million)
% 117.97/18.52 % (2893296)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=3455623709:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 117.97/18.52 % (2893293)------------------------------
% 117.97/18.52 % (2893293)------------------------------
% 117.97/18.52 % (2893298)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=1405626286:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2952 on theBenchmark for (2952ds/150Mi)
% 117.97/18.52 % (2893298)Instruction limit reached!
% 117.97/18.52 % (2893298)------------------------------
% 117.97/18.52 % (2893298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.23/23.13 % (2893298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.23/23.13 % (2893298)CaDiCaL version: 2.1.3
% 150.23/23.13 % (2893298)Termination reason: Instruction limit
% 150.23/23.13 % (2893298)Termination phase: SInE selection
% 150.23/23.13 % (2893298)Time elapsed: 0.097 s
% 150.23/23.13 % (2893298)Peak memory usage: 136 MB
% 150.23/23.13 % (2893298)Instructions burned: 152 (million)
% 150.23/23.13 % (2893300)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2594642919:i=14155:bd=all_2950 on theBenchmark for (2950ds/14155Mi)
% 150.23/23.13 % (2893278)Instruction limit reached!
% 150.23/23.13 % (2893278)------------------------------
% 150.23/23.13 % (2893278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.23/23.13 % (2893278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.23/23.13 % (2893278)CaDiCaL version: 2.1.3
% 150.23/23.13 % (2893278)Termination reason: Instruction limit
% 150.23/23.13 % (2893278)Termination phase: Saturation
% 150.23/23.13 % (2893278)Time elapsed: 6.018 s
% 150.23/23.13 % (2893278)Peak memory usage: 620 MB
% 150.23/23.13 % (2893278)Instructions burned: 5204 (million)
% 150.23/23.13 % (2893302)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1957132139:i=667:av=off:fsr=off_2911 on theBenchmark for (2911ds/667Mi)
% 150.23/23.13 % (2893302)Instruction limit reached!
% 150.23/23.13 % (2893302)------------------------------
% 150.23/23.13 % (2893302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.23/23.13 % (2893302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.23/23.13 % (2893302)CaDiCaL version: 2.1.3
% 150.23/23.13 % (2893302)Termination reason: Instruction limit
% 150.23/23.13 % (2893302)Termination phase: NewCNF
% 150.23/23.13 % (2893302)Time elapsed: 0.824 s
% 150.23/23.13 % (2893302)Peak memory usage: 186 MB
% 150.23/23.13 % (2893302)Instructions burned: 668 (million)
% 150.23/23.13 % (2893304)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=674229157:s2a=on:i=185:s2at=1.8:fdi=4_2900 on theBenchmark for (2900ds/185Mi)
% 150.23/23.13 % (2893304)Instruction limit reached!
% 150.23/23.13 % (2893304)------------------------------
% 150.23/23.13 % (2893304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.23/23.13 % (2893304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.23/23.13 % (2893304)CaDiCaL version: 2.1.3
% 150.23/23.13 % (2893304)Termination reason: Instruction limit
% 150.23/23.13 % (2893304)Termination phase: SInE selection
% 150.23/23.13 % (2893304)Time elapsed: 0.194 s
% 150.23/23.13 % (2893304)Peak memory usage: 136 MB
% 150.23/23.13 % (2893304)Instructions burned: 186 (million)
% 150.23/23.13 % (2893306)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2073317886:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2896 on theBenchmark for (2896ds/193Mi)
% 150.23/23.13 % (2893296)Instruction limit reached!
% 150.23/23.13 % (2893296)------------------------------
% 150.23/23.13 % (2893296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.23/23.13 % (2893296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.23/23.13 % (2893296)CaDiCaL version: 2.1.3
% 150.23/23.13 % (2893296)Termination reason: Instruction limit
% 150.23/23.13 % (2893296)Termination phase: Function definition elimination
% 150.23/23.13 % (2893296)Time elapsed: 5.936 s
% 150.23/23.13 % (2893296)Peak memory usage: 244 MB
% 150.23/23.13 % (2893296)Instructions burned: 6061 (million)
% 150.23/23.13 % (2893306)Instruction limit reached!
% 150.23/23.13 % (2893306)------------------------------
% 150.23/23.13 % (2893306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 150.23/23.13 % (2893306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.23/23.13 % (2893306)CaDiCaL version: 2.1.3
% 150.23/23.13 % (2893306)Termination reason: Instruction limit
% 150.23/23.13 % (2893306)Termination phase: SInE selection
% 150.23/23.13 % (2893306)Time elapsed: 0.215 s
% 150.23/23.13 % (2893306)Peak memory usage: 136 MB
% 150.23/23.13 % (2893306)Instructions burned: 193 (million)
% 150.23/23.13 % (2893308)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2029647356:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2894 on theBenchmark for (2894ds/4850Mi)
% 150.23/23.13 % (2893309)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1471841454:i=12111:sd=1:ss=included_2892 on theBenchmark for (2892ds/12111Mi)
% 129.44/24.71 % (2893300)Instruction limit reached!
% 129.44/24.71 % (2893300)------------------------------
% 129.44/24.71 % (2893300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893300)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893300)Termination reason: Instruction limit
% 129.44/24.71 % (2893300)Termination phase: Saturation
% 129.44/24.71 % (2893300)Time elapsed: 8.530 s
% 129.44/24.71 % (2893300)Peak memory usage: 1175 MB
% 129.44/24.71 % (2893300)Instructions burned: 14157 (million)
% 129.44/24.71 % (2893312)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=665368610:i=319:kws=precedence:fsr=off_2862 on theBenchmark for (2862ds/319Mi)
% 129.44/24.71 % (2893312)Instruction limit reached!
% 129.44/24.71 % (2893312)------------------------------
% 129.44/24.71 % (2893312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893312)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893312)Termination reason: Instruction limit
% 129.44/24.71 % (2893312)Termination phase: Unused predicate definition removal
% 129.44/24.71 % (2893312)Time elapsed: 0.220 s
% 129.44/24.71 % (2893312)Peak memory usage: 142 MB
% 129.44/24.71 % (2893312)Instructions burned: 319 (million)
% 129.44/24.71 % (2893314)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2186215019:i=2064:ep=RST_2858 on theBenchmark for (2858ds/2064Mi)
% 129.44/24.71 % (2893308)Instruction limit reached!
% 129.44/24.71 % (2893308)------------------------------
% 129.44/24.71 % (2893308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893308)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893308)Termination reason: Instruction limit
% 129.44/24.71 % (2893308)Termination phase: Property scanning
% 129.44/24.71 % (2893308)Time elapsed: 4.199 s
% 129.44/24.71 % (2893308)Peak memory usage: 217 MB
% 129.44/24.71 % (2893308)Instructions burned: 4851 (million)
% 129.44/24.71 % (2893316)dis-1011_128_sil=32000:random_seed=1590786431:i=3706:ep=RST:av=off_2849 on theBenchmark for (2849ds/3706Mi)
% 129.44/24.71 % (2893314)Instruction limit reached!
% 129.44/24.71 % (2893314)------------------------------
% 129.44/24.71 % (2893314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893314)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893314)Termination reason: Instruction limit
% 129.44/24.71 % (2893314)Termination phase: Property scanning
% 129.44/24.71 % (2893314)Time elapsed: 1.209 s
% 129.44/24.71 % (2893314)Peak memory usage: 232 MB
% 129.44/24.71 % (2893314)Instructions burned: 2064 (million)
% 129.44/24.71 % (2893320)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4258073010:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2844 on theBenchmark for (2844ds/757Mi)
% 129.44/24.71 % (2893320)Instruction limit reached!
% 129.44/24.71 % (2893320)------------------------------
% 129.44/24.71 % (2893320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893320)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893320)Termination reason: Instruction limit
% 129.44/24.71 % (2893320)Termination phase: Saturation
% 129.44/24.71 % (2893320)Time elapsed: 0.829 s
% 129.44/24.71 % (2893320)Peak memory usage: 149 MB
% 129.44/24.71 % (2893320)Instructions burned: 757 (million)
% 129.44/24.71 % (2893322)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=55918506:i=13913:ss=axioms:sgt=8_2834 on theBenchmark for (2834ds/13913Mi)
% 129.44/24.71 % (2893286)Instruction limit reached!
% 129.44/24.71 % (2893286)------------------------------
% 129.44/24.71 % (2893286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893286)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893286)Termination reason: Instruction limit
% 129.44/24.71 % (2893286)Termination phase: Saturation
% 129.44/24.71 % (2893286)Time elapsed: 13.681 s
% 129.44/24.71 % (2893286)Peak memory usage: 300 MB
% 129.44/24.71 % (2893286)Instructions burned: 13193 (million)
% 129.44/24.71 % (2893324)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4101177107:i=9925:aac=none_2824 on theBenchmark for (2824ds/9925Mi)
% 129.44/24.71 % (2893316)Instruction limit reached!
% 129.44/24.71 % (2893316)------------------------------
% 129.44/24.71 % (2893316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893316)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893316)Termination reason: Instruction limit
% 129.44/24.71 % (2893316)Termination phase: Function definition elimination
% 129.44/24.71 % (2893316)Time elapsed: 3.306 s
% 129.44/24.71 % (2893316)Peak memory usage: 241 MB
% 129.44/24.71 % (2893316)Instructions burned: 3706 (million)
% 129.44/24.71 % (2893328)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=613114944:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2813 on theBenchmark for (2813ds/2479Mi)
% 129.44/24.71 % (2893328)Refutation not found, incomplete strategy
% 129.44/24.71 % (2893328)------------------------------
% 129.44/24.71 % (2893328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893328)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893328)Termination reason: Refutation not found, incomplete strategy
% 129.44/24.71 % (2893328)Time elapsed: 0.538 s
% 129.44/24.71 % (2893328)Peak memory usage: 142 MB
% 129.44/24.71 % (2893328)Instructions burned: 509 (million)
% 129.44/24.71 % (2893309)Instruction limit reached!
% 129.44/24.71 % (2893309)------------------------------
% 129.44/24.71 % (2893309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893309)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893309)Termination reason: Instruction limit
% 129.44/24.71 % (2893309)Termination phase: Saturation
% 129.44/24.71 % (2893309)Time elapsed: 8.538 s
% 129.44/24.71 % (2893309)Peak memory usage: 335 MB
% 129.44/24.71 % (2893309)Instructions burned: 12111 (million)
% 129.44/24.71 % (2893328)------------------------------
% 129.44/24.71 % (2893328)------------------------------
% 129.44/24.71 % (2893330)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4052195450:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2804 on theBenchmark for (2804ds/440Mi)
% 129.44/24.71 % (2893331)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2661856204:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2803 on theBenchmark for (2803ds/11145Mi)
% 129.44/24.71 % (2893330)Instruction limit reached!
% 129.44/24.71 % (2893330)------------------------------
% 129.44/24.71 % (2893330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893330)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893330)Termination reason: Instruction limit
% 129.44/24.71 % (2893330)Termination phase: Property scanning
% 129.44/24.71 % (2893330)Time elapsed: 0.201 s
% 129.44/24.71 % (2893330)Peak memory usage: 136 MB
% 129.44/24.71 % (2893330)Instructions burned: 441 (million)
% 129.44/24.71 % (2893334)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1042068221:cts=off:i=3034:av=off:er=known:fsd=on_2801 on theBenchmark for (2801ds/3034Mi)
% 129.44/24.71 % (2893334)Instruction limit reached!
% 129.44/24.71 % (2893334)------------------------------
% 129.44/24.71 % (2893334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893334)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893334)Termination reason: Instruction limit
% 129.44/24.71 % (2893334)Termination phase: Property scanning
% 129.44/24.71 % (2893334)Time elapsed: 1.714 s
% 129.44/24.71 % (2893334)Peak memory usage: 233 MB
% 129.44/24.71 % (2893334)Instructions burned: 3037 (million)
% 129.44/24.71 % (2893336)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=106764802:st=2:s2a=on:i=524:s2at=2:ss=axioms_2782 on theBenchmark for (2782ds/524Mi)
% 129.44/24.71 % (2893336)Instruction limit reached!
% 129.44/24.71 % (2893336)------------------------------
% 129.44/24.71 % (2893336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893336)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893336)Termination reason: Instruction limit
% 129.44/24.71 % (2893336)Termination phase: SInE selection
% 129.44/24.71 % (2893336)Time elapsed: 0.355 s
% 129.44/24.71 % (2893336)Peak memory usage: 138 MB
% 129.44/24.71 % (2893336)Instructions burned: 525 (million)
% 129.44/24.71 % (2893338)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2349589451:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2776 on theBenchmark for (2776ds/1016Mi)
% 129.44/24.71 % (2893338)Refutation not found, incomplete strategy
% 129.44/24.71 % (2893338)------------------------------
% 129.44/24.71 % (2893338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.44/24.71 % (2893338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.44/24.71 % (2893338)CaDiCaL version: 2.1.3
% 129.44/24.71 % (2893338)Termination reason: Refutation not found, incomplete strategy
% 129.44/24.71 % (2893338)Time elapsed: 0.173 s
% 129.44/24.71 % (2893338)Peak memory usage: 142 MB
% 129.44/24.71 % (2893338)Instructions burned: 255 (million)
% 129.44/24.71 % (2893338)------------------------------
% 129.44/24.71 % (2893338)------------------------------
% 129.44/24.71 % (2893340)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4090882244:i=14123:bd=preordered:ins=4_2770 on theBenchmark for (2770ds/14123Mi)
% 129.44/24.71 % (2893331)First to succeed.
% 129.44/24.71 % (2893331)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2893237"
% 129.44/24.71 % (2893331)Refutation found. Thanks to Tanya!
% 129.44/24.71 % SZS status Theorem for theBenchmark
% 129.44/24.71 % SZS output start Proof for theBenchmark
% See solution above
% 160.36/25.12 % (2893331)------------------------------
% 160.36/25.12 % (2893331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 160.36/25.12 % (2893331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 160.36/25.12 % (2893331)CaDiCaL version: 2.1.3
% 160.36/25.12 % (2893331)Termination reason: Refutation
% 160.36/25.12 % (2893331)Time elapsed: 3.257 s
% 160.36/25.12 % (2893331)Peak memory usage: 223 MB
% 160.36/25.12 % (2893331)Instructions burned: 3156 (million)
% 160.36/25.12 % (2893331)------------------------------
% 160.36/25.12 % (2893331)------------------------------
% 160.36/25.12 % (2893237)Success in time 23.896 s
% 160.36/25.12 % Vampire exiting
%------------------------------------------------------------------------------