%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT322+2 : 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 : n018.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:55 AM UTC 2026
% Result : Theorem 10.06s 2.44s
% Output : Refutation 11.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 26
% Syntax : Number of formulae : 254 ( 30 unt; 9 def)
% Number of atoms : 1147 ( 94 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 1502 ( 609 ~; 689 |; 146 &)
% ( 28 <=>; 28 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 9 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-2 aty)
% Number of variables : 161 ( 0 sgn 150 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2456,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f2503,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
<=> v1_filter_0(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t58_filter_0) ).
fof(f2597,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f2669,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(f2857,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(f2872,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(f2873,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(f2902,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(f2903,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(f2906,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_filter_2(k17_filter_2(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k17_filter_2) ).
fof(f2942,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(f2953,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f2960,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(f2974,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v1_filter_2(X1,X0)
<=> v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t44_filter_2) ).
fof(f2987,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f2992,axiom,
! [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(f2993,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) )
<=> r2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t58_filter_2) ).
fof(f2994,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) )
<=> r2_filter_2(X0,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f2993]) ).
fof(f5492,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2456]) ).
fof(f5493,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5492]) ).
fof(f5568,plain,
! [X0] :
( ! [X1] :
( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,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(ennf_transformation,[],[f2503]) ).
fof(f5569,plain,
! [X0] :
( ! [X1] :
( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,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,[],[f5568]) ).
fof(f5733,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2597]) ).
fof(f5734,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5733]) ).
fof(f5869,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f6048,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,[],[f2857]) ).
fof(f6049,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,[],[f6048]) ).
fof(f6078,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,[],[f2872]) ).
fof(f6079,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,[],[f6078]) ).
fof(f6080,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,[],[f2873]) ).
fof(f6081,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,[],[f6080]) ).
fof(f6138,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,[],[f2902]) ).
fof(f6139,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,[],[f6138]) ).
fof(f6140,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,[],[f2903]) ).
fof(f6141,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,[],[f6140]) ).
fof(f6146,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2906]) ).
fof(f6147,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6146]) ).
fof(f6215,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,[],[f2942]) ).
fof(f6216,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,[],[f6215]) ).
fof(f6237,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2953]) ).
fof(f6238,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6237]) ).
fof(f6251,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,[],[f2960]) ).
fof(f6252,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,[],[f6251]) ).
fof(f6279,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_2(X1,X0)
<=> v2_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,[],[f2974]) ).
fof(f6280,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_2(X1,X0)
<=> v2_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,[],[f6279]) ).
fof(f6305,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2987]) ).
fof(f6306,plain,
! [X0] :
( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
<=> ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6305]) ).
fof(f6315,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,[],[f2992]) ).
fof(f6316,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,[],[f6315]) ).
fof(f6317,plain,
? [X0] :
( ? [X1] :
( ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,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(ennf_transformation,[],[f2994]) ).
fof(f6318,plain,
? [X0] :
( ? [X1] :
( ( ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,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,[],[f6317]) ).
fof(f7874,plain,
! [X0] :
( ! [X1] :
( ( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
| ~ v1_filter_0(X1,X0) )
& ( v1_filter_0(X1,X0)
| k1_filter_0(X0) = X1
| ~ v2_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,[],[f5569]) ).
fof(f7875,plain,
! [X0] :
( ! [X1] :
( ( ( ( X1 != k1_filter_0(X0)
& v2_filter_0(X1,X0) )
| ~ v1_filter_0(X1,X0) )
& ( v1_filter_0(X1,X0)
| k1_filter_0(X0) = X1
| ~ v2_filter_0(X1,X0) ) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7874]) ).
fof(f8023,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,[],[f6079]) ).
fof(f8057,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,[],[f6252]) ).
fof(f8068,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ~ v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)) )
& ( v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ v1_filter_2(X1,X0) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f6280]) ).
fof(f8074,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f6306]) ).
fof(f8075,plain,
! [X0] :
( ( ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
| v3_struct_0(k1_lattice2(X0))
| ~ v10_lattices(k1_lattice2(X0))
| ~ v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(k1_lattice2(X0)) )
& ( ( ~ v3_struct_0(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0))
& v17_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f8074]) ).
fof(f8077,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(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)) ) )
& ( ( 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,[],[f6316]) ).
fof(f8078,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(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)) ) )
& ( ( 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,[],[f8077]) ).
fof(f8079,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(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)) ) )
& ( ( 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,[],[f8078]) ).
fof(f8080,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK1077(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK1077(X0,X1)),X1)
& m1_subset_1(sK1077(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)) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1077]),skolemize(X2,sK1077(X0,X1))],[f8079]) ).
fof(f8081,plain,
? [X0] :
( ? [X1] :
( ( ~ r2_filter_2(X0,X1)
| k17_filter_2(X0) = X1
| ~ v1_filter_2(X1,X0) )
& ( r2_filter_2(X0,X1)
| ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) ) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(nnf_transformation,[],[f6318]) ).
fof(f8082,plain,
? [X0] :
( ? [X1] :
( ( ~ r2_filter_2(X0,X1)
| k17_filter_2(X0) = X1
| ~ v1_filter_2(X1,X0) )
& ( r2_filter_2(X0,X1)
| ( X1 != k17_filter_2(X0)
& v1_filter_2(X1,X0) ) )
& m2_filter_2(X1,X0) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f8081]) ).
fof(f8083,plain,
( ( ~ r2_filter_2(sK1078,sK1079)
| sK1079 = k17_filter_2(sK1078)
| ~ v1_filter_2(sK1079,sK1078) )
& ( r2_filter_2(sK1078,sK1079)
| ( sK1079 != k17_filter_2(sK1078)
& v1_filter_2(sK1079,sK1078) ) )
& m2_filter_2(sK1079,sK1078)
& ~ v3_struct_0(sK1078)
& v10_lattices(sK1078)
& v17_lattices(sK1078)
& l3_lattices(sK1078) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1078,sK1079]),skolemize(X0,sK1078),skolemize(X1,sK1079)],[f8082]) ).
fof(f12566,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5493]) ).
fof(f12653,plain,
! [X0,X1] :
( ~ v2_filter_0(X1,X0)
| k1_filter_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,[],[f7875]) ).
fof(f12654,plain,
! [X0,X1] :
( ~ v1_filter_0(X1,X0)
| v2_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,[],[f7875]) ).
fof(f12926,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5734]) ).
fof(f13047,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5869]) ).
fof(f13309,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,[],[f6049]) ).
fof(f13336,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,[],[f8023]) ).
fof(f13338,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,[],[f6081]) ).
fof(f13371,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,[],[f6139]) ).
fof(f13372,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,[],[f6141]) ).
fof(f13375,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6147]) ).
fof(f13451,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,[],[f6216]) ).
fof(f13476,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6238]) ).
fof(f13492,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,[],[f8057]) ).
fof(f13493,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,[],[f8057]) ).
fof(f13529,plain,
! [X0,X1] :
( v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ v1_filter_2(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8068]) ).
fof(f13530,plain,
! [X0,X1] :
( ~ v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| v1_filter_2(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8068]) ).
fof(f13566,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8075]) ).
fof(f13567,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8075]) ).
fof(f13568,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8075]) ).
fof(f13595,plain,
! [X0,X1] :
( u1_struct_0(X0) != X1
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f8080]) ).
fof(f13599,plain,
l3_lattices(sK1078),
inference(cnf_transformation,[],[f8083]) ).
fof(f13600,plain,
v17_lattices(sK1078),
inference(cnf_transformation,[],[f8083]) ).
fof(f13601,plain,
v10_lattices(sK1078),
inference(cnf_transformation,[],[f8083]) ).
fof(f13602,plain,
~ v3_struct_0(sK1078),
inference(cnf_transformation,[],[f8083]) ).
fof(f13603,plain,
m2_filter_2(sK1079,sK1078),
inference(cnf_transformation,[],[f8083]) ).
fof(f13604,plain,
( r2_filter_2(sK1078,sK1079)
| v1_filter_2(sK1079,sK1078) ),
inference(cnf_transformation,[],[f8083]) ).
fof(f13605,plain,
( r2_filter_2(sK1078,sK1079)
| sK1079 != k17_filter_2(sK1078) ),
inference(cnf_transformation,[],[f8083]) ).
fof(f13606,plain,
( ~ r2_filter_2(sK1078,sK1079)
| sK1079 = k17_filter_2(sK1078)
| ~ v1_filter_2(sK1079,sK1078) ),
inference(cnf_transformation,[],[f8083]) ).
fof(f15531,plain,
! [X0] :
( ~ r2_filter_2(X0,u1_struct_0(X0))
| ~ m2_filter_2(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f13595]) ).
fof(f15532,definition,
sF1080 = k17_filter_2(sK1078),
introduced(definition,[new_symbols(definition,[sF1080])],[function_definition]) ).
fof(f15533,plain,
k17_filter_2(sK1078) = sF1080,
inference(reorient_equations,[],[f15532]) ).
fof(f15534,plain,
( ~ r2_filter_2(sK1078,sK1079)
| sK1079 = sF1080
| ~ v1_filter_2(sK1079,sK1078) ),
inference(definition_folding,[],[f13606,f15533]) ).
fof(f15535,plain,
( r2_filter_2(sK1078,sK1079)
| sK1079 != sF1080 ),
inference(definition_folding,[],[f13605,f15533]) ).
fof(f15537,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f13566]) ).
fof(f15538,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f13567]) ).
fof(f15539,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f13568]) ).
fof(f15599,definition,
( spl1081_1
<=> v1_filter_2(sK1079,sK1078) ),
introduced(definition,[new_symbols(definition,[spl1081_1])],[avatar_definition]) ).
fof(f15600,plain,
( ~ v1_filter_2(sK1079,sK1078)
| spl1081_1 ),
inference(avatar_component_clause,[],[f15599]) ).
fof(f15601,plain,
( v1_filter_2(sK1079,sK1078)
| ~ spl1081_1 ),
inference(avatar_component_clause,[],[f15599]) ).
fof(f15603,definition,
( spl1081_2
<=> r2_filter_2(sK1078,sK1079) ),
introduced(definition,[new_symbols(definition,[spl1081_2])],[avatar_definition]) ).
fof(f15604,plain,
( ~ r2_filter_2(sK1078,sK1079)
| spl1081_2 ),
inference(avatar_component_clause,[],[f15603]) ).
fof(f15605,plain,
( r2_filter_2(sK1078,sK1079)
| ~ spl1081_2 ),
inference(avatar_component_clause,[],[f15603]) ).
fof(f15606,plain,
( spl1081_1
| spl1081_2 ),
inference(avatar_split_clause,[],[f13604,f15603,f15599]) ).
fof(f15608,definition,
( spl1081_3
<=> sK1079 = sF1080 ),
introduced(definition,[new_symbols(definition,[spl1081_3])],[avatar_definition]) ).
fof(f15609,plain,
( sK1079 = sF1080
| ~ spl1081_3 ),
inference(avatar_component_clause,[],[f15608]) ).
fof(f15610,plain,
( sK1079 != sF1080
| spl1081_3 ),
inference(avatar_component_clause,[],[f15608]) ).
fof(f15611,plain,
( ~ spl1081_3
| spl1081_2 ),
inference(avatar_split_clause,[],[f15535,f15603,f15608]) ).
fof(f15612,plain,
( ~ spl1081_1
| spl1081_3
| ~ spl1081_2 ),
inference(avatar_split_clause,[],[f15534,f15603,f15608,f15599]) ).
fof(f18093,plain,
( m2_filter_2(sF1080,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(superposition,[],[f13375,f15533]) ).
fof(f18094,plain,
( m2_filter_2(sF1080,sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18093,f13602]) ).
fof(f18095,plain,
( m2_filter_2(sF1080,sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18094,f13601]) ).
fof(f18096,plain,
m2_filter_2(sF1080,sK1078),
inference(forward_subsumption_resolution,[],[f18095,f13599]) ).
fof(f18097,plain,
( v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| k7_filter_2(sK1078,sK1079) = k15_filter_2(sK1078,sK1079) ),
inference(resolution,[],[f13372,f13603]) ).
fof(f18100,plain,
( ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| k7_filter_2(sK1078,sK1079) = k15_filter_2(sK1078,sK1079) ),
inference(forward_subsumption_resolution,[],[f18097,f13602]) ).
fof(f18101,plain,
( ~ l3_lattices(sK1078)
| k7_filter_2(sK1078,sK1079) = k15_filter_2(sK1078,sK1079) ),
inference(forward_subsumption_resolution,[],[f18100,f13601]) ).
fof(f18102,plain,
k7_filter_2(sK1078,sK1079) = k15_filter_2(sK1078,sK1079),
inference(forward_subsumption_resolution,[],[f18101,f13599]) ).
fof(f18103,plain,
( ~ v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v1_filter_2(sK1079,sK1078)
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(superposition,[],[f13530,f18102]) ).
fof(f18104,plain,
( ~ v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18103,f15600]) ).
fof(f18105,plain,
( ~ v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18104,f13603]) ).
fof(f18106,plain,
( ~ v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18105,f13602]) ).
fof(f18107,plain,
( ~ v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ l3_lattices(sK1078)
| spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18106,f13601]) ).
fof(f18108,plain,
( ~ v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18107,f13599]) ).
fof(f18113,plain,
( v3_struct_0(sK1078)
| k17_filter_2(sK1078) = u1_struct_0(sK1078)
| ~ l3_lattices(sK1078) ),
inference(resolution,[],[f13476,f13601]) ).
fof(f18114,plain,
( k17_filter_2(sK1078) = u1_struct_0(sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18113,f13602]) ).
fof(f18115,plain,
k17_filter_2(sK1078) = u1_struct_0(sK1078),
inference(forward_subsumption_resolution,[],[f18114,f13599]) ).
fof(f18116,plain,
sF1080 = u1_struct_0(sK1078),
inference(forward_demodulation,[],[f18115,f15533]) ).
fof(f18125,plain,
( v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ r2_filter_2(sK1078,sK1079)
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(superposition,[],[f13492,f18102]) ).
fof(f18126,plain,
( v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18125,f15605]) ).
fof(f18127,plain,
( v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18126,f13603]) ).
fof(f18128,plain,
( v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18127,f13602]) ).
fof(f18129,plain,
( v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ l3_lattices(sK1078)
| ~ spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18128,f13601]) ).
fof(f18130,plain,
( v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18129,f13599]) ).
fof(f18131,plain,
( m2_lattice4(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(resolution,[],[f13338,f13603]) ).
fof(f18136,plain,
( m2_lattice4(sK1079,sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18131,f13602]) ).
fof(f18138,plain,
( m2_lattice4(sK1079,sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18136,f13601]) ).
fof(f18140,plain,
m2_lattice4(sK1079,sK1078),
inference(forward_subsumption_resolution,[],[f18138,f13599]) ).
fof(f18142,plain,
( ~ v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| r2_filter_2(sK1078,sK1079)
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(superposition,[],[f13493,f18102]) ).
fof(f18165,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ v1_filter_2(sK1079,sK1078)
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(superposition,[],[f13529,f18102]) ).
fof(f18177,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ m1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_2 ),
inference(resolution,[],[f12654,f18130]) ).
fof(f18178,plain,
( ~ m1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| spl1081_1
| ~ spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18177,f18108]) ).
fof(f18181,definition,
( spl1081_344
<=> l3_lattices(k1_lattice2(sK1078)) ),
introduced(definition,[new_symbols(definition,[spl1081_344])],[avatar_definition]) ).
fof(f18182,plain,
( l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_344 ),
inference(avatar_component_clause,[],[f18181]) ).
fof(f18183,plain,
( ~ l3_lattices(k1_lattice2(sK1078))
| spl1081_344 ),
inference(avatar_component_clause,[],[f18181]) ).
fof(f18185,definition,
( spl1081_345
<=> v17_lattices(k1_lattice2(sK1078)) ),
introduced(definition,[new_symbols(definition,[spl1081_345])],[avatar_definition]) ).
fof(f18186,plain,
( v17_lattices(k1_lattice2(sK1078))
| ~ spl1081_345 ),
inference(avatar_component_clause,[],[f18185]) ).
fof(f18187,plain,
( ~ v17_lattices(k1_lattice2(sK1078))
| spl1081_345 ),
inference(avatar_component_clause,[],[f18185]) ).
fof(f18189,definition,
( spl1081_346
<=> v10_lattices(k1_lattice2(sK1078)) ),
introduced(definition,[new_symbols(definition,[spl1081_346])],[avatar_definition]) ).
fof(f18190,plain,
( v10_lattices(k1_lattice2(sK1078))
| ~ spl1081_346 ),
inference(avatar_component_clause,[],[f18189]) ).
fof(f18191,plain,
( ~ v10_lattices(k1_lattice2(sK1078))
| spl1081_346 ),
inference(avatar_component_clause,[],[f18189]) ).
fof(f18193,definition,
( spl1081_347
<=> v3_struct_0(k1_lattice2(sK1078)) ),
introduced(definition,[new_symbols(definition,[spl1081_347])],[avatar_definition]) ).
fof(f18194,plain,
( ~ v3_struct_0(k1_lattice2(sK1078))
| spl1081_347 ),
inference(avatar_component_clause,[],[f18193]) ).
fof(f18195,plain,
( v3_struct_0(k1_lattice2(sK1078))
| ~ spl1081_347 ),
inference(avatar_component_clause,[],[f18193]) ).
fof(f18197,definition,
( spl1081_348
<=> m1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078)) ),
introduced(definition,[new_symbols(definition,[spl1081_348])],[avatar_definition]) ).
fof(f18198,plain,
( m1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ spl1081_348 ),
inference(avatar_component_clause,[],[f18197]) ).
fof(f18200,plain,
( ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348
| spl1081_1
| ~ spl1081_2 ),
inference(avatar_split_clause,[],[f18178,f15603,f15599,f18197,f18193,f18189,f18185,f18181]) ).
fof(f18202,plain,
( ~ l3_lattices(sK1078)
| spl1081_344 ),
inference(resolution,[],[f13047,f18183]) ).
fof(f18203,plain,
( $false
| spl1081_344 ),
inference(forward_subsumption_resolution,[],[f18202,f13599]) ).
fof(f18204,plain,
spl1081_344,
inference(avatar_contradiction_clause,[],[f18203]) ).
fof(f18219,plain,
( m1_filter_2(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ m2_filter_2(sK1079,sK1078) ),
inference(superposition,[],[f13371,f18102]) ).
fof(f18220,plain,
( m1_filter_2(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ m2_filter_2(sK1079,sK1078) ),
inference(forward_subsumption_resolution,[],[f18219,f13602]) ).
fof(f18223,plain,
( m1_filter_2(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ l3_lattices(sK1078)
| ~ m2_filter_2(sK1079,sK1078) ),
inference(forward_subsumption_resolution,[],[f18220,f13601]) ).
fof(f18226,plain,
( m1_filter_2(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ m2_filter_2(sK1079,sK1078) ),
inference(forward_subsumption_resolution,[],[f18223,f13599]) ).
fof(f18227,plain,
m1_filter_2(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078)),
inference(forward_subsumption_resolution,[],[f18226,f13603]) ).
fof(f18229,plain,
( m1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078)) ),
inference(resolution,[],[f18227,f13336]) ).
fof(f18230,plain,
( m1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ spl1081_344 ),
inference(forward_subsumption_resolution,[],[f18229,f18182]) ).
fof(f18232,plain,
( ~ spl1081_346
| spl1081_347
| spl1081_348
| ~ spl1081_344 ),
inference(avatar_split_clause,[],[f18230,f18181,f18197,f18193,f18189]) ).
fof(f18314,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f13451,f13309]) ).
fof(f18316,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k7_filter_2(X0,X1) = X1 ),
inference(duplicate_literal_removal,[],[f18314]) ).
fof(f18320,plain,
( v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| sK1079 = k7_filter_2(sK1078,sK1079) ),
inference(resolution,[],[f18316,f18140]) ).
fof(f18323,plain,
( ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| sK1079 = k7_filter_2(sK1078,sK1079) ),
inference(forward_subsumption_resolution,[],[f18320,f13602]) ).
fof(f18325,plain,
( ~ l3_lattices(sK1078)
| sK1079 = k7_filter_2(sK1078,sK1079) ),
inference(forward_subsumption_resolution,[],[f18323,f13601]) ).
fof(f18327,plain,
sK1079 = k7_filter_2(sK1078,sK1079),
inference(forward_subsumption_resolution,[],[f18325,f13599]) ).
fof(f18339,plain,
( v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_345 ),
inference(resolution,[],[f15537,f18187]) ).
fof(f18344,plain,
( ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_345 ),
inference(forward_subsumption_resolution,[],[f18339,f13602]) ).
fof(f18347,plain,
( ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_345 ),
inference(forward_subsumption_resolution,[],[f18344,f13601]) ).
fof(f18348,plain,
( ~ l3_lattices(sK1078)
| spl1081_345 ),
inference(forward_subsumption_resolution,[],[f18347,f13600]) ).
fof(f18349,plain,
( $false
| spl1081_345 ),
inference(forward_subsumption_resolution,[],[f18348,f13599]) ).
fof(f18350,plain,
spl1081_345,
inference(avatar_contradiction_clause,[],[f18349]) ).
fof(f18365,plain,
( v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_347 ),
inference(resolution,[],[f18195,f15539]) ).
fof(f18368,plain,
( ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_347 ),
inference(forward_subsumption_resolution,[],[f18365,f13602]) ).
fof(f18371,plain,
( ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_347 ),
inference(forward_subsumption_resolution,[],[f18368,f13601]) ).
fof(f18372,plain,
( ~ l3_lattices(sK1078)
| ~ spl1081_347 ),
inference(forward_subsumption_resolution,[],[f18371,f13600]) ).
fof(f18373,plain,
( $false
| ~ spl1081_347 ),
inference(forward_subsumption_resolution,[],[f18372,f13599]) ).
fof(f18374,plain,
~ spl1081_347,
inference(avatar_contradiction_clause,[],[f18373]) ).
fof(f18375,plain,
( ~ r2_filter_2(sK1078,sF1080)
| ~ m2_filter_2(sF1080,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(superposition,[],[f15531,f18116]) ).
fof(f18451,plain,
( v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_346 ),
inference(resolution,[],[f15538,f18191]) ).
fof(f18460,plain,
( ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_346 ),
inference(forward_subsumption_resolution,[],[f18451,f13602]) ).
fof(f18465,plain,
( ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_346 ),
inference(forward_subsumption_resolution,[],[f18460,f13601]) ).
fof(f18466,plain,
( ~ l3_lattices(sK1078)
| spl1081_346 ),
inference(forward_subsumption_resolution,[],[f18465,f13600]) ).
fof(f18467,plain,
( $false
| spl1081_346 ),
inference(forward_subsumption_resolution,[],[f18466,f13599]) ).
fof(f18468,plain,
spl1081_346,
inference(avatar_contradiction_clause,[],[f18467]) ).
fof(f18469,plain,
( m1_filter_0(sK1079,k1_lattice2(sK1078))
| ~ spl1081_348 ),
inference(forward_demodulation,[],[f18198,f18327]) ).
fof(f18474,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18165,f15601]) ).
fof(f18477,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18474,f13603]) ).
fof(f18480,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| ~ spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18477,f13602]) ).
fof(f18483,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ l3_lattices(sK1078)
| ~ spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18480,f13601]) ).
fof(f18486,plain,
( v2_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ spl1081_1 ),
inference(forward_subsumption_resolution,[],[f18483,f13599]) ).
fof(f18488,plain,
( v2_filter_0(sK1079,k1_lattice2(sK1078))
| ~ spl1081_1 ),
inference(forward_demodulation,[],[f18486,f18327]) ).
fof(f18524,plain,
( ~ r2_filter_2(sK1078,sF1080)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18375,f18096]) ).
fof(f18528,plain,
( ~ r2_filter_2(sK1078,sF1080)
| ~ v10_lattices(sK1078)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18524,f13602]) ).
fof(f18530,plain,
( ~ r2_filter_2(sK1078,sF1080)
| ~ v17_lattices(sK1078)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18528,f13601]) ).
fof(f18532,plain,
( ~ r2_filter_2(sK1078,sF1080)
| ~ l3_lattices(sK1078) ),
inference(forward_subsumption_resolution,[],[f18530,f13600]) ).
fof(f18534,plain,
~ r2_filter_2(sK1078,sF1080),
inference(forward_subsumption_resolution,[],[f18532,f13599]) ).
fof(f18537,plain,
( ~ r2_filter_2(sK1078,sK1079)
| ~ spl1081_3 ),
inference(forward_demodulation,[],[f18534,f15609]) ).
fof(f18538,plain,
( $false
| ~ spl1081_2
| ~ spl1081_3 ),
inference(forward_subsumption_resolution,[],[f18537,f15605]) ).
fof(f18539,plain,
( ~ spl1081_2
| ~ spl1081_3 ),
inference(avatar_contradiction_clause,[],[f18538]) ).
fof(f18544,plain,
( ~ v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ m2_filter_2(sK1079,sK1078)
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18142,f15604]) ).
fof(f18545,plain,
( ~ v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| v3_struct_0(sK1078)
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18544,f13603]) ).
fof(f18546,plain,
( ~ v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ v10_lattices(sK1078)
| ~ l3_lattices(sK1078)
| spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18545,f13602]) ).
fof(f18547,plain,
( ~ v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| ~ l3_lattices(sK1078)
| spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18546,f13601]) ).
fof(f18548,plain,
( ~ v1_filter_0(k7_filter_2(sK1078,sK1079),k1_lattice2(sK1078))
| spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18547,f13599]) ).
fof(f18549,plain,
( ~ v1_filter_0(sK1079,k1_lattice2(sK1078))
| spl1081_2 ),
inference(forward_demodulation,[],[f18548,f18327]) ).
fof(f18551,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| v1_filter_0(sK1079,k1_lattice2(sK1078))
| ~ m1_filter_0(sK1079,k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_1 ),
inference(resolution,[],[f18488,f12653]) ).
fof(f18552,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| ~ m1_filter_0(sK1079,k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2 ),
inference(forward_subsumption_resolution,[],[f18551,f18549]) ).
fof(f18553,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| v3_struct_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2
| ~ spl1081_348 ),
inference(forward_subsumption_resolution,[],[f18552,f18469]) ).
fof(f18554,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| ~ v10_lattices(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2
| spl1081_347
| ~ spl1081_348 ),
inference(forward_subsumption_resolution,[],[f18553,f18194]) ).
fof(f18555,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| ~ v17_lattices(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_subsumption_resolution,[],[f18554,f18190]) ).
fof(f18556,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_subsumption_resolution,[],[f18555,f18186]) ).
fof(f18557,plain,
( sK1079 = k1_filter_0(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_subsumption_resolution,[],[f18556,f18182]) ).
fof(f18577,plain,
( v3_struct_0(k1_lattice2(sK1078))
| k1_filter_0(k1_lattice2(sK1078)) = u1_struct_0(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_346 ),
inference(resolution,[],[f18190,f12566]) ).
fof(f18584,plain,
( k1_filter_0(k1_lattice2(sK1078)) = u1_struct_0(k1_lattice2(sK1078))
| ~ l3_lattices(k1_lattice2(sK1078))
| ~ spl1081_346
| spl1081_347 ),
inference(forward_subsumption_resolution,[],[f18577,f18194]) ).
fof(f18588,plain,
( k1_filter_0(k1_lattice2(sK1078)) = u1_struct_0(k1_lattice2(sK1078))
| ~ spl1081_344
| ~ spl1081_346
| spl1081_347 ),
inference(forward_subsumption_resolution,[],[f18584,f18182]) ).
fof(f18589,plain,
( sK1079 = u1_struct_0(k1_lattice2(sK1078))
| ~ spl1081_1
| spl1081_2
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_demodulation,[],[f18588,f18557]) ).
fof(f18815,plain,
( v3_struct_0(sK1078)
| u1_struct_0(sK1078) = u1_struct_0(k1_lattice2(sK1078)) ),
inference(resolution,[],[f12926,f13599]) ).
fof(f18820,plain,
u1_struct_0(sK1078) = u1_struct_0(k1_lattice2(sK1078)),
inference(forward_subsumption_resolution,[],[f18815,f13602]) ).
fof(f18822,plain,
( sK1079 = u1_struct_0(sK1078)
| ~ spl1081_1
| spl1081_2
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_demodulation,[],[f18820,f18589]) ).
fof(f18823,plain,
( sK1079 = sF1080
| ~ spl1081_1
| spl1081_2
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_demodulation,[],[f18822,f18116]) ).
fof(f18824,plain,
( $false
| ~ spl1081_1
| spl1081_2
| spl1081_3
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(forward_subsumption_resolution,[],[f18823,f15610]) ).
fof(f18825,plain,
( ~ spl1081_1
| spl1081_2
| spl1081_3
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(avatar_contradiction_clause,[],[f18824]) ).
cnf(s1,plain,
( spl1081_1
| spl1081_2 ),
inference(sat_conversion,[],[f15606]) ).
cnf(s2,plain,
( spl1081_2
| ~ spl1081_3 ),
inference(sat_conversion,[],[f15611]) ).
cnf(s3,plain,
( ~ spl1081_1
| ~ spl1081_2
| spl1081_3 ),
inference(sat_conversion,[],[f15612]) ).
cnf(s299,plain,
( spl1081_1
| ~ spl1081_2
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(sat_conversion,[],[f18200]) ).
cnf(s300,plain,
spl1081_344,
inference(sat_conversion,[],[f18204]) ).
cnf(s301,plain,
( ~ spl1081_344
| ~ spl1081_346
| spl1081_347
| spl1081_348 ),
inference(sat_conversion,[],[f18232]) ).
cnf(s307,plain,
spl1081_345,
inference(sat_conversion,[],[f18350]) ).
cnf(s311,plain,
~ spl1081_347,
inference(sat_conversion,[],[f18374]) ).
cnf(s312,plain,
spl1081_346,
inference(sat_conversion,[],[f18468]) ).
cnf(s320,plain,
( ~ spl1081_2
| ~ spl1081_3 ),
inference(sat_conversion,[],[f18539]) ).
cnf(s335,plain,
( ~ spl1081_1
| spl1081_2
| spl1081_3
| ~ spl1081_344
| ~ spl1081_345
| ~ spl1081_346
| spl1081_347
| ~ spl1081_348 ),
inference(sat_conversion,[],[f18825]) ).
cnf(s341,plain,
( ~ spl1081_344
| spl1081_348 ),
inference(rat,[],[s301,s311,s312]) ).
cnf(s345,plain,
spl1081_348,
inference(rat,[],[s341,s300]) ).
cnf(s346,plain,
( spl1081_1
| ~ spl1081_2 ),
inference(rat,[],[s299,s345,s311,s312,s307,s300]) ).
cnf(s356,plain,
spl1081_1,
inference(rat,[],[s1,s346]) ).
cnf(s357,plain,
spl1081_2,
inference(rat,[],[s2,s335,s356,s300,s307,s312,s311,s345]) ).
cnf(s358,plain,
~ spl1081_3,
inference(rat,[],[s320,s357]) ).
cnf(s359,plain,
$false,
inference(rat,[],[s3,s356,s358,s357]) ).
fof(f18826,plain,
$false,
inference(avatar_sat_refutation,[],[s359]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT322+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 14:39:09 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 10.06/2.44 % (2424587)Detected formulas, will run a generic FOF schedule.
% 10.06/2.44 % (2424592)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=3343278301:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.06/2.44 % (2424597)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=730204635:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.06/2.44 % (2424598)dis-21_1_sil=8000:lcm=predicate:random_seed=2275000036:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.06/2.44 % (2424594)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=2859891275:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.06/2.44 % (2424596)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1229997834:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.06/2.44 % (2424593)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=80117447:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.06/2.44 % (2424595)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1705997734:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.06/2.44 % (2424595)Refutation not found, incomplete strategy
% 10.06/2.44 % (2424595)------------------------------
% 10.06/2.44 % (2424595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424595)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424595)Termination reason: Refutation not found, incomplete strategy
% 10.06/2.44 % (2424595)Time elapsed: 0.014 s
% 10.06/2.44 % (2424595)Peak memory usage: 92 MB
% 10.06/2.44 % (2424595)Instructions burned: 16 (million)
% 10.06/2.44 % (2424596)Instruction limit reached!
% 10.06/2.44 % (2424596)------------------------------
% 10.06/2.44 % (2424596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424596)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424596)Termination reason: Instruction limit
% 10.06/2.44 % (2424596)Termination phase: Saturation
% 10.06/2.44 % (2424596)Time elapsed: 0.074 s
% 10.06/2.44 % (2424596)Peak memory usage: 93 MB
% 10.06/2.44 % (2424596)Instructions burned: 119 (million)
% 10.06/2.44 % (2424598)Instruction limit reached!
% 10.06/2.44 % (2424598)------------------------------
% 10.06/2.44 % (2424598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424598)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424598)Termination reason: Instruction limit
% 10.06/2.44 % (2424598)Termination phase: Property scanning
% 10.06/2.44 % (2424598)Time elapsed: 0.078 s
% 10.06/2.44 % (2424598)Peak memory usage: 92 MB
% 10.06/2.44 % (2424598)Instructions burned: 132 (million)
% 10.06/2.44 % (2424597)Instruction limit reached!
% 10.06/2.44 % (2424597)------------------------------
% 10.06/2.44 % (2424597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424597)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424597)Termination reason: Instruction limit
% 10.06/2.44 % (2424597)Termination phase: Property scanning
% 10.06/2.44 % (2424597)Time elapsed: 0.087 s
% 10.06/2.44 % (2424597)Peak memory usage: 94 MB
% 10.06/2.44 % (2424597)Instructions burned: 140 (million)
% 10.06/2.44 % (2424607)lrs+10_1_sil=32000:urr=on:br=off:random_seed=201737037:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.06/2.44 % (2424606)lrs+10_1_sil=8000:sp=occurrence:random_seed=3388734579:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.06/2.44 % (2424608)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3915359673:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.06/2.44 % (2424607)Refutation not found, incomplete strategy
% 10.06/2.44 % (2424607)------------------------------
% 10.06/2.44 % (2424607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424607)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424607)Termination reason: Refutation not found, incomplete strategy
% 10.06/2.44 % (2424607)Time elapsed: 0.029 s
% 10.06/2.44 % (2424607)Peak memory usage: 92 MB
% 10.06/2.44 % (2424607)Instructions burned: 51 (million)
% 10.06/2.44 % (2424595)------------------------------
% 10.06/2.44 % (2424595)------------------------------
% 10.06/2.44 % (2424608)Refutation not found, incomplete strategy
% 10.06/2.44 % (2424608)------------------------------
% 10.06/2.44 % (2424608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424608)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424608)Termination reason: Refutation not found, incomplete strategy
% 10.06/2.44 % (2424608)Time elapsed: 0.015 s
% 10.06/2.44 % (2424608)Peak memory usage: 92 MB
% 10.06/2.44 % (2424608)Instructions burned: 17 (million)
% 10.06/2.44 % (2424606)Instruction limit reached!
% 10.06/2.44 % (2424606)------------------------------
% 10.06/2.44 % (2424606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424606)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424606)Termination reason: Instruction limit
% 10.06/2.44 % (2424606)Termination phase: Saturation
% 10.06/2.44 % (2424606)Time elapsed: 0.181 s
% 10.06/2.44 % (2424606)Peak memory usage: 95 MB
% 10.06/2.44 % (2424606)Instructions burned: 285 (million)
% 10.06/2.44 % (2424612)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=764309076:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 10.06/2.44 % (2424607)------------------------------
% 10.06/2.44 % (2424607)------------------------------
% 10.06/2.44 % (2424608)------------------------------
% 10.06/2.44 % (2424608)------------------------------
% 10.06/2.44 % (2424613)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1376608445:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 10.06/2.44 % (2424612)Instruction limit reached!
% 10.06/2.44 % (2424612)------------------------------
% 10.06/2.44 % (2424612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424612)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424612)Termination reason: Instruction limit
% 10.06/2.44 % (2424612)Termination phase: Saturation
% 10.06/2.44 % (2424612)Time elapsed: 0.143 s
% 10.06/2.44 % (2424612)Peak memory usage: 98 MB
% 10.06/2.44 % (2424612)Instructions burned: 248 (million)
% 10.06/2.44 % (2424613)Refutation not found, incomplete strategy
% 10.06/2.44 % (2424613)------------------------------
% 10.06/2.44 % (2424613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424613)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424613)Termination reason: Refutation not found, incomplete strategy
% 10.06/2.44 % (2424613)Time elapsed: 0.048 s
% 10.06/2.44 % (2424613)Peak memory usage: 93 MB
% 10.06/2.44 % (2424613)Instructions burned: 72 (million)
% 10.06/2.44 % (2424615)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2985432551:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 10.06/2.44 % (2424616)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3732678597:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 10.06/2.44 % (2424616)Instruction limit reached!
% 10.06/2.44 % (2424616)------------------------------
% 10.06/2.44 % (2424616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424616)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424616)Termination reason: Instruction limit
% 10.06/2.44 % (2424616)Termination phase: Saturation
% 10.06/2.44 % (2424616)Time elapsed: 0.066 s
% 10.06/2.44 % (2424616)Peak memory usage: 93 MB
% 10.06/2.44 % (2424616)Instructions burned: 114 (million)
% 10.06/2.44 % (2424618)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=895864862:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 10.06/2.44 % (2424618)Instruction limit reached!
% 10.06/2.44 % (2424618)------------------------------
% 10.06/2.44 % (2424618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424618)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424618)Termination reason: Instruction limit
% 10.06/2.44 % (2424618)Termination phase: Property scanning
% 10.06/2.44 % (2424618)Time elapsed: 0.079 s
% 10.06/2.44 % (2424618)Peak memory usage: 94 MB
% 10.06/2.44 % (2424618)Instructions burned: 129 (million)
% 10.06/2.44 % (2424613)------------------------------
% 10.06/2.44 % (2424613)------------------------------
% 10.06/2.44 % (2424621)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1044672141:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 10.06/2.44 % (2424621)Instruction limit reached!
% 10.06/2.44 % (2424621)------------------------------
% 10.06/2.44 % (2424621)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424621)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424621)Termination reason: Instruction limit
% 10.06/2.44 % (2424621)Termination phase: Property scanning
% 10.06/2.44 % (2424621)Time elapsed: 0.059 s
% 10.06/2.44 % (2424621)Peak memory usage: 91 MB
% 10.06/2.44 % (2424621)Instructions burned: 116 (million)
% 10.06/2.44 % (2424623)lrs+10_1_sil=8000:sp=occurrence:random_seed=3951591100:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 10.06/2.44 % (2424624)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3778470815:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 10.06/2.44 % (2424624)Refutation not found, incomplete strategy
% 10.06/2.44 % (2424624)------------------------------
% 10.06/2.44 % (2424624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.06/2.44 % (2424624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.06/2.44 % (2424624)CaDiCaL version: 2.1.3
% 10.06/2.44 % (2424624)Termination reason: Refutation not found, incomplete strategy
% 10.06/2.44 % (2424624)Time elapsed: 0.050 s
% 10.06/2.44 % (2424624)Peak memory usage: 94 MB
% 10.06/2.44 % (2424624)Instructions burned: 86 (million)
% 10.06/2.44 % (2424592)First to succeed.
% 10.06/2.44 % (2424626)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3154347884:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 10.06/2.44 % (2424592)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2424587"
% 10.06/2.44 % (2424592)Refutation found. Thanks to Tanya!
% 10.06/2.44 % SZS status Theorem for theBenchmark
% 10.06/2.44 % SZS output start Proof for theBenchmark
% See solution above
% 11.23/2.64 % (2424592)------------------------------
% 11.23/2.64 % (2424592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.23/2.64 % (2424592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.23/2.64 % (2424592)CaDiCaL version: 2.1.3
% 11.23/2.64 % (2424592)Termination reason: Refutation
% 11.23/2.64 % (2424592)Time elapsed: 1.197 s
% 11.23/2.64 % (2424592)Peak memory usage: 219 MB
% 11.23/2.64 % (2424592)Instructions burned: 3625 (million)
% 11.23/2.64 % (2424592)------------------------------
% 11.23/2.64 % (2424592)------------------------------
% 11.23/2.64 % (2424587)Success in time 1.595 s
% 11.23/2.64 % Vampire exiting
%------------------------------------------------------------------------------