%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT321+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 13.66s 2.70s
% Output : Refutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 54
% Syntax : Number of formulae : 448 ( 35 unt; 27 def)
% Number of atoms : 2625 ( 137 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 3624 (1447 ~;1782 |; 280 &)
% ( 59 <=>; 54 =>; 0 <=; 2 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 58 ( 56 usr; 27 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-3 aty)
% Number of variables : 345 ( 0 sgn 320 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6660,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc5_lattices) ).
fof(f6731,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k4_lattices(X0,k7_lattices(X0,X1),X1) = k5_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_lattices) ).
fof(f6733,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k7_lattices(X0,k7_lattices(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t49_lattices) ).
fof(f6759,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/sandbox/benchmark/theBenchmark.p',dt_k7_lattices) ).
fof(f8635,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/sandbox/benchmark/theBenchmark.p',t57_filter_0) ).
fof(f8636,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/sandbox/benchmark/theBenchmark.p',t58_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f9363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_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)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,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/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f12317,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f13531,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f13532,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f13546,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/sandbox/benchmark/theBenchmark.p',dt_k6_filter_2) ).
fof(f13561,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/sandbox/benchmark/theBenchmark.p',dt_k15_filter_2) ).
fof(f13562,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/sandbox/benchmark/theBenchmark.p',redefinition_k15_filter_2) ).
fof(f13596,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/sandbox/benchmark/theBenchmark.p',d5_filter_2) ).
fof(f13600,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f13601,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/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f13608,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v13_lattices(X0)
=> r2_hidden(k5_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_filter_2) ).
fof(f13618,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( m2_filter_2(X2,X0)
=> ( r1_tarski(X1,X2)
=> ( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_filter_2) ).
fof(f13619,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/sandbox/benchmark/theBenchmark.p',t33_filter_2) ).
fof(f13632,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( v1_filter_2(X1,X0)
<=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r2_hidden(k4_lattices(X0,X2,X3),X1)
<=> ( r2_hidden(X2,X1)
| r2_hidden(X3,X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_filter_2) ).
fof(f13633,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/sandbox/benchmark/theBenchmark.p',t44_filter_2) ).
fof(f13646,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/sandbox/benchmark/theBenchmark.p',t54_filter_2) ).
fof(f13649,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/sandbox/benchmark/theBenchmark.p',t55_filter_2) ).
fof(f13651,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/sandbox/benchmark/theBenchmark.p',t57_filter_2) ).
fof(f13652,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)],[f13651]) ).
fof(f13733,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,[],[f13531]) ).
fof(f13734,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,[],[f13733]) ).
fof(f13735,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,[],[f13532]) ).
fof(f13736,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,[],[f13735]) ).
fof(f13763,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,[],[f13546]) ).
fof(f13764,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,[],[f13763]) ).
fof(f13793,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,[],[f13561]) ).
fof(f13794,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,[],[f13793]) ).
fof(f13795,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,[],[f13562]) ).
fof(f13796,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,[],[f13795]) ).
fof(f13850,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,[],[f13596]) ).
fof(f13851,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,[],[f13850]) ).
fof(f13858,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13600]) ).
fof(f13859,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13858]) ).
fof(f13860,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,[],[f13601]) ).
fof(f13861,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,[],[f13860]) ).
fof(f13874,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k5_lattices(X0),X1)
| ~ v13_lattices(X0)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13608]) ).
fof(f13875,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k5_lattices(X0),X1)
| ~ v13_lattices(X0)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13874]) ).
fof(f13894,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13618]) ).
fof(f13895,plain,
! [X0] :
( ! [X1] :
( ( r2_filter_2(X0,X1)
<=> ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13894]) ).
fof(f13896,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,[],[f13619]) ).
fof(f13897,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,[],[f13896]) ).
fof(f13922,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_2(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
<=> ( r2_hidden(X2,X1)
| r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13632]) ).
fof(f13923,plain,
! [X0] :
( ! [X1] :
( ( v1_filter_2(X1,X0)
<=> ! [X2] :
( ! [X3] :
( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
<=> ( r2_hidden(X2,X1)
| r2_hidden(X3,X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13922]) ).
fof(f13924,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,[],[f13633]) ).
fof(f13925,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,[],[f13924]) ).
fof(f13950,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,[],[f13646]) ).
fof(f13951,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,[],[f13950]) ).
fof(f13956,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,[],[f13649]) ).
fof(f13957,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,[],[f13956]) ).
fof(f13960,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,[],[f13652]) ).
fof(f13961,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,[],[f13960]) ).
fof(f13972,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,[],[f12317]) ).
fof(f13973,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,[],[f13972]) ).
fof(f14076,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,[],[f9391]) ).
fof(f14077,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,[],[f14076]) ).
fof(f14089,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f14092,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)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9363]) ).
fof(f14093,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)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14092]) ).
fof(f14094,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f14095,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14094]) ).
fof(f14234,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6660]) ).
fof(f14235,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14234]) ).
fof(f14252,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,[],[f6759]) ).
fof(f14253,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,[],[f14252]) ).
fof(f14262,plain,
! [X0] :
( ! [X1] :
( k7_lattices(X0,k7_lattices(X0,X1)) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6733]) ).
fof(f14263,plain,
! [X0] :
( ! [X1] :
( k7_lattices(X0,k7_lattices(X0,X1)) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14262]) ).
fof(f14266,plain,
! [X0] :
( ! [X1] :
( k4_lattices(X0,k7_lattices(X0,X1),X1) = k5_lattices(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,[],[f6731]) ).
fof(f14267,plain,
! [X0] :
( ! [X1] :
( k4_lattices(X0,k7_lattices(X0,X1),X1) = k5_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14266]) ).
fof(f14333,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,[],[f8635]) ).
fof(f14334,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,[],[f14333]) ).
fof(f14343,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,[],[f8636]) ).
fof(f14344,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,[],[f14343]) ).
fof(f14384,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,[],[f13734]) ).
fof(f14404,plain,
! [X0] :
( ! [X1] :
( ( m2_filter_2(X1,X0)
| ~ m1_filter_2(X1,k1_lattice2(X0)) )
& ( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13859]) ).
fof(f14411,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( u1_struct_0(X0) != X2
& ~ r1_filter_2(u1_struct_0(X0),X1,X2)
& r1_tarski(X1,X2)
& m2_filter_2(X2,X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13895]) ).
fof(f14412,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( u1_struct_0(X0) != X2
& ~ r1_filter_2(u1_struct_0(X0),X1,X2)
& r1_tarski(X1,X2)
& m2_filter_2(X2,X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X2] :
( X2 = u1_struct_0(X0)
| r1_filter_2(u1_struct_0(X0),X1,X2)
| ~ r1_tarski(X1,X2)
| ~ m2_filter_2(X2,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14411]) ).
fof(f14413,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ? [X2] :
( u1_struct_0(X0) != X2
& ~ r1_filter_2(u1_struct_0(X0),X1,X2)
& r1_tarski(X1,X2)
& m2_filter_2(X2,X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( u1_struct_0(X0) = X3
| r1_filter_2(u1_struct_0(X0),X1,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f14412]) ).
fof(f14414,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ( u1_struct_0(X0) != sK16(X0,X1)
& ~ r1_filter_2(u1_struct_0(X0),X1,sK16(X0,X1))
& r1_tarski(X1,sK16(X0,X1))
& m2_filter_2(sK16(X0,X1),X0) ) )
& ( ( X1 != u1_struct_0(X0)
& ! [X3] :
( u1_struct_0(X0) = X3
| r1_filter_2(u1_struct_0(X0),X1,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| ~ r2_filter_2(X0,X1) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X2,sK16(X0,X1))],[f14413]) ).
fof(f14415,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,[],[f13897]) ).
fof(f14422,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( ~ r2_hidden(X2,X1)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(X2,X1)
| r2_hidden(X3,X1)
| r2_hidden(k4_lattices(X0,X2,X3),X1) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( ~ r2_hidden(X2,X1)
& ~ r2_hidden(X3,X1) ) )
& ( r2_hidden(X2,X1)
| r2_hidden(X3,X1)
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_filter_2(X1,X0) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13923]) ).
fof(f14423,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( ~ r2_hidden(X2,X1)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(X2,X1)
| r2_hidden(X3,X1)
| r2_hidden(k4_lattices(X0,X2,X3),X1) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X2] :
( ! [X3] :
( ( ( r2_hidden(k4_lattices(X0,X2,X3),X1)
| ( ~ r2_hidden(X2,X1)
& ~ r2_hidden(X3,X1) ) )
& ( r2_hidden(X2,X1)
| r2_hidden(X3,X1)
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) ) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ v1_filter_2(X1,X0) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14422]) ).
fof(f14424,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ? [X2] :
( ? [X3] :
( ( ( ~ r2_hidden(X2,X1)
& ~ r2_hidden(X3,X1) )
| ~ r2_hidden(k4_lattices(X0,X2,X3),X1) )
& ( r2_hidden(X2,X1)
| r2_hidden(X3,X1)
| r2_hidden(k4_lattices(X0,X2,X3),X1) )
& m1_subset_1(X3,u1_struct_0(X0)) )
& m1_subset_1(X2,u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ( ~ r2_hidden(X4,X1)
& ~ r2_hidden(X5,X1) ) )
& ( r2_hidden(X4,X1)
| r2_hidden(X5,X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v1_filter_2(X1,X0) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f14423]) ).
fof(f14425,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ( ( ( ~ r2_hidden(sK20(X0,X1),X1)
& ~ r2_hidden(sK21(X0,X1),X1) )
| ~ r2_hidden(k4_lattices(X0,sK20(X0,X1),sK21(X0,X1)),X1) )
& ( r2_hidden(sK20(X0,X1),X1)
| r2_hidden(sK21(X0,X1),X1)
| r2_hidden(k4_lattices(X0,sK20(X0,X1),sK21(X0,X1)),X1) )
& m1_subset_1(sK21(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK20(X0,X1),u1_struct_0(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( ( r2_hidden(k4_lattices(X0,X4,X5),X1)
| ( ~ r2_hidden(X4,X1)
& ~ r2_hidden(X5,X1) ) )
& ( r2_hidden(X4,X1)
| r2_hidden(X5,X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1) ) )
| ~ m1_subset_1(X5,u1_struct_0(X0)) )
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ v1_filter_2(X1,X0) ) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20,sK21]),skolemize(X2,sK20(X0,X1)),skolemize(X3,sK21(X0,X1))],[f14424]) ).
fof(f14426,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,[],[f13925]) ).
fof(f14430,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,[],[f13951]) ).
fof(f14431,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,[],[f14430]) ).
fof(f14432,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,[],[f13961]) ).
fof(f14433,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,[],[f14432]) ).
fof(f14434,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,[],[f14433]) ).
fof(f14435,plain,
( ( sK25 = u1_struct_0(sK24)
| ( ~ r2_hidden(sK26,sK25)
& ~ r2_hidden(k7_lattices(sK24,sK26),sK25)
& m1_subset_1(sK26,u1_struct_0(sK24)) )
| ~ r2_filter_2(sK24,sK25) )
& ( ( sK25 != u1_struct_0(sK24)
& ! [X3] :
( r2_hidden(X3,sK25)
| r2_hidden(k7_lattices(sK24,X3),sK25)
| ~ m1_subset_1(X3,u1_struct_0(sK24)) ) )
| r2_filter_2(sK24,sK25) )
& m2_filter_2(sK25,sK24)
& ~ v3_struct_0(sK24)
& v10_lattices(sK24)
& v17_lattices(sK24)
& l3_lattices(sK24) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26]),skolemize(X0,sK24),skolemize(X1,sK25),skolemize(X2,sK26)],[f14434]) ).
fof(f14557,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,[],[f14334]) ).
fof(f14558,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,[],[f14557]) ).
fof(f14559,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,[],[f14558]) ).
fof(f14560,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK96(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK96(X0,X1)),X1)
& m1_subset_1(sK96(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,[sK96]),skolemize(X2,sK96(X0,X1))],[f14559]) ).
fof(f14567,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,[],[f14344]) ).
fof(f14568,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,[],[f14567]) ).
fof(f14588,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14384]) ).
fof(f14590,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13736]) ).
fof(f14606,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,[],[f13764]) ).
fof(f14623,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,[],[f13794]) ).
fof(f14624,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = k15_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f13796]) ).
fof(f14680,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(cnf_transformation,[],[f13851]) ).
fof(f14691,plain,
! [X0,X1] :
( m1_filter_2(X1,k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14404]) ).
fof(f14693,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(cnf_transformation,[],[f13861]) ).
fof(f14728,plain,
! [X0,X1] :
( r2_hidden(k5_lattices(X0),X1)
| ~ v13_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13875]) ).
fof(f14743,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)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14414]) ).
fof(f14748,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,[],[f14415]) ).
fof(f14749,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(cnf_transformation,[],[f14415]) ).
fof(f14777,plain,
! [X0,X1,X4,X5] :
( r2_hidden(X4,X1)
| r2_hidden(X5,X1)
| ~ r2_hidden(k4_lattices(X0,X4,X5),X1)
| ~ m1_subset_1(X5,u1_struct_0(X0))
| ~ m1_subset_1(X4,u1_struct_0(X0))
| ~ v1_filter_2(X1,X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14425]) ).
fof(f14786,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(cnf_transformation,[],[f14426]) ).
fof(f14819,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,[],[f14431]) ).
fof(f14843,plain,
! [X2,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(cnf_transformation,[],[f13957]) ).
fof(f14846,plain,
l3_lattices(sK24),
inference(cnf_transformation,[],[f14435]) ).
fof(f14847,plain,
v17_lattices(sK24),
inference(cnf_transformation,[],[f14435]) ).
fof(f14848,plain,
v10_lattices(sK24),
inference(cnf_transformation,[],[f14435]) ).
fof(f14849,plain,
~ v3_struct_0(sK24),
inference(cnf_transformation,[],[f14435]) ).
fof(f14850,plain,
m2_filter_2(sK25,sK24),
inference(cnf_transformation,[],[f14435]) ).
fof(f14851,plain,
! [X3] :
( r2_hidden(X3,sK25)
| r2_hidden(k7_lattices(sK24,X3),sK25)
| ~ m1_subset_1(X3,u1_struct_0(sK24))
| r2_filter_2(sK24,sK25) ),
inference(cnf_transformation,[],[f14435]) ).
fof(f14852,plain,
( sK25 != u1_struct_0(sK24)
| r2_filter_2(sK24,sK25) ),
inference(cnf_transformation,[],[f14435]) ).
fof(f14853,plain,
( sK25 = u1_struct_0(sK24)
| m1_subset_1(sK26,u1_struct_0(sK24))
| ~ r2_filter_2(sK24,sK25) ),
inference(cnf_transformation,[],[f14435]) ).
fof(f14854,plain,
( sK25 = u1_struct_0(sK24)
| ~ r2_hidden(k7_lattices(sK24,sK26),sK25)
| ~ r2_filter_2(sK24,sK25) ),
inference(cnf_transformation,[],[f14435]) ).
fof(f14855,plain,
( sK25 = u1_struct_0(sK24)
| ~ r2_hidden(sK26,sK25)
| ~ r2_filter_2(sK24,sK25) ),
inference(cnf_transformation,[],[f14435]) ).
fof(f14874,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,[],[f13973]) ).
fof(f14973,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14077]) ).
fof(f14994,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14089]) ).
fof(f14997,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14093]) ).
fof(f15007,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14095]) ).
fof(f15228,plain,
! [X0] :
( v13_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14235]) ).
fof(f15265,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,[],[f14253]) ).
fof(f15271,plain,
! [X0,X1] :
( k7_lattices(X0,k7_lattices(X0,X1)) = 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,[],[f14263]) ).
fof(f15273,plain,
! [X0,X1] :
( k5_lattices(X0) = k4_lattices(X0,k7_lattices(X0,X1),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,[],[f14267]) ).
fof(f15388,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| m1_subset_1(sK96(X0,X1),u1_struct_0(X0))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14560]) ).
fof(f15389,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ~ r2_hidden(k7_lattices(X0,sK96(X0,X1)),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14560]) ).
fof(f15390,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ~ r2_hidden(sK96(X0,X1),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14560]) ).
fof(f15405,plain,
! [X0,X1] :
( 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(cnf_transformation,[],[f14568]) ).
fof(f15552,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)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f14743]) ).
fof(f15661,plain,
! [X2,X0] :
( k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2)
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0)))
| sP144(X0) ),
inference(cnf_transformation,[],[f15661_D]) ).
fof(f15661_D,definition,
! [X0] :
( ! [X2] :
( k7_lattices(X0,k6_filter_2(X0,X2)) = k7_lattices(k1_lattice2(X0),X2)
| ~ m1_subset_1(X2,u1_struct_0(k1_lattice2(X0))) )
<=> ~ sP144(X0) ),
introduced(definition,[new_symbols(definition,[sP144])],[general_splitting_component_introduction]) ).
fof(f15662,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ sP144(X0) ),
inference(general_splitting,[],[f14843,f15661_D]) ).
fof(f15710,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f14819]) ).
fof(f15747,definition,
( spl163_1
<=> v3_struct_0(sK24) ),
introduced(definition,[new_symbols(definition,[spl163_1])],[avatar_definition]) ).
fof(f15749,plain,
( ~ v3_struct_0(sK24)
| spl163_1 ),
inference(avatar_component_clause,[],[f15747]) ).
fof(f15750,plain,
~ spl163_1,
inference(avatar_split_clause,[],[f14849,f15747]) ).
fof(f15752,definition,
( spl163_2
<=> r2_filter_2(sK24,sK25) ),
introduced(definition,[new_symbols(definition,[spl163_2])],[avatar_definition]) ).
fof(f15753,plain,
( ~ r2_filter_2(sK24,sK25)
| spl163_2 ),
inference(avatar_component_clause,[],[f15752]) ).
fof(f15754,plain,
( r2_filter_2(sK24,sK25)
| ~ spl163_2 ),
inference(avatar_component_clause,[],[f15752]) ).
fof(f15756,definition,
( spl163_3
<=> sK25 = u1_struct_0(sK24) ),
introduced(definition,[new_symbols(definition,[spl163_3])],[avatar_definition]) ).
fof(f15757,plain,
( sK25 = u1_struct_0(sK24)
| ~ spl163_3 ),
inference(avatar_component_clause,[],[f15756]) ).
fof(f15758,plain,
( sK25 != u1_struct_0(sK24)
| spl163_3 ),
inference(avatar_component_clause,[],[f15756]) ).
fof(f15759,plain,
( spl163_2
| ~ spl163_3 ),
inference(avatar_split_clause,[],[f14852,f15756,f15752]) ).
fof(f15760,plain,
( ~ r2_hidden(sK26,sK25)
| ~ r2_filter_2(sK24,sK25)
| spl163_3 ),
inference(backward_subsumption_resolution,[],[f14855,f15758]) ).
fof(f15761,plain,
( ~ r2_hidden(k7_lattices(sK24,sK26),sK25)
| ~ r2_filter_2(sK24,sK25)
| spl163_3 ),
inference(backward_subsumption_resolution,[],[f14854,f15758]) ).
fof(f15762,plain,
( m1_subset_1(sK26,u1_struct_0(sK24))
| ~ r2_filter_2(sK24,sK25)
| spl163_3 ),
inference(backward_subsumption_resolution,[],[f14853,f15758]) ).
fof(f15764,definition,
( spl163_4
<=> ! [X3] :
( r2_hidden(X3,sK25)
| ~ m1_subset_1(X3,u1_struct_0(sK24))
| r2_hidden(k7_lattices(sK24,X3),sK25) ) ),
introduced(definition,[new_symbols(definition,[spl163_4])],[avatar_definition]) ).
fof(f15765,plain,
( ! [X3] :
( r2_hidden(k7_lattices(sK24,X3),sK25)
| ~ m1_subset_1(X3,u1_struct_0(sK24))
| r2_hidden(X3,sK25) )
| ~ spl163_4 ),
inference(avatar_component_clause,[],[f15764]) ).
fof(f15766,plain,
( spl163_2
| spl163_4 ),
inference(avatar_split_clause,[],[f14851,f15764,f15752]) ).
fof(f15767,plain,
( m1_subset_1(sK26,u1_struct_0(sK24))
| ~ spl163_2
| spl163_3 ),
inference(backward_subsumption_resolution,[],[f15762,f15754]) ).
fof(f15768,plain,
( ~ r2_hidden(k7_lattices(sK24,sK26),sK25)
| ~ spl163_2
| spl163_3 ),
inference(backward_subsumption_resolution,[],[f15761,f15754]) ).
fof(f15769,plain,
( ~ r2_hidden(sK26,sK25)
| ~ spl163_2
| spl163_3 ),
inference(backward_subsumption_resolution,[],[f15760,f15754]) ).
fof(f15770,plain,
( v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ m2_filter_2(sK25,sK24)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_2 ),
inference(resolution,[],[f15754,f14748]) ).
fof(f15773,plain,
( v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_2 ),
inference(forward_subsumption_resolution,[],[f15770,f14850]) ).
fof(f15775,plain,
( v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_2 ),
inference(forward_subsumption_resolution,[],[f15773,f15749]) ).
fof(f15777,plain,
( v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_2 ),
inference(forward_subsumption_resolution,[],[f15775,f14848]) ).
fof(f15779,plain,
( v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| ~ spl163_2 ),
inference(forward_subsumption_resolution,[],[f15777,f14846]) ).
fof(f15781,definition,
( spl163_5
<=> l3_lattices(sK24) ),
introduced(definition,[new_symbols(definition,[spl163_5])],[avatar_definition]) ).
fof(f15783,plain,
( l3_lattices(sK24)
| ~ spl163_5 ),
inference(avatar_component_clause,[],[f15781]) ).
fof(f15784,plain,
spl163_5,
inference(avatar_split_clause,[],[f14846,f15781]) ).
fof(f15786,definition,
( spl163_6
<=> v10_lattices(sK24) ),
introduced(definition,[new_symbols(definition,[spl163_6])],[avatar_definition]) ).
fof(f15788,plain,
( v10_lattices(sK24)
| ~ spl163_6 ),
inference(avatar_component_clause,[],[f15786]) ).
fof(f15789,plain,
spl163_6,
inference(avatar_split_clause,[],[f14848,f15786]) ).
fof(f15791,definition,
( spl163_7
<=> m2_filter_2(sK25,sK24) ),
introduced(definition,[new_symbols(definition,[spl163_7])],[avatar_definition]) ).
fof(f15793,plain,
( m2_filter_2(sK25,sK24)
| ~ spl163_7 ),
inference(avatar_component_clause,[],[f15791]) ).
fof(f15794,plain,
spl163_7,
inference(avatar_split_clause,[],[f14850,f15791]) ).
fof(f15795,plain,
( m2_lattice4(sK25,sK24)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14590]) ).
fof(f15797,plain,
( m1_filter_2(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14623]) ).
fof(f15798,plain,
( k15_filter_2(sK24,sK25) = k7_filter_2(sK24,sK25)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14624]) ).
fof(f15807,plain,
( m1_filter_2(sK25,k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14691]) ).
fof(f15814,plain,
( r2_hidden(k5_lattices(sK24),sK25)
| ~ v13_lattices(sK24)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14728]) ).
fof(f15822,plain,
( r2_filter_2(sK24,sK25)
| ~ v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14749]) ).
fof(f15832,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK25)
| r2_hidden(X1,sK25)
| ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v1_filter_2(sK25,sK24)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24) )
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14777]) ).
fof(f15841,plain,
( v1_filter_2(sK25,sK24)
| ~ v2_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_7 ),
inference(resolution,[],[f15793,f14786]) ).
fof(f15864,plain,
( v1_filter_2(sK25,sK24)
| ~ v2_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15841,f15749]) ).
fof(f15873,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK25)
| r2_hidden(X1,sK25)
| ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v1_filter_2(sK25,sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24) )
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15832,f15749]) ).
fof(f15884,plain,
( r2_hidden(k5_lattices(sK24),sK25)
| ~ v13_lattices(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15814,f15749]) ).
fof(f15891,plain,
( m1_filter_2(sK25,k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15807,f15749]) ).
fof(f15900,plain,
( k15_filter_2(sK24,sK25) = k7_filter_2(sK24,sK25)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15798,f15749]) ).
fof(f15901,plain,
( m1_filter_2(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15797,f15749]) ).
fof(f15903,plain,
( m2_lattice4(sK25,sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15795,f15749]) ).
fof(f15915,plain,
( v1_filter_2(sK25,sK24)
| ~ v2_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15864,f15788]) ).
fof(f15924,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK25)
| r2_hidden(X1,sK25)
| ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v1_filter_2(sK25,sK24)
| ~ l3_lattices(sK24) )
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15873,f15788]) ).
fof(f15935,plain,
( r2_hidden(k5_lattices(sK24),sK25)
| ~ v13_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15884,f15788]) ).
fof(f15942,plain,
( m1_filter_2(sK25,k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15891,f15788]) ).
fof(f15951,plain,
( k15_filter_2(sK24,sK25) = k7_filter_2(sK24,sK25)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15900,f15788]) ).
fof(f15952,plain,
( m1_filter_2(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15901,f15788]) ).
fof(f15954,plain,
( m2_lattice4(sK25,sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15903,f15788]) ).
fof(f15966,plain,
( v1_filter_2(sK25,sK24)
| ~ v2_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15915,f15783]) ).
fof(f15975,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK25)
| r2_hidden(X1,sK25)
| ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v1_filter_2(sK25,sK24) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15924,f15783]) ).
fof(f15986,plain,
( r2_hidden(k5_lattices(sK24),sK25)
| ~ v13_lattices(sK24)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15935,f15783]) ).
fof(f15993,plain,
( m1_filter_2(sK25,k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15942,f15783]) ).
fof(f16002,plain,
( k15_filter_2(sK24,sK25) = k7_filter_2(sK24,sK25)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15951,f15783]) ).
fof(f16003,plain,
( m1_filter_2(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15952,f15783]) ).
fof(f16005,plain,
( m2_lattice4(sK25,sK24)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15954,f15783]) ).
fof(f16019,plain,
( m1_filter_2(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_demodulation,[],[f16003,f16002]) ).
fof(f16043,plain,
( ! [X0] :
( m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK24))) )
| spl163_1 ),
inference(resolution,[],[f15749,f14606]) ).
fof(f16301,plain,
( u1_struct_0(sK24) = u1_struct_0(k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1 ),
inference(resolution,[],[f15749,f14973]) ).
fof(f16326,plain,
( v10_lattices(k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1 ),
inference(resolution,[],[f15749,f14997]) ).
fof(f16336,plain,
( ~ v3_struct_0(k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1 ),
inference(resolution,[],[f15749,f15007]) ).
fof(f16436,plain,
( v13_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1 ),
inference(resolution,[],[f15749,f15228]) ).
fof(f16669,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ sP144(sK24) )
| spl163_1 ),
inference(resolution,[],[f15749,f15662]) ).
fof(f16685,plain,
( v17_lattices(k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1 ),
inference(resolution,[],[f15749,f15710]) ).
fof(f16769,plain,
( v17_lattices(k1_lattice2(sK24))
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f16685,f15788]) ).
fof(f16784,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ sP144(sK24) )
| spl163_1
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f16669,f15788]) ).
fof(f17014,plain,
( v13_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1 ),
inference(forward_subsumption_resolution,[],[f16436,f14847]) ).
fof(f17099,plain,
( ~ v3_struct_0(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f16336,f15783]) ).
fof(f17107,plain,
( v10_lattices(k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f16326,f15788]) ).
fof(f17132,plain,
( u1_struct_0(sK24) = u1_struct_0(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f16301,f15783]) ).
fof(f17388,plain,
( ! [X0] :
( m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24))
| ~ l3_lattices(sK24)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK24))) )
| spl163_1
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f16043,f15788]) ).
fof(f17446,plain,
( v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f16769,f14847]) ).
fof(f17461,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ l3_lattices(sK24)
| ~ sP144(sK24) )
| spl163_1
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f16784,f14847]) ).
fof(f17658,plain,
( v13_lattices(sK24)
| spl163_1
| ~ spl163_5 ),
inference(forward_subsumption_resolution,[],[f17014,f15783]) ).
fof(f17714,plain,
( v10_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f17107,f15783]) ).
fof(f17990,plain,
( ! [X0] :
( m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK24))) )
| spl163_1
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f17388,f15783]) ).
fof(f18013,plain,
( v17_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f17446,f15783]) ).
fof(f18016,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ sP144(sK24) )
| spl163_1
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f17461,f15783]) ).
fof(f18113,plain,
( r2_hidden(k5_lattices(sK24),sK25)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(backward_subsumption_resolution,[],[f15986,f17658]) ).
fof(f18240,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24)) )
| spl163_1
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_demodulation,[],[f17990,f17132]) ).
fof(f18377,definition,
( spl163_8
<=> r2_hidden(k7_lattices(sK24,sK26),sK25) ),
introduced(definition,[new_symbols(definition,[spl163_8])],[avatar_definition]) ).
fof(f18379,plain,
( ~ r2_hidden(k7_lattices(sK24,sK26),sK25)
| spl163_8 ),
inference(avatar_component_clause,[],[f18377]) ).
fof(f18380,plain,
( ~ spl163_8
| ~ spl163_2
| spl163_3 ),
inference(avatar_split_clause,[],[f15768,f15756,f15752,f18377]) ).
fof(f18453,definition,
( spl163_9
<=> v17_lattices(sK24) ),
introduced(definition,[new_symbols(definition,[spl163_9])],[avatar_definition]) ).
fof(f18455,plain,
( v17_lattices(sK24)
| ~ spl163_9 ),
inference(avatar_component_clause,[],[f18453]) ).
fof(f18456,plain,
spl163_9,
inference(avatar_split_clause,[],[f14847,f18453]) ).
fof(f19553,plain,
( l3_lattices(k1_lattice2(sK24))
| ~ spl163_5 ),
inference(resolution,[],[f15783,f14994]) ).
fof(f20329,definition,
( spl163_10
<=> r2_hidden(sK26,sK25) ),
introduced(definition,[new_symbols(definition,[spl163_10])],[avatar_definition]) ).
fof(f20331,plain,
( ~ r2_hidden(sK26,sK25)
| spl163_10 ),
inference(avatar_component_clause,[],[f20329]) ).
fof(f20332,plain,
( ~ spl163_10
| ~ spl163_2
| spl163_3 ),
inference(avatar_split_clause,[],[f15769,f15756,f15752,f20329]) ).
fof(f20370,definition,
( spl163_11
<=> m1_subset_1(sK26,u1_struct_0(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_11])],[avatar_definition]) ).
fof(f20372,plain,
( m1_subset_1(sK26,u1_struct_0(sK24))
| ~ spl163_11 ),
inference(avatar_component_clause,[],[f20370]) ).
fof(f20373,plain,
( spl163_11
| ~ spl163_2
| spl163_3 ),
inference(avatar_split_clause,[],[f15767,f15756,f15752,f20370]) ).
fof(f21083,plain,
( ~ r2_filter_2(sK24,sK25)
| ~ m2_filter_2(sK25,sK24)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_3 ),
inference(superposition,[],[f15552,f15757]) ).
fof(f21344,plain,
( ~ m2_filter_2(sK25,sK24)
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_2
| ~ spl163_3 ),
inference(forward_subsumption_resolution,[],[f21083,f15754]) ).
fof(f22109,plain,
( v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_2
| ~ spl163_3
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f21344,f15793]) ).
fof(f22831,plain,
( ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_2
| ~ spl163_3
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f22109,f15749]) ).
fof(f23455,plain,
( ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_2
| ~ spl163_3
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f22831,f15788]) ).
fof(f23680,plain,
( $false
| spl163_1
| ~ spl163_2
| ~ spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f23455,f15783]) ).
fof(f23681,plain,
( spl163_1
| ~ spl163_2
| ~ spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(avatar_contradiction_clause,[],[f23680]) ).
fof(f24116,plain,
( m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24))
| v3_struct_0(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_11 ),
inference(resolution,[],[f20372,f15265]) ).
fof(f24127,plain,
( sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_11 ),
inference(resolution,[],[f20372,f15271]) ).
fof(f24599,plain,
( sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26))
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f24127,f15749]) ).
fof(f24610,plain,
( m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f24116,f15749]) ).
fof(f24977,plain,
( sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26))
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f24599,f15788]) ).
fof(f24988,plain,
( m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f24610,f15783]) ).
fof(f25347,plain,
( sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_9
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f24977,f18455]) ).
fof(f25562,plain,
( sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_9
| ~ spl163_11 ),
inference(forward_subsumption_resolution,[],[f25347,f15783]) ).
fof(f25773,definition,
( spl163_13
<=> m1_filter_2(sK25,k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_13])],[avatar_definition]) ).
fof(f25775,plain,
( m1_filter_2(sK25,k1_lattice2(sK24))
| ~ spl163_13 ),
inference(avatar_component_clause,[],[f25773]) ).
fof(f25776,plain,
( spl163_13
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(avatar_split_clause,[],[f15993,f15791,f15786,f15781,f15747,f25773]) ).
fof(f25779,plain,
( m1_filter_0(sK25,k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| ~ spl163_13 ),
inference(resolution,[],[f25775,f14588]) ).
fof(f25787,plain,
( m1_filter_0(sK25,k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f25779,f17099]) ).
fof(f25792,plain,
( m1_filter_0(sK25,k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f25787,f17714]) ).
fof(f25795,plain,
( m1_filter_0(sK25,k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13 ),
inference(forward_subsumption_resolution,[],[f25792,f19553]) ).
fof(f25990,definition,
( spl163_16
<=> m2_lattice4(sK25,sK24) ),
introduced(definition,[new_symbols(definition,[spl163_16])],[avatar_definition]) ).
fof(f25992,plain,
( m2_lattice4(sK25,sK24)
| ~ spl163_16 ),
inference(avatar_component_clause,[],[f25990]) ).
fof(f25993,plain,
( spl163_16
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(avatar_split_clause,[],[f16005,f15791,f15786,f15781,f15747,f25990]) ).
fof(f26008,plain,
( m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK24)))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_16 ),
inference(resolution,[],[f25992,f14874]) ).
fof(f26013,plain,
( m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK24)))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_16 ),
inference(forward_subsumption_resolution,[],[f26008,f15749]) ).
fof(f26025,plain,
( m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK24)))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_6
| ~ spl163_16 ),
inference(forward_subsumption_resolution,[],[f26013,f15788]) ).
fof(f26033,plain,
( m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK24)))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16 ),
inference(forward_subsumption_resolution,[],[f26025,f15783]) ).
fof(f26606,definition,
( spl163_23
<=> v2_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_23])],[avatar_definition]) ).
fof(f26608,plain,
( ~ v2_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_23 ),
inference(avatar_component_clause,[],[f26606]) ).
fof(f26610,definition,
( spl163_24
<=> v1_filter_2(sK25,sK24) ),
introduced(definition,[new_symbols(definition,[spl163_24])],[avatar_definition]) ).
fof(f26612,plain,
( v1_filter_2(sK25,sK24)
| ~ spl163_24 ),
inference(avatar_component_clause,[],[f26610]) ).
fof(f26613,plain,
( ~ spl163_23
| spl163_24
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(avatar_split_clause,[],[f15966,f15791,f15786,f15781,f15747,f26610,f26606]) ).
fof(f26614,plain,
( ~ v2_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23 ),
inference(forward_demodulation,[],[f26608,f16002]) ).
fof(f27888,definition,
( spl163_35
<=> m1_filter_2(k7_filter_2(sK24,sK25),k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_35])],[avatar_definition]) ).
fof(f27890,plain,
( m1_filter_2(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ spl163_35 ),
inference(avatar_component_clause,[],[f27888]) ).
fof(f27891,plain,
( spl163_35
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(avatar_split_clause,[],[f16019,f15791,f15786,f15781,f15747,f27888]) ).
fof(f28293,definition,
( spl163_43
<=> l3_lattices(k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_43])],[avatar_definition]) ).
fof(f28295,plain,
( l3_lattices(k1_lattice2(sK24))
| ~ spl163_43 ),
inference(avatar_component_clause,[],[f28293]) ).
fof(f28296,plain,
( spl163_43
| ~ spl163_5 ),
inference(avatar_split_clause,[],[f19553,f15781,f28293]) ).
fof(f28298,definition,
( spl163_44
<=> m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_44])],[avatar_definition]) ).
fof(f28300,plain,
( m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24))
| ~ spl163_44 ),
inference(avatar_component_clause,[],[f28298]) ).
fof(f28301,plain,
( spl163_44
| spl163_1
| ~ spl163_5
| ~ spl163_11 ),
inference(avatar_split_clause,[],[f24988,f20370,f15781,f15747,f28298]) ).
fof(f31196,definition,
( spl163_50
<=> v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_50])],[avatar_definition]) ).
fof(f31198,plain,
( v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ spl163_50 ),
inference(avatar_component_clause,[],[f31196]) ).
fof(f31199,plain,
( spl163_50
| spl163_1
| ~ spl163_2 ),
inference(avatar_split_clause,[],[f15779,f15752,f15747,f31196]) ).
fof(f31200,plain,
( v1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_50 ),
inference(forward_demodulation,[],[f31198,f16002]) ).
fof(f31203,definition,
( spl163_51
<=> m1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_51])],[avatar_definition]) ).
fof(f31204,plain,
( m1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ spl163_51 ),
inference(avatar_component_clause,[],[f31203]) ).
fof(f31205,plain,
( ~ m1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_51 ),
inference(avatar_component_clause,[],[f31203]) ).
fof(f31208,definition,
( spl163_52
<=> v1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_52])],[avatar_definition]) ).
fof(f31209,plain,
( ~ v1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_52 ),
inference(avatar_component_clause,[],[f31208]) ).
fof(f31210,plain,
( v1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ spl163_52 ),
inference(avatar_component_clause,[],[f31208]) ).
fof(f31211,plain,
( spl163_52
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_50 ),
inference(avatar_split_clause,[],[f31200,f31196,f15791,f15786,f15781,f15747,f31208]) ).
fof(f32035,plain,
( v2_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ m1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| ~ spl163_52 ),
inference(resolution,[],[f31210,f15405]) ).
fof(f32928,definition,
( spl163_63
<=> sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26)) ),
introduced(definition,[new_symbols(definition,[spl163_63])],[avatar_definition]) ).
fof(f32930,plain,
( sK26 = k7_lattices(sK24,k7_lattices(sK24,sK26))
| ~ spl163_63 ),
inference(avatar_component_clause,[],[f32928]) ).
fof(f32931,plain,
( spl163_63
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_9
| ~ spl163_11 ),
inference(avatar_split_clause,[],[f25562,f20370,f18453,f15786,f15781,f15747,f32928]) ).
fof(f33008,plain,
( ~ m1_filter_2(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_51 ),
inference(resolution,[],[f31205,f14588]) ).
fof(f33075,plain,
( v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| ~ spl163_35
| spl163_51 ),
inference(forward_subsumption_resolution,[],[f33008,f27890]) ).
fof(f33109,plain,
( ~ v10_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_35
| spl163_51 ),
inference(forward_subsumption_resolution,[],[f33075,f17099]) ).
fof(f33141,plain,
( ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_35
| spl163_51 ),
inference(forward_subsumption_resolution,[],[f33109,f17714]) ).
fof(f33173,plain,
( $false
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_35
| ~ spl163_43
| spl163_51 ),
inference(forward_subsumption_resolution,[],[f33141,f28295]) ).
fof(f33174,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_35
| ~ spl163_43
| spl163_51 ),
inference(avatar_contradiction_clause,[],[f33173]) ).
fof(f33230,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK25)
| r2_hidden(X1,sK25)
| ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24)) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_24 ),
inference(backward_subsumption_resolution,[],[f15975,f26612]) ).
fof(f33286,definition,
( spl163_65
<=> ! [X0,X1] :
( r2_hidden(X0,sK25)
| r2_hidden(X1,sK25)
| ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24)) ) ),
introduced(definition,[new_symbols(definition,[spl163_65])],[avatar_definition]) ).
fof(f33287,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK24,X0,X1),sK25)
| r2_hidden(X1,sK25)
| r2_hidden(X0,sK25)
| ~ m1_subset_1(X1,u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24)) )
| ~ spl163_65 ),
inference(avatar_component_clause,[],[f33286]) ).
fof(f33288,plain,
( spl163_65
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_24 ),
inference(avatar_split_clause,[],[f33230,f26610,f15791,f15786,f15781,f15747,f33286]) ).
fof(f33333,plain,
( ! [X0] :
( ~ r2_hidden(k5_lattices(sK24),sK25)
| r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ m1_subset_1(k7_lattices(sK24,X0),u1_struct_0(sK24))
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24) )
| ~ spl163_65 ),
inference(superposition,[],[f33287,f15273]) ).
fof(f33336,plain,
( ! [X0] :
( ~ r2_hidden(k5_lattices(sK24),sK25)
| r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ m1_subset_1(k7_lattices(sK24,X0),u1_struct_0(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24) )
| ~ spl163_65 ),
inference(duplicate_literal_removal,[],[f33333]) ).
fof(f33357,plain,
( ! [X0] :
( ~ r2_hidden(k5_lattices(sK24),sK25)
| r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24) )
| ~ spl163_65 ),
inference(forward_subsumption_resolution,[],[f33336,f15265]) ).
fof(f33381,plain,
( ! [X0] :
( r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_65 ),
inference(forward_subsumption_resolution,[],[f33357,f18113]) ).
fof(f33401,plain,
( ! [X0] :
( r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v10_lattices(sK24)
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_65 ),
inference(forward_subsumption_resolution,[],[f33381,f15749]) ).
fof(f33416,plain,
( ! [X0] :
( r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ v17_lattices(sK24)
| ~ l3_lattices(sK24) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_65 ),
inference(forward_subsumption_resolution,[],[f33401,f15788]) ).
fof(f33426,plain,
( ! [X0] :
( r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| ~ l3_lattices(sK24) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_9
| ~ spl163_65 ),
inference(forward_subsumption_resolution,[],[f33416,f18455]) ).
fof(f33433,plain,
( ! [X0] :
( r2_hidden(X0,sK25)
| r2_hidden(k7_lattices(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24)) )
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_9
| ~ spl163_65 ),
inference(forward_subsumption_resolution,[],[f33426,f15783]) ).
fof(f33445,plain,
( spl163_4
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_9
| ~ spl163_65 ),
inference(avatar_split_clause,[],[f33433,f33286,f18453,f15791,f15786,f15781,f15747,f15764]) ).
fof(f33516,plain,
( r2_hidden(sK26,sK25)
| ~ m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24))
| r2_hidden(k7_lattices(sK24,sK26),sK25)
| ~ spl163_4
| ~ spl163_63 ),
inference(superposition,[],[f15765,f32930]) ).
fof(f33523,plain,
( ! [X0] :
( r2_hidden(k7_lattices(k1_lattice2(sK24),X0),sK25)
| ~ m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK24)))
| sP144(sK24) )
| ~ spl163_4 ),
inference(superposition,[],[f15765,f15661]) ).
fof(f33528,plain,
( ! [X0] :
( r2_hidden(k7_lattices(k1_lattice2(sK24),X0),sK25)
| ~ m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK24))) )
| spl163_1
| ~ spl163_4
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f33523,f18016]) ).
fof(f33533,plain,
( ~ m1_subset_1(k7_lattices(sK24,sK26),u1_struct_0(sK24))
| r2_hidden(k7_lattices(sK24,sK26),sK25)
| ~ spl163_4
| spl163_10
| ~ spl163_63 ),
inference(forward_subsumption_resolution,[],[f33516,f20331]) ).
fof(f33565,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| r2_hidden(k7_lattices(k1_lattice2(sK24),X0),sK25)
| ~ m1_subset_1(k6_filter_2(sK24,X0),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,X0),sK25) )
| spl163_1
| ~ spl163_4
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_demodulation,[],[f33528,f17132]) ).
fof(f33569,plain,
( r2_hidden(k7_lattices(sK24,sK26),sK25)
| ~ spl163_4
| spl163_10
| ~ spl163_44
| ~ spl163_63 ),
inference(forward_subsumption_resolution,[],[f33533,f28300]) ).
fof(f33597,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| r2_hidden(k7_lattices(k1_lattice2(sK24),X0),sK25)
| r2_hidden(k6_filter_2(sK24,X0),sK25) )
| spl163_1
| ~ spl163_4
| ~ spl163_5
| ~ spl163_6 ),
inference(forward_subsumption_resolution,[],[f33565,f18240]) ).
fof(f33601,plain,
( $false
| ~ spl163_4
| spl163_8
| spl163_10
| ~ spl163_44
| ~ spl163_63 ),
inference(forward_subsumption_resolution,[],[f33569,f18379]) ).
fof(f33602,plain,
( ~ spl163_4
| spl163_8
| spl163_10
| ~ spl163_44
| ~ spl163_63 ),
inference(avatar_contradiction_clause,[],[f33601]) ).
fof(f33646,plain,
( ~ m1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f32035,f26614]) ).
fof(f33657,plain,
( ~ v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_2
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f15822,f15753]) ).
fof(f33665,plain,
( v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_51
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f33646,f31204]) ).
fof(f33671,plain,
( ~ v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| spl163_2
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f33657,f15749]) ).
fof(f33677,plain,
( ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_51
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f33665,f17099]) ).
fof(f33681,plain,
( ~ v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| spl163_2
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f33671,f15788]) ).
fof(f33687,plain,
( ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_51
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f33677,f17714]) ).
fof(f33690,plain,
( ~ v1_filter_0(k15_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| spl163_2
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_subsumption_resolution,[],[f33681,f15783]) ).
fof(f33696,plain,
( ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_51
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f33687,f18013]) ).
fof(f33698,plain,
( ~ v1_filter_0(k7_filter_2(sK24,sK25),k1_lattice2(sK24))
| spl163_1
| spl163_2
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(forward_demodulation,[],[f33690,f16002]) ).
fof(f33704,plain,
( $false
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_43
| ~ spl163_51
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f33696,f28295]) ).
fof(f33705,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_43
| ~ spl163_51
| ~ spl163_52 ),
inference(avatar_contradiction_clause,[],[f33704]) ).
fof(f33707,plain,
( $false
| spl163_1
| spl163_2
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_52 ),
inference(forward_subsumption_resolution,[],[f33698,f31210]) ).
fof(f33708,plain,
( spl163_1
| spl163_2
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_52 ),
inference(avatar_contradiction_clause,[],[f33707]) ).
fof(f33933,definition,
( spl163_67
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK24))
| r2_hidden(k7_lattices(k1_lattice2(sK24),X0),sK25)
| r2_hidden(k6_filter_2(sK24,X0),sK25) ) ),
introduced(definition,[new_symbols(definition,[spl163_67])],[avatar_definition]) ).
fof(f33934,plain,
( ! [X0] :
( r2_hidden(k7_lattices(k1_lattice2(sK24),X0),sK25)
| ~ m1_subset_1(X0,u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,X0),sK25) )
| ~ spl163_67 ),
inference(avatar_component_clause,[],[f33933]) ).
fof(f33935,plain,
( spl163_67
| spl163_1
| ~ spl163_4
| ~ spl163_5
| ~ spl163_6 ),
inference(avatar_split_clause,[],[f33597,f15786,f15781,f15764,f15747,f33933]) ).
fof(f33944,plain,
( ~ v1_filter_0(sK25,k1_lattice2(sK24))
| ~ m1_subset_1(sK25,k1_zfmisc_1(u1_struct_0(sK24)))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_52 ),
inference(superposition,[],[f31209,f14693]) ).
fof(f33949,plain,
( ~ v1_filter_0(sK25,k1_lattice2(sK24))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52 ),
inference(forward_subsumption_resolution,[],[f33944,f26033]) ).
fof(f33959,plain,
( ~ v1_filter_0(sK25,k1_lattice2(sK24))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52 ),
inference(forward_subsumption_resolution,[],[f33949,f15749]) ).
fof(f33967,plain,
( ~ v1_filter_0(sK25,k1_lattice2(sK24))
| ~ l3_lattices(sK24)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52 ),
inference(forward_subsumption_resolution,[],[f33959,f15788]) ).
fof(f33975,plain,
( ~ v1_filter_0(sK25,k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52 ),
inference(forward_subsumption_resolution,[],[f33967,f15783]) ).
fof(f34041,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| v1_filter_0(sK25,k1_lattice2(sK24))
| sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ m1_filter_0(sK25,k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| ~ spl163_67 ),
inference(resolution,[],[f33934,f15389]) ).
fof(f34158,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ m1_filter_0(sK25,k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34041,f33975]) ).
fof(f34193,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| sK25 = u1_struct_0(k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34158,f25795]) ).
fof(f34220,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34193,f17099]) ).
fof(f34241,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34220,f17714]) ).
fof(f34252,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34241,f18013]) ).
fof(f34257,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| sK25 = u1_struct_0(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| ~ spl163_43
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34252,f28295]) ).
fof(f34263,plain,
( sK25 = u1_struct_0(sK24)
| ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| ~ spl163_43
| spl163_52
| ~ spl163_67 ),
inference(forward_demodulation,[],[f34257,f17132]) ).
fof(f34267,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| ~ spl163_43
| spl163_52
| ~ spl163_67 ),
inference(forward_subsumption_resolution,[],[f34263,f15758]) ).
fof(f38857,definition,
( spl163_80
<=> v1_filter_0(sK25,k1_lattice2(sK24)) ),
introduced(definition,[new_symbols(definition,[spl163_80])],[avatar_definition]) ).
fof(f38859,plain,
( ~ v1_filter_0(sK25,k1_lattice2(sK24))
| spl163_80 ),
inference(avatar_component_clause,[],[f38857]) ).
fof(f38860,plain,
( ~ spl163_80
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52 ),
inference(avatar_split_clause,[],[f33975,f31208,f25990,f15786,f15781,f15747,f38857]) ).
fof(f38861,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| ~ m1_filter_0(sK25,k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_80 ),
inference(resolution,[],[f38859,f15388]) ).
fof(f38863,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| ~ m1_filter_0(sK25,k1_lattice2(sK24))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_80 ),
inference(resolution,[],[f38859,f15390]) ).
fof(f38877,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38863,f25795]) ).
fof(f38879,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| v3_struct_0(k1_lattice2(sK24))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38861,f25795]) ).
fof(f38886,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38877,f17099]) ).
fof(f38888,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| ~ v10_lattices(k1_lattice2(sK24))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38879,f17099]) ).
fof(f38893,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38886,f17714]) ).
fof(f38895,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| ~ v17_lattices(k1_lattice2(sK24))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38888,f17714]) ).
fof(f38900,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38893,f18013]) ).
fof(f38902,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| ~ l3_lattices(k1_lattice2(sK24))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38895,f18013]) ).
fof(f38907,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38900,f28295]) ).
fof(f38909,plain,
( sK25 = u1_struct_0(k1_lattice2(sK24))
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38902,f28295]) ).
fof(f38914,plain,
( sK25 = u1_struct_0(sK24)
| ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_demodulation,[],[f38907,f17132]) ).
fof(f38916,plain,
( sK25 = u1_struct_0(sK24)
| m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_demodulation,[],[f38909,f17132]) ).
fof(f38918,plain,
( ~ r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38914,f15758]) ).
fof(f38920,plain,
( m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_subsumption_resolution,[],[f38916,f15758]) ).
fof(f38921,plain,
( m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80 ),
inference(forward_demodulation,[],[f38920,f17132]) ).
fof(f38922,plain,
( r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| ~ spl163_43
| spl163_52
| ~ spl163_67
| spl163_80 ),
inference(backward_subsumption_resolution,[],[f34267,f38921]) ).
fof(f38924,definition,
( spl163_81
<=> r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25) ),
introduced(definition,[new_symbols(definition,[spl163_81])],[avatar_definition]) ).
fof(f38926,plain,
( r2_hidden(k6_filter_2(sK24,sK96(k1_lattice2(sK24),sK25)),sK25)
| ~ spl163_81 ),
inference(avatar_component_clause,[],[f38924]) ).
fof(f38927,plain,
( spl163_81
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| ~ spl163_43
| spl163_52
| ~ spl163_67
| spl163_80 ),
inference(avatar_split_clause,[],[f38922,f38857,f33933,f31208,f28293,f25990,f25773,f15786,f15781,f15756,f15747,f38924]) ).
fof(f38997,plain,
( r2_hidden(sK96(k1_lattice2(sK24),sK25),sK25)
| ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| ~ spl163_81 ),
inference(superposition,[],[f38926,f14680]) ).
fof(f38998,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| v3_struct_0(sK24)
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(forward_subsumption_resolution,[],[f38997,f38918]) ).
fof(f39028,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| ~ v10_lattices(sK24)
| ~ l3_lattices(sK24)
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(forward_subsumption_resolution,[],[f38998,f15749]) ).
fof(f39055,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| ~ l3_lattices(sK24)
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(forward_subsumption_resolution,[],[f39028,f15788]) ).
fof(f39074,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(k1_lattice2(sK24)))
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(forward_subsumption_resolution,[],[f39055,f15783]) ).
fof(f39087,plain,
( ~ m1_subset_1(sK96(k1_lattice2(sK24),sK25),u1_struct_0(sK24))
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(forward_demodulation,[],[f39074,f17132]) ).
fof(f39088,plain,
( $false
| spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(forward_subsumption_resolution,[],[f39087,f38921]) ).
fof(f39089,plain,
( spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(avatar_contradiction_clause,[],[f39088]) ).
cnf(s1,plain,
~ spl163_1,
inference(sat_conversion,[],[f15750]) ).
cnf(s2,plain,
( spl163_2
| ~ spl163_3 ),
inference(sat_conversion,[],[f15759]) ).
cnf(s3,plain,
( spl163_2
| spl163_4 ),
inference(sat_conversion,[],[f15766]) ).
cnf(s4,plain,
spl163_5,
inference(sat_conversion,[],[f15784]) ).
cnf(s5,plain,
spl163_6,
inference(sat_conversion,[],[f15789]) ).
cnf(s6,plain,
spl163_7,
inference(sat_conversion,[],[f15794]) ).
cnf(s7,plain,
( ~ spl163_2
| spl163_3
| ~ spl163_8 ),
inference(sat_conversion,[],[f18380]) ).
cnf(s8,plain,
spl163_9,
inference(sat_conversion,[],[f18456]) ).
cnf(s9,plain,
( ~ spl163_2
| spl163_3
| ~ spl163_10 ),
inference(sat_conversion,[],[f20332]) ).
cnf(s10,plain,
( ~ spl163_2
| spl163_3
| spl163_11 ),
inference(sat_conversion,[],[f20373]) ).
cnf(s12,plain,
( spl163_1
| ~ spl163_2
| ~ spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7 ),
inference(sat_conversion,[],[f23681]) ).
cnf(s15,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_13 ),
inference(sat_conversion,[],[f25776]) ).
cnf(s18,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_16 ),
inference(sat_conversion,[],[f25993]) ).
cnf(s25,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_23
| spl163_24 ),
inference(sat_conversion,[],[f26613]) ).
cnf(s35,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_35 ),
inference(sat_conversion,[],[f27891]) ).
cnf(s43,plain,
( ~ spl163_5
| spl163_43 ),
inference(sat_conversion,[],[f28296]) ).
cnf(s44,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_11
| spl163_44 ),
inference(sat_conversion,[],[f28301]) ).
cnf(s50,plain,
( spl163_1
| ~ spl163_2
| spl163_50 ),
inference(sat_conversion,[],[f31199]) ).
cnf(s52,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_50
| spl163_52 ),
inference(sat_conversion,[],[f31211]) ).
cnf(s63,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_9
| ~ spl163_11
| spl163_63 ),
inference(sat_conversion,[],[f32931]) ).
cnf(s65,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_35
| ~ spl163_43
| spl163_51 ),
inference(sat_conversion,[],[f33174]) ).
cnf(s67,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_24
| spl163_65 ),
inference(sat_conversion,[],[f33288]) ).
cnf(s68,plain,
( spl163_1
| spl163_4
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_9
| ~ spl163_65 ),
inference(sat_conversion,[],[f33445]) ).
cnf(s70,plain,
( ~ spl163_4
| spl163_8
| spl163_10
| ~ spl163_44
| ~ spl163_63 ),
inference(sat_conversion,[],[f33602]) ).
cnf(s72,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| spl163_23
| ~ spl163_43
| ~ spl163_51
| ~ spl163_52 ),
inference(sat_conversion,[],[f33705]) ).
cnf(s73,plain,
( spl163_1
| spl163_2
| ~ spl163_5
| ~ spl163_6
| ~ spl163_7
| ~ spl163_52 ),
inference(sat_conversion,[],[f33708]) ).
cnf(s76,plain,
( spl163_1
| ~ spl163_4
| ~ spl163_5
| ~ spl163_6
| spl163_67 ),
inference(sat_conversion,[],[f33935]) ).
cnf(s90,plain,
( spl163_1
| ~ spl163_5
| ~ spl163_6
| ~ spl163_16
| spl163_52
| ~ spl163_80 ),
inference(sat_conversion,[],[f38860]) ).
cnf(s91,plain,
( spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_16
| ~ spl163_43
| spl163_52
| ~ spl163_67
| spl163_80
| spl163_81 ),
inference(sat_conversion,[],[f38927]) ).
cnf(s92,plain,
( spl163_1
| spl163_3
| ~ spl163_5
| ~ spl163_6
| ~ spl163_13
| ~ spl163_43
| spl163_80
| ~ spl163_81 ),
inference(sat_conversion,[],[f39089]) ).
cnf(s93,plain,
spl163_43,
inference(rat,[],[s43,s4]) ).
cnf(s103,plain,
spl163_35,
inference(rat,[],[s35,s4,s6,s5,s1]) ).
cnf(s106,plain,
spl163_16,
inference(rat,[],[s18,s4,s6,s5,s1]) ).
cnf(s108,plain,
spl163_13,
inference(rat,[],[s15,s4,s6,s5,s1]) ).
cnf(s110,plain,
spl163_51,
inference(rat,[],[s65,s1,s93,s4,s5,s103]) ).
cnf(s124,plain,
spl163_2,
inference(rat,[],[s91,s92,s76,s90,s2,s3,s73,s4,s5,s1,s106,s93,s108,s6]) ).
cnf(s125,plain,
spl163_50,
inference(rat,[],[s50,s1,s124]) ).
cnf(s127,plain,
~ spl163_3,
inference(rat,[],[s12,s6,s5,s4,s1,s124]) ).
cnf(s128,plain,
spl163_52,
inference(rat,[],[s52,s1,s4,s6,s5,s125]) ).
cnf(s133,plain,
spl163_11,
inference(rat,[],[s10,s124,s127]) ).
cnf(s134,plain,
~ spl163_10,
inference(rat,[],[s9,s124,s127]) ).
cnf(s135,plain,
~ spl163_8,
inference(rat,[],[s7,s124,s127]) ).
cnf(s136,plain,
spl163_23,
inference(rat,[],[s72,s110,s1,s93,s4,s6,s5,s128]) ).
cnf(s137,plain,
spl163_63,
inference(rat,[],[s63,s1,s4,s8,s5,s133]) ).
cnf(s138,plain,
spl163_44,
inference(rat,[],[s44,s1,s4,s133]) ).
cnf(s144,plain,
~ spl163_4,
inference(rat,[],[s70,s137,s138,s134,s135]) ).
cnf(s146,plain,
spl163_24,
inference(rat,[],[s25,s1,s4,s6,s5,s136]) ).
cnf(s149,plain,
~ spl163_65,
inference(rat,[],[s68,s1,s8,s6,s5,s4,s144]) ).
cnf(s150,plain,
$false,
inference(rat,[],[s67,s1,s4,s6,s5,s149,s146]) ).
fof(f39090,plain,
$false,
inference(avatar_sat_refutation,[],[s150]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT321+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 14:36:06 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.32 Running first-order theorem proving
% 0.07/0.32 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.94/2.07 % (2439603)Detected formulas, will run a generic FOF schedule.
% 8.94/2.07 % (2439613)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2073347294:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 8.94/2.07 % (2439615)dis-21_1_sil=8000:lcm=predicate:random_seed=1492326819:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 8.94/2.07 % (2439610)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=3283695209:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 8.94/2.07 % (2439612)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2826320280:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 8.94/2.07 % (2439609)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=2882482926:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 8.94/2.07 % (2439611)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=475754959:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 8.94/2.07 % (2439614)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=710612620:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 8.94/2.07 % (2439614)Instruction limit reached!
% 8.94/2.07 % (2439614)------------------------------
% 8.94/2.07 % (2439614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.07 % (2439614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.07 % (2439614)CaDiCaL version: 2.1.3
% 8.94/2.07 % (2439614)Termination reason: Instruction limit
% 8.94/2.07 % (2439614)Termination phase: Property scanning
% 8.94/2.07 % (2439614)Time elapsed: 0.031 s
% 8.94/2.07 % (2439614)Peak memory usage: 102 MB
% 8.94/2.07 % (2439614)Instructions burned: 142 (million)
% 8.94/2.07 % (2439612)Instruction limit reached!
% 8.94/2.07 % (2439612)------------------------------
% 8.94/2.07 % (2439612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.07 % (2439612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.07 % (2439612)CaDiCaL version: 2.1.3
% 8.94/2.07 % (2439612)Termination reason: Instruction limit
% 8.94/2.07 % (2439612)Termination phase: Saturation
% 8.94/2.07 % (2439612)Time elapsed: 0.049 s
% 8.94/2.07 % (2439612)Peak memory usage: 107 MB
% 8.94/2.07 % (2439612)Instructions burned: 113 (million)
% 8.94/2.07 % (2439613)Instruction limit reached!
% 8.94/2.07 % (2439613)------------------------------
% 8.94/2.07 % (2439613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.07 % (2439613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.07 % (2439613)CaDiCaL version: 2.1.3
% 8.94/2.07 % (2439613)Termination reason: Instruction limit
% 8.94/2.07 % (2439613)Termination phase: Function definition elimination
% 8.94/2.07 % (2439613)Time elapsed: 0.054 s
% 8.94/2.07 % (2439613)Peak memory usage: 105 MB
% 8.94/2.07 % (2439613)Instructions burned: 119 (million)
% 8.94/2.07 % (2439615)Instruction limit reached!
% 8.94/2.07 % (2439615)------------------------------
% 8.94/2.07 % (2439615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.94/2.07 % (2439615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.94/2.07 % (2439615)CaDiCaL version: 2.1.3
% 8.94/2.07 % (2439615)Termination reason: Instruction limit
% 8.94/2.07 % (2439615)Termination phase: Preprocessing 1
% 8.94/2.07 % (2439615)Time elapsed: 0.056 s
% 8.94/2.07 % (2439615)Peak memory usage: 103 MB
% 8.94/2.07 % (2439615)Instructions burned: 130 (million)
% 8.94/2.07 % (2439623)lrs+10_1_sil=8000:sp=occurrence:random_seed=1920039930:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 8.94/2.07 % (2439626)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=1826440103:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.94/2.07 % (2439625)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2008811573:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 8.94/2.07 % (2439624)lrs+10_1_sil=32000:urr=on:br=off:random_seed=824183391:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 13.66/2.70 % (2439624)Instruction limit reached!
% 13.66/2.70 % (2439624)------------------------------
% 13.66/2.70 % (2439624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439624)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439624)Termination reason: Instruction limit
% 13.66/2.70 % (2439624)Termination phase: Property scanning
% 13.66/2.70 % (2439624)Time elapsed: 0.035 s
% 13.66/2.70 % (2439624)Peak memory usage: 102 MB
% 13.66/2.70 % (2439624)Instructions burned: 159 (million)
% 13.66/2.70 % (2439626)Instruction limit reached!
% 13.66/2.70 % (2439626)------------------------------
% 13.66/2.70 % (2439626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439626)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439626)Termination reason: Instruction limit
% 13.66/2.70 % (2439626)Termination phase: SInE selection
% 13.66/2.70 % (2439626)Time elapsed: 0.070 s
% 13.66/2.70 % (2439626)Peak memory usage: 103 MB
% 13.66/2.70 % (2439626)Instructions burned: 250 (million)
% 13.66/2.70 % (2439623)Instruction limit reached!
% 13.66/2.70 % (2439623)------------------------------
% 13.66/2.70 % (2439623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439623)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439623)Termination reason: Instruction limit
% 13.66/2.70 % (2439623)Termination phase: Saturation
% 13.66/2.70 % (2439623)Time elapsed: 0.111 s
% 13.66/2.70 % (2439623)Peak memory usage: 110 MB
% 13.66/2.70 % (2439623)Instructions burned: 285 (million)
% 13.66/2.70 % (2439631)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=718570259:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.66/2.70 % (2439625)Instruction limit reached!
% 13.66/2.70 % (2439625)------------------------------
% 13.66/2.70 % (2439625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439625)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439625)Termination reason: Instruction limit
% 13.66/2.70 % (2439625)Termination phase: Saturation
% 13.66/2.70 % (2439625)Time elapsed: 0.130 s
% 13.66/2.70 % (2439625)Peak memory usage: 110 MB
% 13.66/2.70 % (2439625)Instructions burned: 325 (million)
% 13.66/2.70 % (2439632)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1827797655:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 13.66/2.70 % (2439633)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1866920432:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 13.66/2.70 % (2439631)Instruction limit reached!
% 13.66/2.70 % (2439631)------------------------------
% 13.66/2.70 % (2439631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439631)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439631)Termination reason: Instruction limit
% 13.66/2.70 % (2439631)Termination phase: Saturation
% 13.66/2.70 % (2439631)Time elapsed: 0.107 s
% 13.66/2.70 % (2439631)Peak memory usage: 109 MB
% 13.66/2.70 % (2439631)Instructions burned: 296 (million)
% 13.66/2.70 % (2439635)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1194892579:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 13.66/2.70 % (2439633)Instruction limit reached!
% 13.66/2.70 % (2439633)------------------------------
% 13.66/2.70 % (2439633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439633)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439633)Termination reason: Instruction limit
% 13.66/2.70 % (2439633)Termination phase: Preprocessing 3
% 13.66/2.70 % (2439633)Time elapsed: 0.057 s
% 13.66/2.70 % (2439633)Peak memory usage: 105 MB
% 13.66/2.70 % (2439633)Instructions burned: 114 (million)
% 13.66/2.70 % (2439635)Instruction limit reached!
% 13.66/2.70 % (2439635)------------------------------
% 13.66/2.70 % (2439635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439635)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439635)Termination reason: Instruction limit
% 13.66/2.70 % (2439635)Termination phase: Preprocessing 2
% 13.66/2.70 % (2439635)Time elapsed: 0.064 s
% 13.66/2.70 % (2439635)Peak memory usage: 106 MB
% 13.66/2.70 % (2439635)Instructions burned: 127 (million)
% 13.66/2.70 % (2439638)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1337539579:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 13.66/2.70 % (2439640)lrs+10_1_sil=8000:sp=occurrence:random_seed=893657261:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 13.66/2.70 % (2439638)Instruction limit reached!
% 13.66/2.70 % (2439638)------------------------------
% 13.66/2.70 % (2439638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439638)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439638)Termination reason: Instruction limit
% 13.66/2.70 % (2439638)Termination phase: Property scanning
% 13.66/2.70 % (2439638)Time elapsed: 0.028 s
% 13.66/2.70 % (2439638)Peak memory usage: 102 MB
% 13.66/2.70 % (2439638)Instructions burned: 118 (million)
% 13.66/2.70 % (2439641)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1745475570:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 13.66/2.70 % (2439644)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1951365886:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 13.66/2.70 % (2439641)Instruction limit reached!
% 13.66/2.70 % (2439641)------------------------------
% 13.66/2.70 % (2439641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439641)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439641)Termination reason: Instruction limit
% 13.66/2.70 % (2439641)Termination phase: Saturation
% 13.66/2.70 % (2439641)Time elapsed: 0.144 s
% 13.66/2.70 % (2439641)Peak memory usage: 110 MB
% 13.66/2.70 % (2439641)Instructions burned: 438 (million)
% 13.66/2.70 % (2439647)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=633487248:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 13.66/2.70 % (2439640)Instruction limit reached!
% 13.66/2.70 % (2439640)------------------------------
% 13.66/2.70 % (2439640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439640)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439640)Termination reason: Instruction limit
% 13.66/2.70 % (2439640)Termination phase: Saturation
% 13.66/2.70 % (2439640)Time elapsed: 0.342 s
% 13.66/2.70 % (2439640)Peak memory usage: 121 MB
% 13.66/2.70 % (2439640)Instructions burned: 907 (million)
% 13.66/2.70 % (2439647)Instruction limit reached!
% 13.66/2.70 % (2439647)------------------------------
% 13.66/2.70 % (2439647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439647)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439647)Termination reason: Instruction limit
% 13.66/2.70 % (2439647)Termination phase: Property scanning
% 13.66/2.70 % (2439647)Time elapsed: 0.062 s
% 13.66/2.70 % (2439647)Peak memory usage: 106 MB
% 13.66/2.70 % (2439647)Instructions burned: 138 (million)
% 13.66/2.70 % (2439649)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2233547810:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 13.66/2.70 % (2439650)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3130963041:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 13.66/2.70 % (2439632)Instruction limit reached!
% 13.66/2.70 % (2439632)------------------------------
% 13.66/2.70 % (2439632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439632)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439632)Termination reason: Instruction limit
% 13.66/2.70 % (2439632)Termination phase: Saturation
% 13.66/2.70 % (2439632)Time elapsed: 0.833 s
% 13.66/2.70 % (2439632)Peak memory usage: 240 MB
% 13.66/2.70 % (2439632)Instructions burned: 2353 (million)
% 13.66/2.70 % (2439649)Instruction limit reached!
% 13.66/2.70 % (2439649)------------------------------
% 13.66/2.70 % (2439649)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439649)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439649)Termination reason: Instruction limit
% 13.66/2.70 % (2439649)Termination phase: Property scanning
% 13.66/2.70 % (2439649)Time elapsed: 0.238 s
% 13.66/2.70 % (2439649)Peak memory usage: 122 MB
% 13.66/2.70 % (2439649)Instructions burned: 593 (million)
% 13.66/2.70 % (2439653)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=557877224:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 13.66/2.70 % (2439653)Instruction limit reached!
% 13.66/2.70 % (2439653)------------------------------
% 13.66/2.70 % (2439653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439653)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439653)Termination reason: Instruction limit
% 13.66/2.70 % (2439653)Termination phase: Property scanning
% 13.66/2.70 % (2439653)Time elapsed: 0.030 s
% 13.66/2.70 % (2439653)Peak memory usage: 102 MB
% 13.66/2.70 % (2439653)Instructions burned: 130 (million)
% 13.66/2.70 % (2439654)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3860028663:i=134:gtgl=5:slsql=off:gtg=exists_sym_2984 on theBenchmark for (2984ds/134Mi)
% 13.66/2.70 % (2439654)Instruction limit reached!
% 13.66/2.70 % (2439654)------------------------------
% 13.66/2.70 % (2439654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439654)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439654)Termination reason: Instruction limit
% 13.66/2.70 % (2439654)Termination phase: Property scanning
% 13.66/2.70 % (2439654)Time elapsed: 0.033 s
% 13.66/2.70 % (2439654)Peak memory usage: 102 MB
% 13.66/2.70 % (2439654)Instructions burned: 136 (million)
% 13.66/2.70 % (2439656)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3935495713:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 13.66/2.70 % (2439656)Instruction limit reached!
% 13.66/2.70 % (2439656)------------------------------
% 13.66/2.70 % (2439656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439656)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439656)Termination reason: Instruction limit
% 13.66/2.70 % (2439656)Termination phase: Saturation
% 13.66/2.70 % (2439656)Time elapsed: 0.058 s
% 13.66/2.70 % (2439656)Peak memory usage: 107 MB
% 13.66/2.70 % (2439656)Instructions burned: 144 (million)
% 13.66/2.70 % (2439658)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=991002325:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi)
% 13.66/2.70 % (2439661)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3698322907:i=6060:aac=none:ins=25_2981 on theBenchmark for (2981ds/6060Mi)
% 13.66/2.70 % (2439611)First to succeed.
% 13.66/2.70 % (2439658)Instruction limit reached!
% 13.66/2.70 % (2439658)------------------------------
% 13.66/2.70 % (2439658)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.70 % (2439658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.70 % (2439658)CaDiCaL version: 2.1.3
% 13.66/2.70 % (2439658)Termination reason: Instruction limit
% 13.66/2.70 % (2439658)Termination phase: Saturation
% 13.66/2.70 % (2439658)Time elapsed: 0.161 s
% 13.66/2.70 % (2439658)Peak memory usage: 112 MB
% 13.66/2.70 % (2439658)Instructions burned: 434 (million)
% 13.66/2.70 % (2439611)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2439603"
% 13.66/2.70 % (2439663)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=4287752859:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi)
% 13.66/2.70 % (2439611)Refutation found. Thanks to Tanya!
% 13.66/2.70 % SZS status Theorem for theBenchmark
% 13.66/2.70 % SZS output start Proof for theBenchmark
% See solution above
% 0.07/2.80 % (2439611)------------------------------
% 0.07/2.80 % (2439611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.07/2.80 % (2439611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/2.80 % (2439611)CaDiCaL version: 2.1.3
% 0.07/2.80 % (2439611)Termination reason: Refutation
% 0.07/2.80 % (2439611)Time elapsed: 1.592 s
% 0.07/2.80 % (2439611)Peak memory usage: 180 MB
% 0.07/2.80 % (2439611)Instructions burned: 4851 (million)
% 0.07/2.80 % (2439611)------------------------------
% 0.07/2.80 % (2439611)------------------------------
% 0.07/2.80 % (2439603)Success in time 2.174 s
% 0.07/2.80 % Vampire exiting
%------------------------------------------------------------------------------