%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT298+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:39 AM UTC 2026
% Result : Theorem 12.80s 3.02s
% Output : Refutation 14.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 40
% Syntax : Number of formulae : 358 ( 49 unt; 25 def)
% Number of atoms : 1800 ( 109 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 2513 (1071 ~;1247 |; 130 &)
% ( 35 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 48 ( 46 usr; 26 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-6 aty)
% Number of variables : 360 ( 0 sgn 348 !; 12 ?)
% 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] :
( m1_filter_2(X2,X0)
=> m1_filter_2(X2,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_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] :
( m1_filter_2(X2,X0)
=> m1_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(f12,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k4_lattices) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( m1_filter_0(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_filter_0) ).
fof(f15,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_lattices) ).
fof(f32,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f33,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f34,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_2) ).
fof(f39,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(f41,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(f64,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(f81,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
fof(f82,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f83,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(f88,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f94,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m1_filter_2(X2,X1)
& m1_filter_2(X2,X0) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f95,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ m1_filter_2(X2,X1)
& m1_filter_2(X2,X0) )
& g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
& ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f94]) ).
fof(f100,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(f101,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,[],[f100]) ).
fof(f108,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f12]) ).
fof(f109,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f108]) ).
fof(f112,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f113,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_0(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
<=> r2_hidden(k4_lattices(X0,X2,X3),X1) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f115,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f114]) ).
fof(f126,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f127,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f128,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f130,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f129]) ).
fof(f134,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,[],[f39]) ).
fof(f135,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,[],[f41]) ).
fof(f156,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,[],[f64]) ).
fof(f157,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,[],[f156]) ).
fof(f165,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f81]) ).
fof(f166,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f165]) ).
fof(f167,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f168,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f167]) ).
fof(f172,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f88]) ).
fof(f173,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f172]) ).
fof(f178,plain,
( ~ m1_filter_2(sK2,sK1)
& m1_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)],[f95]) ).
fof(f179,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f113]) ).
fof(f180,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f179]) ).
fof(f181,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ~ r2_hidden(k4_lattices(X0,X2,X3),X1)
| ~ r2_hidden(X2,X1)
| ~ r2_hidden(X3,X1) )
& ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( r2_hidden(X2,X1)
& r2_hidden(X3,X1) ) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( ( r2_hidden(X4,X1)
& r2_hidden(X5,X1) )
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f180]) ).
fof(f182,plain,
! [X0] :
( ! [X1] :
( ( ( m1_filter_0(X1,X0)
| ( ( ~ r2_hidden(k4_lattices(X0,sK3(X0,X1),sK4(X0,X1)),X1)
| ~ r2_hidden(sK3(X0,X1),X1)
| ~ r2_hidden(sK4(X0,X1),X1) )
& ( r2_hidden(k4_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(k4_lattices(X0,X4,X5),X1) )
& ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ m1_filter_0(X1,X0) ) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X2,sK3(X0,X1)),skolemize(X3,sK4(X0,X1))],[f181]) ).
fof(f208,plain,
! [X0] :
( ! [X1] :
( ( m1_filter_2(X1,X0)
| ~ m1_filter_0(X1,X0) )
& ( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f168]) ).
fof(f209,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,[],[f83]) ).
fof(f211,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f178]) ).
fof(f212,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f178]) ).
fof(f213,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f178]) ).
fof(f214,plain,
l3_lattices(sK1),
inference(cnf_transformation,[],[f178]) ).
fof(f215,plain,
v10_lattices(sK1),
inference(cnf_transformation,[],[f178]) ).
fof(f216,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f178]) ).
fof(f217,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,[],[f178]) ).
fof(f218,plain,
m1_filter_2(sK2,sK0),
inference(cnf_transformation,[],[f178]) ).
fof(f219,plain,
~ m1_filter_2(sK2,sK1),
inference(cnf_transformation,[],[f178]) ).
fof(f226,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| v6_lattices(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f238,plain,
! [X2,X0,X1] :
( ~ v6_lattices(X0)
| v3_struct_0(X0)
| k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f109]) ).
fof(f240,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f182]) ).
fof(f242,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| 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,[],[f182]) ).
fof(f243,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| m1_subset_1(sK3(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)
| m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f182]) ).
fof(f244,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| m1_subset_1(sK4(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)
| m1_filter_0(X1,X0) ),
inference(cnf_transformation,[],[f182]) ).
fof(f245,plain,
! [X0,X1] :
( r2_hidden(k4_lattices(X0,sK3(X0,X1),sK4(X0,X1)),X1)
| m1_filter_0(X1,X0)
| r2_hidden(sK4(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,[],[f182]) ).
fof(f246,plain,
! [X0,X1] :
( r2_hidden(k4_lattices(X0,sK3(X0,X1),sK4(X0,X1)),X1)
| m1_filter_0(X1,X0)
| r2_hidden(sK3(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,[],[f182]) ).
fof(f247,plain,
! [X0,X1] :
( ~ r2_hidden(sK4(X0,X1),X1)
| ~ r2_hidden(k4_lattices(X0,sK3(X0,X1),sK4(X0,X1)),X1)
| ~ r2_hidden(sK3(X0,X1),X1)
| m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f182]) ).
fof(f248,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f257,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f258,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f259,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f260,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f262,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f265,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,[],[f134]) ).
fof(f266,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,[],[f134]) ).
fof(f267,plain,
! [X0] :
( ~ l1_lattices(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f268,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,[],[f135]) ).
fof(f269,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,[],[f135]) ).
fof(f270,plain,
! [X0] :
( ~ l2_lattices(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(cnf_transformation,[],[f135]) ).
fof(f312,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v1_funct_1(X2)
| 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)
| X2 = X5
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f314,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ v1_funct_1(X2)
| 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)
| X0 = X3
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(cnf_transformation,[],[f157]) ).
fof(f355,plain,
! [X2,X0,X1] :
( ~ v6_lattices(X0)
| v3_struct_0(X0)
| k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f166]) ).
fof(f356,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f357,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f358,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f209]) ).
fof(f365,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(cnf_transformation,[],[f173]) ).
fof(f371,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f240,f365]) ).
fof(f373,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f242,f260]) ).
fof(f374,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_filter_0(X1,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f371,f365]) ).
fof(f376,plain,
! [X0,X1,X4,X5] :
( ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| r2_hidden(X4,X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f373,f259]) ).
fof(f377,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_filter_0(X1,X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f374,f260]) ).
fof(f378,plain,
! [X0,X1,X4,X5] :
( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ r2_hidden(X4,X1)
| ~ r2_hidden(X5,X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f377,f259]) ).
fof(f379,plain,
( m1_filter_0(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolution,[],[f356,f218]) ).
fof(f380,plain,
( m1_filter_0(sK2,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f379,f213]) ).
fof(f381,plain,
( m1_filter_0(sK2,sK0)
| ~ l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f380,f212]) ).
fof(f382,plain,
m1_filter_0(sK2,sK0),
inference(forward_subsumption_resolution,[],[f381,f211]) ).
fof(f391,plain,
! [X0] :
( m1_subset_1(sK4(sK1,X0),u1_struct_0(sK1))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| m1_filter_0(X0,sK1) ),
inference(resolution,[],[f244,f214]) ).
fof(f392,plain,
! [X0] :
( m1_subset_1(sK4(sK1,X0),u1_struct_0(sK1))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| m1_filter_0(X0,sK1) ),
inference(forward_subsumption_resolution,[],[f391,f216]) ).
fof(f394,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(X0)
| m1_subset_1(sK4(sK1,X0),u1_struct_0(sK1))
| m1_filter_0(X0,sK1) ),
inference(forward_subsumption_resolution,[],[f392,f215]) ).
fof(f408,plain,
! [X0] :
( m1_subset_1(sK3(sK1,X0),u1_struct_0(sK1))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| m1_filter_0(X0,sK1) ),
inference(resolution,[],[f243,f214]) ).
fof(f409,plain,
! [X0] :
( m1_subset_1(sK3(sK1,X0),u1_struct_0(sK1))
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| m1_filter_0(X0,sK1) ),
inference(forward_subsumption_resolution,[],[f408,f216]) ).
fof(f411,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(X0)
| m1_subset_1(sK3(sK1,X0),u1_struct_0(sK1))
| m1_filter_0(X0,sK1) ),
inference(forward_subsumption_resolution,[],[f409,f215]) ).
fof(f423,plain,
! [X0] :
( ~ l3_lattices(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(resolution,[],[f270,f257]) ).
fof(f424,plain,
! [X0] :
( m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(resolution,[],[f358,f265]) ).
fof(f425,plain,
! [X0] :
( m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(resolution,[],[f358,f268]) ).
fof(f426,plain,
! [X0] :
( ~ l3_lattices(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(resolution,[],[f267,f258]) ).
fof(f427,plain,
v1_funct_1(u1_lattices(sK0)),
inference(resolution,[],[f426,f211]) ).
fof(f432,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| X0 = X2
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(X0,X0),X0)
| g3_lattices(X2,X3,X4) != g3_lattices(X0,X1,u1_lattices(sK0)) ),
inference(resolution,[],[f427,f314]) ).
fof(f434,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| u1_lattices(sK0) = X4
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(X0,X0),X0)
| g3_lattices(X2,X3,X4) != g3_lattices(X0,X1,u1_lattices(sK0)) ),
inference(resolution,[],[f427,f312]) ).
fof(f435,plain,
v1_funct_1(u2_lattices(sK0)),
inference(resolution,[],[f423,f211]) ).
fof(f453,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_lattices(sK0) = X1
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| g3_lattices(X2,X3,X1) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ l1_lattices(sK0) ),
inference(resolution,[],[f434,f424]) ).
fof(f454,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_lattices(sK0) = X1
| g3_lattices(X2,X3,X1) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ l1_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f453,f266]) ).
fof(f456,definition,
( spl30_1
<=> l1_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f457,plain,
( ~ l1_lattices(sK0)
| spl30_1 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f459,definition,
( spl30_2
<=> ! [X0,X3,X2,X1] :
( ~ v1_funct_1(X0)
| u1_lattices(sK0) = X1
| g3_lattices(X2,X3,X1) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
fof(f460,plain,
( ! [X2,X3,X0,X1] :
( g3_lattices(X2,X3,X1) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| u1_lattices(sK0) = X1
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) )
| ~ spl30_2 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( ~ spl30_1
| spl30_2 ),
inference(avatar_split_clause,[],[f454,f459,f456]) ).
fof(f463,plain,
( ~ l3_lattices(sK0)
| spl30_1 ),
inference(resolution,[],[f457,f258]) ).
fof(f465,plain,
( $false
| spl30_1 ),
inference(forward_subsumption_resolution,[],[f463,f211]) ).
fof(f466,plain,
spl30_1,
inference(avatar_contradiction_clause,[],[f465]) ).
fof(f467,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| u1_lattices(sK0) = u1_lattices(sK1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) )
| ~ spl30_2 ),
inference(superposition,[],[f460,f217]) ).
fof(f470,definition,
( spl30_3
<=> u1_lattices(sK0) = u1_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
fof(f471,plain,
( u1_lattices(sK0) = u1_lattices(sK1)
| ~ spl30_3 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f473,definition,
( spl30_4
<=> ! [X0] :
( g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
fof(f474,plain,
( ! [X0] :
( g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(X0) )
| ~ spl30_4 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f475,plain,
( spl30_3
| spl30_4
| ~ spl30_2 ),
inference(avatar_split_clause,[],[f467,f459,f473,f470]) ).
fof(f476,plain,
( ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| ~ spl30_4 ),
inference(equality_resolution,[],[f474]) ).
fof(f477,plain,
( ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ spl30_4 ),
inference(forward_subsumption_resolution,[],[f476,f435]) ).
fof(f479,definition,
( spl30_5
<=> m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl30_5])],[avatar_definition]) ).
fof(f480,plain,
( ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| spl30_5 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,definition,
( spl30_6
<=> v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
fof(f483,plain,
( ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| spl30_6 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f484,plain,
( ~ spl30_5
| ~ spl30_6
| ~ spl30_4 ),
inference(avatar_split_clause,[],[f477,f473,f482,f479]) ).
fof(f485,plain,
( ~ l2_lattices(sK0)
| spl30_5 ),
inference(resolution,[],[f480,f425]) ).
fof(f487,plain,
( ~ l3_lattices(sK0)
| spl30_5 ),
inference(resolution,[],[f485,f257]) ).
fof(f489,plain,
( $false
| spl30_5 ),
inference(forward_subsumption_resolution,[],[f487,f211]) ).
fof(f490,plain,
spl30_5,
inference(avatar_contradiction_clause,[],[f489]) ).
fof(f493,plain,
( ~ l2_lattices(sK0)
| spl30_6 ),
inference(resolution,[],[f483,f269]) ).
fof(f495,plain,
( ~ l3_lattices(sK0)
| spl30_6 ),
inference(resolution,[],[f493,f257]) ).
fof(f497,plain,
( $false
| spl30_6 ),
inference(forward_subsumption_resolution,[],[f495,f211]) ).
fof(f498,plain,
spl30_6,
inference(avatar_contradiction_clause,[],[f497]) ).
fof(f500,plain,
( g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) = g3_lattices(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK0))
| ~ spl30_3 ),
inference(superposition,[],[f217,f471]) ).
fof(f507,definition,
( spl30_7
<=> l1_lattices(sK1) ),
introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition]) ).
fof(f508,plain,
( ~ l1_lattices(sK1)
| spl30_7 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f532,plain,
( ~ l3_lattices(sK1)
| spl30_7 ),
inference(resolution,[],[f508,f258]) ).
fof(f534,plain,
( $false
| spl30_7 ),
inference(forward_subsumption_resolution,[],[f532,f214]) ).
fof(f535,plain,
spl30_7,
inference(avatar_contradiction_clause,[],[f534]) ).
fof(f549,definition,
( spl30_13
<=> l2_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl30_13])],[avatar_definition]) ).
fof(f550,plain,
( ~ l2_lattices(sK0)
| spl30_13 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f556,plain,
( ~ l3_lattices(sK0)
| spl30_13 ),
inference(resolution,[],[f550,f257]) ).
fof(f558,plain,
( $false
| spl30_13 ),
inference(forward_subsumption_resolution,[],[f556,f211]) ).
fof(f559,plain,
spl30_13,
inference(avatar_contradiction_clause,[],[f558]) ).
fof(f730,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_struct_0(sK0) = X1
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ l1_lattices(sK0) ),
inference(resolution,[],[f432,f424]) ).
fof(f733,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_struct_0(sK0) = X1
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ l1_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f730,f266]) ).
fof(f735,definition,
( spl30_33
<=> ! [X0,X3,X2,X1] :
( ~ v1_funct_1(X0)
| u1_struct_0(sK0) = X1
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_33])],[avatar_definition]) ).
fof(f736,plain,
( ! [X2,X3,X0,X1] :
( ~ m1_relset_1(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| u1_struct_0(sK0) = X1
| g3_lattices(X1,X2,X3) != g3_lattices(u1_struct_0(sK0),X0,u1_lattices(sK0))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) )
| ~ spl30_33 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f737,plain,
( ~ spl30_1
| spl30_33 ),
inference(avatar_split_clause,[],[f733,f735,f456]) ).
fof(f739,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| ~ v1_funct_1(u2_lattices(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ l2_lattices(sK0) )
| ~ spl30_33 ),
inference(resolution,[],[f736,f425]) ).
fof(f740,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| ~ v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ l2_lattices(sK0) )
| ~ spl30_33 ),
inference(forward_subsumption_resolution,[],[f739,f270]) ).
fof(f742,plain,
( ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| ~ l2_lattices(sK0) )
| ~ spl30_33 ),
inference(forward_subsumption_resolution,[],[f740,f269]) ).
fof(f745,definition,
( spl30_34
<=> ! [X2,X0,X1] :
( u1_struct_0(sK0) = X0
| g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_34])],[avatar_definition]) ).
fof(f746,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK0) = X0 )
| ~ spl30_34 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( ~ spl30_13
| spl30_34
| ~ spl30_33 ),
inference(avatar_split_clause,[],[f742,f735,f745,f549]) ).
fof(f753,plain,
( g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)) != g3_lattices(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| u1_struct_0(sK0) = u1_struct_0(sK1)
| ~ spl30_3
| ~ spl30_34 ),
inference(superposition,[],[f746,f500]) ).
fof(f755,plain,
( u1_struct_0(sK0) = u1_struct_0(sK1)
| ~ spl30_3
| ~ spl30_34 ),
inference(trivial_inequality_removal,[],[f753]) ).
fof(f758,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(X0)
| m1_subset_1(sK4(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1) )
| ~ spl30_3
| ~ spl30_34 ),
inference(superposition,[],[f394,f755]) ).
fof(f759,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(X0)
| m1_subset_1(sK3(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1) )
| ~ spl30_3
| ~ spl30_34 ),
inference(superposition,[],[f411,f755]) ).
fof(f766,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK1),X0,X1)
| v3_struct_0(sK1)
| ~ l1_lattices(sK1) )
| ~ spl30_3
| ~ spl30_34 ),
inference(superposition,[],[f248,f755]) ).
fof(f799,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK1),X0,X1)
| ~ l1_lattices(sK1) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f766,f216]) ).
fof(f827,plain,
( ! [X0,X1] :
( k2_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ l1_lattices(sK1) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_demodulation,[],[f799,f471]) ).
fof(f834,definition,
( spl30_40
<=> ! [X0,X1] :
( k2_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_40])],[avatar_definition]) ).
fof(f835,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),X0,X1) )
| ~ spl30_40 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f836,plain,
( ~ spl30_7
| spl30_40
| ~ spl30_3
| ~ spl30_34 ),
inference(avatar_split_clause,[],[f827,f745,f470,f834,f507]) ).
fof(f844,plain,
( ! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK4(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| ~ m1_filter_0(X0,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(resolution,[],[f758,f259]) ).
fof(f847,plain,
( ! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK4(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| ~ m1_filter_0(X0,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f844,f213]) ).
fof(f849,plain,
( ! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK4(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| ~ m1_filter_0(X0,sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f847,f212]) ).
fof(f851,plain,
( ! [X0] :
( ~ m1_filter_0(X0,sK0)
| m1_subset_1(sK4(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| v1_xboole_0(X0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f849,f211]) ).
fof(f852,plain,
( m1_subset_1(sK4(sK1,sK2),u1_struct_0(sK0))
| m1_filter_0(sK2,sK1)
| v1_xboole_0(sK2)
| ~ spl30_3
| ~ spl30_34 ),
inference(resolution,[],[f851,f382]) ).
fof(f854,definition,
( spl30_41
<=> v1_xboole_0(sK2) ),
introduced(definition,[new_symbols(definition,[spl30_41])],[avatar_definition]) ).
fof(f855,plain,
( v1_xboole_0(sK2)
| ~ spl30_41 ),
inference(avatar_component_clause,[],[f854]) ).
fof(f857,definition,
( spl30_42
<=> m1_filter_0(sK2,sK1) ),
introduced(definition,[new_symbols(definition,[spl30_42])],[avatar_definition]) ).
fof(f858,plain,
( m1_filter_0(sK2,sK1)
| ~ spl30_42 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f860,definition,
( spl30_43
<=> m1_subset_1(sK4(sK1,sK2),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl30_43])],[avatar_definition]) ).
fof(f861,plain,
( m1_subset_1(sK4(sK1,sK2),u1_struct_0(sK0))
| ~ spl30_43 ),
inference(avatar_component_clause,[],[f860]) ).
fof(f862,plain,
( spl30_41
| spl30_42
| spl30_43
| ~ spl30_3
| ~ spl30_34 ),
inference(avatar_split_clause,[],[f852,f745,f470,f860,f857,f854]) ).
fof(f864,plain,
( $false
| ~ spl30_41 ),
inference(unit_resulting_resolution,[],[f262,f211,f212,f213,f218,f855]) ).
fof(f868,plain,
~ spl30_41,
inference(avatar_contradiction_clause,[],[f864]) ).
fof(f874,plain,
( m1_filter_2(sK2,sK1)
| v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_42 ),
inference(resolution,[],[f858,f357]) ).
fof(f876,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_42 ),
inference(forward_subsumption_resolution,[],[f874,f219]) ).
fof(f878,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_42 ),
inference(forward_subsumption_resolution,[],[f876,f216]) ).
fof(f880,plain,
( ~ l3_lattices(sK1)
| ~ spl30_42 ),
inference(forward_subsumption_resolution,[],[f878,f215]) ).
fof(f882,plain,
( $false
| ~ spl30_42 ),
inference(forward_subsumption_resolution,[],[f880,f214]) ).
fof(f883,plain,
~ spl30_42,
inference(avatar_contradiction_clause,[],[f882]) ).
fof(f888,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(sK4(sK1,sK2),X1)
| ~ m1_filter_0(X1,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_43 ),
inference(resolution,[],[f861,f376]) ).
fof(f893,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(sK4(sK1,sK2),X1)
| ~ m1_filter_0(X1,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_43 ),
inference(forward_subsumption_resolution,[],[f888,f213]) ).
fof(f897,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(sK4(sK1,sK2),X1)
| ~ m1_filter_0(X1,sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_43 ),
inference(forward_subsumption_resolution,[],[f893,f212]) ).
fof(f907,plain,
( ! [X0,X1] :
( ~ m1_filter_0(X1,sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(sK4(sK1,sK2),X1)
| ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),X1) )
| ~ spl30_43 ),
inference(forward_subsumption_resolution,[],[f897,f211]) ).
fof(f911,plain,
( ! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK3(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| ~ m1_filter_0(X0,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(resolution,[],[f759,f259]) ).
fof(f914,plain,
( ! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK3(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| ~ m1_filter_0(X0,sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f911,f213]) ).
fof(f916,plain,
( ! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK3(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| ~ m1_filter_0(X0,sK0)
| ~ l3_lattices(sK0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f914,f212]) ).
fof(f918,plain,
( ! [X0] :
( ~ m1_filter_0(X0,sK0)
| m1_subset_1(sK3(sK1,X0),u1_struct_0(sK0))
| m1_filter_0(X0,sK1)
| v1_xboole_0(X0) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_subsumption_resolution,[],[f916,f211]) ).
fof(f919,plain,
( m1_subset_1(sK3(sK1,sK2),u1_struct_0(sK0))
| m1_filter_0(sK2,sK1)
| v1_xboole_0(sK2)
| ~ spl30_3
| ~ spl30_34 ),
inference(resolution,[],[f918,f382]) ).
fof(f921,definition,
( spl30_46
<=> m1_subset_1(sK3(sK1,sK2),u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl30_46])],[avatar_definition]) ).
fof(f922,plain,
( m1_subset_1(sK3(sK1,sK2),u1_struct_0(sK0))
| ~ spl30_46 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f923,plain,
( spl30_41
| spl30_42
| spl30_46
| ~ spl30_3
| ~ spl30_34 ),
inference(avatar_split_clause,[],[f919,f745,f470,f921,f857,f854]) ).
fof(f924,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_lattices(sK1,sK3(sK1,sK2),X0) = k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),X0) )
| ~ spl30_40
| ~ spl30_46 ),
inference(resolution,[],[f922,f835]) ).
fof(f927,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),X0) = k2_lattices(sK0,sK3(sK1,sK2),X0)
| v3_struct_0(sK0)
| ~ l1_lattices(sK0) )
| ~ spl30_46 ),
inference(resolution,[],[f922,f248]) ).
fof(f934,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),X0) = k2_lattices(sK0,sK3(sK1,sK2),X0)
| ~ l1_lattices(sK0) )
| ~ spl30_46 ),
inference(forward_subsumption_resolution,[],[f927,f213]) ).
fof(f939,definition,
( spl30_47
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),X0) = k2_lattices(sK0,sK3(sK1,sK2),X0) ) ),
introduced(definition,[new_symbols(definition,[spl30_47])],[avatar_definition]) ).
fof(f940,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),X0) = k2_lattices(sK0,sK3(sK1,sK2),X0) )
| ~ spl30_47 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f941,plain,
( ~ spl30_1
| spl30_47
| ~ spl30_46 ),
inference(avatar_split_clause,[],[f934,f921,f939,f456]) ).
fof(f950,plain,
( k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),sK4(sK1,sK2)) = k2_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_43
| ~ spl30_47 ),
inference(resolution,[],[f940,f861]) ).
fof(f1125,definition,
( spl30_59
<=> r2_hidden(sK3(sK1,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl30_59])],[avatar_definition]) ).
fof(f1126,plain,
( r2_hidden(sK3(sK1,sK2),sK2)
| ~ spl30_59 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1137,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| r2_hidden(sK4(sK1,sK2),sK2)
| ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),sK2) )
| ~ spl30_43 ),
inference(resolution,[],[f907,f382]) ).
fof(f1139,definition,
( spl30_61
<=> r2_hidden(sK4(sK1,sK2),sK2) ),
introduced(definition,[new_symbols(definition,[spl30_61])],[avatar_definition]) ).
fof(f1140,plain,
( r2_hidden(sK4(sK1,sK2),sK2)
| ~ spl30_61 ),
inference(avatar_component_clause,[],[f1139]) ).
fof(f1142,definition,
( spl30_62
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),sK2) ) ),
introduced(definition,[new_symbols(definition,[spl30_62])],[avatar_definition]) ).
fof(f1143,plain,
( ! [X0] :
( ~ r2_hidden(k4_lattices(sK0,sK4(sK1,sK2),X0),sK2)
| ~ m1_subset_1(X0,u1_struct_0(sK0)) )
| ~ spl30_62 ),
inference(avatar_component_clause,[],[f1142]) ).
fof(f1144,plain,
( spl30_61
| spl30_62
| ~ spl30_43 ),
inference(avatar_split_clause,[],[f1137,f860,f1142,f1139]) ).
fof(f1145,plain,
( ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| ~ r2_hidden(sK3(sK1,sK2),sK2)
| m1_filter_0(sK2,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)
| ~ spl30_61 ),
inference(resolution,[],[f1140,f247]) ).
fof(f1148,plain,
( ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,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)
| ~ spl30_59
| ~ spl30_61 ),
inference(forward_subsumption_resolution,[],[f1145,f1126]) ).
fof(f1149,plain,
( ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,sK1)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_59
| ~ spl30_61 ),
inference(forward_subsumption_resolution,[],[f1148,f216]) ).
fof(f1150,plain,
( ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,sK1)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl30_59
| ~ spl30_61 ),
inference(forward_subsumption_resolution,[],[f1149,f215]) ).
fof(f1151,plain,
( ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,sK1)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl30_59
| ~ spl30_61 ),
inference(forward_subsumption_resolution,[],[f1150,f214]) ).
fof(f1152,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,sK1)
| v1_xboole_0(sK2)
| ~ spl30_3
| ~ spl30_34
| ~ spl30_59
| ~ spl30_61 ),
inference(forward_demodulation,[],[f1151,f755]) ).
fof(f1154,definition,
( spl30_63
<=> r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2) ),
introduced(definition,[new_symbols(definition,[spl30_63])],[avatar_definition]) ).
fof(f1155,plain,
( ~ r2_hidden(k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| spl30_63 ),
inference(avatar_component_clause,[],[f1154]) ).
fof(f1157,definition,
( spl30_64
<=> m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0))) ),
introduced(definition,[new_symbols(definition,[spl30_64])],[avatar_definition]) ).
fof(f1158,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| spl30_64 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1159,plain,
( spl30_41
| spl30_42
| ~ spl30_63
| ~ spl30_64
| ~ spl30_3
| ~ spl30_34
| ~ spl30_59
| ~ spl30_61 ),
inference(avatar_split_clause,[],[f1152,f1139,f1125,f745,f470,f1157,f1154,f857,f854]) ).
fof(f1256,plain,
( k2_binop_1(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(sK0),u1_lattices(sK0),sK3(sK1,sK2),sK4(sK1,sK2)) = k2_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46 ),
inference(resolution,[],[f924,f861]) ).
fof(f1273,plain,
( k2_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)) = k2_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47 ),
inference(forward_demodulation,[],[f1256,f950]) ).
fof(f1386,plain,
( v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| v6_lattices(sK0) ),
inference(resolution,[],[f226,f211]) ).
fof(f1387,plain,
( v3_struct_0(sK1)
| ~ v10_lattices(sK1)
| v6_lattices(sK1) ),
inference(resolution,[],[f226,f214]) ).
fof(f1388,plain,
( ~ v10_lattices(sK1)
| v6_lattices(sK1) ),
inference(forward_subsumption_resolution,[],[f1387,f216]) ).
fof(f1389,plain,
( ~ v10_lattices(sK0)
| v6_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f1386,f213]) ).
fof(f1390,plain,
v6_lattices(sK1),
inference(forward_subsumption_resolution,[],[f1388,f215]) ).
fof(f1391,plain,
v6_lattices(sK0),
inference(forward_subsumption_resolution,[],[f1389,f212]) ).
fof(f1394,plain,
! [X0,X1] :
( v3_struct_0(sK1)
| k2_lattices(sK1,X0,X1) = k4_lattices(sK1,X0,X1)
| ~ l1_lattices(sK1)
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ m1_subset_1(X1,u1_struct_0(sK1)) ),
inference(resolution,[],[f1390,f355]) ).
fof(f1397,plain,
! [X0,X1] :
( k2_lattices(sK1,X0,X1) = k4_lattices(sK1,X0,X1)
| ~ l1_lattices(sK1)
| ~ m1_subset_1(X0,u1_struct_0(sK1))
| ~ m1_subset_1(X1,u1_struct_0(sK1)) ),
inference(forward_subsumption_resolution,[],[f1394,f216]) ).
fof(f1400,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k4_lattices(sK1,X0,X1)
| ~ l1_lattices(sK1)
| ~ m1_subset_1(X1,u1_struct_0(sK1)) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_demodulation,[],[f1397,f755]) ).
fof(f1403,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k4_lattices(sK1,X0,X1)
| ~ l1_lattices(sK1) )
| ~ spl30_3
| ~ spl30_34 ),
inference(forward_demodulation,[],[f1400,f755]) ).
fof(f1410,definition,
( spl30_70
<=> ! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k4_lattices(sK1,X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_70])],[avatar_definition]) ).
fof(f1411,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_lattices(sK1,X0,X1) = k4_lattices(sK1,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0)) )
| ~ spl30_70 ),
inference(avatar_component_clause,[],[f1410]) ).
fof(f1412,plain,
( ~ spl30_7
| spl30_70
| ~ spl30_3
| ~ spl30_34 ),
inference(avatar_split_clause,[],[f1403,f745,f470,f1410,f507]) ).
fof(f1433,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k2_lattices(sK1,sK3(sK1,sK2),X0) = k4_lattices(sK1,sK3(sK1,sK2),X0) )
| ~ spl30_46
| ~ spl30_70 ),
inference(resolution,[],[f1411,f922]) ).
fof(f1515,plain,
( k2_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)) = k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_43
| ~ spl30_46
| ~ spl30_70 ),
inference(resolution,[],[f1433,f861]) ).
fof(f1542,plain,
( k2_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)) = k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70 ),
inference(superposition,[],[f1273,f1515]) ).
fof(f1552,plain,
! [X0,X1] :
( v3_struct_0(sK0)
| k4_lattices(sK0,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ l1_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(resolution,[],[f1391,f355]) ).
fof(f1553,plain,
! [X0,X1] :
( v3_struct_0(sK0)
| k4_lattices(sK0,X0,X1) = k4_lattices(sK0,X1,X0)
| ~ l1_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(resolution,[],[f1391,f238]) ).
fof(f1554,plain,
! [X0,X1] :
( k4_lattices(sK0,X0,X1) = k4_lattices(sK0,X1,X0)
| ~ l1_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1553,f213]) ).
fof(f1555,plain,
! [X0,X1] :
( k4_lattices(sK0,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ l1_lattices(sK0)
| ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0)) ),
inference(forward_subsumption_resolution,[],[f1552,f213]) ).
fof(f1558,definition,
( spl30_72
<=> ! [X0,X1] :
( k4_lattices(sK0,X0,X1) = k4_lattices(sK0,X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_72])],[avatar_definition]) ).
fof(f1559,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k4_lattices(sK0,X0,X1) = k4_lattices(sK0,X1,X0) )
| ~ spl30_72 ),
inference(avatar_component_clause,[],[f1558]) ).
fof(f1560,plain,
( ~ spl30_1
| spl30_72 ),
inference(avatar_split_clause,[],[f1554,f1558,f456]) ).
fof(f1562,definition,
( spl30_73
<=> ! [X0,X1] :
( k4_lattices(sK0,X0,X1) = k2_lattices(sK0,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| ~ m1_subset_1(X0,u1_struct_0(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl30_73])],[avatar_definition]) ).
fof(f1563,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| ~ m1_subset_1(X1,u1_struct_0(sK0))
| k4_lattices(sK0,X0,X1) = k2_lattices(sK0,X0,X1) )
| ~ spl30_73 ),
inference(avatar_component_clause,[],[f1562]) ).
fof(f1564,plain,
( ~ spl30_1
| spl30_73 ),
inference(avatar_split_clause,[],[f1555,f1562,f456]) ).
fof(f1569,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k4_lattices(sK0,X0,sK4(sK1,sK2)) = k4_lattices(sK0,sK4(sK1,sK2),X0) )
| ~ spl30_43
| ~ spl30_72 ),
inference(resolution,[],[f1559,f861]) ).
fof(f1592,plain,
( k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)) = k4_lattices(sK0,sK4(sK1,sK2),sK3(sK1,sK2))
| ~ spl30_43
| ~ spl30_46
| ~ spl30_72 ),
inference(resolution,[],[f1569,f922]) ).
fof(f1638,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK0))
| k4_lattices(sK0,sK3(sK1,sK2),X0) = k2_lattices(sK0,sK3(sK1,sK2),X0) )
| ~ spl30_46
| ~ spl30_73 ),
inference(resolution,[],[f1563,f922]) ).
fof(f1659,plain,
( k2_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)) = k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_43
| ~ spl30_46
| ~ spl30_73 ),
inference(resolution,[],[f1638,f861]) ).
fof(f1693,plain,
( k4_lattices(sK1,sK3(sK1,sK2),sK4(sK1,sK2)) = k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2))
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(superposition,[],[f1542,f1659]) ).
fof(f1698,plain,
( ~ r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(superposition,[],[f1155,f1693]) ).
fof(f1699,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,sK1)
| r2_hidden(sK4(sK1,sK2),sK2)
| 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)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(superposition,[],[f245,f1693]) ).
fof(f1700,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| m1_filter_0(sK2,sK1)
| r2_hidden(sK3(sK1,sK2),sK2)
| 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)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(superposition,[],[f246,f1693]) ).
fof(f1865,plain,
( ~ r2_hidden(sK3(sK1,sK2),sK2)
| ~ r2_hidden(sK4(sK1,sK2),sK2)
| ~ m1_filter_0(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(resolution,[],[f1698,f378]) ).
fof(f1867,plain,
( ~ r2_hidden(sK4(sK1,sK2),sK2)
| ~ m1_filter_0(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1865,f1126]) ).
fof(f1891,plain,
( ~ m1_filter_0(sK2,sK1)
| spl30_42 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f1892,plain,
( ~ r2_hidden(sK3(sK1,sK2),sK2)
| spl30_59 ),
inference(avatar_component_clause,[],[f1125]) ).
fof(f1900,plain,
( ~ m1_filter_0(sK2,sK0)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| spl30_64 ),
inference(resolution,[],[f1158,f259]) ).
fof(f1905,plain,
( v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| spl30_64 ),
inference(forward_subsumption_resolution,[],[f1900,f382]) ).
fof(f1907,plain,
( ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| spl30_64 ),
inference(forward_subsumption_resolution,[],[f1905,f213]) ).
fof(f1909,plain,
( ~ l3_lattices(sK0)
| spl30_64 ),
inference(forward_subsumption_resolution,[],[f1907,f212]) ).
fof(f1912,plain,
( $false
| spl30_64 ),
inference(forward_subsumption_resolution,[],[f1909,f211]) ).
fof(f1913,plain,
spl30_64,
inference(avatar_contradiction_clause,[],[f1912]) ).
fof(f1914,plain,
( ~ r2_hidden(sK4(sK1,sK2),sK2)
| v3_struct_0(sK0)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1867,f382]) ).
fof(f1916,plain,
( m1_filter_0(sK2,sK1)
| r2_hidden(sK4(sK1,sK2),sK2)
| 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)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1699,f1698]) ).
fof(f1918,plain,
( ~ r2_hidden(sK4(sK1,sK2),sK2)
| ~ v10_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1914,f213]) ).
fof(f1920,plain,
( r2_hidden(sK4(sK1,sK2),sK2)
| 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)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1916,f1891]) ).
fof(f1922,plain,
( ~ r2_hidden(sK4(sK1,sK2),sK2)
| ~ l3_lattices(sK0)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1918,f212]) ).
fof(f1924,plain,
( r2_hidden(sK4(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1920,f216]) ).
fof(f1926,plain,
( ~ r2_hidden(sK4(sK1,sK2),sK2)
| ~ spl30_40
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1922,f211]) ).
fof(f1928,plain,
( r2_hidden(sK4(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1924,f215]) ).
fof(f1931,plain,
( v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1928,f1926]) ).
fof(f1933,plain,
( v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1931,f214]) ).
fof(f1935,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2)
| ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_demodulation,[],[f1933,f755]) ).
fof(f1936,plain,
( spl30_41
| ~ spl30_64
| ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_70
| ~ spl30_73 ),
inference(avatar_split_clause,[],[f1935,f1562,f1410,f1154,f1125,f939,f921,f860,f857,f834,f745,f470,f1157,f854]) ).
fof(f1937,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| r2_hidden(sK4(sK1,sK2),sK2)
| 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)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1699,f1891]) ).
fof(f1938,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| r2_hidden(sK4(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1937,f216]) ).
fof(f1939,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| r2_hidden(sK4(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1938,f215]) ).
fof(f1940,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| r2_hidden(sK4(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1939,f214]) ).
fof(f1941,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| r2_hidden(sK4(sK1,sK2),sK2)
| v1_xboole_0(sK2)
| ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_demodulation,[],[f1940,f755]) ).
fof(f1943,definition,
( spl30_79
<=> r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2) ),
introduced(definition,[new_symbols(definition,[spl30_79])],[avatar_definition]) ).
fof(f1944,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| ~ spl30_79 ),
inference(avatar_component_clause,[],[f1943]) ).
fof(f1945,plain,
( spl30_41
| spl30_61
| spl30_79
| ~ spl30_64
| ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(avatar_split_clause,[],[f1941,f1562,f1410,f939,f921,f860,f857,f834,f745,f470,f1157,f1943,f1139,f854]) ).
fof(f1952,plain,
( ~ r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| ~ m1_subset_1(sK3(sK1,sK2),u1_struct_0(sK0))
| ~ spl30_43
| ~ spl30_46
| ~ spl30_62
| ~ spl30_72 ),
inference(superposition,[],[f1143,f1592]) ).
fof(f1953,plain,
( ~ m1_subset_1(sK3(sK1,sK2),u1_struct_0(sK0))
| ~ spl30_43
| ~ spl30_46
| ~ spl30_62
| ~ spl30_72
| ~ spl30_79 ),
inference(forward_subsumption_resolution,[],[f1952,f1944]) ).
fof(f1955,plain,
( $false
| ~ spl30_43
| ~ spl30_46
| ~ spl30_62
| ~ spl30_72
| ~ spl30_79 ),
inference(forward_subsumption_resolution,[],[f1953,f922]) ).
fof(f1956,plain,
( ~ spl30_43
| ~ spl30_46
| ~ spl30_62
| ~ spl30_72
| ~ spl30_79 ),
inference(avatar_contradiction_clause,[],[f1955]) ).
fof(f1969,plain,
( $false
| ~ spl30_43
| ~ spl30_46
| spl30_59
| ~ spl30_79 ),
inference(unit_resulting_resolution,[],[f376,f211,f212,f213,f382,f922,f861,f1944,f1892]) ).
fof(f1971,plain,
( ~ spl30_43
| ~ spl30_46
| spl30_59
| ~ spl30_79 ),
inference(avatar_contradiction_clause,[],[f1969]) ).
fof(f1972,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| r2_hidden(sK3(sK1,sK2),sK2)
| 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)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1700,f1891]) ).
fof(f1973,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| 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)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1972,f1892]) ).
fof(f1974,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1973,f216]) ).
fof(f1975,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1974,f215]) ).
fof(f1976,plain,
( r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_subsumption_resolution,[],[f1975,f214]) ).
fof(f1977,plain,
( ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| r2_hidden(k4_lattices(sK0,sK3(sK1,sK2),sK4(sK1,sK2)),sK2)
| v1_xboole_0(sK2)
| ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_70
| ~ spl30_73 ),
inference(forward_demodulation,[],[f1976,f755]) ).
fof(f1978,plain,
( spl30_41
| spl30_79
| ~ spl30_64
| ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_70
| ~ spl30_73 ),
inference(avatar_split_clause,[],[f1977,f1562,f1410,f1125,f939,f921,f860,f857,f834,f745,f470,f1157,f1943,f854]) ).
cnf(s1,plain,
( ~ spl30_1
| spl30_2 ),
inference(sat_conversion,[],[f461]) ).
cnf(s3,plain,
spl30_1,
inference(sat_conversion,[],[f466]) ).
cnf(s4,plain,
( ~ spl30_2
| spl30_3
| spl30_4 ),
inference(sat_conversion,[],[f475]) ).
cnf(s5,plain,
( ~ spl30_4
| ~ spl30_5
| ~ spl30_6 ),
inference(sat_conversion,[],[f484]) ).
cnf(s7,plain,
spl30_5,
inference(sat_conversion,[],[f490]) ).
cnf(s9,plain,
spl30_6,
inference(sat_conversion,[],[f498]) ).
cnf(s16,plain,
spl30_7,
inference(sat_conversion,[],[f535]) ).
cnf(s19,plain,
spl30_13,
inference(sat_conversion,[],[f559]) ).
cnf(s39,plain,
( ~ spl30_1
| spl30_33 ),
inference(sat_conversion,[],[f737]) ).
cnf(s40,plain,
( ~ spl30_13
| ~ spl30_33
| spl30_34 ),
inference(sat_conversion,[],[f747]) ).
cnf(s46,plain,
( ~ spl30_3
| ~ spl30_7
| ~ spl30_34
| spl30_40 ),
inference(sat_conversion,[],[f836]) ).
cnf(s49,plain,
( ~ spl30_3
| ~ spl30_34
| spl30_41
| spl30_42
| spl30_43 ),
inference(sat_conversion,[],[f862]) ).
cnf(s51,plain,
~ spl30_41,
inference(sat_conversion,[],[f868]) ).
cnf(s53,plain,
~ spl30_42,
inference(sat_conversion,[],[f883]) ).
cnf(s56,plain,
( ~ spl30_3
| ~ spl30_34
| spl30_41
| spl30_42
| spl30_46 ),
inference(sat_conversion,[],[f923]) ).
cnf(s57,plain,
( ~ spl30_1
| ~ spl30_46
| spl30_47 ),
inference(sat_conversion,[],[f941]) ).
cnf(s70,plain,
( ~ spl30_43
| spl30_61
| spl30_62 ),
inference(sat_conversion,[],[f1144]) ).
cnf(s71,plain,
( ~ spl30_3
| ~ spl30_34
| spl30_41
| spl30_42
| ~ spl30_59
| ~ spl30_61
| ~ spl30_63
| ~ spl30_64 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s77,plain,
( ~ spl30_3
| ~ spl30_7
| ~ spl30_34
| spl30_70 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s79,plain,
( ~ spl30_1
| spl30_72 ),
inference(sat_conversion,[],[f1560]) ).
cnf(s80,plain,
( ~ spl30_1
| spl30_73 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s95,plain,
spl30_64,
inference(sat_conversion,[],[f1913]) ).
cnf(s97,plain,
( ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_41
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| ~ spl30_59
| spl30_63
| ~ spl30_64
| ~ spl30_70
| ~ spl30_73 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s98,plain,
( ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_41
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_61
| ~ spl30_64
| ~ spl30_70
| ~ spl30_73
| spl30_79 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s99,plain,
( ~ spl30_43
| ~ spl30_46
| ~ spl30_62
| ~ spl30_72
| ~ spl30_79 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s102,plain,
( ~ spl30_43
| ~ spl30_46
| spl30_59
| ~ spl30_79 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s103,plain,
( ~ spl30_3
| ~ spl30_34
| ~ spl30_40
| spl30_41
| spl30_42
| ~ spl30_43
| ~ spl30_46
| ~ spl30_47
| spl30_59
| ~ spl30_64
| ~ spl30_70
| ~ spl30_73
| spl30_79 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s106,plain,
( ~ spl30_3
| ~ spl30_34
| spl30_41
| spl30_42
| ~ spl30_59
| ~ spl30_61
| ~ spl30_63 ),
inference(rat,[],[s71,s95]) ).
cnf(s107,plain,
( ~ spl30_3
| ~ spl30_34
| spl30_43 ),
inference(rat,[],[s49,s53,s51]) ).
cnf(s119,plain,
~ spl30_4,
inference(rat,[],[s5,s9,s7]) ).
cnf(s120,plain,
( ~ spl30_2
| spl30_3 ),
inference(rat,[],[s4,s119]) ).
cnf(s122,plain,
spl30_73,
inference(rat,[],[s80,s3]) ).
cnf(s123,plain,
spl30_72,
inference(rat,[],[s79,s3]) ).
cnf(s124,plain,
spl30_33,
inference(rat,[],[s39,s3]) ).
cnf(s129,plain,
spl30_34,
inference(rat,[],[s40,s19,s124]) ).
cnf(s132,plain,
spl30_2,
inference(rat,[],[s1,s3]) ).
cnf(s133,plain,
spl30_3,
inference(rat,[],[s120,s132]) ).
cnf(s135,plain,
spl30_70,
inference(rat,[],[s77,s129,s16,s133]) ).
cnf(s137,plain,
spl30_46,
inference(rat,[],[s56,s129,s53,s51,s133]) ).
cnf(s138,plain,
spl30_43,
inference(rat,[],[s107,s129,s133]) ).
cnf(s139,plain,
spl30_40,
inference(rat,[],[s46,s129,s16,s133]) ).
cnf(s151,plain,
spl30_47,
inference(rat,[],[s57,s3,s137]) ).
cnf(s172,plain,
spl30_59,
inference(rat,[],[s103,s102,s129,s51,s53,s133,s137,s151,s138,s95,s135,s122,s139]) ).
cnf(s173,plain,
spl30_63,
inference(rat,[],[s97,s122,s135,s95,s139,s138,s151,s137,s133,s53,s51,s129,s172]) ).
cnf(s174,plain,
~ spl30_61,
inference(rat,[],[s106,s172,s133,s129,s53,s51,s173]) ).
cnf(s175,plain,
spl30_62,
inference(rat,[],[s70,s138,s174]) ).
cnf(s176,plain,
spl30_79,
inference(rat,[],[s98,s139,s122,s135,s95,s138,s151,s137,s133,s53,s51,s129,s174]) ).
cnf(s177,plain,
$false,
inference(rat,[],[s99,s138,s123,s137,s176,s175]) ).
fof(f1979,plain,
$false,
inference(avatar_sat_refutation,[],[s177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT298+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/0.42 % Computer : n014.cluster.edu
% 0.18/0.42 % Model : x86_64 x86_64
% 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42 % Memory : 8046.5625MB
% 0.18/0.42 % OS : Linux 6.8.0-71-generic
% 0.18/0.42 % CPULimit : 300
% 0.18/0.42 % WCLimit : 300
% 0.18/0.42 % DateTime : Sun Sep 27 14:21:18 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 Running first-order theorem proving
% 0.23/0.48 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
% 12.80/3.02 % (862774)Detected formulas, will run a generic FOF schedule.
% 12.80/3.02 % (862783)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=755663374:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.80/3.02 % (862785)dis-21_1_sil=8000:lcm=predicate:random_seed=1496400593: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)
% 12.80/3.02 % (862779)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=2338108109:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.80/3.02 % (862781)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=629863611:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.80/3.02 % (862782)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=801722972:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.80/3.02 % (862780)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=383229779:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.80/3.02 % (862784)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3502402478:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.80/3.02 % (862782)Refutation not found, incomplete strategy
% 12.80/3.02 % (862782)------------------------------
% 12.80/3.02 % (862782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862782)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862782)Termination reason: Refutation not found, incomplete strategy
% 12.80/3.02 % (862782)Time elapsed: 0.003 s
% 12.80/3.02 % (862782)Peak memory usage: 88 MB
% 12.80/3.02 % (862782)Instructions burned: 1 (million)
% 12.80/3.02 % (862783)Instruction limit reached!
% 12.80/3.02 % (862783)------------------------------
% 12.80/3.02 % (862783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862783)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862783)Termination reason: Instruction limit
% 12.80/3.02 % (862783)Termination phase: Saturation
% 12.80/3.02 % (862783)Time elapsed: 0.058 s
% 12.80/3.02 % (862783)Peak memory usage: 88 MB
% 12.80/3.02 % (862783)Instructions burned: 120 (million)
% 12.80/3.02 % (862785)Instruction limit reached!
% 12.80/3.02 % (862785)------------------------------
% 12.80/3.02 % (862785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862785)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862785)Termination reason: Instruction limit
% 12.80/3.02 % (862785)Termination phase: Saturation
% 12.80/3.02 % (862785)Time elapsed: 0.083 s
% 12.80/3.02 % (862785)Peak memory usage: 93 MB
% 12.80/3.02 % (862785)Instructions burned: 129 (million)
% 12.80/3.02 % (862784)Instruction limit reached!
% 12.80/3.02 % (862784)------------------------------
% 12.80/3.02 % (862784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862784)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862784)Termination reason: Instruction limit
% 12.80/3.02 % (862784)Termination phase: Saturation
% 12.80/3.02 % (862784)Time elapsed: 0.142 s
% 12.80/3.02 % (862784)Peak memory usage: 90 MB
% 12.80/3.02 % (862784)Instructions burned: 139 (million)
% 12.80/3.02 % (862793)lrs+10_1_sil=8000:sp=occurrence:random_seed=1401765896:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.80/3.02 % (862794)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3925249163:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.80/3.02 % (862794)Refutation not found, incomplete strategy
% 12.80/3.02 % (862794)------------------------------
% 12.80/3.02 % (862794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862794)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862794)Termination reason: Refutation not found, incomplete strategy
% 12.80/3.02 % (862794)Time elapsed: 0.004 s
% 12.80/3.02 % (862794)Peak memory usage: 88 MB
% 12.80/3.02 % (862794)Instructions burned: 2 (million)
% 12.80/3.02 % (862782)------------------------------
% 12.80/3.02 % (862782)------------------------------
% 12.80/3.02 % (862793)Instruction limit reached!
% 12.80/3.02 % (862793)------------------------------
% 12.80/3.02 % (862793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862793)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862793)Termination reason: Instruction limit
% 12.80/3.02 % (862793)Termination phase: Saturation
% 12.80/3.02 % (862793)Time elapsed: 0.147 s
% 12.80/3.02 % (862793)Peak memory usage: 92 MB
% 12.80/3.02 % (862793)Instructions burned: 287 (million)
% 12.80/3.02 % (862795)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1042970058:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.80/3.02 % (862799)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3231894358:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 12.80/3.02 % (862798)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=1403737083:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 12.80/3.02 % (862799)Refutation not found, incomplete strategy
% 12.80/3.02 % (862799)------------------------------
% 12.80/3.02 % (862799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862799)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862799)Termination reason: Refutation not found, incomplete strategy
% 12.80/3.02 % (862799)Time elapsed: 0.007 s
% 12.80/3.02 % (862799)Peak memory usage: 89 MB
% 12.80/3.02 % (862799)Instructions burned: 11 (million)
% 12.80/3.02 % (862795)Instruction limit reached!
% 12.80/3.02 % (862795)------------------------------
% 12.80/3.02 % (862795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862795)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862795)Termination reason: Instruction limit
% 12.80/3.02 % (862795)Termination phase: Saturation
% 12.80/3.02 % (862795)Time elapsed: 0.260 s
% 12.80/3.02 % (862795)Peak memory usage: 91 MB
% 12.80/3.02 % (862795)Instructions burned: 325 (million)
% 12.80/3.02 % (862794)------------------------------
% 12.80/3.02 % (862794)------------------------------
% 12.80/3.02 % (862799)------------------------------
% 12.80/3.02 % (862799)------------------------------
% 12.80/3.02 % (862798)Instruction limit reached!
% 12.80/3.02 % (862798)------------------------------
% 12.80/3.02 % (862798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862798)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862798)Termination reason: Instruction limit
% 12.80/3.02 % (862798)Termination phase: Saturation
% 12.80/3.02 % (862798)Time elapsed: 0.231 s
% 12.80/3.02 % (862798)Peak memory usage: 94 MB
% 12.80/3.02 % (862798)Instructions burned: 249 (million)
% 12.80/3.02 % (862803)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1850326454:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 12.80/3.02 % (862804)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1074876882:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 12.80/3.02 % (862804)Instruction limit reached!
% 12.80/3.02 % (862804)------------------------------
% 12.80/3.02 % (862804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862804)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862804)Termination reason: Instruction limit
% 12.80/3.02 % (862804)Termination phase: Saturation
% 12.80/3.02 % (862804)Time elapsed: 0.119 s
% 12.80/3.02 % (862804)Peak memory usage: 90 MB
% 12.80/3.02 % (862804)Instructions burned: 113 (million)
% 12.80/3.02 % (862805)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=921192611:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 12.80/3.02 % (862806)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3920715548:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 12.80/3.02 % (862806)Refutation not found, incomplete strategy
% 12.80/3.02 % (862806)------------------------------
% 12.80/3.02 % (862806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862806)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862806)Termination reason: Refutation not found, incomplete strategy
% 12.80/3.02 % (862806)Time elapsed: 0.008 s
% 12.80/3.02 % (862806)Peak memory usage: 88 MB
% 12.80/3.02 % (862806)Instructions burned: 6 (million)
% 12.80/3.02 % (862805)Instruction limit reached!
% 12.80/3.02 % (862805)------------------------------
% 12.80/3.02 % (862805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/3.02 % (862805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/3.02 % (862805)CaDiCaL version: 2.1.3
% 12.80/3.02 % (862805)Termination reason: Instruction limit
% 12.80/3.02 % (862805)Termination phase: Saturation
% 12.80/3.02 % (862805)Time elapsed: 0.112 s
% 12.80/3.02 % (862805)Peak memory usage: 89 MB
% 12.80/3.02 % (862805)Instructions burned: 127 (million)
% 12.80/3.02 % (862780)First to succeed.
% 12.80/3.02 % (862780)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-862774"
% 12.80/3.02 % (862809)lrs+10_1_sil=8000:sp=occurrence:random_seed=3217063780:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 12.80/3.02 % (862781)Also succeeded, but the first one will report.
% 12.80/3.02 % (862806)------------------------------
% 12.80/3.02 % (862806)------------------------------
% 12.80/3.02 % (862812)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3771862540:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 12.80/3.02 % (862812)Also succeeded, but the first one will report.
% 12.80/3.02 % (862779)Also succeeded, but the first one will report.
% 12.80/3.02 % (862780)Refutation found. Thanks to Tanya!
% 12.80/3.02 % SZS status Theorem for theBenchmark
% 12.80/3.02 % SZS output start Proof for theBenchmark
% See solution above
% 14.88/3.29 % (862780)------------------------------
% 14.88/3.29 % (862780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.88/3.29 % (862780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.88/3.29 % (862780)CaDiCaL version: 2.1.3
% 14.88/3.29 % (862780)Termination reason: Refutation
% 14.88/3.29 % (862780)Time elapsed: 1.345 s
% 14.88/3.29 % (862780)Peak memory usage: 133 MB
% 14.88/3.29 % (862780)Instructions burned: 1254 (million)
% 14.88/3.29 % (862780)------------------------------
% 14.88/3.29 % (862780)------------------------------
% 14.88/3.29 % (862774)Success in time 2.007 s
% 14.88/3.29 % Vampire exiting
%------------------------------------------------------------------------------