%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT321+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:55 AM UTC 2026
% Result : Theorem 31.79s 8.09s
% Output : Refutation 37.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 51
% Syntax : Number of formulae : 418 ( 33 unt; 25 def)
% Number of atoms : 2508 ( 126 equ)
% Maximal formula atoms : 22 ( 6 avg)
% Number of connectives : 3479 (1389 ~;1702 |; 277 &)
% ( 57 <=>; 52 =>; 0 <=; 2 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 56 ( 54 usr; 25 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 3 con; 0-3 aty)
% Number of variables : 337 ( 0 sgn 312 !; 25 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18128,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(f18199,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(f18227,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(f21562,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(f21563,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(f22747,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(f22752,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(f22780,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(f22852,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(f31985,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(f34606,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(f34607,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(f34621,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(f34636,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(f34637,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(f34671,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(f34675,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(f34676,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(f34683,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(f34693,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(f34694,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(f34707,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(f34708,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(f34721,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(f34724,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(f34726,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(f34727,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)],[f34726]) ).
fof(f34763,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,[],[f34606]) ).
fof(f34764,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,[],[f34763]) ).
fof(f34765,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,[],[f34607]) ).
fof(f34766,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,[],[f34765]) ).
fof(f34793,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,[],[f34621]) ).
fof(f34794,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,[],[f34793]) ).
fof(f34823,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,[],[f34636]) ).
fof(f34824,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,[],[f34823]) ).
fof(f34825,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,[],[f34637]) ).
fof(f34826,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,[],[f34825]) ).
fof(f34890,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,[],[f34671]) ).
fof(f34891,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,[],[f34890]) ).
fof(f34898,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,[],[f34675]) ).
fof(f34899,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,[],[f34898]) ).
fof(f34900,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,[],[f34676]) ).
fof(f34901,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,[],[f34900]) ).
fof(f34914,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,[],[f34683]) ).
fof(f34915,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,[],[f34914]) ).
fof(f34934,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,[],[f34693]) ).
fof(f34935,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,[],[f34934]) ).
fof(f34936,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,[],[f34694]) ).
fof(f34937,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,[],[f34936]) ).
fof(f34962,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,[],[f34707]) ).
fof(f34963,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,[],[f34962]) ).
fof(f34964,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,[],[f34708]) ).
fof(f34965,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,[],[f34964]) ).
fof(f34990,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,[],[f34721]) ).
fof(f34991,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,[],[f34990]) ).
fof(f34996,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,[],[f34724]) ).
fof(f34997,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,[],[f34996]) ).
fof(f35000,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,[],[f34727]) ).
fof(f35001,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,[],[f35000]) ).
fof(f35011,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,[],[f31985]) ).
fof(f35012,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,[],[f35011]) ).
fof(f35106,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f35123,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,[],[f22780]) ).
fof(f35124,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,[],[f35123]) ).
fof(f35126,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f35127,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f35126]) ).
fof(f35377,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,[],[f18128]) ).
fof(f35378,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,[],[f35377]) ).
fof(f35401,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,[],[f18227]) ).
fof(f35402,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,[],[f35401]) ).
fof(f35415,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,[],[f18199]) ).
fof(f35416,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,[],[f35415]) ).
fof(f35482,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,[],[f21562]) ).
fof(f35483,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,[],[f35482]) ).
fof(f35496,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,[],[f21563]) ).
fof(f35497,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,[],[f35496]) ).
fof(f35516,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,[],[f22752]) ).
fof(f35517,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,[],[f35516]) ).
fof(f35541,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,[],[f34764]) ).
fof(f35561,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,[],[f34899]) ).
fof(f35568,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,[],[f34935]) ).
fof(f35569,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,[],[f35568]) ).
fof(f35570,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,[],[f35569]) ).
fof(f35571,plain,
! [X0] :
( ! [X1] :
( ( ( r2_filter_2(X0,X1)
| u1_struct_0(X0) = X1
| ( u1_struct_0(X0) != sK17(X0,X1)
& ~ r1_filter_2(u1_struct_0(X0),X1,sK17(X0,X1))
& r1_tarski(X1,sK17(X0,X1))
& m2_filter_2(sK17(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,[sK17]),skolemize(X2,sK17(X0,X1))],[f35570]) ).
fof(f35572,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,[],[f34937]) ).
fof(f35579,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,[],[f34963]) ).
fof(f35580,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,[],[f35579]) ).
fof(f35581,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,[],[f35580]) ).
fof(f35582,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_2(X1,X0)
| ( ( ( ~ r2_hidden(sK21(X0,X1),X1)
& ~ r2_hidden(sK22(X0,X1),X1) )
| ~ r2_hidden(k4_lattices(X0,sK21(X0,X1),sK22(X0,X1)),X1) )
& ( r2_hidden(sK21(X0,X1),X1)
| r2_hidden(sK22(X0,X1),X1)
| r2_hidden(k4_lattices(X0,sK21(X0,X1),sK22(X0,X1)),X1) )
& m1_subset_1(sK22(X0,X1),u1_struct_0(X0))
& m1_subset_1(sK21(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,[sK21,sK22]),skolemize(X2,sK21(X0,X1)),skolemize(X3,sK22(X0,X1))],[f35581]) ).
fof(f35583,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,[],[f34965]) ).
fof(f35587,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,[],[f34991]) ).
fof(f35588,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,[],[f35587]) ).
fof(f35589,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,[],[f35001]) ).
fof(f35590,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,[],[f35589]) ).
fof(f35591,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,[],[f35590]) ).
fof(f35592,plain,
( ( sK26 = u1_struct_0(sK25)
| ( ~ r2_hidden(sK27,sK26)
& ~ r2_hidden(k7_lattices(sK25,sK27),sK26)
& m1_subset_1(sK27,u1_struct_0(sK25)) )
| ~ r2_filter_2(sK25,sK26) )
& ( ( sK26 != u1_struct_0(sK25)
& ! [X3] :
( r2_hidden(X3,sK26)
| r2_hidden(k7_lattices(sK25,X3),sK26)
| ~ m1_subset_1(X3,u1_struct_0(sK25)) ) )
| r2_filter_2(sK25,sK26) )
& m2_filter_2(sK26,sK25)
& ~ v3_struct_0(sK25)
& v10_lattices(sK25)
& v17_lattices(sK25)
& l3_lattices(sK25) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27]),skolemize(X0,sK25),skolemize(X1,sK26),skolemize(X2,sK27)],[f35591]) ).
fof(f35803,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,[],[f35483]) ).
fof(f35804,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,[],[f35803]) ).
fof(f35805,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,[],[f35804]) ).
fof(f35806,plain,
! [X0] :
( ! [X1] :
( ( ( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ( ~ r2_hidden(sK147(X0,X1),X1)
& ~ r2_hidden(k7_lattices(X0,sK147(X0,X1)),X1)
& m1_subset_1(sK147(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,[sK147]),skolemize(X2,sK147(X0,X1))],[f35805]) ).
fof(f35818,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,[],[f35497]) ).
fof(f35819,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,[],[f35818]) ).
fof(f35842,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,[],[f35541]) ).
fof(f35844,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,[],[f34766]) ).
fof(f35860,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,[],[f34794]) ).
fof(f35877,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,[],[f34824]) ).
fof(f35878,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,[],[f34826]) ).
fof(f35944,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,[],[f34891]) ).
fof(f35955,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,[],[f35561]) ).
fof(f35957,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,[],[f34901]) ).
fof(f35992,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,[],[f34915]) ).
fof(f36007,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,[],[f35571]) ).
fof(f36012,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,[],[f35572]) ).
fof(f36013,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,[],[f35572]) ).
fof(f36041,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,[],[f35582]) ).
fof(f36050,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,[],[f35583]) ).
fof(f36083,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,[],[f35588]) ).
fof(f36107,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,[],[f34997]) ).
fof(f36110,plain,
l3_lattices(sK25),
inference(cnf_transformation,[],[f35592]) ).
fof(f36111,plain,
v17_lattices(sK25),
inference(cnf_transformation,[],[f35592]) ).
fof(f36112,plain,
v10_lattices(sK25),
inference(cnf_transformation,[],[f35592]) ).
fof(f36113,plain,
~ v3_struct_0(sK25),
inference(cnf_transformation,[],[f35592]) ).
fof(f36114,plain,
m2_filter_2(sK26,sK25),
inference(cnf_transformation,[],[f35592]) ).
fof(f36115,plain,
! [X3] :
( r2_hidden(X3,sK26)
| r2_hidden(k7_lattices(sK25,X3),sK26)
| ~ m1_subset_1(X3,u1_struct_0(sK25))
| r2_filter_2(sK25,sK26) ),
inference(cnf_transformation,[],[f35592]) ).
fof(f36116,plain,
( sK26 != u1_struct_0(sK25)
| r2_filter_2(sK25,sK26) ),
inference(cnf_transformation,[],[f35592]) ).
fof(f36117,plain,
( sK26 = u1_struct_0(sK25)
| m1_subset_1(sK27,u1_struct_0(sK25))
| ~ r2_filter_2(sK25,sK26) ),
inference(cnf_transformation,[],[f35592]) ).
fof(f36118,plain,
( sK26 = u1_struct_0(sK25)
| ~ r2_hidden(k7_lattices(sK25,sK27),sK26)
| ~ r2_filter_2(sK25,sK26) ),
inference(cnf_transformation,[],[f35592]) ).
fof(f36119,plain,
( sK26 = u1_struct_0(sK25)
| ~ r2_hidden(sK27,sK26)
| ~ r2_filter_2(sK25,sK26) ),
inference(cnf_transformation,[],[f35592]) ).
fof(f36133,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,[],[f35012]) ).
fof(f36258,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35106]) ).
fof(f36281,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35124]) ).
fof(f36284,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35127]) ).
fof(f36645,plain,
! [X0] :
( v13_lattices(X0)
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35378]) ).
fof(f36687,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,[],[f35402]) ).
fof(f36695,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,[],[f35416]) ).
fof(f36780,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| m1_subset_1(sK147(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,[],[f35806]) ).
fof(f36781,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ~ r2_hidden(k7_lattices(X0,sK147(X0,X1)),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35806]) ).
fof(f36782,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| u1_struct_0(X0) = X1
| ~ r2_hidden(sK147(X0,X1),X1)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35806]) ).
fof(f36806,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,[],[f35819]) ).
fof(f36851,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f35517]) ).
fof(f37042,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,[],[f36007]) ).
fof(f37180,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)))
| sP199(X0) ),
inference(cnf_transformation,[],[f37180_D]) ).
fof(f37180_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))) )
<=> ~ sP199(X0) ),
introduced(definition,[new_symbols(definition,[sP199])],[general_splitting_component_introduction]) ).
fof(f37181,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0)
| ~ sP199(X0) ),
inference(general_splitting,[],[f36107,f37180_D]) ).
fof(f37231,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(duplicate_literal_removal,[],[f36083]) ).
fof(f37257,definition,
( spl219_1
<=> r2_filter_2(sK25,sK26) ),
introduced(definition,[new_symbols(definition,[spl219_1])],[avatar_definition]) ).
fof(f37258,plain,
( ~ r2_filter_2(sK25,sK26)
| spl219_1 ),
inference(avatar_component_clause,[],[f37257]) ).
fof(f37259,plain,
( r2_filter_2(sK25,sK26)
| ~ spl219_1 ),
inference(avatar_component_clause,[],[f37257]) ).
fof(f37261,definition,
( spl219_2
<=> ! [X3] :
( r2_hidden(X3,sK26)
| ~ m1_subset_1(X3,u1_struct_0(sK25))
| r2_hidden(k7_lattices(sK25,X3),sK26) ) ),
introduced(definition,[new_symbols(definition,[spl219_2])],[avatar_definition]) ).
fof(f37262,plain,
( ! [X3] :
( r2_hidden(k7_lattices(sK25,X3),sK26)
| ~ m1_subset_1(X3,u1_struct_0(sK25))
| r2_hidden(X3,sK26) )
| ~ spl219_2 ),
inference(avatar_component_clause,[],[f37261]) ).
fof(f37263,plain,
( spl219_1
| spl219_2 ),
inference(avatar_split_clause,[],[f36115,f37261,f37257]) ).
fof(f37457,definition,
( spl219_3
<=> sK26 = u1_struct_0(sK25) ),
introduced(definition,[new_symbols(definition,[spl219_3])],[avatar_definition]) ).
fof(f37458,plain,
( sK26 = u1_struct_0(sK25)
| ~ spl219_3 ),
inference(avatar_component_clause,[],[f37457]) ).
fof(f37459,plain,
( sK26 != u1_struct_0(sK25)
| spl219_3 ),
inference(avatar_component_clause,[],[f37457]) ).
fof(f37460,plain,
( spl219_1
| ~ spl219_3 ),
inference(avatar_split_clause,[],[f36116,f37457,f37257]) ).
fof(f37462,plain,
( ~ r2_hidden(sK27,sK26)
| ~ r2_filter_2(sK25,sK26)
| spl219_3 ),
inference(backward_subsumption_resolution,[],[f36119,f37459]) ).
fof(f37463,plain,
( ~ r2_hidden(k7_lattices(sK25,sK27),sK26)
| ~ r2_filter_2(sK25,sK26)
| spl219_3 ),
inference(backward_subsumption_resolution,[],[f36118,f37459]) ).
fof(f37464,plain,
( m1_subset_1(sK27,u1_struct_0(sK25))
| ~ r2_filter_2(sK25,sK26)
| spl219_3 ),
inference(backward_subsumption_resolution,[],[f36117,f37459]) ).
fof(f37466,definition,
( spl219_4
<=> v3_struct_0(sK25) ),
introduced(definition,[new_symbols(definition,[spl219_4])],[avatar_definition]) ).
fof(f37468,plain,
( ~ v3_struct_0(sK25)
| spl219_4 ),
inference(avatar_component_clause,[],[f37466]) ).
fof(f37469,plain,
~ spl219_4,
inference(avatar_split_clause,[],[f36113,f37466]) ).
fof(f37471,definition,
( spl219_5
<=> l3_lattices(sK25) ),
introduced(definition,[new_symbols(definition,[spl219_5])],[avatar_definition]) ).
fof(f37473,plain,
( l3_lattices(sK25)
| ~ spl219_5 ),
inference(avatar_component_clause,[],[f37471]) ).
fof(f37474,plain,
spl219_5,
inference(avatar_split_clause,[],[f36110,f37471]) ).
fof(f37476,definition,
( spl219_6
<=> v17_lattices(sK25) ),
introduced(definition,[new_symbols(definition,[spl219_6])],[avatar_definition]) ).
fof(f37478,plain,
( v17_lattices(sK25)
| ~ spl219_6 ),
inference(avatar_component_clause,[],[f37476]) ).
fof(f37479,plain,
spl219_6,
inference(avatar_split_clause,[],[f36111,f37476]) ).
fof(f37481,definition,
( spl219_7
<=> v10_lattices(sK25) ),
introduced(definition,[new_symbols(definition,[spl219_7])],[avatar_definition]) ).
fof(f37483,plain,
( v10_lattices(sK25)
| ~ spl219_7 ),
inference(avatar_component_clause,[],[f37481]) ).
fof(f37484,plain,
spl219_7,
inference(avatar_split_clause,[],[f36112,f37481]) ).
fof(f37486,definition,
( spl219_8
<=> m2_filter_2(sK26,sK25) ),
introduced(definition,[new_symbols(definition,[spl219_8])],[avatar_definition]) ).
fof(f37488,plain,
( m2_filter_2(sK26,sK25)
| ~ spl219_8 ),
inference(avatar_component_clause,[],[f37486]) ).
fof(f37489,plain,
spl219_8,
inference(avatar_split_clause,[],[f36114,f37486]) ).
fof(f37490,plain,
( m2_lattice4(sK26,sK25)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f35844]) ).
fof(f37492,plain,
( m1_filter_2(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f35877]) ).
fof(f37493,plain,
( k15_filter_2(sK25,sK26) = k7_filter_2(sK25,sK26)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f35878]) ).
fof(f37502,plain,
( m1_filter_2(sK26,k1_lattice2(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f35955]) ).
fof(f37509,plain,
( r2_hidden(k5_lattices(sK25),sK26)
| ~ v13_lattices(sK25)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f35992]) ).
fof(f37516,plain,
( v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ r2_filter_2(sK25,sK26)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f36012]) ).
fof(f37517,plain,
( r2_filter_2(sK25,sK26)
| ~ v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f36013]) ).
fof(f37527,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK26)
| r2_hidden(X1,sK26)
| ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v1_filter_2(sK26,sK25)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25) )
| ~ spl219_8 ),
inference(resolution,[],[f37488,f36041]) ).
fof(f37536,plain,
( v1_filter_2(sK26,sK25)
| ~ v2_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_8 ),
inference(resolution,[],[f37488,f36050]) ).
fof(f37559,plain,
( v1_filter_2(sK26,sK25)
| ~ v2_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37536,f37468]) ).
fof(f37568,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK26)
| r2_hidden(X1,sK26)
| ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v1_filter_2(sK26,sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25) )
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37527,f37468]) ).
fof(f37578,plain,
( r2_filter_2(sK25,sK26)
| ~ v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37517,f37468]) ).
fof(f37579,plain,
( v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ r2_filter_2(sK25,sK26)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37516,f37468]) ).
fof(f37586,plain,
( r2_hidden(k5_lattices(sK25),sK26)
| ~ v13_lattices(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37509,f37468]) ).
fof(f37593,plain,
( m1_filter_2(sK26,k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37502,f37468]) ).
fof(f37602,plain,
( k15_filter_2(sK25,sK26) = k7_filter_2(sK25,sK26)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37493,f37468]) ).
fof(f37603,plain,
( m1_filter_2(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37492,f37468]) ).
fof(f37605,plain,
( m2_lattice4(sK26,sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37490,f37468]) ).
fof(f37617,plain,
( v1_filter_2(sK26,sK25)
| ~ v2_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37559,f37483]) ).
fof(f37626,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK26)
| r2_hidden(X1,sK26)
| ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v1_filter_2(sK26,sK25)
| ~ l3_lattices(sK25) )
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37568,f37483]) ).
fof(f37636,plain,
( r2_filter_2(sK25,sK26)
| ~ v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37578,f37483]) ).
fof(f37637,plain,
( v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ r2_filter_2(sK25,sK26)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37579,f37483]) ).
fof(f37644,plain,
( r2_hidden(k5_lattices(sK25),sK26)
| ~ v13_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37586,f37483]) ).
fof(f37651,plain,
( m1_filter_2(sK26,k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37593,f37483]) ).
fof(f37660,plain,
( k15_filter_2(sK25,sK26) = k7_filter_2(sK25,sK26)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37602,f37483]) ).
fof(f37661,plain,
( m1_filter_2(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37603,f37483]) ).
fof(f37663,plain,
( m2_lattice4(sK26,sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37605,f37483]) ).
fof(f37675,plain,
( v1_filter_2(sK26,sK25)
| ~ v2_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37617,f37473]) ).
fof(f37684,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK26)
| r2_hidden(X1,sK26)
| ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v1_filter_2(sK26,sK25) )
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37626,f37473]) ).
fof(f37694,plain,
( r2_filter_2(sK25,sK26)
| ~ v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37636,f37473]) ).
fof(f37695,plain,
( v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ r2_filter_2(sK25,sK26)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37637,f37473]) ).
fof(f37702,plain,
( r2_hidden(k5_lattices(sK25),sK26)
| ~ v13_lattices(sK25)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37644,f37473]) ).
fof(f37709,plain,
( m1_filter_2(sK26,k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37651,f37473]) ).
fof(f37718,plain,
( k15_filter_2(sK25,sK26) = k7_filter_2(sK25,sK26)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37660,f37473]) ).
fof(f37719,plain,
( m1_filter_2(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37661,f37473]) ).
fof(f37721,plain,
( m2_lattice4(sK26,sK25)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f37663,f37473]) ).
fof(f37739,plain,
( m1_filter_2(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_demodulation,[],[f37719,f37718]) ).
fof(f37765,plain,
( ! [X0] :
( m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK25))) )
| spl219_4 ),
inference(resolution,[],[f37468,f35860]) ).
fof(f38058,plain,
( u1_struct_0(sK25) = u1_struct_0(k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4 ),
inference(resolution,[],[f37468,f36281]) ).
fof(f38060,plain,
( ~ v3_struct_0(k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4 ),
inference(resolution,[],[f37468,f36284]) ).
fof(f38175,plain,
( v13_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4 ),
inference(resolution,[],[f37468,f36645]) ).
fof(f38295,plain,
( v10_lattices(k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4 ),
inference(resolution,[],[f37468,f36851]) ).
fof(f38413,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ sP199(sK25) )
| spl219_4 ),
inference(resolution,[],[f37468,f37181]) ).
fof(f38429,plain,
( v17_lattices(k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4 ),
inference(resolution,[],[f37468,f37231]) ).
fof(f38482,plain,
( v17_lattices(k1_lattice2(sK25))
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f38429,f37483]) ).
fof(f38497,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ sP199(sK25) )
| spl219_4
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f38413,f37483]) ).
fof(f38612,plain,
( v10_lattices(k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f38295,f37483]) ).
fof(f38732,plain,
( v13_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f38175,f37478]) ).
fof(f38844,plain,
( ~ v3_struct_0(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5 ),
inference(forward_subsumption_resolution,[],[f38060,f37473]) ).
fof(f38845,plain,
( u1_struct_0(sK25) = u1_struct_0(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5 ),
inference(forward_subsumption_resolution,[],[f38058,f37473]) ).
fof(f39136,plain,
( ! [X0] :
( m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25))
| ~ l3_lattices(sK25)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK25))) )
| spl219_4
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f37765,f37483]) ).
fof(f39179,plain,
( v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f38482,f37478]) ).
fof(f39194,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ l3_lattices(sK25)
| ~ sP199(sK25) )
| spl219_4
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f38497,f37478]) ).
fof(f39286,plain,
( v10_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f38612,f37473]) ).
fof(f39396,plain,
( v13_lattices(sK25)
| spl219_4
| ~ spl219_5
| ~ spl219_6 ),
inference(forward_subsumption_resolution,[],[f38732,f37473]) ).
fof(f39759,plain,
( ! [X0] :
( m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK25))) )
| spl219_4
| ~ spl219_5
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f39136,f37473]) ).
fof(f39782,plain,
( v17_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f39179,f37473]) ).
fof(f39785,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ sP199(sK25) )
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f39194,f37473]) ).
fof(f39881,plain,
( r2_hidden(k5_lattices(sK25),sK26)
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8 ),
inference(backward_subsumption_resolution,[],[f37702,f39396]) ).
fof(f40021,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25)) )
| spl219_4
| ~ spl219_5
| ~ spl219_7 ),
inference(forward_demodulation,[],[f39759,f38845]) ).
fof(f40248,definition,
( spl219_9
<=> r2_hidden(k7_lattices(sK25,sK27),sK26) ),
introduced(definition,[new_symbols(definition,[spl219_9])],[avatar_definition]) ).
fof(f40250,plain,
( ~ r2_hidden(k7_lattices(sK25,sK27),sK26)
| spl219_9 ),
inference(avatar_component_clause,[],[f40248]) ).
fof(f40251,plain,
( ~ spl219_1
| ~ spl219_9
| spl219_3 ),
inference(avatar_split_clause,[],[f37463,f37457,f40248,f37257]) ).
fof(f40256,plain,
( ~ v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(backward_subsumption_resolution,[],[f37694,f37258]) ).
fof(f40257,plain,
( ~ v1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_demodulation,[],[f40256,f37718]) ).
fof(f41384,plain,
( l3_lattices(k1_lattice2(sK25))
| ~ spl219_5 ),
inference(resolution,[],[f37473,f36258]) ).
fof(f42089,definition,
( spl219_10
<=> r2_hidden(sK27,sK26) ),
introduced(definition,[new_symbols(definition,[spl219_10])],[avatar_definition]) ).
fof(f42092,plain,
( ~ spl219_1
| ~ spl219_10
| spl219_3 ),
inference(avatar_split_clause,[],[f37462,f37457,f42089,f37257]) ).
fof(f42094,definition,
( spl219_11
<=> v1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_11])],[avatar_definition]) ).
fof(f42095,plain,
( v1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ spl219_11 ),
inference(avatar_component_clause,[],[f42094]) ).
fof(f42096,plain,
( ~ v1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_11 ),
inference(avatar_component_clause,[],[f42094]) ).
fof(f42097,plain,
( ~ spl219_11
| spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(avatar_split_clause,[],[f40257,f37486,f37481,f37471,f37466,f37257,f42094]) ).
fof(f42099,definition,
( spl219_12
<=> m1_subset_1(sK27,u1_struct_0(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_12])],[avatar_definition]) ).
fof(f42101,plain,
( m1_subset_1(sK27,u1_struct_0(sK25))
| ~ spl219_12 ),
inference(avatar_component_clause,[],[f42099]) ).
fof(f42102,plain,
( ~ spl219_1
| spl219_12
| spl219_3 ),
inference(avatar_split_clause,[],[f37464,f37457,f42099,f37257]) ).
fof(f42441,plain,
( v1_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(backward_subsumption_resolution,[],[f37695,f37259]) ).
fof(f42443,plain,
( v1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_demodulation,[],[f42441,f37718]) ).
fof(f42445,plain,
( $false
| ~ spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_11 ),
inference(forward_subsumption_resolution,[],[f42443,f42096]) ).
fof(f42446,plain,
( ~ spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_11 ),
inference(avatar_contradiction_clause,[],[f42445]) ).
fof(f44727,definition,
( spl219_20
<=> m2_lattice4(sK26,sK25) ),
introduced(definition,[new_symbols(definition,[spl219_20])],[avatar_definition]) ).
fof(f44729,plain,
( m2_lattice4(sK26,sK25)
| ~ spl219_20 ),
inference(avatar_component_clause,[],[f44727]) ).
fof(f44730,plain,
( spl219_20
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(avatar_split_clause,[],[f37721,f37486,f37481,f37471,f37466,f44727]) ).
fof(f44745,plain,
( m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK25)))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_20 ),
inference(resolution,[],[f44729,f36133]) ).
fof(f44750,plain,
( m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK25)))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f44745,f37468]) ).
fof(f44762,plain,
( m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK25)))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_7
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f44750,f37483]) ).
fof(f44770,plain,
( m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK25)))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f44762,f37473]) ).
fof(f45236,definition,
( spl219_23
<=> m1_filter_2(sK26,k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_23])],[avatar_definition]) ).
fof(f45238,plain,
( m1_filter_2(sK26,k1_lattice2(sK25))
| ~ spl219_23 ),
inference(avatar_component_clause,[],[f45236]) ).
fof(f45239,plain,
( spl219_23
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(avatar_split_clause,[],[f37709,f37486,f37481,f37471,f37466,f45236]) ).
fof(f45329,plain,
( ! [X0] :
( r2_hidden(k7_lattices(k1_lattice2(sK25),X0),sK26)
| ~ m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK25)))
| sP199(sK25) )
| ~ spl219_2 ),
inference(superposition,[],[f37262,f37180]) ).
fof(f45334,plain,
( ! [X0] :
( r2_hidden(k7_lattices(k1_lattice2(sK25),X0),sK26)
| ~ m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(k1_lattice2(sK25))) )
| ~ spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f45329,f39785]) ).
fof(f45366,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| r2_hidden(k7_lattices(k1_lattice2(sK25),X0),sK26)
| ~ m1_subset_1(k6_filter_2(sK25,X0),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,X0),sK26) )
| ~ spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_demodulation,[],[f45334,f38845]) ).
fof(f45394,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| r2_hidden(k7_lattices(k1_lattice2(sK25),X0),sK26)
| r2_hidden(k6_filter_2(sK25,X0),sK26) )
| ~ spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(forward_subsumption_resolution,[],[f45366,f40021]) ).
fof(f45562,plain,
( ~ v1_filter_0(sK26,k1_lattice2(sK25))
| ~ m1_subset_1(sK26,k1_zfmisc_1(u1_struct_0(sK25)))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_11 ),
inference(superposition,[],[f42096,f35957]) ).
fof(f45567,plain,
( ~ v1_filter_0(sK26,k1_lattice2(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f45562,f44770]) ).
fof(f45578,plain,
( ~ v1_filter_0(sK26,k1_lattice2(sK25))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f45567,f37468]) ).
fof(f45587,plain,
( ~ v1_filter_0(sK26,k1_lattice2(sK25))
| ~ l3_lattices(sK25)
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f45578,f37483]) ).
fof(f45596,plain,
( ~ v1_filter_0(sK26,k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20 ),
inference(forward_subsumption_resolution,[],[f45587,f37473]) ).
fof(f45611,definition,
( spl219_25
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK25))
| r2_hidden(k7_lattices(k1_lattice2(sK25),X0),sK26)
| r2_hidden(k6_filter_2(sK25,X0),sK26) ) ),
introduced(definition,[new_symbols(definition,[spl219_25])],[avatar_definition]) ).
fof(f45612,plain,
( ! [X0] :
( r2_hidden(k7_lattices(k1_lattice2(sK25),X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,X0),sK26) )
| ~ spl219_25 ),
inference(avatar_component_clause,[],[f45611]) ).
fof(f45613,plain,
( spl219_25
| ~ spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7 ),
inference(avatar_split_clause,[],[f45394,f37481,f37476,f37471,f37466,f37261,f45611]) ).
fof(f49549,plain,
( m1_filter_0(sK26,k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_23 ),
inference(resolution,[],[f45238,f35842]) ).
fof(f49557,plain,
( m1_filter_0(sK26,k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_23 ),
inference(forward_subsumption_resolution,[],[f49549,f38844]) ).
fof(f49562,plain,
( m1_filter_0(sK26,k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_23 ),
inference(forward_subsumption_resolution,[],[f49557,f39286]) ).
fof(f49565,plain,
( m1_filter_0(sK26,k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_23 ),
inference(forward_subsumption_resolution,[],[f49562,f41384]) ).
fof(f49572,definition,
( spl219_26
<=> v2_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_26])],[avatar_definition]) ).
fof(f49574,plain,
( ~ v2_filter_0(k15_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_26 ),
inference(avatar_component_clause,[],[f49572]) ).
fof(f49576,definition,
( spl219_27
<=> v1_filter_2(sK26,sK25) ),
introduced(definition,[new_symbols(definition,[spl219_27])],[avatar_definition]) ).
fof(f49578,plain,
( v1_filter_2(sK26,sK25)
| ~ spl219_27 ),
inference(avatar_component_clause,[],[f49576]) ).
fof(f49579,plain,
( ~ spl219_26
| spl219_27
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(avatar_split_clause,[],[f37675,f37486,f37481,f37471,f37466,f49576,f49572]) ).
fof(f49580,plain,
( ~ v2_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_26 ),
inference(forward_demodulation,[],[f49574,f37718]) ).
fof(f49582,definition,
( spl219_28
<=> v2_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_28])],[avatar_definition]) ).
fof(f49584,plain,
( ~ v2_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_28 ),
inference(avatar_component_clause,[],[f49582]) ).
fof(f49585,plain,
( ~ spl219_28
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_26 ),
inference(avatar_split_clause,[],[f49580,f49572,f37486,f37481,f37471,f37466,f49582]) ).
fof(f49587,plain,
( ~ v1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_28 ),
inference(resolution,[],[f49584,f36806]) ).
fof(f49604,plain,
( ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_11
| spl219_28 ),
inference(forward_subsumption_resolution,[],[f49587,f42095]) ).
fof(f49614,plain,
( ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_11
| spl219_28 ),
inference(forward_subsumption_resolution,[],[f49604,f38844]) ).
fof(f49622,plain,
( ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_11
| spl219_28 ),
inference(forward_subsumption_resolution,[],[f49614,f39286]) ).
fof(f49627,plain,
( ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_11
| spl219_28 ),
inference(forward_subsumption_resolution,[],[f49622,f39782]) ).
fof(f49629,plain,
( ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_11
| spl219_28 ),
inference(forward_subsumption_resolution,[],[f49627,f41384]) ).
fof(f49631,definition,
( spl219_29
<=> m1_filter_2(k7_filter_2(sK25,sK26),k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_29])],[avatar_definition]) ).
fof(f49633,plain,
( m1_filter_2(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| ~ spl219_29 ),
inference(avatar_component_clause,[],[f49631]) ).
fof(f49634,plain,
( spl219_29
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(avatar_split_clause,[],[f37739,f37486,f37481,f37471,f37466,f49631]) ).
fof(f49896,plain,
( ~ m1_subset_1(sK27,u1_struct_0(sK25))
| r2_hidden(sK27,sK26)
| ~ spl219_2
| spl219_9 ),
inference(resolution,[],[f37262,f40250]) ).
fof(f50278,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| v1_filter_0(sK26,k1_lattice2(sK25))
| sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ m1_filter_0(sK26,k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_25 ),
inference(resolution,[],[f45612,f36781]) ).
fof(f50397,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ m1_filter_0(sK26,k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50278,f45596]) ).
fof(f50432,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| sK26 = u1_struct_0(k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50397,f49565]) ).
fof(f50460,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50432,f38844]) ).
fof(f50481,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50460,f39286]) ).
fof(f50492,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50481,f39782]) ).
fof(f50497,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| sK26 = u1_struct_0(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50492,f41384]) ).
fof(f50503,plain,
( sK26 = u1_struct_0(sK25)
| ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_demodulation,[],[f50497,f38845]) ).
fof(f50507,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25 ),
inference(forward_subsumption_resolution,[],[f50503,f37459]) ).
fof(f51286,plain,
( ~ r2_filter_2(sK25,sK26)
| ~ m2_filter_2(sK26,sK25)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_3 ),
inference(superposition,[],[f37042,f37458]) ).
fof(f51535,plain,
( ~ m2_filter_2(sK26,sK25)
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_1
| ~ spl219_3 ),
inference(forward_subsumption_resolution,[],[f51286,f37259]) ).
fof(f52323,plain,
( v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_1
| ~ spl219_3
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f51535,f37488]) ).
fof(f53079,plain,
( ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_1
| ~ spl219_3
| spl219_4
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f52323,f37468]) ).
fof(f53742,plain,
( ~ l3_lattices(sK25)
| ~ spl219_1
| ~ spl219_3
| spl219_4
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f53079,f37483]) ).
fof(f53983,plain,
( $false
| ~ spl219_1
| ~ spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(forward_subsumption_resolution,[],[f53742,f37473]) ).
fof(f53984,plain,
( ~ spl219_1
| ~ spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(avatar_contradiction_clause,[],[f53983]) ).
fof(f54155,plain,
( r2_hidden(sK27,sK26)
| ~ spl219_2
| spl219_9
| ~ spl219_12 ),
inference(forward_subsumption_resolution,[],[f49896,f42101]) ).
fof(f56227,definition,
( spl219_40
<=> m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_40])],[avatar_definition]) ).
fof(f56229,plain,
( ~ m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| spl219_40 ),
inference(avatar_component_clause,[],[f56227]) ).
fof(f56230,plain,
( ~ spl219_40
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_11
| spl219_28 ),
inference(avatar_split_clause,[],[f49629,f49582,f42094,f37481,f37476,f37471,f37466,f56227]) ).
fof(f58055,definition,
( spl219_53
<=> m1_filter_0(sK26,k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_53])],[avatar_definition]) ).
fof(f58057,plain,
( m1_filter_0(sK26,k1_lattice2(sK25))
| ~ spl219_53 ),
inference(avatar_component_clause,[],[f58055]) ).
fof(f58058,plain,
( spl219_53
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_23 ),
inference(avatar_split_clause,[],[f49565,f45236,f37481,f37471,f37466,f58055]) ).
fof(f58763,plain,
( m1_filter_0(k7_filter_2(sK25,sK26),k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_29 ),
inference(resolution,[],[f49633,f35842]) ).
fof(f58771,plain,
( v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_29
| spl219_40 ),
inference(forward_subsumption_resolution,[],[f58763,f56229]) ).
fof(f58776,plain,
( ~ v10_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_29
| spl219_40 ),
inference(forward_subsumption_resolution,[],[f58771,f38844]) ).
fof(f58779,plain,
( ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_29
| spl219_40 ),
inference(forward_subsumption_resolution,[],[f58776,f39286]) ).
fof(f58782,plain,
( $false
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_29
| spl219_40 ),
inference(forward_subsumption_resolution,[],[f58779,f41384]) ).
fof(f58783,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_29
| spl219_40 ),
inference(avatar_contradiction_clause,[],[f58782]) ).
fof(f58789,plain,
( ! [X0,X1] :
( r2_hidden(X0,sK26)
| r2_hidden(X1,sK26)
| ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25)) )
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| ~ spl219_27 ),
inference(backward_subsumption_resolution,[],[f37684,f49578]) ).
fof(f58795,definition,
( spl219_61
<=> ! [X0,X1] :
( r2_hidden(X0,sK26)
| r2_hidden(X1,sK26)
| ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25)) ) ),
introduced(definition,[new_symbols(definition,[spl219_61])],[avatar_definition]) ).
fof(f58796,plain,
( ! [X0,X1] :
( ~ r2_hidden(k4_lattices(sK25,X0,X1),sK26)
| r2_hidden(X1,sK26)
| r2_hidden(X0,sK26)
| ~ m1_subset_1(X1,u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25)) )
| ~ spl219_61 ),
inference(avatar_component_clause,[],[f58795]) ).
fof(f58797,plain,
( spl219_61
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| ~ spl219_27 ),
inference(avatar_split_clause,[],[f58789,f49576,f37486,f37481,f37471,f37466,f58795]) ).
fof(f58852,plain,
( ! [X0] :
( ~ r2_hidden(k5_lattices(sK25),sK26)
| r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ m1_subset_1(k7_lattices(sK25,X0),u1_struct_0(sK25))
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25) )
| ~ spl219_61 ),
inference(superposition,[],[f58796,f36695]) ).
fof(f58855,plain,
( ! [X0] :
( ~ r2_hidden(k5_lattices(sK25),sK26)
| r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ m1_subset_1(k7_lattices(sK25,X0),u1_struct_0(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25) )
| ~ spl219_61 ),
inference(duplicate_literal_removal,[],[f58852]) ).
fof(f58877,plain,
( ! [X0] :
( ~ r2_hidden(k5_lattices(sK25),sK26)
| r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25) )
| ~ spl219_61 ),
inference(forward_subsumption_resolution,[],[f58855,f36687]) ).
fof(f58902,plain,
( ! [X0] :
( r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25) )
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(forward_subsumption_resolution,[],[f58877,f39881]) ).
fof(f58923,plain,
( ! [X0] :
( r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v10_lattices(sK25)
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25) )
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(forward_subsumption_resolution,[],[f58902,f37468]) ).
fof(f58939,plain,
( ! [X0] :
( r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ v17_lattices(sK25)
| ~ l3_lattices(sK25) )
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(forward_subsumption_resolution,[],[f58923,f37483]) ).
fof(f58950,plain,
( ! [X0] :
( r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25))
| ~ l3_lattices(sK25) )
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(forward_subsumption_resolution,[],[f58939,f37478]) ).
fof(f58957,plain,
( ! [X0] :
( r2_hidden(X0,sK26)
| r2_hidden(k7_lattices(sK25,X0),sK26)
| ~ m1_subset_1(X0,u1_struct_0(sK25)) )
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(forward_subsumption_resolution,[],[f58950,f37473]) ).
fof(f58969,plain,
( spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(avatar_split_clause,[],[f58957,f58795,f37486,f37481,f37476,f37471,f37466,f37261]) ).
fof(f59168,plain,
( spl219_10
| ~ spl219_2
| spl219_9
| ~ spl219_12 ),
inference(avatar_split_clause,[],[f54155,f42099,f40248,f37261,f42089]) ).
fof(f60404,definition,
( spl219_64
<=> v1_filter_0(sK26,k1_lattice2(sK25)) ),
introduced(definition,[new_symbols(definition,[spl219_64])],[avatar_definition]) ).
fof(f60406,plain,
( ~ v1_filter_0(sK26,k1_lattice2(sK25))
| spl219_64 ),
inference(avatar_component_clause,[],[f60404]) ).
fof(f60407,plain,
( ~ spl219_64
| spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20 ),
inference(avatar_split_clause,[],[f45596,f44727,f42094,f37481,f37471,f37466,f60404]) ).
fof(f60408,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| ~ m1_filter_0(sK26,k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_64 ),
inference(resolution,[],[f60406,f36780]) ).
fof(f60410,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| ~ m1_filter_0(sK26,k1_lattice2(sK25))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_64 ),
inference(resolution,[],[f60406,f36782]) ).
fof(f60425,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60410,f58057]) ).
fof(f60427,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| v3_struct_0(k1_lattice2(sK25))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60408,f58057]) ).
fof(f60435,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60425,f38844]) ).
fof(f60437,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| ~ v10_lattices(k1_lattice2(sK25))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60427,f38844]) ).
fof(f60443,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60435,f39286]) ).
fof(f60445,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| ~ v17_lattices(k1_lattice2(sK25))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60437,f39286]) ).
fof(f60451,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60443,f39782]) ).
fof(f60453,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| ~ l3_lattices(k1_lattice2(sK25))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60445,f39782]) ).
fof(f60459,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60451,f41384]) ).
fof(f60461,plain,
( sK26 = u1_struct_0(k1_lattice2(sK25))
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60453,f41384]) ).
fof(f60467,plain,
( sK26 = u1_struct_0(sK25)
| ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_demodulation,[],[f60459,f38845]) ).
fof(f60469,plain,
( sK26 = u1_struct_0(sK25)
| m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_demodulation,[],[f60461,f38845]) ).
fof(f60471,plain,
( ~ r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60467,f37459]) ).
fof(f60473,plain,
( m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_subsumption_resolution,[],[f60469,f37459]) ).
fof(f60474,plain,
( m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64 ),
inference(forward_demodulation,[],[f60473,f38845]) ).
fof(f60475,plain,
( r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25
| ~ spl219_53
| spl219_64 ),
inference(backward_subsumption_resolution,[],[f50507,f60474]) ).
fof(f60942,definition,
( spl219_68
<=> r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26) ),
introduced(definition,[new_symbols(definition,[spl219_68])],[avatar_definition]) ).
fof(f60944,plain,
( r2_hidden(k6_filter_2(sK25,sK147(k1_lattice2(sK25),sK26)),sK26)
| ~ spl219_68 ),
inference(avatar_component_clause,[],[f60942]) ).
fof(f60945,plain,
( spl219_68
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25
| ~ spl219_53
| spl219_64 ),
inference(avatar_split_clause,[],[f60475,f60404,f58055,f45611,f45236,f44727,f42094,f37481,f37476,f37471,f37466,f37457,f60942]) ).
fof(f65343,plain,
( r2_hidden(sK147(k1_lattice2(sK25),sK26),sK26)
| ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| ~ spl219_68 ),
inference(superposition,[],[f60944,f35944]) ).
fof(f65344,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| v3_struct_0(sK25)
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(forward_subsumption_resolution,[],[f65343,f60471]) ).
fof(f65374,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| ~ v10_lattices(sK25)
| ~ l3_lattices(sK25)
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(forward_subsumption_resolution,[],[f65344,f37468]) ).
fof(f65401,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| ~ l3_lattices(sK25)
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(forward_subsumption_resolution,[],[f65374,f37483]) ).
fof(f65421,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(k1_lattice2(sK25)))
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(forward_subsumption_resolution,[],[f65401,f37473]) ).
fof(f65434,plain,
( ~ m1_subset_1(sK147(k1_lattice2(sK25),sK26),u1_struct_0(sK25))
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(forward_demodulation,[],[f65421,f38845]) ).
fof(f65435,plain,
( $false
| spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(forward_subsumption_resolution,[],[f65434,f60474]) ).
fof(f65436,plain,
( spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(avatar_contradiction_clause,[],[f65435]) ).
cnf(s1,plain,
( spl219_1
| spl219_2 ),
inference(sat_conversion,[],[f37263]) ).
cnf(s2,plain,
( spl219_1
| ~ spl219_3 ),
inference(sat_conversion,[],[f37460]) ).
cnf(s3,plain,
~ spl219_4,
inference(sat_conversion,[],[f37469]) ).
cnf(s4,plain,
spl219_5,
inference(sat_conversion,[],[f37474]) ).
cnf(s5,plain,
spl219_6,
inference(sat_conversion,[],[f37479]) ).
cnf(s6,plain,
spl219_7,
inference(sat_conversion,[],[f37484]) ).
cnf(s7,plain,
spl219_8,
inference(sat_conversion,[],[f37489]) ).
cnf(s8,plain,
( ~ spl219_1
| spl219_3
| ~ spl219_9 ),
inference(sat_conversion,[],[f40251]) ).
cnf(s9,plain,
( ~ spl219_1
| spl219_3
| ~ spl219_10 ),
inference(sat_conversion,[],[f42092]) ).
cnf(s10,plain,
( spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| ~ spl219_11 ),
inference(sat_conversion,[],[f42097]) ).
cnf(s11,plain,
( ~ spl219_1
| spl219_3
| spl219_12 ),
inference(sat_conversion,[],[f42102]) ).
cnf(s15,plain,
( ~ spl219_1
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_11 ),
inference(sat_conversion,[],[f42446]) ).
cnf(s19,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_20 ),
inference(sat_conversion,[],[f44730]) ).
cnf(s22,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_23 ),
inference(sat_conversion,[],[f45239]) ).
cnf(s24,plain,
( ~ spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_25 ),
inference(sat_conversion,[],[f45613]) ).
cnf(s26,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| ~ spl219_26
| spl219_27 ),
inference(sat_conversion,[],[f49579]) ).
cnf(s27,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_26
| ~ spl219_28 ),
inference(sat_conversion,[],[f49585]) ).
cnf(s28,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| spl219_29 ),
inference(sat_conversion,[],[f49634]) ).
cnf(s41,plain,
( ~ spl219_1
| ~ spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8 ),
inference(sat_conversion,[],[f53984]) ).
cnf(s46,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_11
| spl219_28
| ~ spl219_40 ),
inference(sat_conversion,[],[f56230]) ).
cnf(s59,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_23
| spl219_53 ),
inference(sat_conversion,[],[f58058]) ).
cnf(s67,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_29
| spl219_40 ),
inference(sat_conversion,[],[f58783]) ).
cnf(s68,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| ~ spl219_8
| ~ spl219_27
| spl219_61 ),
inference(sat_conversion,[],[f58797]) ).
cnf(s69,plain,
( spl219_2
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_8
| ~ spl219_61 ),
inference(sat_conversion,[],[f58969]) ).
cnf(s72,plain,
( ~ spl219_2
| spl219_9
| spl219_10
| ~ spl219_12 ),
inference(sat_conversion,[],[f59168]) ).
cnf(s76,plain,
( spl219_4
| ~ spl219_5
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_64 ),
inference(sat_conversion,[],[f60407]) ).
cnf(s80,plain,
( spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| spl219_11
| ~ spl219_20
| ~ spl219_23
| ~ spl219_25
| ~ spl219_53
| spl219_64
| spl219_68 ),
inference(sat_conversion,[],[f60945]) ).
cnf(s99,plain,
( spl219_3
| spl219_4
| ~ spl219_5
| ~ spl219_6
| ~ spl219_7
| ~ spl219_53
| spl219_64
| ~ spl219_68 ),
inference(sat_conversion,[],[f65436]) ).
cnf(s114,plain,
spl219_29,
inference(rat,[],[s28,s4,s7,s6,s3]) ).
cnf(s115,plain,
spl219_23,
inference(rat,[],[s22,s4,s7,s6,s3]) ).
cnf(s117,plain,
spl219_20,
inference(rat,[],[s19,s4,s7,s6,s3]) ).
cnf(s121,plain,
spl219_40,
inference(rat,[],[s67,s3,s4,s6,s114]) ).
cnf(s123,plain,
spl219_53,
inference(rat,[],[s59,s3,s4,s6,s115]) ).
cnf(s137,plain,
spl219_1,
inference(rat,[],[s80,s99,s24,s76,s1,s2,s10,s4,s5,s6,s3,s117,s115,s123,s7]) ).
cnf(s138,plain,
~ spl219_3,
inference(rat,[],[s41,s7,s6,s4,s3,s137]) ).
cnf(s139,plain,
spl219_11,
inference(rat,[],[s15,s3,s7,s6,s4,s137]) ).
cnf(s143,plain,
spl219_12,
inference(rat,[],[s11,s137,s138]) ).
cnf(s144,plain,
~ spl219_10,
inference(rat,[],[s9,s137,s138]) ).
cnf(s145,plain,
~ spl219_9,
inference(rat,[],[s8,s137,s138]) ).
cnf(s146,plain,
spl219_28,
inference(rat,[],[s46,s121,s3,s4,s6,s5,s139]) ).
cnf(s154,plain,
~ spl219_2,
inference(rat,[],[s72,s143,s144,s145]) ).
cnf(s158,plain,
spl219_26,
inference(rat,[],[s27,s3,s4,s7,s6,s146]) ).
cnf(s162,plain,
~ spl219_61,
inference(rat,[],[s69,s3,s7,s6,s5,s4,s154]) ).
cnf(s164,plain,
spl219_27,
inference(rat,[],[s26,s3,s4,s7,s6,s158]) ).
cnf(s165,plain,
$false,
inference(rat,[],[s68,s3,s4,s7,s6,s162,s164]) ).
fof(f65437,plain,
$false,
inference(avatar_sat_refutation,[],[s165]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT321+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.19/0.46 % Computer : n006.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 27 14:36:31 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 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
% 25.00/6.49 % (3048375)Detected formulas, will run a generic FOF schedule.
% 25.00/6.49 % (3048380)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=3468161672:i=141193_2977 on theBenchmark for (2977ds/141193Mi)
% 25.00/6.49 % (3048381)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=796665947:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2977 on theBenchmark for (2977ds/134677Mi)
% 25.00/6.49 % (3048382)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=3497688807:i=141695:sd=1:nm=32:gsp=on:ss=included_2977 on theBenchmark for (2977ds/141695Mi)
% 25.00/6.49 % (3048383)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=44708189:i=109:sd=1:ins=1:gsp=on:ss=axioms_2977 on theBenchmark for (2977ds/109Mi)
% 25.00/6.49 % (3048384)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3117185129:i=119:av=off:ss=axioms_2977 on theBenchmark for (2977ds/119Mi)
% 25.00/6.49 % (3048385)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1979539411:s2a=on:i=139:gtg=position_2977 on theBenchmark for (2977ds/139Mi)
% 25.00/6.49 % (3048386)dis-21_1_sil=8000:lcm=predicate:random_seed=1249692887:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2977 on theBenchmark for (2977ds/129Mi)
% 25.00/6.49 % (3048383)Instruction limit reached!
% 25.00/6.49 % (3048383)------------------------------
% 25.00/6.49 % (3048383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/6.49 % (3048383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/6.49 % (3048383)CaDiCaL version: 2.1.3
% 25.00/6.49 % (3048383)Termination reason: Instruction limit
% 25.00/6.49 % (3048383)Termination phase: SInE selection
% 25.00/6.49 % (3048383)Time elapsed: 0.118 s
% 25.00/6.49 % (3048383)Peak memory usage: 136 MB
% 25.00/6.49 % (3048383)Instructions burned: 109 (million)
% 25.00/6.49 % (3048385)Instruction limit reached!
% 25.00/6.49 % (3048385)------------------------------
% 25.00/6.49 % (3048385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/6.49 % (3048385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/6.49 % (3048385)CaDiCaL version: 2.1.3
% 25.00/6.49 % (3048385)Termination reason: Instruction limit
% 25.00/6.49 % (3048385)Termination phase: Property scanning
% 25.00/6.49 % (3048385)Time elapsed: 0.120 s
% 25.00/6.49 % (3048385)Peak memory usage: 136 MB
% 25.00/6.49 % (3048385)Instructions burned: 139 (million)
% 25.00/6.49 % (3048384)Instruction limit reached!
% 25.00/6.49 % (3048384)------------------------------
% 25.00/6.49 % (3048384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/6.49 % (3048384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/6.49 % (3048384)CaDiCaL version: 2.1.3
% 25.00/6.49 % (3048384)Termination reason: Instruction limit
% 25.00/6.49 % (3048384)Termination phase: SInE selection
% 25.00/6.49 % (3048384)Time elapsed: 0.128 s
% 25.00/6.49 % (3048384)Peak memory usage: 136 MB
% 25.00/6.49 % (3048384)Instructions burned: 120 (million)
% 25.00/6.49 % (3048386)Instruction limit reached!
% 25.00/6.49 % (3048386)------------------------------
% 25.00/6.49 % (3048386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.00/6.49 % (3048386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.00/6.49 % (3048386)CaDiCaL version: 2.1.3
% 25.00/6.49 % (3048386)Termination reason: Instruction limit
% 25.00/6.49 % (3048386)Termination phase: SInE selection
% 25.00/6.49 % (3048386)Time elapsed: 0.136 s
% 25.00/6.49 % (3048386)Peak memory usage: 136 MB
% 25.00/6.49 % (3048386)Instructions burned: 129 (million)
% 25.00/6.49 % (3048394)lrs+10_1_sil=8000:sp=occurrence:random_seed=2383923309:i=285:sd=3:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/285Mi)
% 25.00/6.49 % (3048396)lrs+1011_1_sil=32000:sp=occurrence:random_seed=766307112:i=325:sd=1:ss=axioms:sgt=32_2973 on theBenchmark for (2973ds/325Mi)
% 25.00/6.49 % (3048395)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1541885641:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/157Mi)
% 25.00/6.49 % (3048397)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=2793668494:s2a=on:i=248:s2at=1.23:gtg=position_2973 on theBenchmark for (2973ds/248Mi)
% 25.00/6.49 % (3048395)Instruction limit reached!
% 32.10/7.51 % (3048395)------------------------------
% 32.10/7.51 % (3048395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048395)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048395)Termination reason: Instruction limit
% 32.10/7.51 % (3048395)Termination phase: Property scanning
% 32.10/7.51 % (3048395)Time elapsed: 0.134 s
% 32.10/7.51 % (3048395)Peak memory usage: 136 MB
% 32.10/7.51 % (3048395)Instructions burned: 157 (million)
% 32.10/7.51 % (3048397)Instruction limit reached!
% 32.10/7.51 % (3048397)------------------------------
% 32.10/7.51 % (3048397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048397)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048397)Termination reason: Instruction limit
% 32.10/7.51 % (3048397)Termination phase: Property scanning
% 32.10/7.51 % (3048397)Time elapsed: 0.210 s
% 32.10/7.51 % (3048397)Peak memory usage: 136 MB
% 32.10/7.51 % (3048397)Instructions burned: 248 (million)
% 32.10/7.51 % (3048394)Instruction limit reached!
% 32.10/7.51 % (3048394)------------------------------
% 32.10/7.51 % (3048394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048394)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048394)Termination reason: Instruction limit
% 32.10/7.51 % (3048394)Termination phase: Saturation
% 32.10/7.51 % (3048394)Time elapsed: 0.326 s
% 32.10/7.51 % (3048394)Peak memory usage: 141 MB
% 32.10/7.51 % (3048394)Instructions burned: 286 (million)
% 32.10/7.51 % (3048396)Instruction limit reached!
% 32.10/7.51 % (3048396)------------------------------
% 32.10/7.51 % (3048396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048396)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048396)Termination reason: Instruction limit
% 32.10/7.51 % (3048396)Termination phase: Saturation
% 32.10/7.51 % (3048396)Time elapsed: 0.381 s
% 32.10/7.51 % (3048396)Peak memory usage: 142 MB
% 32.10/7.51 % (3048396)Instructions burned: 325 (million)
% 32.10/7.51 % (3048402)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3421297054:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2969 on theBenchmark for (2969ds/294Mi)
% 32.10/7.51 % (3048403)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4211255700:i=2350_2968 on theBenchmark for (2968ds/2350Mi)
% 32.10/7.51 % (3048404)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=416163286:cts=off:i=113:fsr=off:ss=included:sgt=4_2967 on theBenchmark for (2967ds/113Mi)
% 32.10/7.51 % (3048405)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1470794879:i=127:av=off:fsr=off:sup=off_2967 on theBenchmark for (2967ds/127Mi)
% 32.10/7.51 % (3048402)Instruction limit reached!
% 32.10/7.51 % (3048402)------------------------------
% 32.10/7.51 % (3048402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048402)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048402)Termination reason: Instruction limit
% 32.10/7.51 % (3048402)Termination phase: SInE selection
% 32.10/7.51 % (3048402)Time elapsed: 0.277 s
% 32.10/7.51 % (3048402)Peak memory usage: 137 MB
% 32.10/7.51 % (3048402)Instructions burned: 294 (million)
% 32.10/7.51 % (3048404)Instruction limit reached!
% 32.10/7.51 % (3048404)------------------------------
% 32.10/7.51 % (3048404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048404)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048404)Termination reason: Instruction limit
% 32.10/7.51 % (3048404)Termination phase: SInE selection
% 32.10/7.51 % (3048404)Time elapsed: 0.130 s
% 32.10/7.51 % (3048404)Peak memory usage: 136 MB
% 32.10/7.51 % (3048404)Instructions burned: 113 (million)
% 32.10/7.51 % (3048405)Instruction limit reached!
% 32.10/7.51 % (3048405)------------------------------
% 32.10/7.51 % (3048405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.10/7.51 % (3048405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.10/7.51 % (3048405)CaDiCaL version: 2.1.3
% 32.10/7.51 % (3048405)Termination reason: Instruction limit
% 31.79/8.09 % (3048405)Termination phase: Preprocessing 1
% 31.79/8.09 % (3048405)Time elapsed: 0.168 s
% 31.79/8.09 % (3048405)Peak memory usage: 137 MB
% 31.79/8.09 % (3048405)Instructions burned: 127 (million)
% 31.79/8.09 % (3048411)lrs+10_1_sil=8000:sp=occurrence:random_seed=3495203163:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 31.79/8.09 % (3048410)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1714141329:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2963 on theBenchmark for (2963ds/114Mi)
% 31.79/8.09 % (3048410)Instruction limit reached!
% 31.79/8.09 % (3048410)------------------------------
% 31.79/8.09 % (3048410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048410)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048410)Termination reason: Instruction limit
% 31.79/8.09 % (3048410)Termination phase: Property scanning
% 31.79/8.09 % (3048410)Time elapsed: 0.100 s
% 31.79/8.09 % (3048410)Peak memory usage: 136 MB
% 31.79/8.09 % (3048410)Instructions burned: 116 (million)
% 31.79/8.09 % (3048412)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1569910033:i=437:sd=1:aac=none:ss=included_2962 on theBenchmark for (2962ds/437Mi)
% 31.79/8.09 % (3048415)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1379231973:i=5202:ss=axioms:sgt=16_2960 on theBenchmark for (2960ds/5202Mi)
% 31.79/8.09 % (3048412)Instruction limit reached!
% 31.79/8.09 % (3048412)------------------------------
% 31.79/8.09 % (3048412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048412)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048412)Termination reason: Instruction limit
% 31.79/8.09 % (3048412)Termination phase: Saturation
% 31.79/8.09 % (3048412)Time elapsed: 0.470 s
% 31.79/8.09 % (3048412)Peak memory usage: 144 MB
% 31.79/8.09 % (3048412)Instructions burned: 437 (million)
% 31.79/8.09 % (3048411)Instruction limit reached!
% 31.79/8.09 % (3048411)------------------------------
% 31.79/8.09 % (3048411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048411)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048411)Termination reason: Instruction limit
% 31.79/8.09 % (3048411)Termination phase: Property scanning
% 31.79/8.09 % (3048411)Time elapsed: 0.890 s
% 31.79/8.09 % (3048411)Peak memory usage: 158 MB
% 31.79/8.09 % (3048411)Instructions burned: 907 (million)
% 31.79/8.09 % (3048418)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1785978434:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2954 on theBenchmark for (2954ds/134Mi)
% 31.79/8.09 % (3048418)Instruction limit reached!
% 31.79/8.09 % (3048418)------------------------------
% 31.79/8.09 % (3048418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048418)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048418)Termination reason: Instruction limit
% 31.79/8.09 % (3048418)Termination phase: SInE selection
% 31.79/8.09 % (3048418)Time elapsed: 0.085 s
% 31.79/8.09 % (3048418)Peak memory usage: 136 MB
% 31.79/8.09 % (3048418)Instructions burned: 134 (million)
% 31.79/8.09 % (3048419)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4121284150:st=8:i=592:sd=3:ep=RST:ss=axioms_2952 on theBenchmark for (2952ds/592Mi)
% 31.79/8.09 % (3048421)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=285713576:st=3:i=13193:sd=3:ss=axioms_2951 on theBenchmark for (2951ds/13193Mi)
% 31.79/8.09 % (3048403)Instruction limit reached!
% 31.79/8.09 % (3048403)------------------------------
% 31.79/8.09 % (3048403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048403)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048403)Termination reason: Instruction limit
% 31.79/8.09 % (3048403)Termination phase: Property scanning
% 31.79/8.09 % (3048403)Time elapsed: 1.858 s
% 31.79/8.09 % (3048403)Peak memory usage: 232 MB
% 31.79/8.09 % (3048403)Instructions burned: 2352 (million)
% 31.79/8.09 % (3048424)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=3493280401:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2946 on theBenchmark for (2946ds/125Mi)
% 31.79/8.09 % (3048424)Instruction limit reached!
% 31.79/8.09 % (3048424)------------------------------
% 31.79/8.09 % (3048424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048424)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048424)Termination reason: Instruction limit
% 31.79/8.09 % (3048424)Termination phase: Property scanning
% 31.79/8.09 % (3048424)Time elapsed: 0.032 s
% 31.79/8.09 % (3048424)Peak memory usage: 136 MB
% 31.79/8.09 % (3048424)Instructions burned: 130 (million)
% 31.79/8.09 % (3048426)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1222975244:i=134:gtgl=5:slsql=off:gtg=exists_sym_2945 on theBenchmark for (2945ds/134Mi)
% 31.79/8.09 % (3048426)Instruction limit reached!
% 31.79/8.09 % (3048426)------------------------------
% 31.79/8.09 % (3048426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048426)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048426)Termination reason: Instruction limit
% 31.79/8.09 % (3048426)Termination phase: Property scanning
% 31.79/8.09 % (3048426)Time elapsed: 0.034 s
% 31.79/8.09 % (3048426)Peak memory usage: 136 MB
% 31.79/8.09 % (3048426)Instructions burned: 138 (million)
% 31.79/8.09 % (3048419)Instruction limit reached!
% 31.79/8.09 % (3048419)------------------------------
% 31.79/8.09 % (3048419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048419)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048419)Termination reason: Instruction limit
% 31.79/8.09 % (3048419)Termination phase: Naming
% 31.79/8.09 % (3048419)Time elapsed: 0.650 s
% 31.79/8.09 % (3048419)Peak memory usage: 154 MB
% 31.79/8.09 % (3048419)Instructions burned: 596 (million)
% 31.79/8.09 % (3048429)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1151687344:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2943 on theBenchmark for (2943ds/431Mi)
% 31.79/8.09 % (3048428)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1228237691:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2943 on theBenchmark for (2943ds/141Mi)
% 31.79/8.09 % (3048428)Instruction limit reached!
% 31.79/8.09 % (3048428)------------------------------
% 31.79/8.09 % (3048428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048428)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048428)Termination reason: Instruction limit
% 31.79/8.09 % (3048428)Termination phase: SInE selection
% 31.79/8.09 % (3048428)Time elapsed: 0.154 s
% 31.79/8.09 % (3048428)Peak memory usage: 136 MB
% 31.79/8.09 % (3048428)Instructions burned: 141 (million)
% 31.79/8.09 % (3048429)Instruction limit reached!
% 31.79/8.09 % (3048429)------------------------------
% 31.79/8.09 % (3048429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048429)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048429)Termination reason: Instruction limit
% 31.79/8.09 % (3048429)Termination phase: Saturation
% 31.79/8.09 % (3048429)Time elapsed: 0.316 s
% 31.79/8.09 % (3048429)Peak memory usage: 144 MB
% 31.79/8.09 % (3048429)Instructions burned: 433 (million)
% 31.79/8.09 % (3048432)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=3504277919:i=6060:aac=none:ins=25_2939 on theBenchmark for (2939ds/6060Mi)
% 31.79/8.09 % (3048433)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=1162395291:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2938 on theBenchmark for (2938ds/150Mi)
% 31.79/8.09 % (3048433)Instruction limit reached!
% 31.79/8.09 % (3048433)------------------------------
% 31.79/8.09 % (3048433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.79/8.09 % (3048433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.79/8.09 % (3048433)CaDiCaL version: 2.1.3
% 31.79/8.09 % (3048433)Termination reason: Instruction limit
% 31.79/8.09 % (3048433)Termination phase: SInE selection
% 31.79/8.09 % (3048433)Time elapsed: 0.119 s
% 31.79/8.09 % (3048433)Peak memory usage: 136 MB
% 31.79/8.09 % (3048433)Instructions burned: 150 (million)
% 31.79/8.09 % (3048436)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2387114925:i=14155:bd=all_2935 on theBenchmark for (2935ds/14155Mi)
% 31.79/8.09 % (3048382)First to succeed.
% 31.79/8.09 % (3048382)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3048375"
% 31.79/8.09 % (3048382)Refutation found. Thanks to Tanya!
% 31.79/8.09 % SZS status Theorem for theBenchmark
% 31.79/8.09 % SZS output start Proof for theBenchmark
% See solution above
% 37.12/8.34 % (3048382)------------------------------
% 37.12/8.34 % (3048382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.12/8.34 % (3048382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.12/8.34 % (3048382)CaDiCaL version: 2.1.3
% 37.12/8.34 % (3048382)Termination reason: Refutation
% 37.12/8.34 % (3048382)Time elapsed: 4.350 s
% 37.12/8.34 % (3048382)Peak memory usage: 223 MB
% 37.12/8.34 % (3048382)Instructions burned: 6416 (million)
% 37.12/8.34 % (3048382)------------------------------
% 37.12/8.34 % (3048382)------------------------------
% 37.12/8.34 % (3048375)Success in time 7.047 s
% 37.12/8.34 % Vampire exiting
%------------------------------------------------------------------------------