%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT321+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:54 AM UTC 2026
% Result : Theorem 7.23s 2.32s
% Output : Refutation 9.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 52
% Syntax : Number of formulae : 478 ( 50 unt; 28 def)
% Number of atoms : 2346 ( 216 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 3185 (1317 ~;1556 |; 233 &)
% ( 36 <=>; 41 =>; 0 <=; 2 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 59 ( 57 usr; 25 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-3 aty)
% Number of variables : 372 ( 0 sgn 356 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t57_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(X0)
=> X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f15,axiom,
! [X0] :
( l3_lattices(X0)
=> k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattice2) ).
fof(f16,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f17,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
=> k6_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_filter_2) ).
fof(f18,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f20,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f21,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f26,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) )
=> m1_subset_1(k6_filter_2(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_filter_2) ).
fof(f28,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_lattices) ).
fof(f32,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f37,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/sandbox2/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f38,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f40,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/sandbox2/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f42,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/sandbox2/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(f55,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f62,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v12_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_filter_2) ).
fof(f67,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/sandbox2/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f85,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m2_filter_2(X1,X0) )
=> k15_filter_2(X0,X1) = k7_filter_2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f86,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f87,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f91,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_filter_2) ).
fof(f94,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
=> ( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
& k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t55_filter_2) ).
fof(f95,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( v1_filter_0(X1,X0)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t57_filter_0) ).
fof(f110,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) ) ),
inference(pure_predicate_removal,[],[f62]) ).
fof(f115,plain,
? [X0] :
( ? [X1] :
( ( r2_filter_2(X0,X1)
<~> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f116,plain,
? [X0] :
( ? [X1] :
( ( r2_filter_2(X0,X1)
<~> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f118,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f117]) ).
fof(f138,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f139,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f140,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f139]) ).
fof(f141,plain,
! [X0] :
( ! [X1] :
( k6_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f142,plain,
! [X0] :
( ! [X1] :
( k6_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f141]) ).
fof(f143,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = 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,[],[f18]) ).
fof(f144,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f143]) ).
fof(f147,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f148,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f147]) ).
fof(f149,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f152,plain,
! [X0,X1] :
( m1_subset_1(k6_filter_2(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(ennf_transformation,[],[f26]) ).
fof(f153,plain,
! [X0,X1] :
( m1_subset_1(k6_filter_2(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(flattening,[],[f152]) ).
fof(f156,plain,
! [X0,X1] :
( m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f28]) ).
fof(f157,plain,
! [X0,X1] :
( m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f156]) ).
fof(f160,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f165,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,[],[f37]) ).
fof(f166,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,[],[f165]) ).
fof(f167,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,[],[f38]) ).
fof(f168,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,[],[f167]) ).
fof(f170,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,[],[f40]) ).
fof(f171,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,[],[f42]) ).
fof(f182,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f183,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f182]) ).
fof(f192,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f110]) ).
fof(f193,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f192]) ).
fof(f202,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,[],[f67]) ).
fof(f203,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,[],[f202]) ).
fof(f209,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(ennf_transformation,[],[f85]) ).
fof(f210,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(flattening,[],[f209]) ).
fof(f211,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,[],[f86]) ).
fof(f212,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,[],[f211]) ).
fof(f216,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f91]) ).
fof(f217,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f216]) ).
fof(f221,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
& k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2) )
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f222,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1)) = k7_lattices(X0,X1)
& k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2) )
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f221]) ).
fof(f223,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_0(X1,X0)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f95]) ).
fof(f224,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_0(X1,X0)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f223]) ).
fof(f229,definition,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f230,plain,
! [X0] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f193,f229]) ).
fof(f233,plain,
? [X0] :
( ? [X1] :
( ( u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ r2_filter_2(X0,X1) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| r2_filter_2(X0,X1) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f116]) ).
fof(f234,plain,
? [X0] :
( ? [X1] :
( ( u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ r2_filter_2(X0,X1) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| r2_filter_2(X0,X1) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f233]) ).
fof(f235,plain,
? [X0] :
( ? [X1] :
( ( u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) )
| ~ r2_filter_2(X0,X1) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| r2_filter_2(X0,X1) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(rectify,[],[f234]) ).
fof(f236,plain,
( ( sK3 = u1_struct_0(sK2)
| ( ~ r2_hidden(sK4,sK3)
& ~ r2_hidden(k7_lattices(sK2,sK4),sK3)
& m1_subset_1(sK4,u1_struct_0(sK2)) )
| ~ r2_filter_2(sK2,sK3) )
& ( ( sK3 != u1_struct_0(sK2)
& ! [X3] :
( r2_hidden(X3,sK3)
| r2_hidden(k7_lattices(sK2,X3),sK3)
| ~ m1_subset_1(X3,u1_struct_0(sK2)) ) )
| r2_filter_2(sK2,sK3) )
& m2_filter_2(sK3,sK2)
& ~ v3_struct_0(sK2)
& v10_lattices(sK2)
& v17_lattices(sK2)
& l3_lattices(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f235]) ).
fof(f248,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v11_lattices(k1_lattice2(X0))
& v13_lattices(k1_lattice2(X0))
& v14_lattices(k1_lattice2(X0))
& v15_lattices(k1_lattice2(X0))
& v16_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f229]) ).
fof(f267,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,[],[f212]) ).
fof(f268,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,[],[f87]) ).
fof(f269,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
& ( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f217]) ).
fof(f270,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ v1_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f224]) ).
fof(f271,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( r2_hidden(X2,X1)
| r2_hidden(k7_lattices(X0,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ v1_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f270]) ).
fof(f272,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ? [X2] :
( ~ r2_hidden(X2,X1)
& ~ r2_hidden(k7_lattices(X0,X2),X1)
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f271]) ).
fof(f273,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK33(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK33(X0,X1)),X1)
& m1_subset_1(sK33(X0,X1),u1_struct_0(X0)) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( r2_hidden(X3,X1)
| r2_hidden(k7_lattices(X0,X3),X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ v1_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X2,sK33(X0,X1))],[f272]) ).
fof(f274,plain,
l3_lattices(sK2),
inference(cnf_transformation,[],[f236]) ).
fof(f275,plain,
v17_lattices(sK2),
inference(cnf_transformation,[],[f236]) ).
fof(f276,plain,
v10_lattices(sK2),
inference(cnf_transformation,[],[f236]) ).
fof(f277,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f236]) ).
fof(f278,plain,
m2_filter_2(sK3,sK2),
inference(cnf_transformation,[],[f236]) ).
fof(f279,plain,
! [X3] :
( r2_hidden(X3,sK3)
| r2_hidden(k7_lattices(sK2,X3),sK3)
| ~ m1_subset_1(X3,u1_struct_0(sK2))
| r2_filter_2(sK2,sK3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f280,plain,
( sK3 != u1_struct_0(sK2)
| r2_filter_2(sK2,sK3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f281,plain,
( sK3 = u1_struct_0(sK2)
| m1_subset_1(sK4,u1_struct_0(sK2))
| ~ r2_filter_2(sK2,sK3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f282,plain,
( sK3 = u1_struct_0(sK2)
| ~ r2_hidden(k7_lattices(sK2,sK4),sK3)
| ~ r2_filter_2(sK2,sK3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f283,plain,
( sK3 = u1_struct_0(sK2)
| ~ r2_hidden(sK4,sK3)
| ~ r2_filter_2(sK2,sK3) ),
inference(cnf_transformation,[],[f236]) ).
fof(f284,plain,
! [X0] :
( ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f320,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf_transformation,[],[f138]) ).
fof(f321,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f322,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0)))
| k6_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f142]) ).
fof(f323,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f326,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f327,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f328,plain,
! [X0] :
( v3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f330,plain,
! [X0,X1] :
( m1_subset_1(k6_filter_2(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(k1_lattice2(X0))) ),
inference(cnf_transformation,[],[f153]) ).
fof(f332,plain,
! [X0,X1] :
( m1_subset_1(k7_lattices(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f157]) ).
fof(f335,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f160]) ).
fof(f336,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f160]) ).
fof(f341,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f166]) ).
fof(f343,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,[],[f168]) ).
fof(f345,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,[],[f170]) ).
fof(f346,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,[],[f170]) ).
fof(f347,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f348,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,[],[f171]) ).
fof(f349,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,[],[f171]) ).
fof(f350,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f171]) ).
fof(f364,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f376,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f382,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f391,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f230]) ).
fof(f411,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3
| ~ 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,[],[f203]) ).
fof(f502,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k7_filter_2(X0,X1) = k15_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f210]) ).
fof(f503,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,[],[f267]) ).
fof(f505,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f268]) ).
fof(f510,plain,
! [X0,X1] :
( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f511,plain,
! [X0,X1] :
( ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f514,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
| k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f515,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
| k7_lattices(X0,X1) = k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f516,plain,
! [X3,X0,X1] :
( r2_hidden(k7_lattices(X0,X3),X1)
| r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f517,plain,
! [X0,X1] :
( u1_struct_0(X0) != X1
| ~ v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f518,plain,
! [X0,X1] :
( m1_subset_1(sK33(X0,X1),u1_struct_0(X0))
| u1_struct_0(X0) = X1
| v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f519,plain,
! [X0,X1] :
( ~ r2_hidden(k7_lattices(X0,sK33(X0,X1)),X1)
| u1_struct_0(X0) = X1
| v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f520,plain,
! [X0,X1] :
( ~ r2_hidden(sK33(X0,X1),X1)
| u1_struct_0(X0) = X1
| v1_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f525,plain,
! [X0] :
( ~ v1_filter_0(u1_struct_0(X0),X0)
| ~ m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f517]) ).
fof(f526,definition,
sF34 = u1_struct_0(sK2),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f527,plain,
u1_struct_0(sK2) = sF34,
inference(reorient_equations,[],[f526]) ).
fof(f528,plain,
( sK3 = sF34
| ~ r2_hidden(sK4,sK3)
| ~ r2_filter_2(sK2,sK3) ),
inference(definition_folding,[],[f283,f527]) ).
fof(f529,definition,
sF35 = k7_lattices(sK2,sK4),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f530,plain,
k7_lattices(sK2,sK4) = sF35,
inference(reorient_equations,[],[f529]) ).
fof(f531,plain,
( sK3 = sF34
| ~ r2_hidden(sF35,sK3)
| ~ r2_filter_2(sK2,sK3) ),
inference(definition_folding,[],[f282,f530,f527]) ).
fof(f532,plain,
( sK3 = sF34
| m1_subset_1(sK4,sF34)
| ~ r2_filter_2(sK2,sK3) ),
inference(definition_folding,[],[f281,f527,f527]) ).
fof(f533,plain,
( sK3 != sF34
| r2_filter_2(sK2,sK3) ),
inference(definition_folding,[],[f280,f527]) ).
fof(f534,definition,
! [X3] : sF36(X3) = k7_lattices(sK2,X3),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f535,plain,
! [X3] : k7_lattices(sK2,X3) = sF36(X3),
inference(reorient_equations,[],[f534]) ).
fof(f536,plain,
! [X3] :
( r2_hidden(X3,sK3)
| r2_hidden(sF36(X3),sK3)
| ~ m1_subset_1(X3,sF34)
| r2_filter_2(sK2,sK3) ),
inference(definition_folding,[],[f279,f527,f535]) ).
fof(f538,definition,
( spl37_1
<=> r2_filter_2(sK2,sK3) ),
introduced(definition,[new_symbols(definition,[spl37_1])],[avatar_definition]) ).
fof(f539,plain,
( ~ r2_filter_2(sK2,sK3)
| spl37_1 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( r2_filter_2(sK2,sK3)
| ~ spl37_1 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f542,definition,
( spl37_2
<=> ! [X3] :
( r2_hidden(X3,sK3)
| ~ m1_subset_1(X3,sF34)
| r2_hidden(sF36(X3),sK3) ) ),
introduced(definition,[new_symbols(definition,[spl37_2])],[avatar_definition]) ).
fof(f543,plain,
( ! [X3] :
( r2_hidden(sF36(X3),sK3)
| ~ m1_subset_1(X3,sF34)
| r2_hidden(X3,sK3) )
| ~ spl37_2 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f544,plain,
( spl37_1
| spl37_2 ),
inference(avatar_split_clause,[],[f536,f542,f538]) ).
fof(f546,definition,
( spl37_3
<=> sK3 = sF34 ),
introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition]) ).
fof(f547,plain,
( sK3 = sF34
| ~ spl37_3 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f548,plain,
( sK3 != sF34
| spl37_3 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f549,plain,
( spl37_1
| ~ spl37_3 ),
inference(avatar_split_clause,[],[f533,f546,f538]) ).
fof(f551,definition,
( spl37_4
<=> m1_subset_1(sK4,sF34) ),
introduced(definition,[new_symbols(definition,[spl37_4])],[avatar_definition]) ).
fof(f553,plain,
( m1_subset_1(sK4,sF34)
| ~ spl37_4 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f554,plain,
( ~ spl37_1
| spl37_4
| spl37_3 ),
inference(avatar_split_clause,[],[f532,f546,f551,f538]) ).
fof(f556,definition,
( spl37_5
<=> r2_hidden(sF35,sK3) ),
introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition]) ).
fof(f558,plain,
( ~ r2_hidden(sF35,sK3)
| spl37_5 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f559,plain,
( ~ spl37_1
| ~ spl37_5
| spl37_3 ),
inference(avatar_split_clause,[],[f531,f546,f556,f538]) ).
fof(f561,definition,
( spl37_6
<=> r2_hidden(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl37_6])],[avatar_definition]) ).
fof(f563,plain,
( ~ r2_hidden(sK4,sK3)
| spl37_6 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f564,plain,
( ~ spl37_1
| ~ spl37_6
| spl37_3 ),
inference(avatar_split_clause,[],[f528,f546,f561,f538]) ).
fof(f566,plain,
sF35 = sF36(sK4),
inference(superposition,[],[f530,f535]) ).
fof(f569,plain,
( v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| k7_filter_2(sK2,sK3) = k15_filter_2(sK2,sK3) ),
inference(resolution,[],[f502,f278]) ).
fof(f570,plain,
( ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| k7_filter_2(sK2,sK3) = k15_filter_2(sK2,sK3) ),
inference(forward_subsumption_resolution,[],[f569,f277]) ).
fof(f571,plain,
( ~ l3_lattices(sK2)
| k7_filter_2(sK2,sK3) = k15_filter_2(sK2,sK3) ),
inference(forward_subsumption_resolution,[],[f570,f276]) ).
fof(f572,plain,
k7_filter_2(sK2,sK3) = k15_filter_2(sK2,sK3),
inference(forward_subsumption_resolution,[],[f571,f274]) ).
fof(f575,plain,
( v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ r2_filter_2(sK2,sK3)
| ~ m2_filter_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(superposition,[],[f510,f572]) ).
fof(f576,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| r2_filter_2(sK2,sK3)
| ~ m2_filter_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(superposition,[],[f511,f572]) ).
fof(f577,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ m2_filter_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f576,f539]) ).
fof(f578,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f577,f278]) ).
fof(f579,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f578,f277]) ).
fof(f580,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f579,f276]) ).
fof(f581,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f580,f274]) ).
fof(f582,plain,
( m1_filter_2(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ m2_filter_2(sK3,sK2) ),
inference(superposition,[],[f326,f572]) ).
fof(f583,plain,
( m1_filter_2(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ m2_filter_2(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f582,f277]) ).
fof(f584,plain,
( m1_filter_2(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ l3_lattices(sK2)
| ~ m2_filter_2(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f583,f276]) ).
fof(f585,plain,
( m1_filter_2(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ m2_filter_2(sK3,sK2) ),
inference(forward_subsumption_resolution,[],[f584,f274]) ).
fof(f586,plain,
m1_filter_2(k7_filter_2(sK2,sK3),k1_lattice2(sK2)),
inference(forward_subsumption_resolution,[],[f585,f278]) ).
fof(f589,plain,
! [X0] :
( m1_subset_1(k7_lattices(sK2,X0),sF34)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2)
| ~ m1_subset_1(X0,sF34) ),
inference(superposition,[],[f332,f527]) ).
fof(f590,plain,
! [X0] :
( m1_subset_1(k7_lattices(sK2,X0),sF34)
| ~ l3_lattices(sK2)
| ~ m1_subset_1(X0,sF34) ),
inference(forward_subsumption_resolution,[],[f589,f277]) ).
fof(f593,plain,
! [X0] :
( m1_subset_1(k7_lattices(sK2,X0),sF34)
| ~ m1_subset_1(X0,sF34) ),
inference(forward_subsumption_resolution,[],[f590,f274]) ).
fof(f596,plain,
! [X0] :
( m1_subset_1(sF36(X0),sF34)
| ~ m1_subset_1(X0,sF34) ),
inference(forward_demodulation,[],[f593,f535]) ).
fof(f615,plain,
( m1_subset_1(sF35,sF34)
| ~ m1_subset_1(sK4,sF34) ),
inference(superposition,[],[f596,f566]) ).
fof(f662,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| k5_filter_2(sK2,X0) = X0
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(superposition,[],[f321,f527]) ).
fof(f664,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| k5_filter_2(sK2,X0) = X0
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f662,f277]) ).
fof(f665,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| k5_filter_2(sK2,X0) = X0
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f664,f276]) ).
fof(f666,plain,
! [X0] :
( ~ m1_subset_1(X0,sF34)
| k5_filter_2(sK2,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f665,f274]) ).
fof(f671,plain,
! [X0,X1] :
( u1_struct_0(k1_lattice2(X0)) = X1
| v1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| sK33(k1_lattice2(X0),X1) = k6_filter_2(X0,sK33(k1_lattice2(X0),X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f518,f322]) ).
fof(f676,plain,
! [X0,X1] :
( u1_struct_0(k1_lattice2(X0)) = X1
| v1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0))
| sK33(k1_lattice2(X0),X1) = k6_filter_2(X0,sK33(k1_lattice2(X0),X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f671,f364]) ).
fof(f678,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,k1_lattice2(X0))
| v1_filter_0(X1,k1_lattice2(X0))
| u1_struct_0(k1_lattice2(X0)) = X1
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| sK33(k1_lattice2(X0),X1) = k6_filter_2(X0,sK33(k1_lattice2(X0),X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f676,f327]) ).
fof(f685,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| k7_filter_2(sK2,X0) = X0
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(superposition,[],[f323,f527]) ).
fof(f686,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| k7_filter_2(sK2,X0) = X0
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f685,f277]) ).
fof(f687,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| k7_filter_2(sK2,X0) = X0
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f686,f276]) ).
fof(f688,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF34))
| k7_filter_2(sK2,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f687,f274]) ).
fof(f689,plain,
( m2_lattice4(sK3,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(resolution,[],[f341,f278]) ).
fof(f690,plain,
( m2_lattice4(sK3,sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f689,f277]) ).
fof(f691,plain,
( m2_lattice4(sK3,sK2)
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f690,f276]) ).
fof(f692,plain,
m2_lattice4(sK3,sK2),
inference(forward_subsumption_resolution,[],[f691,f274]) ).
fof(f693,plain,
( v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ v17_lattices(sK2)
| sP0(sK2) ),
inference(resolution,[],[f391,f274]) ).
fof(f695,plain,
( ~ v10_lattices(sK2)
| ~ v17_lattices(sK2)
| sP0(sK2) ),
inference(forward_subsumption_resolution,[],[f693,f277]) ).
fof(f696,plain,
( ~ v17_lattices(sK2)
| sP0(sK2) ),
inference(forward_subsumption_resolution,[],[f695,f276]) ).
fof(f697,plain,
sP0(sK2),
inference(forward_subsumption_resolution,[],[f696,f275]) ).
fof(f702,plain,
( m1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2)) ),
inference(resolution,[],[f586,f503]) ).
fof(f704,definition,
( spl37_13
<=> l3_lattices(k1_lattice2(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_13])],[avatar_definition]) ).
fof(f705,plain,
( l3_lattices(k1_lattice2(sK2))
| ~ spl37_13 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f706,plain,
( ~ l3_lattices(k1_lattice2(sK2))
| spl37_13 ),
inference(avatar_component_clause,[],[f704]) ).
fof(f708,definition,
( spl37_14
<=> v10_lattices(k1_lattice2(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_14])],[avatar_definition]) ).
fof(f709,plain,
( v10_lattices(k1_lattice2(sK2))
| ~ spl37_14 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f710,plain,
( ~ v10_lattices(k1_lattice2(sK2))
| spl37_14 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f712,definition,
( spl37_15
<=> v3_struct_0(k1_lattice2(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_15])],[avatar_definition]) ).
fof(f713,plain,
( ~ v3_struct_0(k1_lattice2(sK2))
| spl37_15 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f714,plain,
( v3_struct_0(k1_lattice2(sK2))
| ~ spl37_15 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f716,definition,
( spl37_16
<=> m1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_16])],[avatar_definition]) ).
fof(f718,plain,
( m1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ spl37_16 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f719,plain,
( ~ spl37_13
| ~ spl37_14
| spl37_15
| spl37_16 ),
inference(avatar_split_clause,[],[f702,f716,f712,f708,f704]) ).
fof(f720,plain,
( ~ l3_lattices(sK2)
| spl37_13 ),
inference(resolution,[],[f706,f327]) ).
fof(f721,plain,
( $false
| spl37_13 ),
inference(forward_subsumption_resolution,[],[f720,f274]) ).
fof(f722,plain,
spl37_13,
inference(avatar_contradiction_clause,[],[f721]) ).
fof(f767,plain,
! [X2,X0,X1] :
( k7_lattices(X0,k6_filter_2(X0,sK33(k1_lattice2(X0),X1))) = k7_lattices(k1_lattice2(X0),sK33(k1_lattice2(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| u1_struct_0(k1_lattice2(X0)) = X1
| v1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) ),
inference(resolution,[],[f514,f518]) ).
fof(f768,plain,
! [X2,X0,X1] :
( k7_lattices(X0,k6_filter_2(X0,sK33(k1_lattice2(X0),X1))) = k7_lattices(k1_lattice2(X0),sK33(k1_lattice2(X0),X1))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| u1_struct_0(k1_lattice2(X0)) = X1
| v1_filter_0(X1,k1_lattice2(X0))
| ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[],[f767,f364]) ).
fof(f770,plain,
! [X2,X0,X1] :
( ~ m1_filter_0(X1,k1_lattice2(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| u1_struct_0(k1_lattice2(X0)) = X1
| v1_filter_0(X1,k1_lattice2(X0))
| k7_lattices(X0,k6_filter_2(X0,sK33(k1_lattice2(X0),X1))) = k7_lattices(k1_lattice2(X0),sK33(k1_lattice2(X0),X1))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0)) ),
inference(forward_subsumption_resolution,[],[f768,f327]) ).
fof(f776,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ m2_lattice4(X0,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(superposition,[],[f343,f527]) ).
fof(f778,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ m2_lattice4(X0,sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f776,f277]) ).
fof(f780,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ m2_lattice4(X0,sK2)
| ~ l3_lattices(sK2) ),
inference(forward_subsumption_resolution,[],[f778,f276]) ).
fof(f781,plain,
! [X0] :
( m1_subset_1(X0,k1_zfmisc_1(sF34))
| ~ m2_lattice4(X0,sK2) ),
inference(forward_subsumption_resolution,[],[f780,f274]) ).
fof(f782,plain,
! [X0] :
( ~ m2_lattice4(X0,sK2)
| k7_filter_2(sK2,X0) = X0 ),
inference(resolution,[],[f781,f688]) ).
fof(f785,plain,
sK3 = k7_filter_2(sK2,sK3),
inference(resolution,[],[f782,f692]) ).
fof(f787,plain,
( ~ v1_filter_0(sK3,k1_lattice2(sK2))
| spl37_1 ),
inference(superposition,[],[f581,f785]) ).
fof(f819,plain,
( v3_struct_0(sK2)
| ~ l3_lattices(sK2)
| ~ spl37_15 ),
inference(resolution,[],[f714,f364]) ).
fof(f820,plain,
( ~ l3_lattices(sK2)
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f819,f277]) ).
fof(f821,plain,
( $false
| ~ spl37_15 ),
inference(forward_subsumption_resolution,[],[f820,f274]) ).
fof(f822,plain,
~ spl37_15,
inference(avatar_contradiction_clause,[],[f821]) ).
fof(f874,plain,
k1_lattice2(sK2) = g3_lattices(u1_struct_0(sK2),u1_lattices(sK2),u2_lattices(sK2)),
inference(resolution,[],[f320,f274]) ).
fof(f877,plain,
k1_lattice2(sK2) = g3_lattices(sF34,u1_lattices(sK2),u2_lattices(sK2)),
inference(forward_demodulation,[],[f874,f527]) ).
fof(f880,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(k1_lattice2(X0)),u2_lattices(k1_lattice2(X0)),u1_lattices(k1_lattice2(X0)))
| ~ l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(resolution,[],[f284,f328]) ).
fof(f881,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_lattice2(X0) = g3_lattices(u1_struct_0(k1_lattice2(X0)),u2_lattices(k1_lattice2(X0)),u1_lattices(k1_lattice2(X0))) ),
inference(forward_subsumption_resolution,[],[f880,f327]) ).
fof(f884,plain,
l2_lattices(sK2),
inference(resolution,[],[f335,f274]) ).
fof(f887,plain,
l1_lattices(sK2),
inference(resolution,[],[f336,f274]) ).
fof(f894,plain,
( ~ sP0(sK2)
| spl37_14 ),
inference(resolution,[],[f382,f710]) ).
fof(f895,plain,
( $false
| spl37_14 ),
inference(forward_subsumption_resolution,[],[f894,f697]) ).
fof(f896,plain,
spl37_14,
inference(avatar_contradiction_clause,[],[f895]) ).
fof(f897,plain,
( m1_filter_0(sK3,k1_lattice2(sK2))
| ~ spl37_16 ),
inference(forward_demodulation,[],[f718,f785]) ).
fof(f922,definition,
( spl37_24
<=> v17_lattices(k1_lattice2(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_24])],[avatar_definition]) ).
fof(f923,plain,
( v17_lattices(k1_lattice2(sK2))
| ~ spl37_24 ),
inference(avatar_component_clause,[],[f922]) ).
fof(f924,plain,
( ~ v17_lattices(k1_lattice2(sK2))
| spl37_24 ),
inference(avatar_component_clause,[],[f922]) ).
fof(f944,plain,
( v1_filter_0(sK3,k1_lattice2(sK2))
| sK3 = u1_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ spl37_16 ),
inference(resolution,[],[f897,f678]) ).
fof(f996,plain,
( ~ sP0(sK2)
| spl37_24 ),
inference(resolution,[],[f376,f924]) ).
fof(f997,plain,
( $false
| spl37_24 ),
inference(forward_subsumption_resolution,[],[f996,f697]) ).
fof(f998,plain,
spl37_24,
inference(avatar_contradiction_clause,[],[f997]) ).
fof(f1000,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1
| ~ spl37_16 ),
inference(forward_subsumption_resolution,[],[f944,f787]) ).
fof(f1002,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1
| ~ spl37_14
| ~ spl37_16 ),
inference(forward_subsumption_resolution,[],[f1000,f709]) ).
fof(f1004,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24 ),
inference(forward_subsumption_resolution,[],[f1002,f923]) ).
fof(f1006,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24 ),
inference(forward_subsumption_resolution,[],[f1004,f277]) ).
fof(f1008,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| ~ l3_lattices(sK2)
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24 ),
inference(forward_subsumption_resolution,[],[f1006,f276]) ).
fof(f1010,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24 ),
inference(forward_subsumption_resolution,[],[f1008,f274]) ).
fof(f1013,definition,
( spl37_30
<=> sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3)) ),
introduced(definition,[new_symbols(definition,[spl37_30])],[avatar_definition]) ).
fof(f1015,plain,
( sK33(k1_lattice2(sK2),sK3) = k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))
| ~ spl37_30 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1017,definition,
( spl37_31
<=> sK3 = u1_struct_0(k1_lattice2(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_31])],[avatar_definition]) ).
fof(f1018,plain,
( sK3 != u1_struct_0(k1_lattice2(sK2))
| spl37_31 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1019,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| ~ spl37_31 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1020,plain,
( spl37_30
| spl37_31
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24 ),
inference(avatar_split_clause,[],[f1010,f922,f716,f708,f538,f1017,f1013]) ).
fof(f1024,definition,
( spl37_32
<=> ! [X0] :
( sF36(X0) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X0))
| ~ m1_subset_1(X0,sF34) ) ),
introduced(definition,[new_symbols(definition,[spl37_32])],[avatar_definition]) ).
fof(f1025,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF34)
| sF36(X0) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X0)) )
| ~ spl37_32 ),
inference(avatar_component_clause,[],[f1024]) ).
fof(f1098,definition,
( spl37_35
<=> ! [X1] : ~ m1_subset_1(X1,sF34) ),
introduced(definition,[new_symbols(definition,[spl37_35])],[avatar_definition]) ).
fof(f1099,plain,
( ! [X1] : ~ m1_subset_1(X1,sF34)
| ~ spl37_35 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1101,plain,
( m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2)))
| ~ spl37_30 ),
inference(superposition,[],[f330,f1015]) ).
fof(f1102,plain,
( m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(sK2))
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2)))
| ~ spl37_30 ),
inference(forward_subsumption_resolution,[],[f1101,f277]) ).
fof(f1103,plain,
( m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2)))
| ~ spl37_30 ),
inference(forward_subsumption_resolution,[],[f1102,f276]) ).
fof(f1104,plain,
( m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(sK2))
| ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2)))
| ~ spl37_30 ),
inference(forward_subsumption_resolution,[],[f1103,f274]) ).
fof(f1105,plain,
( m1_subset_1(sK33(k1_lattice2(sK2),sK3),sF34)
| ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2)))
| ~ spl37_30 ),
inference(forward_demodulation,[],[f1104,f527]) ).
fof(f1107,definition,
( spl37_36
<=> m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2))) ),
introduced(definition,[new_symbols(definition,[spl37_36])],[avatar_definition]) ).
fof(f1109,plain,
( ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),u1_struct_0(k1_lattice2(sK2)))
| spl37_36 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1111,definition,
( spl37_37
<=> m1_subset_1(sK33(k1_lattice2(sK2),sK3),sF34) ),
introduced(definition,[new_symbols(definition,[spl37_37])],[avatar_definition]) ).
fof(f1113,plain,
( m1_subset_1(sK33(k1_lattice2(sK2),sK3),sF34)
| ~ spl37_37 ),
inference(avatar_component_clause,[],[f1111]) ).
fof(f1114,plain,
( ~ spl37_36
| spl37_37
| ~ spl37_30 ),
inference(avatar_split_clause,[],[f1105,f1013,f1111,f1107]) ).
fof(f1115,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_36 ),
inference(resolution,[],[f1109,f518]) ).
fof(f1116,plain,
( v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1115,f1018]) ).
fof(f1117,plain,
( ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1116,f787]) ).
fof(f1118,plain,
( v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_16
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1117,f897]) ).
fof(f1119,plain,
( ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| spl37_15
| ~ spl37_16
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1118,f713]) ).
fof(f1120,plain,
( ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_14
| spl37_15
| ~ spl37_16
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1119,f709]) ).
fof(f1121,plain,
( ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1120,f923]) ).
fof(f1122,plain,
( $false
| spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| spl37_36 ),
inference(forward_subsumption_resolution,[],[f1121,f705]) ).
fof(f1123,plain,
( spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| spl37_36 ),
inference(avatar_contradiction_clause,[],[f1122]) ).
fof(f1124,plain,
( v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ m2_filter_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ spl37_1 ),
inference(forward_subsumption_resolution,[],[f575,f540]) ).
fof(f1127,plain,
( v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ spl37_1 ),
inference(forward_subsumption_resolution,[],[f1124,f278]) ).
fof(f1130,plain,
( v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| ~ spl37_1 ),
inference(forward_subsumption_resolution,[],[f1127,f277]) ).
fof(f1133,plain,
( v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ l3_lattices(sK2)
| ~ spl37_1 ),
inference(forward_subsumption_resolution,[],[f1130,f276]) ).
fof(f1136,plain,
( v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ spl37_1 ),
inference(forward_subsumption_resolution,[],[f1133,f274]) ).
fof(f1139,plain,
( v1_filter_0(sK3,k1_lattice2(sK2))
| ~ spl37_1 ),
inference(forward_demodulation,[],[f1136,f785]) ).
fof(f1211,plain,
k1_lattice2(sK2) = g3_lattices(u1_struct_0(k1_lattice2(sK2)),u2_lattices(k1_lattice2(sK2)),u1_lattices(k1_lattice2(sK2))),
inference(resolution,[],[f881,f274]) ).
fof(f1257,definition,
( spl37_46
<=> m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl37_46])],[avatar_definition]) ).
fof(f1258,plain,
( m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_46 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1259,plain,
( ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| spl37_46 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1261,definition,
( spl37_47
<=> v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl37_47])],[avatar_definition]) ).
fof(f1262,plain,
( v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_47 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1263,plain,
( ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| spl37_47 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1265,definition,
( spl37_48
<=> v1_funct_1(u2_lattices(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_48])],[avatar_definition]) ).
fof(f1266,plain,
( v1_funct_1(u2_lattices(sK2))
| ~ spl37_48 ),
inference(avatar_component_clause,[],[f1265]) ).
fof(f1267,plain,
( ~ v1_funct_1(u2_lattices(sK2))
| spl37_48 ),
inference(avatar_component_clause,[],[f1265]) ).
fof(f1269,definition,
( spl37_49
<=> m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl37_49])],[avatar_definition]) ).
fof(f1270,plain,
( m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_49 ),
inference(avatar_component_clause,[],[f1269]) ).
fof(f1273,definition,
( spl37_50
<=> v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl37_50])],[avatar_definition]) ).
fof(f1274,plain,
( v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_50 ),
inference(avatar_component_clause,[],[f1273]) ).
fof(f1277,definition,
( spl37_51
<=> v1_funct_1(u1_lattices(sK2)) ),
introduced(definition,[new_symbols(definition,[spl37_51])],[avatar_definition]) ).
fof(f1278,plain,
( v1_funct_1(u1_lattices(sK2))
| ~ spl37_51 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1279,plain,
( ~ v1_funct_1(u1_lattices(sK2))
| spl37_51 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1289,plain,
( ~ l1_lattices(sK2)
| spl37_51 ),
inference(resolution,[],[f1279,f347]) ).
fof(f1290,plain,
( $false
| spl37_51 ),
inference(forward_subsumption_resolution,[],[f1289,f887]) ).
fof(f1291,plain,
spl37_51,
inference(avatar_contradiction_clause,[],[f1290]) ).
fof(f1306,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0
| ~ v1_funct_1(u1_lattices(sK2))
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ v1_funct_1(u2_lattices(sK2))
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) ),
inference(superposition,[],[f411,f877]) ).
fof(f1316,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ v1_funct_1(u2_lattices(sK2))
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1306,f1278]) ).
fof(f1317,plain,
( ! [X2,X0,X1] :
( sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ v1_funct_1(u2_lattices(sK2))
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_3
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1316,f547]) ).
fof(f1318,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ v1_funct_1(u2_lattices(sK2))
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_3
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1317,f547]) ).
fof(f1319,plain,
( ! [X2,X0,X1] :
( ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2))
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_3
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1318,f547]) ).
fof(f1320,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2))
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_3
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1319,f547]) ).
fof(f1321,plain,
( ! [X2,X0,X1] :
( ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2)) )
| ~ spl37_3
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1320,f547]) ).
fof(f1485,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,[],[f345,f505]) ).
fof(f1486,plain,
( m2_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ l1_lattices(sK2) ),
inference(superposition,[],[f345,f527]) ).
fof(f1487,plain,
m2_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34),
inference(forward_subsumption_resolution,[],[f1486,f887]) ).
fof(f1488,plain,
( m2_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_3 ),
inference(forward_demodulation,[],[f1487,f547]) ).
fof(f1489,plain,
( m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_3 ),
inference(resolution,[],[f1488,f505]) ).
fof(f1490,plain,
( spl37_49
| ~ spl37_3 ),
inference(avatar_split_clause,[],[f1489,f546,f1269]) ).
fof(f1492,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,[],[f348,f505]) ).
fof(f1493,plain,
( m2_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ l2_lattices(sK2) ),
inference(superposition,[],[f348,f527]) ).
fof(f1494,plain,
m2_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34),
inference(forward_subsumption_resolution,[],[f1493,f884]) ).
fof(f1495,plain,
( m2_relset_1(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_3 ),
inference(forward_demodulation,[],[f1494,f547]) ).
fof(f1496,plain,
( m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_3 ),
inference(resolution,[],[f1495,f505]) ).
fof(f1497,plain,
( $false
| ~ spl37_3
| spl37_46 ),
inference(forward_subsumption_resolution,[],[f1496,f1259]) ).
fof(f1498,plain,
( ~ spl37_3
| spl37_46 ),
inference(avatar_contradiction_clause,[],[f1497]) ).
fof(f1582,plain,
( m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ l1_lattices(sK2) ),
inference(superposition,[],[f1485,f527]) ).
fof(f1583,plain,
m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34),
inference(forward_subsumption_resolution,[],[f1582,f887]) ).
fof(f1600,plain,
( m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ l2_lattices(sK2) ),
inference(superposition,[],[f1492,f527]) ).
fof(f1601,plain,
m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34),
inference(forward_subsumption_resolution,[],[f1600,f884]) ).
fof(f1612,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ v17_lattices(sK2)
| ~ l3_lattices(sK2)
| sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_16 ),
inference(resolution,[],[f770,f897]) ).
fof(f1622,plain,
( v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ l1_lattices(sK2) ),
inference(superposition,[],[f346,f527]) ).
fof(f1623,plain,
v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34),
inference(forward_subsumption_resolution,[],[f1622,f887]) ).
fof(f1626,plain,
( v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_3 ),
inference(forward_demodulation,[],[f1623,f547]) ).
fof(f1627,plain,
( spl37_50
| ~ spl37_3 ),
inference(avatar_split_clause,[],[f1626,f546,f1273]) ).
fof(f1636,plain,
( v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ l2_lattices(sK2) ),
inference(superposition,[],[f349,f527]) ).
fof(f1637,plain,
v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34),
inference(forward_subsumption_resolution,[],[f1636,f884]) ).
fof(f1640,plain,
( v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ spl37_3 ),
inference(forward_demodulation,[],[f1637,f547]) ).
fof(f1641,plain,
( $false
| ~ spl37_3
| spl37_47 ),
inference(forward_subsumption_resolution,[],[f1640,f1263]) ).
fof(f1642,plain,
( ~ spl37_3
| spl37_47 ),
inference(avatar_contradiction_clause,[],[f1641]) ).
fof(f1643,plain,
( ~ l2_lattices(sK2)
| spl37_48 ),
inference(resolution,[],[f1267,f350]) ).
fof(f1644,plain,
( $false
| spl37_48 ),
inference(forward_subsumption_resolution,[],[f1643,f884]) ).
fof(f1645,plain,
spl37_48,
inference(avatar_contradiction_clause,[],[f1644]) ).
fof(f1649,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2)) )
| ~ spl37_3
| ~ spl37_46
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1321,f1258]) ).
fof(f1653,plain,
( ! [X2,X0,X1] :
( ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2)) )
| ~ spl37_3
| ~ spl37_46
| ~ spl37_47
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1649,f1262]) ).
fof(f1657,plain,
( ! [X2,X0,X1] :
( ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sK3,sK3),sK3)
| sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2)) )
| ~ spl37_3
| ~ spl37_46
| ~ spl37_47
| ~ spl37_49
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1653,f1270]) ).
fof(f1661,plain,
( ! [X2,X0,X1] :
( sK3 = X0
| g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| ~ v1_funct_1(u2_lattices(sK2)) )
| ~ spl37_3
| ~ spl37_46
| ~ spl37_47
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1657,f1274]) ).
fof(f1665,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sK3 = X0 )
| ~ spl37_3
| ~ spl37_46
| ~ spl37_47
| ~ spl37_48
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1661,f1266]) ).
fof(f1682,plain,
( k1_lattice2(sK2) != k1_lattice2(sK2)
| sK3 = u1_struct_0(k1_lattice2(sK2))
| ~ spl37_3
| ~ spl37_46
| ~ spl37_47
| ~ spl37_48
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(superposition,[],[f1665,f1211]) ).
fof(f1683,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| ~ spl37_3
| ~ spl37_46
| ~ spl37_47
| ~ spl37_48
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(trivial_inequality_removal,[],[f1682]) ).
fof(f1685,plain,
( $false
| ~ spl37_3
| spl37_31
| ~ spl37_46
| ~ spl37_47
| ~ spl37_48
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1683,f1018]) ).
fof(f1686,plain,
( ~ spl37_3
| spl37_31
| ~ spl37_46
| ~ spl37_47
| ~ spl37_48
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(avatar_contradiction_clause,[],[f1685]) ).
fof(f1714,plain,
( ~ v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_31 ),
inference(superposition,[],[f525,f1019]) ).
fof(f1722,plain,
( ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_31 ),
inference(forward_subsumption_resolution,[],[f1714,f1139]) ).
fof(f1737,plain,
( v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_16
| ~ spl37_31 ),
inference(forward_subsumption_resolution,[],[f1722,f897]) ).
fof(f1747,plain,
( ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_1
| spl37_15
| ~ spl37_16
| ~ spl37_31 ),
inference(forward_subsumption_resolution,[],[f1737,f713]) ).
fof(f1755,plain,
( ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_31 ),
inference(forward_subsumption_resolution,[],[f1747,f709]) ).
fof(f1759,plain,
( ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_31 ),
inference(forward_subsumption_resolution,[],[f1755,f923]) ).
fof(f1763,plain,
( $false
| ~ spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_31 ),
inference(forward_subsumption_resolution,[],[f1759,f705]) ).
fof(f1764,plain,
( ~ spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_31 ),
inference(avatar_contradiction_clause,[],[f1763]) ).
fof(f1767,plain,
( m1_subset_1(sF35,sF34)
| ~ spl37_4 ),
inference(forward_subsumption_resolution,[],[f615,f553]) ).
fof(f1774,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0
| ~ v1_funct_2(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1316,f1266]) ).
fof(f1780,plain,
( $false
| ~ spl37_4
| ~ spl37_35 ),
inference(forward_subsumption_resolution,[],[f1767,f1099]) ).
fof(f1781,plain,
( ~ spl37_4
| ~ spl37_35 ),
inference(avatar_contradiction_clause,[],[f1780]) ).
fof(f1783,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0
| ~ m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1774,f1623]) ).
fof(f1785,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0
| ~ v1_funct_2(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34)
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1783,f1583]) ).
fof(f1787,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0
| ~ m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(sF34,sF34),sF34) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1785,f1637]) ).
fof(f1789,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k1_lattice2(sK2)
| sF34 = X0 )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1787,f1601]) ).
fof(f1790,plain,
( sF36(sK4) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,sK4))
| ~ spl37_4
| ~ spl37_32 ),
inference(resolution,[],[f553,f1025]) ).
fof(f1791,plain,
( sK4 = k5_filter_2(sK2,sK4)
| ~ spl37_4 ),
inference(resolution,[],[f553,f666]) ).
fof(f1794,plain,
( sF36(sK4) = k7_lattices(k1_lattice2(sK2),sK4)
| ~ spl37_4
| ~ spl37_32 ),
inference(forward_demodulation,[],[f1790,f1791]) ).
fof(f1795,plain,
( sF35 = k7_lattices(k1_lattice2(sK2),sK4)
| ~ spl37_4
| ~ spl37_32 ),
inference(forward_demodulation,[],[f1794,f566]) ).
fof(f1797,plain,
( k1_lattice2(sK2) != k1_lattice2(sK2)
| sF34 = u1_struct_0(k1_lattice2(sK2))
| ~ spl37_48
| ~ spl37_51 ),
inference(superposition,[],[f1789,f1211]) ).
fof(f1798,plain,
( sF34 = u1_struct_0(k1_lattice2(sK2))
| ~ spl37_48
| ~ spl37_51 ),
inference(trivial_inequality_removal,[],[f1797]) ).
fof(f1813,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF34)
| k7_lattices(sK2,X1) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ v17_lattices(sK2)
| ~ l3_lattices(sK2) )
| ~ spl37_48
| ~ spl37_51 ),
inference(superposition,[],[f515,f1798]) ).
fof(f1849,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF34)
| k7_lattices(sK2,X1) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK2))
| ~ v10_lattices(sK2)
| ~ v17_lattices(sK2)
| ~ l3_lattices(sK2) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1813,f277]) ).
fof(f1871,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF34)
| k7_lattices(sK2,X1) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK2))
| ~ v17_lattices(sK2)
| ~ l3_lattices(sK2) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1849,f276]) ).
fof(f1886,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF34)
| k7_lattices(sK2,X1) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK2))
| ~ l3_lattices(sK2) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1871,f275]) ).
fof(f1895,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF34)
| k7_lattices(sK2,X1) = k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1))
| ~ m1_subset_1(X1,u1_struct_0(sK2)) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1886,f274]) ).
fof(f1909,plain,
( ! [X0,X1] :
( k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1)) = sF36(X1)
| ~ m1_subset_1(X0,sF34)
| ~ m1_subset_1(X1,u1_struct_0(sK2)) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1895,f535]) ).
fof(f1912,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,sF34)
| k7_lattices(k1_lattice2(sK2),k5_filter_2(sK2,X1)) = sF36(X1)
| ~ m1_subset_1(X0,sF34) )
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1909,f527]) ).
fof(f1947,plain,
( ! [X0] :
( r2_hidden(sF35,X0)
| r2_hidden(sK4,X0)
| ~ m1_subset_1(sK4,u1_struct_0(k1_lattice2(sK2)))
| ~ v1_filter_0(X0,k1_lattice2(sK2))
| ~ m1_filter_0(X0,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2)) )
| ~ spl37_4
| ~ spl37_32 ),
inference(superposition,[],[f516,f1795]) ).
fof(f1950,plain,
( ! [X0] :
( r2_hidden(sF35,X0)
| r2_hidden(sK4,X0)
| ~ m1_subset_1(sK4,u1_struct_0(k1_lattice2(sK2)))
| ~ v1_filter_0(X0,k1_lattice2(sK2))
| ~ m1_filter_0(X0,k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2)) )
| ~ spl37_4
| spl37_15
| ~ spl37_32 ),
inference(forward_subsumption_resolution,[],[f1947,f713]) ).
fof(f1953,plain,
( ! [X0] :
( r2_hidden(sF35,X0)
| r2_hidden(sK4,X0)
| ~ m1_subset_1(sK4,u1_struct_0(k1_lattice2(sK2)))
| ~ v1_filter_0(X0,k1_lattice2(sK2))
| ~ m1_filter_0(X0,k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2)) )
| ~ spl37_4
| ~ spl37_14
| spl37_15
| ~ spl37_32 ),
inference(forward_subsumption_resolution,[],[f1950,f709]) ).
fof(f1956,plain,
( ! [X0] :
( r2_hidden(sF35,X0)
| r2_hidden(sK4,X0)
| ~ m1_subset_1(sK4,u1_struct_0(k1_lattice2(sK2)))
| ~ v1_filter_0(X0,k1_lattice2(sK2))
| ~ m1_filter_0(X0,k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2)) )
| ~ spl37_4
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32 ),
inference(forward_subsumption_resolution,[],[f1953,f923]) ).
fof(f1957,plain,
( ! [X0] :
( r2_hidden(sF35,X0)
| r2_hidden(sK4,X0)
| ~ m1_subset_1(sK4,u1_struct_0(k1_lattice2(sK2)))
| ~ v1_filter_0(X0,k1_lattice2(sK2))
| ~ m1_filter_0(X0,k1_lattice2(sK2)) )
| ~ spl37_4
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32 ),
inference(forward_subsumption_resolution,[],[f1956,f705]) ).
fof(f1958,plain,
( ! [X0] :
( ~ m1_subset_1(sK4,sF34)
| r2_hidden(sF35,X0)
| r2_hidden(sK4,X0)
| ~ v1_filter_0(X0,k1_lattice2(sK2))
| ~ m1_filter_0(X0,k1_lattice2(sK2)) )
| ~ spl37_4
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1957,f1798]) ).
fof(f1959,plain,
( ! [X0] :
( ~ v1_filter_0(X0,k1_lattice2(sK2))
| r2_hidden(sK4,X0)
| r2_hidden(sF35,X0)
| ~ m1_filter_0(X0,k1_lattice2(sK2)) )
| ~ spl37_4
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f1958,f553]) ).
fof(f2056,plain,
( r2_hidden(sK4,sK3)
| r2_hidden(sF35,sK3)
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_4
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(resolution,[],[f1959,f1139]) ).
fof(f2057,plain,
( r2_hidden(sF35,sK3)
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_4
| spl37_6
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f2056,f563]) ).
fof(f2059,plain,
( ~ m1_filter_0(sK3,k1_lattice2(sK2))
| ~ spl37_1
| ~ spl37_4
| spl37_5
| spl37_6
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f2057,f558]) ).
fof(f2061,plain,
( $false
| ~ spl37_1
| ~ spl37_4
| spl37_5
| spl37_6
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f2059,f897]) ).
fof(f2062,plain,
( ~ spl37_1
| ~ spl37_4
| spl37_5
| spl37_6
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(avatar_contradiction_clause,[],[f2061]) ).
fof(f2065,plain,
( spl37_35
| spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(avatar_split_clause,[],[f1912,f1277,f1265,f1024,f1098]) ).
fof(f2073,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ m2_filter_2(sK3,sK2)
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f576,f539]) ).
fof(f2075,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| ~ v10_lattices(sK2)
| ~ v17_lattices(sK2)
| ~ l3_lattices(sK2)
| sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_16 ),
inference(forward_subsumption_resolution,[],[f1612,f277]) ).
fof(f2076,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| v3_struct_0(sK2)
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f2073,f278]) ).
fof(f2078,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| ~ v17_lattices(sK2)
| ~ l3_lattices(sK2)
| sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_16 ),
inference(forward_subsumption_resolution,[],[f2075,f276]) ).
fof(f2079,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ v10_lattices(sK2)
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f2076,f277]) ).
fof(f2081,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_16 ),
inference(forward_subsumption_resolution,[],[f2078,f275]) ).
fof(f2082,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| ~ l3_lattices(sK2)
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f2079,f276]) ).
fof(f2084,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_16 ),
inference(forward_subsumption_resolution,[],[f2081,f274]) ).
fof(f2085,plain,
( ~ v1_filter_0(k7_filter_2(sK2,sK3),k1_lattice2(sK2))
| spl37_1 ),
inference(forward_subsumption_resolution,[],[f2082,f274]) ).
fof(f2087,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_16
| spl37_31 ),
inference(forward_subsumption_resolution,[],[f2084,f1018]) ).
fof(f2088,plain,
( ~ v1_filter_0(sK3,k1_lattice2(sK2))
| spl37_1 ),
inference(forward_demodulation,[],[f2085,f785]) ).
fof(f2089,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v17_lattices(k1_lattice2(sK2)) )
| ~ spl37_14
| ~ spl37_16
| spl37_31 ),
inference(forward_subsumption_resolution,[],[f2087,f709]) ).
fof(f2090,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3))
| ~ v17_lattices(k1_lattice2(sK2)) )
| spl37_1
| ~ spl37_14
| ~ spl37_16
| spl37_31 ),
inference(forward_subsumption_resolution,[],[f2089,f2088]) ).
fof(f2091,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK2))
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3)) )
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| spl37_31 ),
inference(forward_subsumption_resolution,[],[f2090,f923]) ).
fof(f2092,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF34)
| k7_lattices(sK2,k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3))) = k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3)) )
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| spl37_31 ),
inference(forward_demodulation,[],[f2091,f527]) ).
fof(f2093,plain,
( ! [X0] :
( k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3)) = sF36(k6_filter_2(sK2,sK33(k1_lattice2(sK2),sK3)))
| ~ m1_subset_1(X0,sF34) )
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| spl37_31 ),
inference(forward_demodulation,[],[f2092,f535]) ).
fof(f2094,plain,
( ! [X0] :
( k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3)) = sF36(sK33(k1_lattice2(sK2),sK3))
| ~ m1_subset_1(X0,sF34) )
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| ~ spl37_30
| spl37_31 ),
inference(forward_demodulation,[],[f2093,f1015]) ).
fof(f2096,definition,
( spl37_63
<=> k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3)) = sF36(sK33(k1_lattice2(sK2),sK3)) ),
introduced(definition,[new_symbols(definition,[spl37_63])],[avatar_definition]) ).
fof(f2098,plain,
( k7_lattices(k1_lattice2(sK2),sK33(k1_lattice2(sK2),sK3)) = sF36(sK33(k1_lattice2(sK2),sK3))
| ~ spl37_63 ),
inference(avatar_component_clause,[],[f2096]) ).
fof(f2099,plain,
( spl37_35
| spl37_63
| spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| ~ spl37_30
| spl37_31 ),
inference(avatar_split_clause,[],[f2094,f1017,f1013,f922,f716,f708,f538,f2096,f1098]) ).
fof(f2140,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| ~ spl37_63 ),
inference(superposition,[],[f519,f2098]) ).
fof(f2145,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2140,f1018]) ).
fof(f2149,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2145,f2088]) ).
fof(f2153,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_16
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2149,f897]) ).
fof(f2156,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| spl37_15
| ~ spl37_16
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2153,f713]) ).
fof(f2158,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_14
| spl37_15
| ~ spl37_16
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2156,f709]) ).
fof(f2160,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2158,f923]) ).
fof(f2161,plain,
( ~ r2_hidden(sF36(sK33(k1_lattice2(sK2),sK3)),sK3)
| spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2160,f705]) ).
fof(f2162,plain,
( ~ m1_subset_1(sK33(k1_lattice2(sK2),sK3),sF34)
| r2_hidden(sK33(k1_lattice2(sK2),sK3),sK3)
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_63 ),
inference(resolution,[],[f2161,f543]) ).
fof(f2164,plain,
( r2_hidden(sK33(k1_lattice2(sK2),sK3),sK3)
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2162,f1113]) ).
fof(f2165,plain,
( sK3 = u1_struct_0(k1_lattice2(sK2))
| v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(resolution,[],[f2164,f520]) ).
fof(f2171,plain,
( v1_filter_0(sK3,k1_lattice2(sK2))
| ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2165,f1018]) ).
fof(f2172,plain,
( ~ m1_filter_0(sK3,k1_lattice2(sK2))
| v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2171,f2088]) ).
fof(f2173,plain,
( v3_struct_0(k1_lattice2(sK2))
| ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2172,f897]) ).
fof(f2174,plain,
( ~ v10_lattices(k1_lattice2(sK2))
| ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2173,f713]) ).
fof(f2175,plain,
( ~ v17_lattices(k1_lattice2(sK2))
| ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2174,f709]) ).
fof(f2176,plain,
( ~ l3_lattices(k1_lattice2(sK2))
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2175,f923]) ).
fof(f2177,plain,
( $false
| spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(forward_subsumption_resolution,[],[f2176,f705]) ).
fof(f2178,plain,
( spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(avatar_contradiction_clause,[],[f2177]) ).
fof(f2179,plain,
( sK3 = sF34
| ~ spl37_31
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_demodulation,[],[f1019,f1798]) ).
fof(f2184,plain,
( $false
| spl37_3
| ~ spl37_31
| ~ spl37_48
| ~ spl37_51 ),
inference(forward_subsumption_resolution,[],[f2179,f548]) ).
fof(f2185,plain,
( spl37_3
| ~ spl37_31
| ~ spl37_48
| ~ spl37_51 ),
inference(avatar_contradiction_clause,[],[f2184]) ).
fof(f2218,plain,
( $false
| ~ spl37_35
| ~ spl37_37 ),
inference(resolution,[],[f1099,f1113]) ).
fof(f2220,plain,
( ~ spl37_35
| ~ spl37_37 ),
inference(avatar_contradiction_clause,[],[f2218]) ).
cnf(s1,plain,
( spl37_1
| spl37_2 ),
inference(sat_conversion,[],[f544]) ).
cnf(s2,plain,
( spl37_1
| ~ spl37_3 ),
inference(sat_conversion,[],[f549]) ).
cnf(s3,plain,
( ~ spl37_1
| spl37_3
| spl37_4 ),
inference(sat_conversion,[],[f554]) ).
cnf(s4,plain,
( ~ spl37_1
| spl37_3
| ~ spl37_5 ),
inference(sat_conversion,[],[f559]) ).
cnf(s5,plain,
( ~ spl37_1
| spl37_3
| ~ spl37_6 ),
inference(sat_conversion,[],[f564]) ).
cnf(s10,plain,
( ~ spl37_13
| ~ spl37_14
| spl37_15
| spl37_16 ),
inference(sat_conversion,[],[f719]) ).
cnf(s11,plain,
spl37_13,
inference(sat_conversion,[],[f722]) ).
cnf(s15,plain,
~ spl37_15,
inference(sat_conversion,[],[f822]) ).
cnf(s18,plain,
spl37_14,
inference(sat_conversion,[],[f896]) ).
cnf(s22,plain,
spl37_24,
inference(sat_conversion,[],[f998]) ).
cnf(s23,plain,
( spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| spl37_30
| spl37_31 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s27,plain,
( ~ spl37_30
| ~ spl37_36
| spl37_37 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s28,plain,
( spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| spl37_36 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s34,plain,
spl37_51,
inference(sat_conversion,[],[f1291]) ).
cnf(s39,plain,
( ~ spl37_3
| spl37_49 ),
inference(sat_conversion,[],[f1490]) ).
cnf(s40,plain,
( ~ spl37_3
| spl37_46 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s46,plain,
( ~ spl37_3
| spl37_50 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s50,plain,
( ~ spl37_3
| spl37_47 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s51,plain,
spl37_48,
inference(sat_conversion,[],[f1645]) ).
cnf(s53,plain,
( ~ spl37_3
| spl37_31
| ~ spl37_46
| ~ spl37_47
| ~ spl37_48
| ~ spl37_49
| ~ spl37_50
| ~ spl37_51 ),
inference(sat_conversion,[],[f1686]) ).
cnf(s54,plain,
( ~ spl37_1
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_31 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s57,plain,
( ~ spl37_4
| ~ spl37_35 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s63,plain,
( ~ spl37_1
| ~ spl37_4
| spl37_5
| spl37_6
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| ~ spl37_32
| ~ spl37_48
| ~ spl37_51 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s65,plain,
( spl37_32
| spl37_35
| ~ spl37_48
| ~ spl37_51 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s66,plain,
( spl37_1
| ~ spl37_14
| ~ spl37_16
| ~ spl37_24
| ~ spl37_30
| spl37_31
| spl37_35
| spl37_63 ),
inference(sat_conversion,[],[f2099]) ).
cnf(s68,plain,
( spl37_1
| ~ spl37_2
| ~ spl37_13
| ~ spl37_14
| spl37_15
| ~ spl37_16
| ~ spl37_24
| spl37_31
| ~ spl37_37
| ~ spl37_63 ),
inference(sat_conversion,[],[f2178]) ).
cnf(s69,plain,
( spl37_3
| ~ spl37_31
| ~ spl37_48
| ~ spl37_51 ),
inference(sat_conversion,[],[f2185]) ).
cnf(s72,plain,
( ~ spl37_35
| ~ spl37_37 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s89,plain,
spl37_16,
inference(rat,[],[s10,s15,s18,s11]) ).
cnf(s90,plain,
spl37_1,
inference(rat,[],[s66,s68,s72,s27,s23,s28,s69,s1,s2,s18,s22,s89,s11,s15,s51,s34]) ).
cnf(s91,plain,
~ spl37_31,
inference(rat,[],[s54,s89,s22,s11,s15,s18,s90]) ).
cnf(s92,plain,
spl37_3,
inference(rat,[],[s65,s63,s57,s4,s3,s5,s51,s34,s90,s11,s18,s15,s89,s22]) ).
cnf(s93,plain,
spl37_47,
inference(rat,[],[s50,s92]) ).
cnf(s94,plain,
spl37_50,
inference(rat,[],[s46,s92]) ).
cnf(s95,plain,
spl37_46,
inference(rat,[],[s40,s92]) ).
cnf(s96,plain,
spl37_49,
inference(rat,[],[s39,s92]) ).
cnf(s98,plain,
$false,
inference(rat,[],[s53,s34,s94,s96,s51,s93,s91,s95,s92]) ).
fof(f2223,plain,
$false,
inference(avatar_sat_refutation,[],[s98]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT321+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.44 % Computer : n013.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 27 14:35:21 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.50 Running first-order theorem proving
% 0.22/0.50 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.23/2.32 % (293837)Detected formulas, will run a generic FOF schedule.
% 7.23/2.32 % (293842)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=3798319719:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.23/2.32 % (293843)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=365824011:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.23/2.32 % (293847)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1765635400:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.23/2.32 % (293844)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=1163252388:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.23/2.32 % (293848)dis-21_1_sil=8000:lcm=predicate:random_seed=1809221965: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)
% 7.23/2.32 % (293846)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3952476370:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.23/2.32 % (293845)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1189816703:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.23/2.32 % (293845)Refutation not found, incomplete strategy
% 7.23/2.32 % (293845)------------------------------
% 7.23/2.32 % (293845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293845)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293845)Termination reason: Refutation not found, incomplete strategy
% 7.23/2.32 % (293845)Time elapsed: 0.005 s
% 7.23/2.32 % (293845)Peak memory usage: 88 MB
% 7.23/2.32 % (293845)Instructions burned: 2 (million)
% 7.23/2.32 % (293846)Instruction limit reached!
% 7.23/2.32 % (293846)------------------------------
% 7.23/2.32 % (293846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293846)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293846)Termination reason: Instruction limit
% 7.23/2.32 % (293846)Termination phase: Saturation
% 7.23/2.32 % (293846)Time elapsed: 0.106 s
% 7.23/2.32 % (293846)Peak memory usage: 88 MB
% 7.23/2.32 % (293846)Instructions burned: 119 (million)
% 7.23/2.32 % (293848)Instruction limit reached!
% 7.23/2.32 % (293848)------------------------------
% 7.23/2.32 % (293848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293848)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293848)Termination reason: Instruction limit
% 7.23/2.32 % (293848)Termination phase: Saturation
% 7.23/2.32 % (293848)Time elapsed: 0.107 s
% 7.23/2.32 % (293848)Peak memory usage: 92 MB
% 7.23/2.32 % (293848)Instructions burned: 130 (million)
% 7.23/2.32 % (293847)Instruction limit reached!
% 7.23/2.32 % (293847)------------------------------
% 7.23/2.32 % (293847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293847)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293847)Termination reason: Instruction limit
% 7.23/2.32 % (293847)Termination phase: Saturation
% 7.23/2.32 % (293847)Time elapsed: 0.141 s
% 7.23/2.32 % (293847)Peak memory usage: 90 MB
% 7.23/2.32 % (293847)Instructions burned: 140 (million)
% 7.23/2.32 % (293856)lrs+10_1_sil=8000:sp=occurrence:random_seed=503720441:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 7.23/2.32 % (293857)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2419716852:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 7.23/2.32 % (293845)------------------------------
% 7.23/2.32 % (293845)------------------------------
% 7.23/2.32 % (293858)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4150972662:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 7.23/2.32 % (293857)Instruction limit reached!
% 7.23/2.32 % (293857)------------------------------
% 7.23/2.32 % (293857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293857)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293857)Termination reason: Instruction limit
% 7.23/2.32 % (293857)Termination phase: Saturation
% 7.23/2.32 % (293857)Time elapsed: 0.116 s
% 7.23/2.32 % (293857)Peak memory usage: 89 MB
% 7.23/2.32 % (293857)Instructions burned: 158 (million)
% 7.23/2.32 % (293856)Instruction limit reached!
% 7.23/2.32 % (293856)------------------------------
% 7.23/2.32 % (293856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293856)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293856)Termination reason: Instruction limit
% 7.23/2.32 % (293856)Termination phase: Saturation
% 7.23/2.32 % (293856)Time elapsed: 0.266 s
% 7.23/2.32 % (293856)Peak memory usage: 92 MB
% 7.23/2.32 % (293856)Instructions burned: 285 (million)
% 7.23/2.32 % (293842)First to succeed.
% 7.23/2.32 % (293842)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-293837"
% 7.23/2.32 % (293861)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=3444347908:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 7.23/2.32 % (293863)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1798789131:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 7.23/2.32 % (293863)Refutation not found, incomplete strategy
% 7.23/2.32 % (293863)------------------------------
% 7.23/2.32 % (293863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293863)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293863)Termination reason: Refutation not found, incomplete strategy
% 7.23/2.32 % (293863)Time elapsed: 0.010 s
% 7.23/2.32 % (293863)Peak memory usage: 88 MB
% 7.23/2.32 % (293863)Instructions burned: 8 (million)
% 7.23/2.32 % (293858)Instruction limit reached!
% 7.23/2.32 % (293858)------------------------------
% 7.23/2.32 % (293858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.23/2.32 % (293858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/2.32 % (293858)CaDiCaL version: 2.1.3
% 7.23/2.32 % (293858)Termination reason: Instruction limit
% 7.23/2.32 % (293858)Termination phase: Saturation
% 7.23/2.32 % (293858)Time elapsed: 0.308 s
% 7.23/2.32 % (293858)Peak memory usage: 91 MB
% 7.23/2.32 % (293858)Instructions burned: 326 (million)
% 7.23/2.32 % (293864)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1228487462:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 7.23/2.32 % (293842)Refutation found. Thanks to Tanya!
% 7.23/2.32 % SZS status Theorem for theBenchmark
% 7.23/2.32 % SZS output start Proof for theBenchmark
% See solution above
% 9.25/2.61 % (293842)------------------------------
% 9.25/2.61 % (293842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.25/2.61 % (293842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.25/2.61 % (293842)CaDiCaL version: 2.1.3
% 9.25/2.61 % (293842)Termination reason: Refutation
% 9.25/2.61 % (293842)Time elapsed: 0.700 s
% 9.25/2.61 % (293842)Peak memory usage: 133 MB
% 9.25/2.61 % (293842)Instructions burned: 1247 (million)
% 9.25/2.61 % (293842)------------------------------
% 9.25/2.61 % (293842)------------------------------
% 9.25/2.61 % (293837)Success in time 1.174 s
% 9.25/2.61 % Vampire exiting
%------------------------------------------------------------------------------