%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT299+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:40 AM UTC 2026
% Result : Theorem 5.53s 16.76s
% Output : Refutation 6.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 55
% Syntax : Number of formulae : 424 ( 61 unt; 41 def)
% Number of atoms : 2246 ( 107 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 3181 (1359 ~;1597 |; 142 &)
% ( 49 <=>; 32 =>; 0 <=; 2 <~>)
% Maximal formula depth : 18 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 63 ( 61 usr; 42 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-6 aty)
% Number of variables : 372 ( 0 sgn 352 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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] :
( m2_filter_2(X2,X0)
=> m2_filter_2(X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t17_filter_2) ).
fof(f2,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] :
( m2_filter_2(X2,X0)
=> m2_filter_2(X2,X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f6,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_lattices) ).
fof(f15,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ( m2_filter_2(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(k3_lattices(X0,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_filter_2) ).
fof(f32,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f35,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f36,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/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f38,axiom,
! [X0] :
( l1_lattices(X0)
=> ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f40,axiom,
! [X0] :
( l2_lattices(X0)
=> ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(f62,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f79,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& l2_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_lattices) ).
fof(f80,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f82,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))) )
=> ( ! [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(k3_lattices(X0,X2,X3),X1) ) ) )
=> m2_filter_2(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_2) ).
fof(f89,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f104,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_filter_2(X2,X1)
& m2_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,[],[f2]) ).
fof(f105,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m2_filter_2(X2,X1)
& m2_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,[],[f104]) ).
fof(f110,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f111,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f110]) ).
fof(f122,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f123,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f122]) ).
fof(f124,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k3_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)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f125,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k3_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)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f124]) ).
fof(f136,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f137,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f138,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f137]) ).
fof(f139,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,[],[f36]) ).
fof(f140,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,[],[f139]) ).
fof(f142,plain,
! [X0] :
( ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f143,plain,
! [X0] :
( ( v1_funct_1(u2_lattices(X0))
& v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f162,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f163,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f162]) ).
fof(f171,plain,
! [X0,X1,X2] :
( k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f79]) ).
fof(f172,plain,
! [X0,X1,X2] :
( k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f171]) ).
fof(f173,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<~> r2_hidden(k3_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,[],[f82]) ).
fof(f174,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<~> r2_hidden(k3_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,[],[f173]) ).
fof(f183,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f89]) ).
fof(f185,plain,
( ~ m2_filter_2(sK2,sK1)
& m2_filter_2(sK2,sK0)
& g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1))
& ~ v3_struct_0(sK1)
& v10_lattices(sK1)
& l3_lattices(sK1)
& ~ v3_struct_0(sK0)
& v10_lattices(sK0)
& l3_lattices(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f105]) ).
fof(f186,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_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(k3_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k3_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)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f125]) ).
fof(f187,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_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(k3_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k3_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)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f186]) ).
fof(f188,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_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(k3_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k3_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)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f187]) ).
fof(f189,plain,
! [X0] :
( ! [X1] :
( ( ( m2_filter_2(X1,X0)
| ( ( ~ r2_hidden(k3_lattices(X0,sK3(X0,X1),sK4(X0,X1)),X1)
| ~ r2_hidden(sK3(X0,X1),X1)
| ~ r2_hidden(sK4(X0,X1),X1) )
& ( r2_hidden(k3_lattices(X0,sK3(X0,X1),sK4(X0,X1)),X1)
| ( r2_hidden(sK3(X0,X1),X1)
& r2_hidden(sK4(X0,X1),X1) ) )
& m1_subset_1(sK4(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK3(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k3_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)) )
| ~ m2_filter_2(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X2,sK3(X0,X1)),skolemize(X3,sK4(X0,X1))],[f188]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f80]) ).
fof(f215,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_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)) )
| 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,[],[f174]) ).
fof(f216,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k3_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k3_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)) )
| 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,[],[f215]) ).
fof(f217,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
| ( ( ~ r2_hidden(k3_lattices(X0,sK29(X0,X1),sK30(X0,X1)),X1)
| ~ r2_hidden(sK29(X0,X1),X1)
| ~ r2_hidden(sK30(X0,X1),X1) )
& ( r2_hidden(k3_lattices(X0,sK29(X0,X1),sK30(X0,X1)),X1)
| ( r2_hidden(sK29(X0,X1),X1)
& r2_hidden(sK30(X0,X1),X1) ) )
& m1_subset_1(sK30(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK29(X0,X1),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(skolemize,[status(esa),new_symbols(skolem,[sK29,sK30]),skolemize(X2,sK29(X0,X1)),skolemize(X3,sK30(X0,X1))],[f216]) ).
fof(f218,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f185]) ).
fof(f219,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f185]) ).
fof(f220,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f185]) ).
fof(f221,plain,
l3_lattices(sK1),
inference(cnf_transformation,[],[f185]) ).
fof(f222,plain,
v10_lattices(sK1),
inference(cnf_transformation,[],[f185]) ).
fof(f223,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f185]) ).
fof(f224,plain,
g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1)),
inference(cnf_transformation,[],[f185]) ).
fof(f225,plain,
m2_filter_2(sK2,sK0),
inference(cnf_transformation,[],[f185]) ).
fof(f226,plain,
~ m2_filter_2(sK2,sK1),
inference(cnf_transformation,[],[f185]) ).
fof(f235,plain,
! [X0] :
( v4_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f246,plain,
! [X2,X0,X1] :
( k1_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u2_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f247,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k3_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))
| ~ m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f248,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X5,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f249,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| ~ r2_hidden(k3_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m2_filter_2(X1,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f263,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f264,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f265,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f266,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f267,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,[],[f140]) ).
fof(f269,plain,
! [X0] :
( m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f270,plain,
! [X0] :
( v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f271,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f272,plain,
! [X0] :
( m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f273,plain,
! [X0] :
( v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f274,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f307,plain,
! [X2,X3,X0,X1,X4,X5] :
( X1 = X4
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f163]) ).
fof(f308,plain,
! [X2,X3,X0,X1,X4,X5] :
( X0 = X3
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f163]) ).
fof(f348,plain,
! [X2,X0,X1] :
( k3_lattices(X0,X1,X2) = k1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f172]) ).
fof(f349,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f214]) ).
fof(f352,plain,
! [X0,X1] :
( m2_filter_2(X1,X0)
| m1_subset_1(sK29(X0,X1),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(cnf_transformation,[],[f217]) ).
fof(f353,plain,
! [X0,X1] :
( m2_filter_2(X1,X0)
| m1_subset_1(sK30(X0,X1),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(cnf_transformation,[],[f217]) ).
fof(f354,plain,
! [X0,X1] :
( m2_filter_2(X1,X0)
| r2_hidden(k3_lattices(X0,sK29(X0,X1),sK30(X0,X1)),X1)
| r2_hidden(sK30(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,[],[f217]) ).
fof(f355,plain,
! [X0,X1] :
( m2_filter_2(X1,X0)
| r2_hidden(k3_lattices(X0,sK29(X0,X1),sK30(X0,X1)),X1)
| r2_hidden(sK29(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,[],[f217]) ).
fof(f356,plain,
! [X0,X1] :
( m2_filter_2(X1,X0)
| ~ r2_hidden(k3_lattices(X0,sK29(X0,X1),sK30(X0,X1)),X1)
| ~ r2_hidden(sK29(X0,X1),X1)
| ~ r2_hidden(sK30(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,[],[f217]) ).
fof(f363,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f183]) ).
fof(f369,definition,
( spl32_1
<=> m2_filter_2(sK2,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
fof(f371,plain,
( m2_filter_2(sK2,sK0)
| ~ spl32_1 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f372,plain,
spl32_1,
inference(avatar_split_clause,[],[f225,f369]) ).
fof(f374,definition,
( spl32_2
<=> v10_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
fof(f376,plain,
( v10_lattices(sK1)
| ~ spl32_2 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f377,plain,
spl32_2,
inference(avatar_split_clause,[],[f222,f374]) ).
fof(f379,definition,
( spl32_3
<=> l3_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
fof(f381,plain,
( l3_lattices(sK1)
| ~ spl32_3 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f382,plain,
spl32_3,
inference(avatar_split_clause,[],[f221,f379]) ).
fof(f384,definition,
( spl32_4
<=> v10_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl32_4])],[avatar_definition]) ).
fof(f386,plain,
( v10_lattices(sK0)
| ~ spl32_4 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f387,plain,
spl32_4,
inference(avatar_split_clause,[],[f219,f384]) ).
fof(f389,definition,
( spl32_5
<=> l3_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
fof(f391,plain,
( l3_lattices(sK0)
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,plain,
spl32_5,
inference(avatar_split_clause,[],[f218,f389]) ).
fof(f394,definition,
( spl32_6
<=> v3_struct_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
fof(f396,plain,
( ~ v3_struct_0(sK0)
| spl32_6 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
~ spl32_6,
inference(avatar_split_clause,[],[f220,f394]) ).
fof(f403,plain,
( v4_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_4 ),
inference(resolution,[],[f386,f235]) ).
fof(f444,plain,
( v4_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_4
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f403,f396]) ).
fof(f470,plain,
( v4_lattices(sK0)
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f444,f391]) ).
fof(f489,plain,
( v4_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(sK1)
| ~ spl32_2 ),
inference(resolution,[],[f376,f235]) ).
fof(f530,plain,
( v4_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl32_2 ),
inference(forward_subsumption_resolution,[],[f489,f223]) ).
fof(f556,plain,
( v4_lattices(sK1)
| ~ spl32_2
| ~ spl32_3 ),
inference(forward_subsumption_resolution,[],[f530,f381]) ).
fof(f586,plain,
( l2_lattices(sK1)
| ~ spl32_3 ),
inference(resolution,[],[f381,f263]) ).
fof(f587,plain,
( l1_lattices(sK1)
| ~ spl32_3 ),
inference(resolution,[],[f381,f264]) ).
fof(f620,plain,
( l2_lattices(sK0)
| ~ spl32_5 ),
inference(resolution,[],[f391,f263]) ).
fof(f637,plain,
( m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_1 ),
inference(resolution,[],[f371,f265]) ).
fof(f638,plain,
( ~ v1_xboole_0(sK2)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_1 ),
inference(resolution,[],[f371,f266]) ).
fof(f639,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v1_xboole_0(sK2)
| ~ m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1 ),
inference(resolution,[],[f371,f247]) ).
fof(f640,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| v1_xboole_0(sK2)
| ~ m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1 ),
inference(resolution,[],[f371,f248]) ).
fof(f641,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v1_xboole_0(sK2)
| ~ m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1 ),
inference(resolution,[],[f371,f249]) ).
fof(f642,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f641,f363]) ).
fof(f643,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f640,f363]) ).
fof(f644,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1 ),
inference(forward_subsumption_resolution,[],[f639,f363]) ).
fof(f645,plain,
( ~ v1_xboole_0(sK2)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_1
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f638,f396]) ).
fof(f646,plain,
( m2_lattice4(sK2,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_1
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f637,f396]) ).
fof(f647,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f642,f396]) ).
fof(f648,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f643,f396]) ).
fof(f649,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f644,f396]) ).
fof(f650,plain,
( ~ v1_xboole_0(sK2)
| ~ l3_lattices(sK0)
| ~ spl32_1
| ~ spl32_4
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f645,f386]) ).
fof(f651,plain,
( m2_lattice4(sK2,sK0)
| ~ l3_lattices(sK0)
| ~ spl32_1
| ~ spl32_4
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f646,f386]) ).
fof(f652,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1
| ~ spl32_4
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f647,f386]) ).
fof(f653,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1
| ~ spl32_4
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f648,f386]) ).
fof(f654,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0)
| ~ l3_lattices(sK0) )
| ~ spl32_1
| ~ spl32_4
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f649,f386]) ).
fof(f655,plain,
( ~ v1_xboole_0(sK2)
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f650,f391]) ).
fof(f656,plain,
( m2_lattice4(sK2,sK0)
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f651,f391]) ).
fof(f657,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0) )
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f652,f391]) ).
fof(f658,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0) )
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f653,f391]) ).
fof(f659,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m2_lattice4(sK2,sK0) )
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f654,f391]) ).
fof(f660,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f657,f656]) ).
fof(f661,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f658,f656]) ).
fof(f662,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f659,f656]) ).
fof(f664,definition,
( spl32_7
<=> v3_struct_0(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_7])],[avatar_definition]) ).
fof(f666,plain,
( ~ v3_struct_0(sK1)
| spl32_7 ),
inference(avatar_component_clause,[],[f664]) ).
fof(f667,plain,
~ spl32_7,
inference(avatar_split_clause,[],[f223,f664]) ).
fof(f669,definition,
( spl32_8
<=> m2_filter_2(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
fof(f671,plain,
( ~ m2_filter_2(sK2,sK1)
| spl32_8 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
~ spl32_8,
inference(avatar_split_clause,[],[f226,f669]) ).
fof(f678,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1))
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl32_8 ),
inference(resolution,[],[f671,f352]) ).
fof(f679,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1))
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| spl32_8 ),
inference(resolution,[],[f671,f353]) ).
fof(f686,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f679,f655]) ).
fof(f687,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f678,f655]) ).
fof(f696,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f686,f666]) ).
fof(f697,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f687,f666]) ).
fof(f706,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl32_1
| ~ spl32_2
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f696,f376]) ).
fof(f707,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl32_1
| ~ spl32_2
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f697,f376]) ).
fof(f716,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl32_1
| ~ spl32_2
| ~ spl32_3
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f706,f381]) ).
fof(f717,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl32_1
| ~ spl32_2
| ~ spl32_3
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(forward_subsumption_resolution,[],[f707,f381]) ).
fof(f764,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ v4_lattices(sK0)
| ~ l2_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| spl32_6 ),
inference(resolution,[],[f396,f348]) ).
fof(f771,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ l2_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f764,f470]) ).
fof(f782,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(forward_subsumption_resolution,[],[f771,f620]) ).
fof(f856,definition,
( spl32_9
<=> m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
introduced(definition,[new_symbols(definition,[spl32_9])],[avatar_definition]) ).
fof(f858,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| spl32_9 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f860,definition,
( spl32_10
<=> r2_hidden(sK29(sK1,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
fof(f862,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ spl32_10 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f876,definition,
( spl32_12
<=> r2_hidden(sK30(sK1,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl32_12])],[avatar_definition]) ).
fof(f877,plain,
( ~ r2_hidden(sK30(sK1,sK2),sK2)
| spl32_12 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f878,plain,
( r2_hidden(sK30(sK1,sK2),sK2)
| ~ spl32_12 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f881,definition,
( spl32_13
<=> m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_13])],[avatar_definition]) ).
fof(f883,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK1))
| ~ spl32_13 ),
inference(avatar_component_clause,[],[f881]) ).
fof(f884,plain,
( ~ spl32_9
| spl32_13
| ~ spl32_1
| ~ spl32_2
| ~ spl32_3
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(avatar_split_clause,[],[f717,f669,f664,f394,f389,f384,f379,f374,f369,f881,f856]) ).
fof(f887,definition,
( spl32_14
<=> m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
fof(f889,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK1))
| ~ spl32_14 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f890,plain,
( ~ spl32_9
| spl32_14
| ~ spl32_1
| ~ spl32_2
| ~ spl32_3
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8 ),
inference(avatar_split_clause,[],[f716,f669,f664,f394,f389,f384,f379,f374,f369,f887,f856]) ).
fof(f892,definition,
( spl32_15
<=> g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_15])],[avatar_definition]) ).
fof(f894,plain,
( g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1))
| ~ spl32_15 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f895,plain,
spl32_15,
inference(avatar_split_clause,[],[f224,f892]) ).
fof(f904,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15 ),
inference(superposition,[],[f307,f894]) ).
fof(f906,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15 ),
inference(superposition,[],[f308,f894]) ).
fof(f909,definition,
( spl32_16
<=> l2_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_16])],[avatar_definition]) ).
fof(f911,plain,
( l2_lattices(sK1)
| ~ spl32_16 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f912,plain,
( spl32_16
| ~ spl32_3 ),
inference(avatar_split_clause,[],[f586,f379,f909]) ).
fof(f918,plain,
( m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl32_16 ),
inference(resolution,[],[f911,f272]) ).
fof(f919,plain,
( v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl32_16 ),
inference(resolution,[],[f911,f273]) ).
fof(f920,plain,
( v1_funct_1(u2_lattices(sK1))
| ~ spl32_16 ),
inference(resolution,[],[f911,f274]) ).
fof(f937,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16 ),
inference(backward_subsumption_resolution,[],[f904,f920]) ).
fof(f938,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16 ),
inference(backward_subsumption_resolution,[],[f906,f920]) ).
fof(f947,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16 ),
inference(forward_subsumption_resolution,[],[f937,f919]) ).
fof(f948,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16 ),
inference(forward_subsumption_resolution,[],[f938,f919]) ).
fof(f969,definition,
( spl32_21
<=> l2_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl32_21])],[avatar_definition]) ).
fof(f971,plain,
( l2_lattices(sK0)
| ~ spl32_21 ),
inference(avatar_component_clause,[],[f969]) ).
fof(f972,plain,
( spl32_21
| ~ spl32_5 ),
inference(avatar_split_clause,[],[f620,f389,f969]) ).
fof(f1031,definition,
( spl32_25
<=> ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_25])],[avatar_definition]) ).
fof(f1032,plain,
( ! [X0,X1] :
( ~ r2_hidden(k3_lattices(sK0,X1,X0),sK2)
| r2_hidden(X0,sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_25 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1033,plain,
( spl32_25
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f661,f394,f389,f384,f369,f1031]) ).
fof(f1059,definition,
( spl32_26
<=> ! [X0,X1] :
( r2_hidden(X0,sK2)
| ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_26])],[avatar_definition]) ).
fof(f1060,plain,
( ! [X0,X1] :
( ~ r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| r2_hidden(X0,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_26 ),
inference(avatar_component_clause,[],[f1059]) ).
fof(f1061,plain,
( spl32_26
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f660,f394,f389,f384,f369,f1059]) ).
fof(f1111,definition,
( spl32_28
<=> ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_28])],[avatar_definition]) ).
fof(f1112,plain,
( ! [X0,X1] :
( r2_hidden(k3_lattices(sK0,X0,X1),sK2)
| ~ r2_hidden(X0,sK2)
| ~ r2_hidden(X1,sK2)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_28 ),
inference(avatar_component_clause,[],[f1111]) ).
fof(f1113,plain,
( spl32_28
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f662,f394,f389,f384,f369,f1111]) ).
fof(f1149,definition,
( spl32_29
<=> m2_lattice4(sK2,sK0) ),
introduced(definition,[new_symbols(definition,[spl32_29])],[avatar_definition]) ).
fof(f1151,plain,
( m2_lattice4(sK2,sK0)
| ~ spl32_29 ),
inference(avatar_component_clause,[],[f1149]) ).
fof(f1152,plain,
( spl32_29
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f656,f394,f389,f384,f369,f1149]) ).
fof(f1161,plain,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl32_29 ),
inference(resolution,[],[f1151,f267]) ).
fof(f1162,plain,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| spl32_6
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f1161,f396]) ).
fof(f1164,plain,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ spl32_4
| spl32_6
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f1162,f386]) ).
fof(f1165,plain,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl32_4
| ~ spl32_5
| spl32_6
| ~ spl32_29 ),
inference(forward_subsumption_resolution,[],[f1164,f391]) ).
fof(f1167,definition,
( spl32_30
<=> m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_30])],[avatar_definition]) ).
fof(f1168,plain,
( m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl32_30 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1169,plain,
( ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl32_30 ),
inference(avatar_component_clause,[],[f1167]) ).
fof(f1179,definition,
( spl32_33
<=> m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
introduced(definition,[new_symbols(definition,[spl32_33])],[avatar_definition]) ).
fof(f1180,plain,
( m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl32_33 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1181,plain,
( ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl32_33 ),
inference(avatar_component_clause,[],[f1179]) ).
fof(f1187,plain,
( ~ m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl32_30 ),
inference(resolution,[],[f1169,f349]) ).
fof(f1189,definition,
( spl32_35
<=> ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_35])],[avatar_definition]) ).
fof(f1190,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_35 ),
inference(avatar_component_clause,[],[f1189]) ).
fof(f1191,plain,
( spl32_35
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f782,f394,f389,f384,f1189]) ).
fof(f1201,definition,
( spl32_37
<=> l1_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_37])],[avatar_definition]) ).
fof(f1203,plain,
( l1_lattices(sK1)
| ~ spl32_37 ),
inference(avatar_component_clause,[],[f1201]) ).
fof(f1204,plain,
( spl32_37
| ~ spl32_3 ),
inference(avatar_split_clause,[],[f587,f379,f1201]) ).
fof(f1206,plain,
( m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl32_37 ),
inference(resolution,[],[f1203,f269]) ).
fof(f1207,plain,
( v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ spl32_37 ),
inference(resolution,[],[f1203,f270]) ).
fof(f1208,plain,
( v1_funct_1(u1_lattices(sK1))
| ~ spl32_37 ),
inference(resolution,[],[f1203,f271]) ).
fof(f1219,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_37 ),
inference(backward_subsumption_resolution,[],[f948,f1208]) ).
fof(f1220,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_37 ),
inference(backward_subsumption_resolution,[],[f947,f1208]) ).
fof(f1224,plain,
( $false
| spl32_30
| ~ spl32_37 ),
inference(forward_subsumption_resolution,[],[f1206,f1187]) ).
fof(f1225,plain,
( spl32_30
| ~ spl32_37 ),
inference(avatar_contradiction_clause,[],[f1224]) ).
fof(f1228,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_37 ),
inference(forward_subsumption_resolution,[],[f1219,f1207]) ).
fof(f1229,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_37 ),
inference(forward_subsumption_resolution,[],[f1220,f1207]) ).
fof(f1233,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_37 ),
inference(forward_subsumption_resolution,[],[f1228,f1168]) ).
fof(f1234,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_37 ),
inference(forward_subsumption_resolution,[],[f1229,f1168]) ).
fof(f1240,plain,
( ~ m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| spl32_33 ),
inference(resolution,[],[f1181,f349]) ).
fof(f1241,plain,
( $false
| ~ spl32_16
| spl32_33 ),
inference(forward_subsumption_resolution,[],[f1240,f918]) ).
fof(f1242,plain,
( ~ spl32_16
| spl32_33 ),
inference(avatar_contradiction_clause,[],[f1241]) ).
fof(f1246,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1 )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_33
| ~ spl32_37 ),
inference(backward_subsumption_resolution,[],[f1234,f1180]) ).
fof(f1247,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0 )
| ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_33
| ~ spl32_37 ),
inference(backward_subsumption_resolution,[],[f1233,f1180]) ).
fof(f1363,definition,
( spl32_38
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl32_38])],[avatar_definition]) ).
fof(f1364,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK1) = X0 )
| ~ spl32_38 ),
inference(avatar_component_clause,[],[f1363]) ).
fof(f1365,plain,
( spl32_38
| ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_33
| ~ spl32_37 ),
inference(avatar_split_clause,[],[f1247,f1201,f1179,f1167,f909,f892,f1363]) ).
fof(f1368,plain,
( u1_struct_0(sK0) = u1_struct_0(sK1)
| ~ spl32_38 ),
inference(equality_resolution,[],[f1364]) ).
fof(f1373,definition,
( spl32_39
<=> u1_struct_0(sK0) = u1_struct_0(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_39])],[avatar_definition]) ).
fof(f1375,plain,
( u1_struct_0(sK0) = u1_struct_0(sK1)
| ~ spl32_39 ),
inference(avatar_component_clause,[],[f1373]) ).
fof(f1376,plain,
( spl32_39
| ~ spl32_38 ),
inference(avatar_split_clause,[],[f1368,f1363,f1373]) ).
fof(f1380,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| spl32_9
| ~ spl32_39 ),
inference(superposition,[],[f858,f1375]) ).
fof(f1413,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k3_lattices(sK1,X0,X1) = k1_lattices(sK1,X0,X1)
| v3_struct_0(sK1)
| ~ v4_lattices(sK1)
| ~ l2_lattices(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_39 ),
inference(superposition,[],[f348,f1375]) ).
fof(f1428,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k3_lattices(sK1,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ v4_lattices(sK1)
| ~ l2_lattices(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| spl32_7
| ~ spl32_39 ),
inference(forward_subsumption_resolution,[],[f1413,f666]) ).
fof(f1460,plain,
( $false
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_9
| ~ spl32_29
| ~ spl32_39 ),
inference(forward_subsumption_resolution,[],[f1380,f1165]) ).
fof(f1461,plain,
( ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_9
| ~ spl32_29
| ~ spl32_39 ),
inference(avatar_contradiction_clause,[],[f1460]) ).
fof(f1469,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k3_lattices(sK1,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ l2_lattices(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_2
| ~ spl32_3
| spl32_7
| ~ spl32_39 ),
inference(forward_subsumption_resolution,[],[f1428,f556]) ).
fof(f1504,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k3_lattices(sK1,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_2
| ~ spl32_3
| spl32_7
| ~ spl32_16
| ~ spl32_39 ),
inference(forward_subsumption_resolution,[],[f1469,f911]) ).
fof(f1534,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_13
| ~ spl32_39 ),
inference(forward_demodulation,[],[f883,f1375]) ).
fof(f1535,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_14
| ~ spl32_39 ),
inference(forward_demodulation,[],[f889,f1375]) ).
fof(f1567,definition,
( spl32_40
<=> m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_40])],[avatar_definition]) ).
fof(f1569,plain,
( m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_40 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1570,plain,
( spl32_40
| ~ spl32_14
| ~ spl32_39 ),
inference(avatar_split_clause,[],[f1535,f1373,f887,f1567]) ).
fof(f1654,definition,
( spl32_41
<=> m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl32_41])],[avatar_definition]) ).
fof(f1656,plain,
( m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_41 ),
inference(avatar_component_clause,[],[f1654]) ).
fof(f1657,plain,
( spl32_41
| ~ spl32_13
| ~ spl32_39 ),
inference(avatar_split_clause,[],[f1534,f1373,f881,f1654]) ).
fof(f1882,definition,
( spl32_52
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1 ) ),
introduced(definition,[new_symbols(definition,[spl32_52])],[avatar_definition]) ).
fof(f1883,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u2_lattices(sK1) = X1 )
| ~ spl32_52 ),
inference(avatar_component_clause,[],[f1882]) ).
fof(f1884,plain,
( spl32_52
| ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_33
| ~ spl32_37 ),
inference(avatar_split_clause,[],[f1246,f1201,f1179,f1167,f909,f892,f1882]) ).
fof(f1887,plain,
( u2_lattices(sK0) = u2_lattices(sK1)
| ~ spl32_52 ),
inference(equality_resolution,[],[f1883]) ).
fof(f1892,definition,
( spl32_53
<=> u2_lattices(sK0) = u2_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl32_53])],[avatar_definition]) ).
fof(f1894,plain,
( u2_lattices(sK0) = u2_lattices(sK1)
| ~ spl32_53 ),
inference(avatar_component_clause,[],[f1892]) ).
fof(f1895,plain,
( spl32_53
| ~ spl32_52 ),
inference(avatar_split_clause,[],[f1887,f1882,f1892]) ).
fof(f1899,plain,
( ! [X0,X1] :
( k1_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| v3_struct_0(sK1)
| ~ l2_lattices(sK1) )
| ~ spl32_53 ),
inference(superposition,[],[f246,f1894]) ).
fof(f1913,plain,
( ! [X0,X1] :
( k1_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ l2_lattices(sK1) )
| spl32_7
| ~ spl32_53 ),
inference(forward_subsumption_resolution,[],[f1899,f666]) ).
fof(f1921,plain,
( ! [X0,X1] :
( k1_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK1),u1_struct_0(sK1),u1_struct_0(sK1),u2_lattices(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1)) )
| spl32_7
| ~ spl32_16
| ~ spl32_53 ),
inference(forward_subsumption_resolution,[],[f1913,f911]) ).
fof(f1925,plain,
( ! [X0,X1] :
( k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK1))
| ~ m1_subset_1(X0,u1_struct_0(sK1)) )
| spl32_7
| ~ spl32_16
| ~ spl32_39
| ~ spl32_53 ),
inference(forward_demodulation,[],[f1921,f1375]) ).
fof(f1929,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK1)) )
| spl32_7
| ~ spl32_16
| ~ spl32_39
| ~ spl32_53 ),
inference(forward_demodulation,[],[f1925,f1375]) ).
fof(f1930,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,X1) = k1_lattices(sK1,X0,X1) )
| spl32_7
| ~ spl32_16
| ~ spl32_39
| ~ spl32_53 ),
inference(forward_demodulation,[],[f1929,f1375]) ).
fof(f1936,definition,
( spl32_54
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k3_lattices(sK1,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_54])],[avatar_definition]) ).
fof(f1937,plain,
( ! [X0,X1] :
( k3_lattices(sK1,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_54 ),
inference(avatar_component_clause,[],[f1936]) ).
fof(f1938,plain,
( spl32_54
| ~ spl32_2
| ~ spl32_3
| spl32_7
| ~ spl32_16
| ~ spl32_39 ),
inference(avatar_split_clause,[],[f1504,f1373,f909,f664,f379,f374,f1936]) ).
fof(f2428,definition,
( spl32_63
<=> m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0))) ),
introduced(definition,[new_symbols(definition,[spl32_63])],[avatar_definition]) ).
fof(f2430,plain,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl32_63 ),
inference(avatar_component_clause,[],[f2428]) ).
fof(f2431,plain,
( spl32_63
| ~ spl32_4
| ~ spl32_5
| spl32_6
| ~ spl32_29 ),
inference(avatar_split_clause,[],[f1165,f1149,f394,f389,f384,f2428]) ).
fof(f2450,definition,
( spl32_64
<=> v1_xboole_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl32_64])],[avatar_definition]) ).
fof(f2452,plain,
( ~ v1_xboole_0(sK2)
| spl32_64 ),
inference(avatar_component_clause,[],[f2450]) ).
fof(f2453,plain,
( ~ spl32_64
| ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6 ),
inference(avatar_split_clause,[],[f655,f394,f389,f384,f369,f2450]) ).
fof(f2474,plain,
( ! [X0] :
( m2_filter_2(sK2,X0)
| r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| r2_hidden(sK30(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl32_64 ),
inference(resolution,[],[f2452,f354]) ).
fof(f2475,plain,
( ! [X0] :
( m2_filter_2(sK2,X0)
| r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| r2_hidden(sK29(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl32_64 ),
inference(resolution,[],[f2452,f355]) ).
fof(f2476,plain,
( ! [X0] :
( m2_filter_2(sK2,X0)
| ~ r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| ~ r2_hidden(sK29(X0,sK2),sK2)
| ~ r2_hidden(sK30(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| spl32_64 ),
inference(resolution,[],[f2452,f356]) ).
fof(f2877,definition,
( spl32_72
<=> ! [X0] :
( m2_filter_2(sK2,X0)
| ~ r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| ~ r2_hidden(sK29(X0,sK2),sK2)
| ~ r2_hidden(sK30(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ) ),
introduced(definition,[new_symbols(definition,[spl32_72])],[avatar_definition]) ).
fof(f2878,plain,
( ! [X0] :
( ~ r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| m2_filter_2(sK2,X0)
| ~ r2_hidden(sK29(X0,sK2),sK2)
| ~ r2_hidden(sK30(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| ~ spl32_72 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2879,plain,
( spl32_72
| spl32_64 ),
inference(avatar_split_clause,[],[f2476,f2450,f2877]) ).
fof(f2943,definition,
( spl32_77
<=> ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,X1) = k1_lattices(sK1,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl32_77])],[avatar_definition]) ).
fof(f2944,plain,
( ! [X0,X1] :
( k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u2_lattices(sK0),X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_77 ),
inference(avatar_component_clause,[],[f2943]) ).
fof(f2945,plain,
( spl32_77
| spl32_7
| ~ spl32_16
| ~ spl32_39
| ~ spl32_53 ),
inference(avatar_split_clause,[],[f1930,f1892,f1373,f909,f664,f2943]) ).
fof(f2948,plain,
( ! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_77 ),
inference(superposition,[],[f246,f2944]) ).
fof(f2953,plain,
( ! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l2_lattices(sK0) )
| ~ spl32_77 ),
inference(duplicate_literal_removal,[],[f2948]) ).
fof(f2957,plain,
( ! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ l2_lattices(sK0) )
| spl32_6
| ~ spl32_77 ),
inference(forward_subsumption_resolution,[],[f2953,f396]) ).
fof(f2961,plain,
( ! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| spl32_6
| ~ spl32_21
| ~ spl32_77 ),
inference(forward_subsumption_resolution,[],[f2957,f971]) ).
fof(f2969,definition,
( spl32_78
<=> ! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_78])],[avatar_definition]) ).
fof(f2970,plain,
( ! [X0,X1] :
( k1_lattices(sK0,X0,X1) = k1_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_78 ),
inference(avatar_component_clause,[],[f2969]) ).
fof(f2971,plain,
( spl32_78
| spl32_6
| ~ spl32_21
| ~ spl32_77 ),
inference(avatar_split_clause,[],[f2961,f2943,f969,f394,f2969]) ).
fof(f2975,plain,
( ! [X0,X1] :
( k3_lattices(sK1,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl32_54
| ~ spl32_78 ),
inference(superposition,[],[f1937,f2970]) ).
fof(f2979,plain,
( ! [X0,X1] :
( k3_lattices(sK1,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_54
| ~ spl32_78 ),
inference(duplicate_literal_removal,[],[f2975]) ).
fof(f3711,definition,
( spl32_114
<=> ! [X0,X1] :
( k3_lattices(sK1,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_114])],[avatar_definition]) ).
fof(f3712,plain,
( ! [X0,X1] :
( k3_lattices(sK1,X0,X1) = k1_lattices(sK0,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_114 ),
inference(avatar_component_clause,[],[f3711]) ).
fof(f3713,plain,
( spl32_114
| ~ spl32_54
| ~ spl32_78 ),
inference(avatar_split_clause,[],[f2979,f2969,f1936,f3711]) ).
fof(f3720,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k3_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_35
| ~ spl32_114 ),
inference(superposition,[],[f1190,f3712]) ).
fof(f3733,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k3_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_35
| ~ spl32_114 ),
inference(duplicate_literal_removal,[],[f3720]) ).
fof(f3873,definition,
( spl32_124
<=> ! [X0] :
( m2_filter_2(sK2,X0)
| r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| r2_hidden(sK29(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ) ),
introduced(definition,[new_symbols(definition,[spl32_124])],[avatar_definition]) ).
fof(f3874,plain,
( ! [X0] :
( r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| m2_filter_2(sK2,X0)
| r2_hidden(sK29(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| ~ spl32_124 ),
inference(avatar_component_clause,[],[f3873]) ).
fof(f3875,plain,
( spl32_124
| spl32_64 ),
inference(avatar_split_clause,[],[f2475,f2450,f3873]) ).
fof(f4001,definition,
( spl32_133
<=> ! [X0] :
( m2_filter_2(sK2,X0)
| r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| r2_hidden(sK30(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ) ),
introduced(definition,[new_symbols(definition,[spl32_133])],[avatar_definition]) ).
fof(f4002,plain,
( ! [X0] :
( r2_hidden(k3_lattices(X0,sK29(X0,sK2),sK30(X0,sK2)),sK2)
| m2_filter_2(sK2,X0)
| r2_hidden(sK30(X0,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) )
| ~ spl32_133 ),
inference(avatar_component_clause,[],[f4001]) ).
fof(f4003,plain,
( spl32_133
| spl32_64 ),
inference(avatar_split_clause,[],[f2474,f2450,f4001]) ).
fof(f5077,definition,
( spl32_167
<=> ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k3_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl32_167])],[avatar_definition]) ).
fof(f5078,plain,
( ! [X0,X1] :
( k3_lattices(sK0,X0,X1) = k3_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl32_167 ),
inference(avatar_component_clause,[],[f5077]) ).
fof(f5079,plain,
( spl32_167
| ~ spl32_35
| ~ spl32_114 ),
inference(avatar_split_clause,[],[f3733,f3711,f1189,f5077]) ).
fof(f5117,plain,
( r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| m2_filter_2(sK2,sK1)
| r2_hidden(sK30(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_133
| ~ spl32_167 ),
inference(superposition,[],[f4002,f5078]) ).
fof(f5118,plain,
( r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| m2_filter_2(sK2,sK1)
| r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_124
| ~ spl32_167 ),
inference(superposition,[],[f3874,f5078]) ).
fof(f5119,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| m2_filter_2(sK2,sK1)
| ~ r2_hidden(sK29(sK1,sK2),sK2)
| ~ r2_hidden(sK30(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_72
| ~ spl32_167 ),
inference(superposition,[],[f2878,f5078]) ).
fof(f5127,plain,
( m2_filter_2(sK2,sK1)
| r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_26
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5118,f1060]) ).
fof(f5128,plain,
( m2_filter_2(sK2,sK1)
| r2_hidden(sK30(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_25
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5117,f1032]) ).
fof(f5149,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_8
| ~ spl32_26
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5127,f671]) ).
fof(f5150,plain,
( r2_hidden(sK30(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_8
| ~ spl32_25
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5128,f671]) ).
fof(f5168,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5149,f666]) ).
fof(f5169,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5150,f877]) ).
fof(f5177,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5168,f376]) ).
fof(f5178,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5169,f666]) ).
fof(f5184,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5177,f381]) ).
fof(f5185,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5178,f376]) ).
fof(f5188,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_41
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5184,f1656]) ).
fof(f5189,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5185,f381]) ).
fof(f5193,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_40
| ~ spl32_41
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5188,f1569]) ).
fof(f5194,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_41
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5189,f1656]) ).
fof(f5198,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| r2_hidden(sK29(sK1,sK2),sK2)
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_demodulation,[],[f5193,f1375]) ).
fof(f5199,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_40
| ~ spl32_41
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5194,f1569]) ).
fof(f5200,plain,
( r2_hidden(sK29(sK1,sK2),sK2)
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_124
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5198,f2430]) ).
fof(f5201,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_demodulation,[],[f5199,f1375]) ).
fof(f5202,plain,
( $false
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_133
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5201,f2430]) ).
fof(f5203,plain,
( ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_133
| ~ spl32_167 ),
inference(avatar_contradiction_clause,[],[f5202]) ).
fof(f5211,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| m2_filter_2(sK2,sK1)
| ~ r2_hidden(sK29(sK1,sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_25
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5119,f1032]) ).
fof(f5215,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| m2_filter_2(sK2,sK1)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_25
| ~ spl32_26
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5211,f1060]) ).
fof(f5248,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5215,f671]) ).
fof(f5251,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5248,f666]) ).
fof(f5252,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5251,f376]) ).
fof(f5253,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5252,f381]) ).
fof(f5254,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_41
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5253,f1656]) ).
fof(f5255,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_40
| ~ spl32_41
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5254,f1569]) ).
fof(f5256,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_demodulation,[],[f5255,f1375]) ).
fof(f5257,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_72
| ~ spl32_167 ),
inference(forward_subsumption_resolution,[],[f5256,f2430]) ).
fof(f5289,plain,
( spl32_10
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_124
| ~ spl32_167 ),
inference(avatar_split_clause,[],[f5200,f5077,f3873,f2428,f1654,f1567,f1373,f1059,f669,f664,f379,f374,f860]) ).
fof(f5305,definition,
( spl32_168
<=> r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2) ),
introduced(definition,[new_symbols(definition,[spl32_168])],[avatar_definition]) ).
fof(f5307,plain,
( ~ r2_hidden(k3_lattices(sK0,sK29(sK1,sK2),sK30(sK1,sK2)),sK2)
| spl32_168 ),
inference(avatar_component_clause,[],[f5305]) ).
fof(f5308,plain,
( ~ spl32_168
| ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_72
| ~ spl32_167 ),
inference(avatar_split_clause,[],[f5257,f5077,f2877,f2428,f1654,f1567,f1373,f1059,f1031,f669,f664,f379,f374,f5305]) ).
fof(f5318,plain,
( ~ r2_hidden(sK29(sK1,sK2),sK2)
| ~ r2_hidden(sK30(sK1,sK2),sK2)
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_28
| spl32_168 ),
inference(resolution,[],[f5307,f1112]) ).
fof(f5331,plain,
( ~ r2_hidden(sK30(sK1,sK2),sK2)
| ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_10
| ~ spl32_28
| spl32_168 ),
inference(forward_subsumption_resolution,[],[f5318,f862]) ).
fof(f5337,plain,
( ~ m1_subset_1(sK30(sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_10
| ~ spl32_12
| ~ spl32_28
| spl32_168 ),
inference(forward_subsumption_resolution,[],[f5331,f878]) ).
fof(f5341,plain,
( ~ m1_subset_1(sK29(sK1,sK2),u1_struct_0(sK0))
| ~ spl32_10
| ~ spl32_12
| ~ spl32_28
| ~ spl32_40
| spl32_168 ),
inference(forward_subsumption_resolution,[],[f5337,f1569]) ).
fof(f5347,plain,
( $false
| ~ spl32_10
| ~ spl32_12
| ~ spl32_28
| ~ spl32_40
| ~ spl32_41
| spl32_168 ),
inference(forward_subsumption_resolution,[],[f5341,f1656]) ).
fof(f5348,plain,
( ~ spl32_10
| ~ spl32_12
| ~ spl32_28
| ~ spl32_40
| ~ spl32_41
| spl32_168 ),
inference(avatar_contradiction_clause,[],[f5347]) ).
cnf(s1,plain,
spl32_1,
inference(sat_conversion,[],[f372]) ).
cnf(s2,plain,
spl32_2,
inference(sat_conversion,[],[f377]) ).
cnf(s3,plain,
spl32_3,
inference(sat_conversion,[],[f382]) ).
cnf(s4,plain,
spl32_4,
inference(sat_conversion,[],[f387]) ).
cnf(s5,plain,
spl32_5,
inference(sat_conversion,[],[f392]) ).
cnf(s6,plain,
~ spl32_6,
inference(sat_conversion,[],[f397]) ).
cnf(s7,plain,
~ spl32_7,
inference(sat_conversion,[],[f667]) ).
cnf(s8,plain,
~ spl32_8,
inference(sat_conversion,[],[f672]) ).
cnf(s11,plain,
( ~ spl32_1
| ~ spl32_2
| ~ spl32_3
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8
| ~ spl32_9
| spl32_13 ),
inference(sat_conversion,[],[f884]) ).
cnf(s13,plain,
( ~ spl32_1
| ~ spl32_2
| ~ spl32_3
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_7
| spl32_8
| ~ spl32_9
| spl32_14 ),
inference(sat_conversion,[],[f890]) ).
cnf(s14,plain,
spl32_15,
inference(sat_conversion,[],[f895]) ).
cnf(s15,plain,
( ~ spl32_3
| spl32_16 ),
inference(sat_conversion,[],[f912]) ).
cnf(s18,plain,
( ~ spl32_5
| spl32_21 ),
inference(sat_conversion,[],[f972]) ).
cnf(s23,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_25 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s24,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_26 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s26,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_28 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s27,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_29 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s29,plain,
( ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_35 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s31,plain,
( ~ spl32_3
| spl32_37 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s32,plain,
( spl32_30
| ~ spl32_37 ),
inference(sat_conversion,[],[f1225]) ).
cnf(s35,plain,
( ~ spl32_16
| spl32_33 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s36,plain,
( ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_33
| ~ spl32_37
| spl32_38 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s37,plain,
( ~ spl32_38
| spl32_39 ),
inference(sat_conversion,[],[f1376]) ).
cnf(s38,plain,
( ~ spl32_4
| ~ spl32_5
| spl32_6
| spl32_9
| ~ spl32_29
| ~ spl32_39 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s39,plain,
( ~ spl32_14
| ~ spl32_39
| spl32_40 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s40,plain,
( ~ spl32_13
| ~ spl32_39
| spl32_41 ),
inference(sat_conversion,[],[f1657]) ).
cnf(s51,plain,
( ~ spl32_15
| ~ spl32_16
| ~ spl32_30
| ~ spl32_33
| ~ spl32_37
| spl32_52 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s52,plain,
( ~ spl32_52
| spl32_53 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s53,plain,
( ~ spl32_2
| ~ spl32_3
| spl32_7
| ~ spl32_16
| ~ spl32_39
| spl32_54 ),
inference(sat_conversion,[],[f1938]) ).
cnf(s62,plain,
( ~ spl32_4
| ~ spl32_5
| spl32_6
| ~ spl32_29
| spl32_63 ),
inference(sat_conversion,[],[f2431]) ).
cnf(s63,plain,
( ~ spl32_1
| ~ spl32_4
| ~ spl32_5
| spl32_6
| ~ spl32_64 ),
inference(sat_conversion,[],[f2453]) ).
cnf(s71,plain,
( spl32_64
| spl32_72 ),
inference(sat_conversion,[],[f2879]) ).
cnf(s76,plain,
( spl32_7
| ~ spl32_16
| ~ spl32_39
| ~ spl32_53
| spl32_77 ),
inference(sat_conversion,[],[f2945]) ).
cnf(s77,plain,
( spl32_6
| ~ spl32_21
| ~ spl32_77
| spl32_78 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s112,plain,
( ~ spl32_54
| ~ spl32_78
| spl32_114 ),
inference(sat_conversion,[],[f3713]) ).
cnf(s122,plain,
( spl32_64
| spl32_124 ),
inference(sat_conversion,[],[f3875]) ).
cnf(s131,plain,
( spl32_64
| spl32_133 ),
inference(sat_conversion,[],[f4003]) ).
cnf(s166,plain,
( ~ spl32_35
| ~ spl32_114
| spl32_167 ),
inference(sat_conversion,[],[f5079]) ).
cnf(s167,plain,
( ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_12
| ~ spl32_25
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_133
| ~ spl32_167 ),
inference(sat_conversion,[],[f5203]) ).
cnf(s175,plain,
( ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| spl32_10
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_124
| ~ spl32_167 ),
inference(sat_conversion,[],[f5289]) ).
cnf(s176,plain,
( ~ spl32_2
| ~ spl32_3
| spl32_7
| spl32_8
| ~ spl32_25
| ~ spl32_26
| ~ spl32_39
| ~ spl32_40
| ~ spl32_41
| ~ spl32_63
| ~ spl32_72
| ~ spl32_167
| ~ spl32_168 ),
inference(sat_conversion,[],[f5308]) ).
cnf(s179,plain,
( ~ spl32_10
| ~ spl32_12
| ~ spl32_28
| ~ spl32_40
| ~ spl32_41
| spl32_168 ),
inference(sat_conversion,[],[f5348]) ).
cnf(s183,plain,
spl32_21,
inference(rat,[],[s18,s5]) ).
cnf(s202,plain,
spl32_35,
inference(rat,[],[s29,s5,s6,s4]) ).
cnf(s205,plain,
spl32_37,
inference(rat,[],[s31,s3]) ).
cnf(s206,plain,
spl32_16,
inference(rat,[],[s15,s3]) ).
cnf(s209,plain,
spl32_30,
inference(rat,[],[s32,s205]) ).
cnf(s213,plain,
spl32_33,
inference(rat,[],[s35,s206]) ).
cnf(s222,plain,
spl32_52,
inference(rat,[],[s51,s209,s205,s206,s14,s213]) ).
cnf(s223,plain,
spl32_38,
inference(rat,[],[s36,s209,s205,s206,s14,s213]) ).
cnf(s225,plain,
spl32_53,
inference(rat,[],[s52,s222]) ).
cnf(s226,plain,
spl32_39,
inference(rat,[],[s37,s223]) ).
cnf(s239,plain,
spl32_77,
inference(rat,[],[s76,s225,s206,s7,s226]) ).
cnf(s243,plain,
spl32_78,
inference(rat,[],[s77,s183,s6,s239]) ).
cnf(s276,plain,
spl32_54,
inference(rat,[],[s53,s226,s206,s3,s7,s2]) ).
cnf(s280,plain,
spl32_114,
inference(rat,[],[s112,s243,s276]) ).
cnf(s281,plain,
spl32_167,
inference(rat,[],[s166,s202,s280]) ).
cnf(s282,plain,
~ spl32_64,
inference(rat,[],[s63,s4,s6,s5,s1]) ).
cnf(s283,plain,
spl32_29,
inference(rat,[],[s27,s4,s6,s5,s1]) ).
cnf(s284,plain,
spl32_28,
inference(rat,[],[s26,s4,s6,s5,s1]) ).
cnf(s285,plain,
spl32_26,
inference(rat,[],[s24,s4,s6,s5,s1]) ).
cnf(s286,plain,
spl32_25,
inference(rat,[],[s23,s4,s6,s5,s1]) ).
cnf(s289,plain,
spl32_133,
inference(rat,[],[s131,s282]) ).
cnf(s290,plain,
spl32_124,
inference(rat,[],[s122,s282]) ).
cnf(s293,plain,
spl32_72,
inference(rat,[],[s71,s282]) ).
cnf(s295,plain,
spl32_63,
inference(rat,[],[s62,s4,s5,s6,s283]) ).
cnf(s296,plain,
spl32_9,
inference(rat,[],[s38,s226,s4,s5,s6,s283]) ).
cnf(s297,plain,
spl32_14,
inference(rat,[],[s13,s1,s2,s8,s7,s6,s5,s4,s3,s296]) ).
cnf(s298,plain,
spl32_13,
inference(rat,[],[s11,s1,s2,s8,s7,s6,s5,s4,s3,s296]) ).
cnf(s299,plain,
spl32_40,
inference(rat,[],[s39,s226,s297]) ).
cnf(s300,plain,
spl32_41,
inference(rat,[],[s40,s226,s298]) ).
cnf(s313,plain,
spl32_10,
inference(rat,[],[s175,s281,s290,s295,s300,s285,s226,s2,s3,s8,s7,s299]) ).
cnf(s315,plain,
spl32_12,
inference(rat,[],[s167,s281,s289,s295,s300,s286,s226,s2,s3,s8,s7,s299]) ).
cnf(s328,plain,
~ spl32_168,
inference(rat,[],[s176,s299,s281,s293,s295,s286,s285,s226,s2,s3,s8,s7,s300]) ).
cnf(s329,plain,
$false,
inference(rat,[],[s179,s328,s300,s299,s284,s315,s313]) ).
fof(f5356,plain,
$false,
inference(avatar_sat_refutation,[],[s329]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT299+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/15.39 % Computer : n006.cluster.edu
% 0.11/15.39 % Model : x86_64 x86_64
% 0.11/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/15.39 % Memory : 8046.5625MB
% 0.11/15.39 % OS : Linux 6.8.0-71-generic
% 0.11/15.39 % CPULimit : 300
% 0.11/15.39 % WCLimit : 300
% 0.11/15.39 % DateTime : Sun Sep 27 14:21:44 UTC 2026
% 0.15/15.40 % CPUTime :
% 0.15/15.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/15.42 Running first-order theorem proving
% 0.15/15.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.53/16.76 % (3023096)Detected formulas, will run a generic FOF schedule.
% 5.53/16.76 % (3023103)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=389415417:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.53/16.76 % (3023106)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2625052747:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.53/16.76 % (3023107)dis-21_1_sil=8000:lcm=predicate:random_seed=1186855319:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 5.53/16.76 % (3023105)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1131612506:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.53/16.76 % (3023104)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2973484760:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.53/16.76 % (3023101)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=1975850349:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.53/16.76 % (3023102)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=2264606198:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.53/16.76 % (3023104)Refutation not found, incomplete strategy
% 5.53/16.76 % (3023104)------------------------------
% 5.53/16.76 % (3023104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023104)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023104)Termination reason: Refutation not found, incomplete strategy
% 5.53/16.76 % (3023104)Time elapsed: 0.003 s
% 5.53/16.76 % (3023104)Peak memory usage: 88 MB
% 5.53/16.76 % (3023104)Instructions burned: 3 (million)
% 5.53/16.76 % (3023105)Instruction limit reached!
% 5.53/16.76 % (3023105)------------------------------
% 5.53/16.76 % (3023105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023105)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023105)Termination reason: Instruction limit
% 5.53/16.76 % (3023105)Termination phase: Saturation
% 5.53/16.76 % (3023105)Time elapsed: 0.069 s
% 5.53/16.76 % (3023105)Peak memory usage: 88 MB
% 5.53/16.76 % (3023105)Instructions burned: 119 (million)
% 5.53/16.76 % (3023107)Instruction limit reached!
% 5.53/16.76 % (3023107)------------------------------
% 5.53/16.76 % (3023107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023107)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023107)Termination reason: Instruction limit
% 5.53/16.76 % (3023107)Termination phase: Saturation
% 5.53/16.76 % (3023107)Time elapsed: 0.072 s
% 5.53/16.76 % (3023107)Peak memory usage: 93 MB
% 5.53/16.76 % (3023107)Instructions burned: 129 (million)
% 5.53/16.76 % (3023106)Instruction limit reached!
% 5.53/16.76 % (3023106)------------------------------
% 5.53/16.76 % (3023106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023106)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023106)Termination reason: Instruction limit
% 5.53/16.76 % (3023106)Termination phase: Saturation
% 5.53/16.76 % (3023106)Time elapsed: 0.097 s
% 5.53/16.76 % (3023106)Peak memory usage: 90 MB
% 5.53/16.76 % (3023106)Instructions burned: 140 (million)
% 5.53/16.76 % (3023116)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2426305639:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.53/16.76 % (3023115)lrs+10_1_sil=8000:sp=occurrence:random_seed=3496377867:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.53/16.76 % (3023116)Refutation not found, incomplete strategy
% 5.53/16.76 % (3023116)------------------------------
% 5.53/16.76 % (3023116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023116)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023116)Termination reason: Refutation not found, incomplete strategy
% 5.53/16.76 % (3023116)Time elapsed: 0.004 s
% 5.53/16.76 % (3023116)Peak memory usage: 88 MB
% 5.53/16.76 % (3023116)Instructions burned: 4 (million)
% 5.53/16.76 % (3023117)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3134382468:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.53/16.76 % (3023104)------------------------------
% 5.53/16.76 % (3023104)------------------------------
% 5.53/16.76 % (3023117)Instruction limit reached!
% 5.53/16.76 % (3023117)------------------------------
% 5.53/16.76 % (3023117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023117)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023117)Termination reason: Instruction limit
% 5.53/16.76 % (3023117)Termination phase: Saturation
% 5.53/16.76 % (3023117)Time elapsed: 0.154 s
% 5.53/16.76 % (3023117)Peak memory usage: 91 MB
% 5.53/16.76 % (3023117)Instructions burned: 325 (million)
% 5.53/16.76 % (3023115)Instruction limit reached!
% 5.53/16.76 % (3023115)------------------------------
% 5.53/16.76 % (3023115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023115)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023115)Termination reason: Instruction limit
% 5.53/16.76 % (3023115)Termination phase: Saturation
% 5.53/16.76 % (3023115)Time elapsed: 0.167 s
% 5.53/16.76 % (3023115)Peak memory usage: 91 MB
% 5.53/16.76 % (3023115)Instructions burned: 285 (million)
% 5.53/16.76 % (3023121)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=470744853:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.53/16.76 % (3023116)------------------------------
% 5.53/16.76 % (3023116)------------------------------
% 5.53/16.76 % (3023123)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3219307392:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.53/16.76 % (3023124)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2735614416:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.53/16.76 % (3023123)Refutation not found, incomplete strategy
% 5.53/16.76 % (3023123)------------------------------
% 5.53/16.76 % (3023123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023123)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023123)Termination reason: Refutation not found, incomplete strategy
% 5.53/16.76 % (3023123)Time elapsed: 0.007 s
% 5.53/16.76 % (3023123)Peak memory usage: 89 MB
% 5.53/16.76 % (3023123)Instructions burned: 11 (million)
% 5.53/16.76 % (3023121)Instruction limit reached!
% 5.53/16.76 % (3023121)------------------------------
% 5.53/16.76 % (3023121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023121)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023121)Termination reason: Instruction limit
% 5.53/16.76 % (3023121)Termination phase: Saturation
% 5.53/16.76 % (3023121)Time elapsed: 0.144 s
% 5.53/16.76 % (3023121)Peak memory usage: 93 MB
% 5.53/16.76 % (3023121)Instructions burned: 248 (million)
% 5.53/16.76 % (3023103)First to succeed.
% 5.53/16.76 % (3023103)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3023096"
% 5.53/16.76 % (3023125)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2522526338:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 5.53/16.76 % (3023128)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=888503369:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 5.53/16.76 % (3023125)Instruction limit reached!
% 5.53/16.76 % (3023125)------------------------------
% 5.53/16.76 % (3023125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023125)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023125)Termination reason: Instruction limit
% 5.53/16.76 % (3023125)Termination phase: Saturation
% 5.53/16.76 % (3023125)Time elapsed: 0.075 s
% 5.53/16.76 % (3023125)Peak memory usage: 90 MB
% 5.53/16.76 % (3023125)Instructions burned: 113 (million)
% 5.53/16.76 % (3023128)Instruction limit reached!
% 5.53/16.76 % (3023128)------------------------------
% 5.53/16.76 % (3023128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/16.76 % (3023128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/16.76 % (3023128)CaDiCaL version: 2.1.3
% 5.53/16.76 % (3023128)Termination reason: Instruction limit
% 5.53/16.76 % (3023128)Termination phase: Saturation
% 5.53/16.76 % (3023128)Time elapsed: 0.068 s
% 5.53/16.76 % (3023128)Peak memory usage: 89 MB
% 5.53/16.76 % (3023128)Instructions burned: 128 (million)
% 5.53/16.76 % (3023103)Refutation found. Thanks to Tanya!
% 5.53/16.76 % SZS status Theorem for theBenchmark
% 5.53/16.76 % SZS output start Proof for theBenchmark
% See solution above
% 6.80/16.86 % (3023103)------------------------------
% 6.80/16.86 % (3023103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.80/16.86 % (3023103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.80/16.86 % (3023103)CaDiCaL version: 2.1.3
% 6.80/16.86 % (3023103)Termination reason: Refutation
% 6.80/16.86 % (3023103)Time elapsed: 0.619 s
% 6.80/16.86 % (3023103)Peak memory usage: 136 MB
% 6.80/16.86 % (3023103)Instructions burned: 1672 (million)
% 6.80/16.86 % (3023103)------------------------------
% 6.80/16.86 % (3023103)------------------------------
% 6.80/16.86 % (3023096)Success in time 0.896 s
% 6.80/16.86 % Vampire exiting
%------------------------------------------------------------------------------