%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP648+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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 10:18:24 AM UTC 2026
% Result : Theorem 39.40s 8.71s
% Output : Refutation 39.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 82
% Syntax : Number of formulae : 725 ( 81 unt; 42 def)
% Number of atoms : 3353 ( 253 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 4230 (1602 ~;2197 |; 280 &)
% ( 67 <=>; 82 =>; 0 <=; 2 <~>)
% Maximal formula depth : 22 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 77 ( 75 usr; 43 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-6 aty)
% Number of variables : 779 ( 1 sgn 768 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
=> ( ( X3 = X1
& X4 = X2 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> m1_group_6(X1,X0,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t31_latsubgr) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
=> ( ( X3 = X1
& X4 = X2 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> m1_group_6(X1,X0,X2) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0] :
( l1_group_1(X0)
=> ( v1_group_1(X0)
=> X0 = g1_group_1(u1_struct_0(X0),u1_group_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v1_group_1) ).
fof(f4,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(X0)
=> X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k4_lattices) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0)
& m1_group_2(X2,X0) )
=> k9_group_2(X0,X1,X2) = k9_group_2(X0,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k9_group_2) ).
fof(f12,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
=> ( X1 = k10_group_4(X0)
<=> ! [X2] :
( m1_subset_1(X2,k1_group_3(X0))
=> ! [X3] :
( m1_subset_1(X3,k1_group_3(X0))
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ( ( X2 = X4
& X3 = X5 )
=> k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X2,X3) = k9_group_2(X0,X4,X5) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_group_4) ).
fof(f13,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> k11_group_4(X0) = g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_group_4) ).
fof(f14,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_lattices) ).
fof(f15,axiom,
! [X0,X1] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0) )
=> ( v1_group_1(g1_group_1(X0,X1))
& l1_group_1(g1_group_1(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_g1_group_1) ).
fof(f16,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_g3_lattices) ).
fof(f17,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k10_group_4(X0))
& v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k10_group_4) ).
fof(f18,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_group_4) ).
fof(f23,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
& m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
& m1_subset_1(X4,X0)
& m1_subset_1(X5,X1) )
=> m1_subset_1(k2_binop_1(X0,X1,X2,X3,X4,X5),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_binop_1) ).
fof(f28,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0)
& m1_group_2(X2,X0) )
=> ( v1_group_1(k9_group_2(X0,X1,X2))
& m1_group_2(k9_group_2(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_group_2) ).
fof(f29,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( v1_funct_1(k9_group_4(X0))
& v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k9_group_4) ).
fof(f33,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f34,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f35,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f40,axiom,
! [X0] :
( l1_group_1(X0)
=> ( v1_funct_1(u1_group_1(X0))
& v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_group_1) ).
fof(f41,axiom,
! [X0] :
( l1_lattices(X0)
=> ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(f52,axiom,
! [X0] :
? [X1] : m1_subset_1(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f54,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ~ v1_xboole_0(k1_group_3(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_group_3) ).
fof(f55,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0))
& v14_lattices(k11_group_4(X0))
& v15_lattices(k11_group_4(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_group_4) ).
fof(f56,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f61,axiom,
! [X0,X1,X2] :
( ( v1_funct_1(X1)
& v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
& m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X0 = X3
& X1 = X4
& X2 = X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f71,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& l1_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
fof(f73,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& m1_group_2(X1,X0) )
=> ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_group_6) ).
fof(f74,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f75,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0)
& v1_group_1(X1)
& m1_group_2(X1,X0)
& v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
fof(f76,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f78,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f79,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> r3_lattices(X0,X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r3_lattices) ).
fof(f81,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
=> ( m1_group_2(X2,X1)
<=> r1_group_2(X0,k9_group_2(X0,X2,X1),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t107_group_2) ).
fof(f83,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r1_lattices(X0,X1,X2)
<=> k2_lattices(X0,X1,X2) = X1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_lattices) ).
fof(f84,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
=> ! [X2] :
( m1_group_2(X2,X0)
=> ( X1 = X2
=> ( v1_group_1(X2)
& m1_group_2(X2,X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t29_latsubgr) ).
fof(f85,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f86,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
=> ( ( X3 = X1
& X4 = X2 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_latsubgr) ).
fof(f87,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f88,axiom,
! [X0,X1,X2] :
( ( r2_hidden(X0,X1)
& m1_subset_1(X1,k1_zfmisc_1(X2)) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f90,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( m1_group_2(X2,X0)
=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
=> m1_group_2(X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t66_group_2) ).
fof(f94,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f78]) ).
fof(f95,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0))
& v14_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f55]) ).
fof(f96,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f95]) ).
fof(f97,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f97]) ).
fof(f99,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f98]) ).
fof(f100,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f99]) ).
fof(f101,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f18]) ).
fof(f102,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) )
=> ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f100]) ).
fof(f106,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<~> m1_group_6(X1,X0,X2) )
& X3 = X1
& X4 = X2
& m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
& m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
& m1_group_2(X2,X0) )
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f107,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ? [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<~> m1_group_6(X1,X0,X2) )
& X3 = X1
& X4 = X2
& m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
& m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
& m1_group_2(X2,X0) )
& m1_group_2(X1,X0) )
& ~ v3_struct_0(X0)
& v3_group_1(X0)
& v4_group_1(X0)
& l1_group_1(X0) ),
inference(flattening,[],[f106]) ).
fof(f108,plain,
! [X0] :
( X0 = g1_group_1(u1_struct_0(X0),u1_group_1(X0))
| ~ v1_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f109,plain,
! [X0] :
( X0 = g1_group_1(u1_struct_0(X0),u1_group_1(X0))
| ~ v1_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f108]) ).
fof(f110,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f111,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f110]) ).
fof(f119,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f10]) ).
fof(f120,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f119]) ).
fof(f121,plain,
! [X0,X1,X2] :
( k9_group_2(X0,X1,X2) = k9_group_2(X0,X2,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f122,plain,
! [X0,X1,X2] :
( k9_group_2(X0,X1,X2) = k9_group_2(X0,X2,X1)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0) ),
inference(flattening,[],[f121]) ).
fof(f123,plain,
! [X0] :
( ! [X1] :
( ( X1 = k10_group_4(X0)
<=> ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X2,X3) = k9_group_2(X0,X4,X5)
| X2 != X4
| X3 != X5
| ~ m1_group_2(X5,X0) )
| ~ m1_group_2(X4,X0) )
| ~ m1_subset_1(X3,k1_group_3(X0)) )
| ~ m1_subset_1(X2,k1_group_3(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f124,plain,
! [X0] :
( ! [X1] :
( ( X1 = k10_group_4(X0)
<=> ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X2,X3) = k9_group_2(X0,X4,X5)
| X2 != X4
| X3 != X5
| ~ m1_group_2(X5,X0) )
| ~ m1_group_2(X4,X0) )
| ~ m1_subset_1(X3,k1_group_3(X0)) )
| ~ m1_subset_1(X2,k1_group_3(X0)) ) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f123]) ).
fof(f125,plain,
! [X0] :
( k11_group_4(X0) = g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f126,plain,
! [X0] :
( k11_group_4(X0) = g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f125]) ).
fof(f127,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f128,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( ( v1_group_1(g1_group_1(X0,X1))
& l1_group_1(g1_group_1(X0,X1)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f130,plain,
! [X0,X1] :
( ( v1_group_1(g1_group_1(X0,X1))
& l1_group_1(g1_group_1(X0,X1)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f129]) ).
fof(f131,plain,
! [X0,X1,X2] :
( ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f132,plain,
! [X0,X1,X2] :
( ( v3_lattices(g3_lattices(X0,X1,X2))
& l3_lattices(g3_lattices(X0,X1,X2)) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f131]) ).
fof(f133,plain,
! [X0] :
( ( v1_funct_1(k10_group_4(X0))
& v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f134,plain,
! [X0] :
( ( v1_funct_1(k10_group_4(X0))
& v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f133]) ).
fof(f135,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f101]) ).
fof(f136,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& l3_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
! [X0,X1,X2,X3,X4,X5] :
( m1_subset_1(k2_binop_1(X0,X1,X2,X3,X4,X5),X2)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f138,plain,
! [X0,X1,X2,X3,X4,X5] :
( m1_subset_1(k2_binop_1(X0,X1,X2,X3,X4,X5),X2)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ m1_subset_1(X4,X0)
| ~ m1_subset_1(X5,X1) ),
inference(flattening,[],[f137]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ( v1_group_1(k9_group_2(X0,X1,X2))
& m1_group_2(k9_group_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ( v1_group_1(k9_group_2(X0,X1,X2))
& m1_group_2(k9_group_2(X0,X1,X2),X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0) ),
inference(flattening,[],[f145]) ).
fof(f147,plain,
! [X0] :
( ( v1_funct_1(k9_group_4(X0))
& v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f148,plain,
! [X0] :
( ( v1_funct_1(k9_group_4(X0))
& v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& m2_relset_1(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f147]) ).
fof(f151,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f152,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f153,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f154,plain,
! [X0] :
( ! [X1] :
( ( ~ v3_struct_0(X1)
& v3_group_1(X1)
& l1_group_1(X1) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f153]) ).
fof(f158,plain,
! [X0] :
( ( v1_funct_1(u1_group_1(X0))
& v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f40]) ).
fof(f159,plain,
! [X0] :
( ( v1_funct_1(u1_lattices(X0))
& v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) )
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f41]) ).
fof(f165,plain,
! [X0] :
( ~ v1_xboole_0(k1_group_3(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f54]) ).
fof(f166,plain,
! [X0] :
( ~ v1_xboole_0(k1_group_3(X0))
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f165]) ).
fof(f167,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f102]) ).
fof(f168,plain,
! [X0] :
( ( ~ v3_struct_0(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0)) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f167]) ).
fof(f169,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f170,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f169]) ).
fof(f175,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f176,plain,
! [X0,X1,X2] :
( ! [X3,X4,X5] :
( ( X0 = X3
& X1 = X4
& X2 = X5 )
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) )
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(flattening,[],[f175]) ).
fof(f182,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f71]) ).
fof(f183,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ l1_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f182]) ).
fof(f186,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f73]) ).
fof(f187,plain,
! [X0,X1] :
( ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(flattening,[],[f186]) ).
fof(f188,plain,
! [X0,X1,X2] :
( ( r1_group_2(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(ennf_transformation,[],[f75]) ).
fof(f189,plain,
! [X0,X1,X2] :
( ( r1_group_2(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) ),
inference(flattening,[],[f188]) ).
fof(f190,plain,
! [X0,X1,X2] :
( ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f76]) ).
fof(f191,plain,
! [X0,X1,X2] :
( ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f190]) ).
fof(f194,plain,
! [X0,X1,X2] :
( r3_lattices(X0,X1,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f79]) ).
fof(f195,plain,
! [X0,X1,X2] :
( r3_lattices(X0,X1,X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f194]) ).
fof(f198,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( m1_group_2(X2,X1)
<=> r1_group_2(X0,k9_group_2(X0,X2,X1),X2) )
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f199,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( m1_group_2(X2,X1)
<=> r1_group_2(X0,k9_group_2(X0,X2,X1),X2) )
| ~ v1_group_1(X2)
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f198]) ).
fof(f201,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_lattices(X0,X1,X2)
<=> k2_lattices(X0,X1,X2) = X1 )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f202,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r1_lattices(X0,X1,X2)
<=> k2_lattices(X0,X1,X2) = X1 )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f201]) ).
fof(f203,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| X1 != X2
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f204,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( v1_group_1(X2)
& m1_group_2(X2,X0) )
| X1 != X2
| ~ m1_group_2(X2,X0) )
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0))) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f203]) ).
fof(f205,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f85]) ).
fof(f206,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f86]) ).
fof(f208,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) )
| X1 != X3
| X2 != X4
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0))) )
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0))) )
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f207]) ).
fof(f209,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(ennf_transformation,[],[f88]) ).
fof(f210,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(flattening,[],[f209]) ).
fof(f212,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(ennf_transformation,[],[f90]) ).
fof(f213,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_group_2(X1,X2)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ m1_group_2(X2,X0) )
| ~ m1_group_2(X1,X0) )
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0) ),
inference(flattening,[],[f212]) ).
fof(f217,plain,
( m1_group_6(sK1,sK0,sK2)
| r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(cnf_transformation,[],[f107]) ).
fof(f218,plain,
( ~ m1_group_6(sK1,sK0,sK2)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(cnf_transformation,[],[f107]) ).
fof(f219,plain,
m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0))),
inference(cnf_transformation,[],[f107]) ).
fof(f220,plain,
sK2 = sK4,
inference(cnf_transformation,[],[f107]) ).
fof(f221,plain,
sK1 = sK3,
inference(cnf_transformation,[],[f107]) ).
fof(f222,plain,
m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0))),
inference(cnf_transformation,[],[f107]) ).
fof(f223,plain,
m1_group_2(sK2,sK0),
inference(cnf_transformation,[],[f107]) ).
fof(f224,plain,
m1_group_2(sK1,sK0),
inference(cnf_transformation,[],[f107]) ).
fof(f225,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f107]) ).
fof(f226,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f107]) ).
fof(f227,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f107]) ).
fof(f228,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f107]) ).
fof(f229,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v1_group_1(X0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0 ),
inference(cnf_transformation,[],[f109]) ).
fof(f230,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(cnf_transformation,[],[f111]) ).
fof(f236,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k9_group_2(X0,X1,X2) = k9_group_2(X0,X2,X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f242,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_1(X1)
| ~ m1_subset_1(X2,k1_group_3(X0))
| ~ m1_subset_1(X3,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| X3 != X5
| X2 != X4
| k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X2,X3) = k9_group_2(X0,X4,X5)
| k10_group_4(X0) != X1 ),
inference(cnf_transformation,[],[f124]) ).
fof(f246,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k11_group_4(X0) = g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0)) ),
inference(cnf_transformation,[],[f126]) ).
fof(f247,plain,
! [X2,X0,X1] :
( ~ l1_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2) ),
inference(cnf_transformation,[],[f128]) ).
fof(f249,plain,
! [X0,X1] :
( ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| v1_group_1(g1_group_1(X0,X1)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f250,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| l3_lattices(g3_lattices(X0,X1,X2)) ),
inference(cnf_transformation,[],[f132]) ).
fof(f252,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f253,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f254,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_funct_1(k10_group_4(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f255,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l3_lattices(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f136]) ).
fof(f256,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v3_lattices(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f136]) ).
fof(f257,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f136]) ).
fof(f258,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_subset_1(X5,X1)
| ~ m1_subset_1(X4,X0)
| ~ m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| v1_xboole_0(X0)
| m1_subset_1(k2_binop_1(X0,X1,X2,X3,X4,X5),X2) ),
inference(cnf_transformation,[],[f138]) ).
fof(f263,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(k9_group_2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f264,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_group_1(k9_group_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f146]) ).
fof(f265,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m2_relset_1(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f266,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f267,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_funct_1(k9_group_4(X0)) ),
inference(cnf_transformation,[],[f148]) ).
fof(f270,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f271,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f272,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f273,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| l1_group_1(X1) ),
inference(cnf_transformation,[],[f154]) ).
fof(f278,plain,
! [X0] :
( ~ l1_group_1(X0)
| m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f158]) ).
fof(f279,plain,
! [X0] :
( ~ l1_group_1(X0)
| v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f158]) ).
fof(f280,plain,
! [X0] :
( ~ l1_group_1(X0)
| v1_funct_1(u1_group_1(X0)) ),
inference(cnf_transformation,[],[f158]) ).
fof(f283,plain,
! [X0] :
( ~ l1_lattices(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f295,plain,
! [X0] : m1_subset_1(sK17(X0),X0),
inference(cnf_transformation,[],[f52]) ).
fof(f297,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k1_group_3(X0)) ),
inference(cnf_transformation,[],[f166]) ).
fof(f298,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v9_lattices(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f299,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v8_lattices(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f300,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v6_lattices(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f303,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f170]) ).
fof(f309,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X2 = X5 ),
inference(cnf_transformation,[],[f176]) ).
fof(f311,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| X0 = X3 ),
inference(cnf_transformation,[],[f176]) ).
fof(f328,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f183]) ).
fof(f330,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X1)
| m1_group_6(X2,X0,X1) ),
inference(cnf_transformation,[],[f187]) ).
fof(f331,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(X2,X1)
| ~ m1_group_6(X2,X0,X1) ),
inference(cnf_transformation,[],[f187]) ).
fof(f333,plain,
! [X2,X0,X1] :
( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f74]) ).
fof(f335,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| X1 = X2
| ~ r1_group_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f189]) ).
fof(f336,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| ~ r1_lattices(X0,X1,X2)
| r3_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f191]) ).
fof(f337,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| r1_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f191]) ).
fof(f339,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f94]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| r3_lattices(X0,X1,X1) ),
inference(cnf_transformation,[],[f195]) ).
fof(f343,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| r1_group_2(X0,k9_group_2(X0,X2,X1),X2)
| ~ m1_group_2(X2,X1) ),
inference(cnf_transformation,[],[f199]) ).
fof(f345,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k2_lattices(X0,X1,X2) != X1
| r1_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f202]) ).
fof(f346,plain,
! [X2,X0,X1] :
( ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k2_lattices(X0,X1,X2) = X1
| ~ r1_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f202]) ).
fof(f347,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| X1 != X2
| v1_group_1(X2) ),
inference(cnf_transformation,[],[f204]) ).
fof(f348,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f206]) ).
fof(f350,plain,
! [X2,X3,X0,X1,X4] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| X2 != X4
| X1 != X3
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ r3_lattices(k11_group_4(X0),X3,X4) ),
inference(cnf_transformation,[],[f208]) ).
fof(f351,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f353,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f210]) ).
fof(f355,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| m1_group_2(X1,X2) ),
inference(cnf_transformation,[],[f213]) ).
fof(f359,plain,
m1_group_2(sK3,sK0),
inference(definition_unfolding,[],[f224,f221]) ).
fof(f360,plain,
m1_group_2(sK4,sK0),
inference(definition_unfolding,[],[f223,f220]) ).
fof(f361,plain,
( ~ m1_group_6(sK3,sK0,sK4)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(definition_unfolding,[],[f218,f221,f220]) ).
fof(f362,plain,
( m1_group_6(sK3,sK0,sK4)
| r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(definition_unfolding,[],[f217,f221,f220]) ).
fof(f363,plain,
! [X2,X0,X1,X4,X5] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_1(X1)
| ~ m1_subset_1(X2,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| X2 != X4
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X2,X5)
| k10_group_4(X0) != X1 ),
inference(equality_resolution,[],[f242]) ).
fof(f364,plain,
! [X0,X1,X4,X5] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_2(X1,k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_1(X1)
| ~ m1_subset_1(X4,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X4,X5)
| k10_group_4(X0) != X1 ),
inference(equality_resolution,[],[f363]) ).
fof(f365,plain,
! [X0,X4,X5] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_1(k10_group_4(X0))
| ~ m1_subset_1(X4,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X4,X5) ),
inference(equality_resolution,[],[f364]) ).
fof(f367,plain,
! [X2,X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| v1_group_1(X2) ),
inference(equality_resolution,[],[f347]) ).
fof(f368,plain,
! [X3,X0,X1,X4] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X4,X0)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| X1 != X3
| r1_tarski(u1_struct_0(X1),u1_struct_0(X4))
| ~ r3_lattices(k11_group_4(X0),X3,X4) ),
inference(equality_resolution,[],[f350]) ).
fof(f369,plain,
! [X3,X0,X4] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X3,X0)
| ~ m1_group_2(X4,X0)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| r1_tarski(u1_struct_0(X3),u1_struct_0(X4))
| ~ r3_lattices(k11_group_4(X0),X3,X4) ),
inference(equality_resolution,[],[f368]) ).
fof(f372,plain,
~ l1_group_1(sK0),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f373,plain,
( ~ m1_group_6(sK3,sK0,sK4)
| r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(consistent_polarity_flipping,[],[f361]) ).
fof(f374,plain,
( m1_group_6(sK3,sK0,sK4)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(consistent_polarity_flipping,[],[f362]) ).
fof(f375,plain,
! [X0] :
( v1_group_1(X0)
| l1_group_1(X0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f376,plain,
! [X0] :
( ~ v3_lattices(X0)
| l3_lattices(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f382,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| l1_lattices(X0)
| v6_lattices(X0)
| v3_struct_0(X0)
| k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1) ),
inference(consistent_polarity_flipping,[],[f236]) ).
fof(f383,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| l1_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k9_group_2(X0,X1,X2) = k9_group_2(X0,X2,X1) ),
inference(consistent_polarity_flipping,[],[f237]) ).
fof(f387,plain,
! [X0,X4,X5] :
( l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_1(k10_group_4(X0))
| ~ m1_subset_1(X4,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X4,X5) ),
inference(consistent_polarity_flipping,[],[f365]) ).
fof(f392,plain,
! [X0] :
( ~ v4_group_1(X0)
| l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| k11_group_4(X0) = g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0)) ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f393,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| l1_lattices(X0)
| k2_lattices(X0,X1,X2) = k2_binop_1(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),u1_lattices(X0),X1,X2) ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f394,plain,
! [X0,X1] :
( ~ v1_group_1(g1_group_1(X0,X1))
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0) ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f397,plain,
! [X2,X0,X1] :
( ~ l3_lattices(g3_lattices(X0,X1,X2))
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0) ),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f398,plain,
! [X0] :
( v1_funct_1(k10_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f254]) ).
fof(f399,plain,
! [X0] :
( v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f253]) ).
fof(f400,plain,
! [X0] :
( m2_relset_1(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f252]) ).
fof(f401,plain,
! [X0] :
( ~ v3_struct_0(k11_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f257]) ).
fof(f402,plain,
! [X0] :
( v3_lattices(k11_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f256]) ).
fof(f403,plain,
! [X0] :
( ~ l3_lattices(k11_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f404,plain,
! [X2,X3,X0,X1,X4,X5] :
( m1_subset_1(k2_binop_1(X0,X1,X2,X3,X4,X5),X2)
| ~ m1_subset_1(X4,X0)
| m1_relset_1(X3,k2_zfmisc_1(X0,X1),X2)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X1),X2)
| ~ v1_funct_1(X3)
| ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X0)
| ~ m1_subset_1(X5,X1) ),
inference(consistent_polarity_flipping,[],[f258]) ).
fof(f409,plain,
! [X2,X0,X1] :
( ~ v1_group_1(k9_group_2(X0,X1,X2))
| ~ m1_group_2(X1,X0)
| l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X0) ),
inference(consistent_polarity_flipping,[],[f264]) ).
fof(f410,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_group_2(X1,X0)
| l1_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(k9_group_2(X0,X1,X2),X0) ),
inference(consistent_polarity_flipping,[],[f263]) ).
fof(f411,plain,
! [X0] :
( v1_funct_1(k9_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f267]) ).
fof(f412,plain,
! [X0] :
( v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f413,plain,
! [X0] :
( m2_relset_1(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f265]) ).
fof(f416,plain,
! [X0] :
( ~ l1_struct_0(X0)
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f270]) ).
fof(f417,plain,
! [X0] :
( ~ l1_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f418,plain,
! [X0] :
( ~ l2_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f271]) ).
fof(f421,plain,
! [X0,X1] :
( ~ l1_group_1(X1)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f273]) ).
fof(f423,plain,
! [X0] :
( v1_funct_1(u1_group_1(X0))
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f280]) ).
fof(f424,plain,
! [X0] :
( v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f279]) ).
fof(f425,plain,
! [X0] :
( m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f278]) ).
fof(f426,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| l1_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f283]) ).
fof(f440,plain,
! [X0] :
( v1_xboole_0(k1_group_3(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f297]) ).
fof(f443,plain,
! [X0] :
( ~ v6_lattices(k11_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f444,plain,
! [X0] :
( v8_lattices(k11_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f299]) ).
fof(f445,plain,
! [X0] :
( ~ v9_lattices(k11_group_4(X0))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f298]) ).
fof(f446,plain,
! [X0] :
( v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| l1_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f452,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| X0 = X3 ),
inference(consistent_polarity_flipping,[],[f311]) ).
fof(f454,plain,
! [X2,X3,X0,X1,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| X2 = X5 ),
inference(consistent_polarity_flipping,[],[f309]) ).
fof(f466,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| l1_lattices(X0)
| v6_lattices(X0)
| v3_struct_0(X0)
| k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f328]) ).
fof(f468,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(X2,X1)
| ~ m1_group_6(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f331]) ).
fof(f469,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| l1_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X2,X1)
| m1_group_6(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f330]) ).
fof(f470,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ),
inference(consistent_polarity_flipping,[],[f333]) ).
fof(f472,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| v1_group_1(X2)
| ~ m1_group_2(X1,X0)
| v1_group_1(X1)
| l1_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| X1 = X2
| ~ r1_group_2(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f335]) ).
fof(f474,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| l3_lattices(X0)
| v9_lattices(X0)
| ~ v8_lattices(X0)
| v6_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r3_lattices(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f475,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| l3_lattices(X0)
| v9_lattices(X0)
| ~ v8_lattices(X0)
| v6_lattices(X0)
| v3_struct_0(X0)
| ~ r1_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f336]) ).
fof(f477,plain,
! [X0] : ~ r1_tarski(X0,X0),
inference(consistent_polarity_flipping,[],[f339]) ).
fof(f478,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| l3_lattices(X0)
| v9_lattices(X0)
| ~ v8_lattices(X0)
| v6_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(consistent_polarity_flipping,[],[f340]) ).
fof(f480,plain,
! [X2,X0,X1] :
( r1_group_2(X0,k9_group_2(X0,X2,X1),X2)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0)
| v1_group_1(X2)
| l1_group_1(X0)
| ~ m1_group_2(X2,X1) ),
inference(consistent_polarity_flipping,[],[f343]) ).
fof(f483,plain,
! [X2,X0,X1] :
( ~ v8_lattices(X0)
| v9_lattices(X0)
| l3_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| k2_lattices(X0,X1,X2) = X1
| ~ r1_lattices(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f484,plain,
! [X2,X0,X1] :
( k2_lattices(X0,X1,X2) != X1
| v9_lattices(X0)
| ~ v8_lattices(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| l3_lattices(X0)
| r1_lattices(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f345]) ).
fof(f485,plain,
! [X2,X0] :
( ~ v1_group_1(X2)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X2,X0)
| l1_group_1(X0) ),
inference(consistent_polarity_flipping,[],[f367]) ).
fof(f486,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(consistent_polarity_flipping,[],[f348]) ).
fof(f487,plain,
! [X3,X0,X4] :
( ~ r1_tarski(u1_struct_0(X3),u1_struct_0(X4))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X3,X0)
| ~ m1_group_2(X4,X0)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X0)))
| l1_group_1(X0)
| r3_lattices(k11_group_4(X0),X3,X4) ),
inference(consistent_polarity_flipping,[],[f369]) ).
fof(f490,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f491,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f493,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| m1_group_2(X1,X2) ),
inference(consistent_polarity_flipping,[],[f355]) ).
fof(f499,definition,
( spl27_1
<=> r3_lattices(k11_group_4(sK0),sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl27_1])],[avatar_definition]) ).
fof(f500,plain,
( r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_1 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f501,plain,
( ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| spl27_1 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f503,definition,
( spl27_2
<=> m1_group_6(sK3,sK0,sK4) ),
introduced(definition,[new_symbols(definition,[spl27_2])],[avatar_definition]) ).
fof(f504,plain,
( ~ m1_group_6(sK3,sK0,sK4)
| spl27_2 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f505,plain,
( m1_group_6(sK3,sK0,sK4)
| ~ spl27_2 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f506,plain,
( ~ spl27_1
| spl27_2 ),
inference(avatar_split_clause,[],[f374,f503,f499]) ).
fof(f507,plain,
( spl27_1
| ~ spl27_2 ),
inference(avatar_split_clause,[],[f373,f503,f499]) ).
fof(f550,plain,
! [X2,X0,X1] :
( r2_hidden(X0,X1)
| m1_subset_1(X0,X2)
| r1_tarski(X1,X2) ),
inference(resolution,[],[f491,f490]) ).
fof(f581,definition,
( spl27_7
<=> l1_group_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_7])],[avatar_definition]) ).
fof(f582,plain,
( ~ l1_group_1(sK3)
| spl27_7 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( l1_group_1(sK3)
| ~ spl27_7 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f619,plain,
! [X0] :
( l3_lattices(k11_group_4(X0))
| k11_group_4(X0) = g3_lattices(u1_struct_0(k11_group_4(X0)),u2_lattices(k11_group_4(X0)),u1_lattices(k11_group_4(X0)))
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(resolution,[],[f376,f402]) ).
fof(f620,plain,
! [X0] :
( ~ v4_group_1(X0)
| k11_group_4(X0) = g3_lattices(u1_struct_0(k11_group_4(X0)),u2_lattices(k11_group_4(X0)),u1_lattices(k11_group_4(X0)))
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f619,f403]) ).
fof(f640,plain,
( l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k11_group_4(sK0) = g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)) ),
inference(resolution,[],[f392,f226]) ).
fof(f641,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k11_group_4(sK0) = g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)) ),
inference(forward_subsumption_resolution,[],[f640,f372]) ).
fof(f642,plain,
( v3_struct_0(sK0)
| k11_group_4(sK0) = g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)) ),
inference(forward_subsumption_resolution,[],[f641,f227]) ).
fof(f643,plain,
k11_group_4(sK0) = g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)),
inference(forward_subsumption_resolution,[],[f642,f228]) ).
fof(f677,plain,
( ! [X0] :
( ~ m1_group_2(sK3,X0)
| v3_struct_0(X0)
| ~ v3_group_1(X0)
| l1_group_1(X0) )
| ~ spl27_7 ),
inference(resolution,[],[f583,f421]) ).
fof(f687,plain,
! [X0,X1] :
( l1_group_1(sK0)
| ~ m1_group_2(X0,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| m1_group_2(X1,X0)
| ~ m1_group_6(X1,sK0,X0) ),
inference(resolution,[],[f468,f226]) ).
fof(f688,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| m1_group_2(X1,X0)
| ~ m1_group_6(X1,sK0,X0) ),
inference(forward_subsumption_resolution,[],[f687,f372]) ).
fof(f689,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| v3_struct_0(sK0)
| m1_group_2(X1,X0)
| ~ m1_group_6(X1,sK0,X0) ),
inference(forward_subsumption_resolution,[],[f688,f227]) ).
fof(f690,plain,
! [X0,X1] :
( ~ m1_group_6(X1,sK0,X0)
| m1_group_2(X1,X0)
| ~ m1_group_2(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f689,f228]) ).
fof(f691,plain,
! [X0,X1] :
( l1_group_1(sK0)
| ~ m1_group_2(X0,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,X0)
| m1_group_6(X1,sK0,X0) ),
inference(resolution,[],[f469,f226]) ).
fof(f692,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,X0)
| m1_group_6(X1,sK0,X0) ),
inference(forward_subsumption_resolution,[],[f691,f372]) ).
fof(f693,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,X0)
| m1_group_6(X1,sK0,X0) ),
inference(forward_subsumption_resolution,[],[f692,f227]) ).
fof(f694,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,X0)
| m1_group_6(X1,sK0,X0) ),
inference(forward_subsumption_resolution,[],[f693,f228]) ).
fof(f695,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X1,X0)
| l1_group_1(X0)
| l1_group_1(X1)
| g1_group_1(u1_struct_0(X1),u1_group_1(X1)) = X1 ),
inference(resolution,[],[f485,f375]) ).
fof(f696,plain,
! [X0,X1] :
( ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_group_2(X1,X0)
| l1_group_1(X0)
| g1_group_1(u1_struct_0(X1),u1_group_1(X1)) = X1 ),
inference(forward_subsumption_resolution,[],[f695,f421]) ).
fof(f727,plain,
! [X0,X1] :
( l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| m1_group_2(X0,X1) ),
inference(resolution,[],[f493,f226]) ).
fof(f728,plain,
! [X0,X1] :
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f727,f372]) ).
fof(f729,plain,
! [X0,X1] :
( v3_struct_0(sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f728,f227]) ).
fof(f730,plain,
! [X0,X1] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f729,f228]) ).
fof(f753,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l1_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| k4_lattices(k11_group_4(sK0),sK3,X0) = k4_lattices(k11_group_4(sK0),X0,sK3) ),
inference(resolution,[],[f382,f222]) ).
fof(f760,definition,
( spl27_28
<=> v3_struct_0(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_28])],[avatar_definition]) ).
fof(f761,plain,
( ~ v3_struct_0(k11_group_4(sK0))
| spl27_28 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f762,plain,
( v3_struct_0(k11_group_4(sK0))
| ~ spl27_28 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f764,definition,
( spl27_29
<=> v6_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_29])],[avatar_definition]) ).
fof(f765,plain,
( ~ v6_lattices(k11_group_4(sK0))
| spl27_29 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f766,plain,
( v6_lattices(k11_group_4(sK0))
| ~ spl27_29 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f768,definition,
( spl27_30
<=> l1_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_30])],[avatar_definition]) ).
fof(f769,plain,
( ~ l1_lattices(k11_group_4(sK0))
| spl27_30 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f770,plain,
( l1_lattices(k11_group_4(sK0))
| ~ spl27_30 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f772,definition,
( spl27_31
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k4_lattices(k11_group_4(sK0),sK3,X0) = k4_lattices(k11_group_4(sK0),X0,sK3) ) ),
introduced(definition,[new_symbols(definition,[spl27_31])],[avatar_definition]) ).
fof(f773,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k4_lattices(k11_group_4(sK0),sK3,X0) = k4_lattices(k11_group_4(sK0),X0,sK3) )
| ~ spl27_31 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f774,plain,
( spl27_28
| spl27_29
| spl27_30
| spl27_31 ),
inference(avatar_split_clause,[],[f753,f772,f768,f764,f760]) ).
fof(f779,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) ),
inference(resolution,[],[f383,f226]) ).
fof(f780,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) ),
inference(forward_subsumption_resolution,[],[f779,f372]) ).
fof(f781,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| v3_struct_0(sK0)
| k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) ),
inference(forward_subsumption_resolution,[],[f780,f227]) ).
fof(f782,plain,
! [X0,X1] :
( ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) ),
inference(forward_subsumption_resolution,[],[f781,f228]) ).
fof(f783,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l1_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| k4_lattices(k11_group_4(sK0),sK4,X0) = k2_lattices(k11_group_4(sK0),sK4,X0) ),
inference(resolution,[],[f466,f219]) ).
fof(f784,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l1_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| k4_lattices(k11_group_4(sK0),sK3,X0) = k2_lattices(k11_group_4(sK0),sK3,X0) ),
inference(resolution,[],[f466,f222]) ).
fof(f791,definition,
( spl27_33
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k4_lattices(k11_group_4(sK0),sK3,X0) = k2_lattices(k11_group_4(sK0),sK3,X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_33])],[avatar_definition]) ).
fof(f792,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k4_lattices(k11_group_4(sK0),sK3,X0) = k2_lattices(k11_group_4(sK0),sK3,X0) )
| ~ spl27_33 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f793,plain,
( spl27_28
| spl27_29
| spl27_30
| spl27_33 ),
inference(avatar_split_clause,[],[f784,f791,f768,f764,f760]) ).
fof(f795,definition,
( spl27_34
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k4_lattices(k11_group_4(sK0),sK4,X0) = k2_lattices(k11_group_4(sK0),sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_34])],[avatar_definition]) ).
fof(f796,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k4_lattices(k11_group_4(sK0),sK4,X0) = k2_lattices(k11_group_4(sK0),sK4,X0) )
| ~ spl27_34 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f797,plain,
( spl27_28
| spl27_29
| spl27_30
| spl27_34 ),
inference(avatar_split_clause,[],[f783,f795,f768,f764,f760]) ).
fof(f798,plain,
( l3_lattices(k11_group_4(sK0))
| ~ spl27_30 ),
inference(resolution,[],[f770,f417]) ).
fof(f803,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_30 ),
inference(resolution,[],[f798,f403]) ).
fof(f804,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_30 ),
inference(forward_subsumption_resolution,[],[f803,f226]) ).
fof(f805,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_30 ),
inference(forward_subsumption_resolution,[],[f804,f227]) ).
fof(f806,plain,
( l1_group_1(sK0)
| ~ spl27_30 ),
inference(forward_subsumption_resolution,[],[f805,f228]) ).
fof(f807,plain,
( $false
| ~ spl27_30 ),
inference(forward_subsumption_resolution,[],[f806,f372]) ).
fof(f808,plain,
~ spl27_30,
inference(avatar_contradiction_clause,[],[f807]) ).
fof(f809,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_29 ),
inference(resolution,[],[f766,f443]) ).
fof(f810,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_29 ),
inference(forward_subsumption_resolution,[],[f809,f226]) ).
fof(f811,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_29 ),
inference(forward_subsumption_resolution,[],[f810,f227]) ).
fof(f812,plain,
( l1_group_1(sK0)
| ~ spl27_29 ),
inference(forward_subsumption_resolution,[],[f811,f228]) ).
fof(f813,plain,
( $false
| ~ spl27_29 ),
inference(forward_subsumption_resolution,[],[f812,f372]) ).
fof(f814,plain,
~ spl27_29,
inference(avatar_contradiction_clause,[],[f813]) ).
fof(f817,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_28 ),
inference(resolution,[],[f762,f401]) ).
fof(f819,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_28 ),
inference(forward_subsumption_resolution,[],[f817,f226]) ).
fof(f820,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_28 ),
inference(forward_subsumption_resolution,[],[f819,f227]) ).
fof(f821,plain,
( l1_group_1(sK0)
| ~ spl27_28 ),
inference(forward_subsumption_resolution,[],[f820,f228]) ).
fof(f822,plain,
( $false
| ~ spl27_28 ),
inference(forward_subsumption_resolution,[],[f821,f372]) ).
fof(f823,plain,
~ spl27_28,
inference(avatar_contradiction_clause,[],[f822]) ).
fof(f824,plain,
! [X0,X1] :
( v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| v1_group_1(X1)
| l1_group_1(sK0)
| ~ m1_group_2(X0,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| X0 = X1
| ~ r1_group_2(sK0,X1,X0) ),
inference(resolution,[],[f472,f226]) ).
fof(f825,plain,
! [X0,X1] :
( v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| v1_group_1(X1)
| ~ m1_group_2(X0,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| X0 = X1
| ~ r1_group_2(sK0,X1,X0) ),
inference(forward_subsumption_resolution,[],[f824,f372]) ).
fof(f826,plain,
! [X0,X1] :
( v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| v1_group_1(X1)
| ~ m1_group_2(X0,sK0)
| v3_struct_0(sK0)
| X0 = X1
| ~ r1_group_2(sK0,X1,X0) ),
inference(forward_subsumption_resolution,[],[f825,f227]) ).
fof(f827,plain,
! [X0,X1] :
( ~ r1_group_2(sK0,X1,X0)
| ~ m1_group_2(X1,sK0)
| v1_group_1(X1)
| ~ m1_group_2(X0,sK0)
| X0 = X1
| v1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f826,f228]) ).
fof(f832,plain,
( v3_struct_0(sK0)
| ~ v3_group_1(sK0)
| l1_group_1(sK0)
| ~ spl27_7 ),
inference(resolution,[],[f677,f359]) ).
fof(f833,plain,
( ~ v3_group_1(sK0)
| l1_group_1(sK0)
| ~ spl27_7 ),
inference(forward_subsumption_resolution,[],[f832,f228]) ).
fof(f834,plain,
( l1_group_1(sK0)
| ~ spl27_7 ),
inference(forward_subsumption_resolution,[],[f833,f227]) ).
fof(f835,plain,
( $false
| ~ spl27_7 ),
inference(forward_subsumption_resolution,[],[f834,f372]) ).
fof(f836,plain,
~ spl27_7,
inference(avatar_contradiction_clause,[],[f835]) ).
fof(f854,plain,
! [X2,X0,X1] :
( v9_lattices(k11_group_4(X0))
| l3_lattices(k11_group_4(X0))
| v3_struct_0(k11_group_4(X0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| k2_lattices(k11_group_4(X0),X1,X2) = X1
| ~ r1_lattices(k11_group_4(X0),X1,X2)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(resolution,[],[f483,f444]) ).
fof(f855,plain,
! [X2,X0,X1] :
( l3_lattices(k11_group_4(X0))
| v3_struct_0(k11_group_4(X0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| k2_lattices(k11_group_4(X0),X1,X2) = X1
| ~ r1_lattices(k11_group_4(X0),X1,X2)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f854,f445]) ).
fof(f856,plain,
! [X2,X0,X1] :
( v3_struct_0(k11_group_4(X0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| k2_lattices(k11_group_4(X0),X1,X2) = X1
| ~ r1_lattices(k11_group_4(X0),X1,X2)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f855,f403]) ).
fof(f857,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| k2_lattices(k11_group_4(X0),X1,X2) = X1
| ~ r1_lattices(k11_group_4(X0),X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| l1_group_1(X0) ),
inference(forward_subsumption_resolution,[],[f856,f401]) ).
fof(f866,plain,
! [X0] :
( v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l1_lattices(k11_group_4(sK0))
| k2_lattices(k11_group_4(sK0),X0,sK3) = k2_binop_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)),X0,sK3) ),
inference(resolution,[],[f393,f222]) ).
fof(f872,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l1_lattices(k11_group_4(sK0))
| k2_lattices(k11_group_4(sK0),X0,sK3) = k2_binop_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)),X0,sK3) )
| spl27_28 ),
inference(forward_subsumption_resolution,[],[f866,f761]) ).
fof(f874,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k2_lattices(k11_group_4(sK0),X0,sK3) = k2_binop_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)),X0,sK3) )
| spl27_28
| spl27_30 ),
inference(forward_subsumption_resolution,[],[f872,f769]) ).
fof(f895,plain,
( ~ l3_lattices(k11_group_4(sK0))
| ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k10_group_4(sK0))
| m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k9_group_4(sK0))
| m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
inference(superposition,[],[f397,f643]) ).
fof(f897,definition,
( spl27_39
<=> m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_39])],[avatar_definition]) ).
fof(f898,plain,
( ~ m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_39 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f899,plain,
( m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_39 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f901,definition,
( spl27_40
<=> v1_funct_1(k9_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_40])],[avatar_definition]) ).
fof(f902,plain,
( v1_funct_1(k9_group_4(sK0))
| ~ spl27_40 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f903,plain,
( ~ v1_funct_1(k9_group_4(sK0))
| spl27_40 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f905,definition,
( spl27_41
<=> v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_41])],[avatar_definition]) ).
fof(f907,plain,
( ~ v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_41 ),
inference(avatar_component_clause,[],[f905]) ).
fof(f909,definition,
( spl27_42
<=> m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_42])],[avatar_definition]) ).
fof(f911,plain,
( m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_42 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f913,definition,
( spl27_43
<=> v1_funct_1(k10_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_43])],[avatar_definition]) ).
fof(f915,plain,
( ~ v1_funct_1(k10_group_4(sK0))
| spl27_43 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f917,definition,
( spl27_44
<=> v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_44])],[avatar_definition]) ).
fof(f918,plain,
( v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_44 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f919,plain,
( ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_44 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f921,definition,
( spl27_45
<=> l3_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_45])],[avatar_definition]) ).
fof(f923,plain,
( ~ l3_lattices(k11_group_4(sK0))
| spl27_45 ),
inference(avatar_component_clause,[],[f921]) ).
fof(f924,plain,
( spl27_39
| ~ spl27_40
| ~ spl27_41
| spl27_42
| ~ spl27_43
| ~ spl27_44
| ~ spl27_45 ),
inference(avatar_split_clause,[],[f895,f921,f917,f913,f909,f905,f901,f897]) ).
fof(f925,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_40 ),
inference(resolution,[],[f903,f411]) ).
fof(f926,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_40 ),
inference(forward_subsumption_resolution,[],[f925,f226]) ).
fof(f927,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_40 ),
inference(forward_subsumption_resolution,[],[f926,f227]) ).
fof(f928,plain,
( l1_group_1(sK0)
| spl27_40 ),
inference(forward_subsumption_resolution,[],[f927,f228]) ).
fof(f929,plain,
( $false
| spl27_40 ),
inference(forward_subsumption_resolution,[],[f928,f372]) ).
fof(f930,plain,
spl27_40,
inference(avatar_contradiction_clause,[],[f929]) ).
fof(f975,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k10_group_4(sK0))
| m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k9_group_4(sK0))
| m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| k1_group_3(sK0) = X0 ),
inference(superposition,[],[f452,f643]) ).
fof(f978,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k10_group_4(sK0))
| m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| k1_group_3(sK0) = X0 )
| ~ spl27_40 ),
inference(forward_subsumption_resolution,[],[f975,f902]) ).
fof(f980,definition,
( spl27_46
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| k1_group_3(sK0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl27_46])],[avatar_definition]) ).
fof(f981,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| k1_group_3(sK0) = X0 )
| ~ spl27_46 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f982,plain,
( spl27_39
| ~ spl27_41
| spl27_42
| ~ spl27_43
| ~ spl27_44
| spl27_46
| ~ spl27_40 ),
inference(avatar_split_clause,[],[f978,f901,f980,f917,f913,f909,f905,f897]) ).
fof(f991,plain,
! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k10_group_4(sK0))
| m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k9_group_4(sK0))
| m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| k10_group_4(sK0) = X2 ),
inference(superposition,[],[f454,f643]) ).
fof(f994,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_1(k10_group_4(sK0))
| m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| k10_group_4(sK0) = X2 )
| ~ spl27_40 ),
inference(forward_subsumption_resolution,[],[f991,f902]) ).
fof(f996,definition,
( spl27_48
<=> ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| k10_group_4(sK0) = X2 ) ),
introduced(definition,[new_symbols(definition,[spl27_48])],[avatar_definition]) ).
fof(f997,plain,
( ! [X2,X0,X1] :
( g3_lattices(X0,X1,X2) != k11_group_4(sK0)
| k10_group_4(sK0) = X2 )
| ~ spl27_48 ),
inference(avatar_component_clause,[],[f996]) ).
fof(f998,plain,
( spl27_39
| ~ spl27_41
| spl27_42
| ~ spl27_43
| ~ spl27_44
| spl27_48
| ~ spl27_40 ),
inference(avatar_split_clause,[],[f994,f901,f996,f917,f913,f909,f905,f897]) ).
fof(f1005,plain,
! [X0,X4,X5] :
( l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v1_funct_2(k10_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
| ~ v1_funct_1(k10_group_4(X0))
| ~ m1_subset_1(X4,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X4,X5) ),
inference(forward_subsumption_resolution,[],[f387,f400]) ).
fof(f1006,plain,
! [X0,X4,X5] :
( l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v1_funct_1(k10_group_4(X0))
| ~ m1_subset_1(X4,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X4,X5) ),
inference(forward_subsumption_resolution,[],[f1005,f399]) ).
fof(f1007,plain,
! [X0,X4,X5] :
( ~ v4_group_1(X0)
| l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X4,k1_group_3(X0))
| ~ m1_subset_1(X5,k1_group_3(X0))
| ~ m1_group_2(X4,X0)
| ~ m1_group_2(X5,X0)
| k9_group_2(X0,X4,X5) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X4,X5) ),
inference(forward_subsumption_resolution,[],[f1006,f398]) ).
fof(f1008,plain,
! [X0,X1] :
( l1_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X0,X1) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) ),
inference(resolution,[],[f1007,f226]) ).
fof(f1009,plain,
! [X0,X1] :
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X0,X1) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) ),
inference(forward_subsumption_resolution,[],[f1008,f372]) ).
fof(f1010,plain,
! [X0,X1] :
( v3_struct_0(sK0)
| ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X0,X1) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) ),
inference(forward_subsumption_resolution,[],[f1009,f227]) ).
fof(f1011,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X0,X1) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) ),
inference(forward_subsumption_resolution,[],[f1010,f228]) ).
fof(f1019,plain,
! [X0] :
( ~ m1_group_2(X0,sK4)
| m1_group_6(X0,sK0,sK4) ),
inference(resolution,[],[f694,f360]) ).
fof(f1036,plain,
! [X2,X0,X1] :
( ~ v4_group_1(X2)
| ~ m1_group_2(X1,sK0)
| m1_group_2(X1,X0)
| ~ m1_group_2(X0,sK0)
| ~ v3_group_1(X2)
| v3_struct_0(X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X2)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X2)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(X2)))
| l1_group_1(X2)
| r3_lattices(k11_group_4(X2),X1,X0) ),
inference(resolution,[],[f730,f487]) ).
fof(f1042,plain,
! [X0] :
( ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,sK3) = k9_group_2(sK0,sK3,X0) ),
inference(resolution,[],[f782,f359]) ).
fof(f1056,plain,
( k4_lattices(k11_group_4(sK0),sK3,sK4) = k4_lattices(k11_group_4(sK0),sK4,sK3)
| ~ spl27_31 ),
inference(resolution,[],[f773,f219]) ).
fof(f1078,plain,
( k4_lattices(k11_group_4(sK0),sK3,sK4) = k2_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_33 ),
inference(resolution,[],[f792,f219]) ).
fof(f1090,plain,
( k4_lattices(k11_group_4(sK0),sK4,sK3) = k2_lattices(k11_group_4(sK0),sK4,sK3)
| ~ spl27_34 ),
inference(resolution,[],[f796,f222]) ).
fof(f1101,plain,
! [X0,X1] :
( ~ m1_group_2(k9_group_2(sK0,X0,X1),sK0)
| v1_group_1(k9_group_2(sK0,X0,X1))
| ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| v1_group_1(X0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(resolution,[],[f827,f480]) ).
fof(f1102,plain,
! [X0,X1] :
( ~ m1_group_2(k9_group_2(sK0,X0,X1),sK0)
| v1_group_1(k9_group_2(sK0,X0,X1))
| ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(duplicate_literal_removal,[],[f1101]) ).
fof(f1104,plain,
! [X0,X1] :
( v1_group_1(k9_group_2(sK0,X0,X1))
| ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1102,f410]) ).
fof(f1105,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1104,f409]) ).
fof(f1106,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1105,f226]) ).
fof(f1107,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| v3_struct_0(sK0)
| ~ m1_group_2(X1,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1106,f227]) ).
fof(f1108,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| l1_group_1(sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1107,f228]) ).
fof(f1109,plain,
! [X0,X1] :
( ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X0,X1) = X0
| v1_group_1(X0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[],[f1108,f372]) ).
fof(f1122,plain,
( k2_lattices(k11_group_4(sK0),sK4,sK3) = k2_binop_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)),sK4,sK3)
| spl27_28
| spl27_30 ),
inference(resolution,[],[f874,f219]) ).
fof(f1123,plain,
( k2_lattices(k11_group_4(sK0),sK3,sK3) = k2_binop_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)),sK3,sK3)
| spl27_28
| spl27_30 ),
inference(resolution,[],[f874,f222]) ).
fof(f1331,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_group_3(sK0))
| r1_tarski(X1,k1_group_3(sK0))
| r2_hidden(X0,X1)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X2,sK0)
| k9_group_2(sK0,X0,X2) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X2) ),
inference(resolution,[],[f550,f1011]) ).
fof(f1354,plain,
( k11_group_4(sK0) = g3_lattices(u1_struct_0(k11_group_4(sK0)),u2_lattices(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)))
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0) ),
inference(resolution,[],[f620,f226]) ).
fof(f1355,plain,
( k11_group_4(sK0) = g3_lattices(u1_struct_0(k11_group_4(sK0)),u2_lattices(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)))
| v3_struct_0(sK0)
| l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1354,f227]) ).
fof(f1356,plain,
( k11_group_4(sK0) = g3_lattices(u1_struct_0(k11_group_4(sK0)),u2_lattices(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0)))
| l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1355,f228]) ).
fof(f1357,plain,
k11_group_4(sK0) = g3_lattices(u1_struct_0(k11_group_4(sK0)),u2_lattices(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0))),
inference(forward_subsumption_resolution,[],[f1356,f372]) ).
fof(f1358,plain,
! [X0] :
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_group_2(X0,sK0)
| l1_group_1(sK0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0 ),
inference(resolution,[],[f696,f226]) ).
fof(f1359,plain,
! [X0] :
( v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_group_2(X0,sK0)
| l1_group_1(sK0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f1358,f227]) ).
fof(f1360,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_group_2(X0,sK0)
| l1_group_1(sK0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f1359,f228]) ).
fof(f1361,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_group_2(X0,sK0)
| g1_group_1(u1_struct_0(X0),u1_group_1(X0)) = X0 ),
inference(forward_subsumption_resolution,[],[f1360,f372]) ).
fof(f1465,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k2_lattices(k11_group_4(sK0),X1,X0) = X1
| ~ r1_lattices(k11_group_4(sK0),X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0) ),
inference(resolution,[],[f857,f226]) ).
fof(f1466,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k2_lattices(k11_group_4(sK0),X1,X0) = X1
| ~ r1_lattices(k11_group_4(sK0),X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| v3_struct_0(sK0)
| l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1465,f227]) ).
fof(f1467,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| k2_lattices(k11_group_4(sK0),X1,X0) = X1
| ~ r1_lattices(k11_group_4(sK0),X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| l1_group_1(sK0) ),
inference(forward_subsumption_resolution,[],[f1466,f228]) ).
fof(f1468,plain,
! [X0,X1] :
( ~ r1_lattices(k11_group_4(sK0),X1,X0)
| k2_lattices(k11_group_4(sK0),X1,X0) = X1
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) ),
inference(forward_subsumption_resolution,[],[f1467,f372]) ).
fof(f1850,plain,
( ~ m2_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_39 ),
inference(resolution,[],[f899,f470]) ).
fof(f1855,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_44 ),
inference(resolution,[],[f919,f399]) ).
fof(f1856,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_44 ),
inference(forward_subsumption_resolution,[],[f1855,f226]) ).
fof(f1857,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_44 ),
inference(forward_subsumption_resolution,[],[f1856,f227]) ).
fof(f1858,plain,
( l1_group_1(sK0)
| spl27_44 ),
inference(forward_subsumption_resolution,[],[f1857,f228]) ).
fof(f1859,plain,
( $false
| spl27_44 ),
inference(forward_subsumption_resolution,[],[f1858,f372]) ).
fof(f1860,plain,
spl27_44,
inference(avatar_contradiction_clause,[],[f1859]) ).
fof(f1891,plain,
( k4_lattices(k11_group_4(sK0),sK3,sK4) = k2_lattices(k11_group_4(sK0),sK4,sK3)
| ~ spl27_31
| ~ spl27_34 ),
inference(superposition,[],[f1056,f1090]) ).
fof(f1893,plain,
( k2_lattices(k11_group_4(sK0),sK3,sK4) = k2_lattices(k11_group_4(sK0),sK4,sK3)
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34 ),
inference(forward_demodulation,[],[f1891,f1078]) ).
fof(f1898,plain,
k9_group_2(sK0,sK4,sK3) = k9_group_2(sK0,sK3,sK4),
inference(resolution,[],[f1042,f360]) ).
fof(f1963,definition,
( spl27_95
<=> m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0))) ),
introduced(definition,[new_symbols(definition,[spl27_95])],[avatar_definition]) ).
fof(f1965,plain,
( m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ spl27_95 ),
inference(avatar_component_clause,[],[f1963]) ).
fof(f1979,definition,
( spl27_99
<=> v1_funct_1(u1_lattices(k11_group_4(sK0))) ),
introduced(definition,[new_symbols(definition,[spl27_99])],[avatar_definition]) ).
fof(f1980,plain,
( v1_funct_1(u1_lattices(k11_group_4(sK0)))
| ~ spl27_99 ),
inference(avatar_component_clause,[],[f1979]) ).
fof(f1981,plain,
( ~ v1_funct_1(u1_lattices(k11_group_4(sK0)))
| spl27_99 ),
inference(avatar_component_clause,[],[f1979]) ).
fof(f1983,definition,
( spl27_100
<=> v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0))) ),
introduced(definition,[new_symbols(definition,[spl27_100])],[avatar_definition]) ).
fof(f1985,plain,
( ~ v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| spl27_100 ),
inference(avatar_component_clause,[],[f1983]) ).
fof(f2030,plain,
( ~ m1_group_2(sK3,sK0)
| sK3 = g1_group_1(u1_struct_0(sK3),u1_group_1(sK3)) ),
inference(resolution,[],[f1361,f222]) ).
fof(f2047,plain,
sK3 = g1_group_1(u1_struct_0(sK3),u1_group_1(sK3)),
inference(forward_subsumption_resolution,[],[f2030,f359]) ).
fof(f2069,definition,
( spl27_107
<=> v1_xboole_0(k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_107])],[avatar_definition]) ).
fof(f2070,plain,
( v1_xboole_0(k1_group_3(sK0))
| ~ spl27_107 ),
inference(avatar_component_clause,[],[f2069]) ).
fof(f2071,plain,
( ~ v1_xboole_0(k1_group_3(sK0))
| spl27_107 ),
inference(avatar_component_clause,[],[f2069]) ).
fof(f2130,plain,
( l1_lattices(k11_group_4(sK0))
| spl27_99 ),
inference(resolution,[],[f1981,f426]) ).
fof(f2131,plain,
( $false
| spl27_30
| spl27_99 ),
inference(forward_subsumption_resolution,[],[f2130,f769]) ).
fof(f2132,plain,
( spl27_30
| spl27_99 ),
inference(avatar_contradiction_clause,[],[f2131]) ).
fof(f2140,plain,
! [X0] :
( ~ m1_group_2(X0,sK4)
| v1_group_1(X0)
| ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,sK4) = X0 ),
inference(resolution,[],[f1109,f360]) ).
fof(f2216,definition,
( spl27_115
<=> v1_xboole_0(u1_struct_0(k11_group_4(sK0))) ),
introduced(definition,[new_symbols(definition,[spl27_115])],[avatar_definition]) ).
fof(f2218,plain,
( ~ v1_xboole_0(u1_struct_0(k11_group_4(sK0)))
| spl27_115 ),
inference(avatar_component_clause,[],[f2216]) ).
fof(f2238,plain,
( m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_1(u1_lattices(k11_group_4(sK0)))
| ~ v1_xboole_0(u1_struct_0(k11_group_4(sK0)))
| ~ v1_xboole_0(u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| spl27_28
| spl27_30 ),
inference(superposition,[],[f404,f1123]) ).
fof(f2239,plain,
( m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_1(u1_lattices(k11_group_4(sK0)))
| ~ v1_xboole_0(u1_struct_0(k11_group_4(sK0)))
| spl27_28
| spl27_30 ),
inference(duplicate_literal_removal,[],[f2238]) ).
fof(f2240,plain,
( m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),u1_struct_0(k11_group_4(sK0)))
| m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_1(u1_lattices(k11_group_4(sK0)))
| ~ v1_xboole_0(u1_struct_0(k11_group_4(sK0)))
| spl27_28
| spl27_30 ),
inference(forward_subsumption_resolution,[],[f2239,f222]) ).
fof(f2241,plain,
( m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),u1_struct_0(k11_group_4(sK0)))
| m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0))),u1_struct_0(k11_group_4(sK0)))
| ~ v1_xboole_0(u1_struct_0(k11_group_4(sK0)))
| spl27_28
| spl27_30
| ~ spl27_99 ),
inference(forward_subsumption_resolution,[],[f2240,f1980]) ).
fof(f2243,definition,
( spl27_120
<=> m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),u1_struct_0(k11_group_4(sK0))) ),
introduced(definition,[new_symbols(definition,[spl27_120])],[avatar_definition]) ).
fof(f2245,plain,
( m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),u1_struct_0(k11_group_4(sK0)))
| ~ spl27_120 ),
inference(avatar_component_clause,[],[f2243]) ).
fof(f2246,plain,
( ~ spl27_115
| ~ spl27_100
| spl27_95
| spl27_120
| spl27_28
| spl27_30
| ~ spl27_99 ),
inference(avatar_split_clause,[],[f2241,f1979,f768,f760,f2243,f1963,f1983,f2216]) ).
fof(f2298,plain,
( ~ v1_group_1(sK3)
| ~ v1_funct_2(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3))
| ~ v1_funct_1(u1_group_1(sK3))
| m1_relset_1(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3)) ),
inference(superposition,[],[f394,f2047]) ).
fof(f2300,definition,
( spl27_123
<=> m1_relset_1(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_123])],[avatar_definition]) ).
fof(f2302,plain,
( m1_relset_1(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3))
| ~ spl27_123 ),
inference(avatar_component_clause,[],[f2300]) ).
fof(f2304,definition,
( spl27_124
<=> v1_funct_1(u1_group_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_124])],[avatar_definition]) ).
fof(f2306,plain,
( ~ v1_funct_1(u1_group_1(sK3))
| spl27_124 ),
inference(avatar_component_clause,[],[f2304]) ).
fof(f2308,definition,
( spl27_125
<=> v1_funct_2(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3)) ),
introduced(definition,[new_symbols(definition,[spl27_125])],[avatar_definition]) ).
fof(f2310,plain,
( ~ v1_funct_2(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3))
| spl27_125 ),
inference(avatar_component_clause,[],[f2308]) ).
fof(f2312,definition,
( spl27_126
<=> v1_group_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl27_126])],[avatar_definition]) ).
fof(f2314,plain,
( ~ v1_group_1(sK3)
| spl27_126 ),
inference(avatar_component_clause,[],[f2312]) ).
fof(f2315,plain,
( spl27_123
| ~ spl27_124
| ~ spl27_125
| ~ spl27_126 ),
inference(avatar_split_clause,[],[f2298,f2312,f2308,f2304,f2300]) ).
fof(f2338,plain,
( l1_group_1(sK3)
| spl27_124 ),
inference(resolution,[],[f2306,f423]) ).
fof(f2339,plain,
( $false
| spl27_7
| spl27_124 ),
inference(forward_subsumption_resolution,[],[f2338,f582]) ).
fof(f2340,plain,
( spl27_7
| spl27_124 ),
inference(avatar_contradiction_clause,[],[f2339]) ).
fof(f2341,plain,
! [X0,X1] :
( k2_lattices(k11_group_4(sK0),X0,X1) = X0
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(resolution,[],[f1468,f474]) ).
fof(f2342,plain,
! [X0,X1] :
( k2_lattices(k11_group_4(sK0),X0,X1) = X0
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(duplicate_literal_removal,[],[f2341]) ).
fof(f2343,plain,
( ! [X0,X1] :
( k2_lattices(k11_group_4(sK0),X0,X1) = X0
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| r3_lattices(k11_group_4(sK0),X0,X1) )
| spl27_29 ),
inference(forward_subsumption_resolution,[],[f2342,f765]) ).
fof(f2344,plain,
( ! [X0,X1] :
( k2_lattices(k11_group_4(sK0),X0,X1) = X0
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| r3_lattices(k11_group_4(sK0),X0,X1) )
| spl27_28
| spl27_29 ),
inference(forward_subsumption_resolution,[],[f2343,f761]) ).
fof(f2346,definition,
( spl27_130
<=> v8_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_130])],[avatar_definition]) ).
fof(f2347,plain,
( v8_lattices(k11_group_4(sK0))
| ~ spl27_130 ),
inference(avatar_component_clause,[],[f2346]) ).
fof(f2348,plain,
( ~ v8_lattices(k11_group_4(sK0))
| spl27_130 ),
inference(avatar_component_clause,[],[f2346]) ).
fof(f2350,definition,
( spl27_131
<=> v9_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_131])],[avatar_definition]) ).
fof(f2351,plain,
( ~ v9_lattices(k11_group_4(sK0))
| spl27_131 ),
inference(avatar_component_clause,[],[f2350]) ).
fof(f2352,plain,
( v9_lattices(k11_group_4(sK0))
| ~ spl27_131 ),
inference(avatar_component_clause,[],[f2350]) ).
fof(f2354,definition,
( spl27_132
<=> ! [X0,X1] :
( k2_lattices(k11_group_4(sK0),X0,X1) = X0
| r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) ) ),
introduced(definition,[new_symbols(definition,[spl27_132])],[avatar_definition]) ).
fof(f2355,plain,
( ! [X0,X1] :
( k2_lattices(k11_group_4(sK0),X0,X1) = X0
| r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| ~ spl27_132 ),
inference(avatar_component_clause,[],[f2354]) ).
fof(f2356,plain,
( ~ spl27_130
| spl27_131
| spl27_45
| spl27_132
| spl27_28
| spl27_29 ),
inference(avatar_split_clause,[],[f2344,f764,f760,f2354,f921,f2350,f2346]) ).
fof(f2357,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_130 ),
inference(resolution,[],[f2348,f444]) ).
fof(f2358,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_130 ),
inference(forward_subsumption_resolution,[],[f2357,f226]) ).
fof(f2359,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_130 ),
inference(forward_subsumption_resolution,[],[f2358,f227]) ).
fof(f2360,plain,
( l1_group_1(sK0)
| spl27_130 ),
inference(forward_subsumption_resolution,[],[f2359,f228]) ).
fof(f2361,plain,
( $false
| spl27_130 ),
inference(forward_subsumption_resolution,[],[f2360,f372]) ).
fof(f2362,plain,
spl27_130,
inference(avatar_contradiction_clause,[],[f2361]) ).
fof(f2382,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_131 ),
inference(resolution,[],[f2352,f445]) ).
fof(f2383,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_131 ),
inference(forward_subsumption_resolution,[],[f2382,f226]) ).
fof(f2384,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| ~ spl27_131 ),
inference(forward_subsumption_resolution,[],[f2383,f227]) ).
fof(f2385,plain,
( l1_group_1(sK0)
| ~ spl27_131 ),
inference(forward_subsumption_resolution,[],[f2384,f228]) ).
fof(f2386,plain,
( $false
| ~ spl27_131 ),
inference(forward_subsumption_resolution,[],[f2385,f372]) ).
fof(f2387,plain,
~ spl27_131,
inference(avatar_contradiction_clause,[],[f2386]) ).
fof(f2867,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| l1_group_1(sK0)
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(resolution,[],[f1036,f226]) ).
fof(f2868,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| l1_group_1(sK0)
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(duplicate_literal_removal,[],[f2867]) ).
fof(f2869,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| v3_struct_0(sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| l1_group_1(sK0)
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(forward_subsumption_resolution,[],[f2868,f227]) ).
fof(f2870,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| l1_group_1(sK0)
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(forward_subsumption_resolution,[],[f2869,f228]) ).
fof(f2871,plain,
! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(forward_subsumption_resolution,[],[f2870,f372]) ).
fof(f2877,definition,
( spl27_165
<=> u1_struct_0(k11_group_4(sK0)) = k1_group_3(sK0) ),
introduced(definition,[new_symbols(definition,[spl27_165])],[avatar_definition]) ).
fof(f2879,plain,
( u1_struct_0(k11_group_4(sK0)) = k1_group_3(sK0)
| ~ spl27_165 ),
inference(avatar_component_clause,[],[f2877]) ).
fof(f2888,definition,
( spl27_166
<=> k10_group_4(sK0) = u1_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_166])],[avatar_definition]) ).
fof(f2890,plain,
( k10_group_4(sK0) = u1_lattices(k11_group_4(sK0))
| ~ spl27_166 ),
inference(avatar_component_clause,[],[f2888]) ).
fof(f3056,definition,
( spl27_171
<=> l2_lattices(k11_group_4(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_171])],[avatar_definition]) ).
fof(f3058,plain,
( l2_lattices(k11_group_4(sK0))
| ~ spl27_171 ),
inference(avatar_component_clause,[],[f3056]) ).
fof(f3204,plain,
( v3_struct_0(k11_group_4(sK0))
| l1_struct_0(k11_group_4(sK0))
| spl27_115 ),
inference(resolution,[],[f2218,f446]) ).
fof(f3208,plain,
( l1_struct_0(k11_group_4(sK0))
| spl27_28
| spl27_115 ),
inference(forward_subsumption_resolution,[],[f3204,f761]) ).
fof(f3209,plain,
( l2_lattices(k11_group_4(sK0))
| spl27_28
| spl27_115 ),
inference(resolution,[],[f3208,f416]) ).
fof(f3215,plain,
( spl27_171
| spl27_28
| spl27_115 ),
inference(avatar_split_clause,[],[f3209,f2216,f760,f3056]) ).
fof(f3561,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_107 ),
inference(resolution,[],[f2071,f440]) ).
fof(f3565,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_107 ),
inference(forward_subsumption_resolution,[],[f3561,f226]) ).
fof(f3566,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_107 ),
inference(forward_subsumption_resolution,[],[f3565,f227]) ).
fof(f3567,plain,
( l1_group_1(sK0)
| spl27_107 ),
inference(forward_subsumption_resolution,[],[f3566,f228]) ).
fof(f3568,plain,
( $false
| spl27_107 ),
inference(forward_subsumption_resolution,[],[f3567,f372]) ).
fof(f3569,plain,
spl27_107,
inference(avatar_contradiction_clause,[],[f3568]) ).
fof(f3589,definition,
( spl27_207
<=> ! [X1] : ~ m1_subset_1(X1,k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_207])],[avatar_definition]) ).
fof(f3590,plain,
( ! [X1] : ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ spl27_207 ),
inference(avatar_component_clause,[],[f3589]) ).
fof(f3636,plain,
( $false
| ~ spl27_207 ),
inference(resolution,[],[f3590,f295]) ).
fof(f3640,plain,
~ spl27_207,
inference(avatar_contradiction_clause,[],[f3636]) ).
fof(f3756,definition,
( spl27_213
<=> m2_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_213])],[avatar_definition]) ).
fof(f3758,plain,
( ~ m2_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_213 ),
inference(avatar_component_clause,[],[f3756]) ).
fof(f5334,plain,
( ~ spl27_213
| ~ spl27_39 ),
inference(avatar_split_clause,[],[f1850,f897,f3756]) ).
fof(f5453,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_213 ),
inference(resolution,[],[f3758,f400]) ).
fof(f5455,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_213 ),
inference(forward_subsumption_resolution,[],[f5453,f226]) ).
fof(f5456,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_213 ),
inference(forward_subsumption_resolution,[],[f5455,f227]) ).
fof(f5457,plain,
( l1_group_1(sK0)
| spl27_213 ),
inference(forward_subsumption_resolution,[],[f5456,f228]) ).
fof(f5458,plain,
( $false
| spl27_213 ),
inference(forward_subsumption_resolution,[],[f5457,f372]) ).
fof(f5459,plain,
spl27_213,
inference(avatar_contradiction_clause,[],[f5458]) ).
fof(f5521,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_43 ),
inference(resolution,[],[f915,f398]) ).
fof(f5522,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_43 ),
inference(forward_subsumption_resolution,[],[f5521,f226]) ).
fof(f5523,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_43 ),
inference(forward_subsumption_resolution,[],[f5522,f227]) ).
fof(f5524,plain,
( l1_group_1(sK0)
| spl27_43 ),
inference(forward_subsumption_resolution,[],[f5523,f228]) ).
fof(f5525,plain,
( $false
| spl27_43 ),
inference(forward_subsumption_resolution,[],[f5524,f372]) ).
fof(f5526,plain,
spl27_43,
inference(avatar_contradiction_clause,[],[f5525]) ).
fof(f5724,definition,
( spl27_263
<=> m2_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
introduced(definition,[new_symbols(definition,[spl27_263])],[avatar_definition]) ).
fof(f5726,plain,
( ~ m2_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_263 ),
inference(avatar_component_clause,[],[f5724]) ).
fof(f5740,plain,
( ~ m2_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_42 ),
inference(resolution,[],[f911,f470]) ).
fof(f5741,plain,
( ~ spl27_263
| ~ spl27_42 ),
inference(avatar_split_clause,[],[f5740,f909,f5724]) ).
fof(f5842,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_263 ),
inference(resolution,[],[f5726,f413]) ).
fof(f5844,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_263 ),
inference(forward_subsumption_resolution,[],[f5842,f226]) ).
fof(f5845,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_263 ),
inference(forward_subsumption_resolution,[],[f5844,f227]) ).
fof(f5846,plain,
( l1_group_1(sK0)
| spl27_263 ),
inference(forward_subsumption_resolution,[],[f5845,f228]) ).
fof(f5847,plain,
( $false
| spl27_263 ),
inference(forward_subsumption_resolution,[],[f5846,f372]) ).
fof(f5848,plain,
spl27_263,
inference(avatar_contradiction_clause,[],[f5847]) ).
fof(f5859,plain,
( ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_41 ),
inference(resolution,[],[f907,f412]) ).
fof(f5860,plain,
( ~ v3_group_1(sK0)
| v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_41 ),
inference(forward_subsumption_resolution,[],[f5859,f226]) ).
fof(f5861,plain,
( v3_struct_0(sK0)
| l1_group_1(sK0)
| spl27_41 ),
inference(forward_subsumption_resolution,[],[f5860,f227]) ).
fof(f5862,plain,
( l1_group_1(sK0)
| spl27_41 ),
inference(forward_subsumption_resolution,[],[f5861,f228]) ).
fof(f5863,plain,
( $false
| spl27_41 ),
inference(forward_subsumption_resolution,[],[f5862,f372]) ).
fof(f5864,plain,
spl27_41,
inference(avatar_contradiction_clause,[],[f5863]) ).
fof(f5929,plain,
( k11_group_4(sK0) != k11_group_4(sK0)
| u1_struct_0(k11_group_4(sK0)) = k1_group_3(sK0)
| ~ spl27_46 ),
inference(superposition,[],[f981,f1357]) ).
fof(f5930,plain,
( u1_struct_0(k11_group_4(sK0)) = k1_group_3(sK0)
| ~ spl27_46 ),
inference(trivial_inequality_removal,[],[f5929]) ).
fof(f5931,plain,
( spl27_165
| ~ spl27_46 ),
inference(avatar_split_clause,[],[f5930,f980,f2877]) ).
fof(f5935,plain,
( k11_group_4(sK0) != k11_group_4(sK0)
| k10_group_4(sK0) = u1_lattices(k11_group_4(sK0))
| ~ spl27_48 ),
inference(superposition,[],[f997,f1357]) ).
fof(f5936,plain,
( k10_group_4(sK0) = u1_lattices(k11_group_4(sK0))
| ~ spl27_48 ),
inference(trivial_inequality_removal,[],[f5935]) ).
fof(f5937,plain,
( spl27_166
| ~ spl27_48 ),
inference(avatar_split_clause,[],[f5936,f996,f2888]) ).
fof(f5938,plain,
( m1_subset_1(sK4,k1_group_3(sK0))
| ~ spl27_165 ),
inference(superposition,[],[f219,f2879]) ).
fof(f5939,plain,
( m1_subset_1(sK3,k1_group_3(sK0))
| ~ spl27_165 ),
inference(superposition,[],[f222,f2879]) ).
fof(f6000,plain,
( m1_subset_1(k2_lattices(k11_group_4(sK0),sK3,sK3),k1_group_3(sK0))
| ~ spl27_120
| ~ spl27_165 ),
inference(superposition,[],[f2245,f2879]) ).
fof(f6501,plain,
( l3_lattices(k11_group_4(sK0))
| ~ spl27_171 ),
inference(resolution,[],[f3058,f418]) ).
fof(f6502,plain,
( $false
| spl27_45
| ~ spl27_171 ),
inference(forward_subsumption_resolution,[],[f6501,f923]) ).
fof(f6503,plain,
( spl27_45
| ~ spl27_171 ),
inference(avatar_contradiction_clause,[],[f6502]) ).
fof(f6504,plain,
( k2_lattices(k11_group_4(sK0),sK4,sK3) = k2_binop_1(u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),u1_struct_0(k11_group_4(sK0)),k10_group_4(sK0),sK4,sK3)
| spl27_28
| spl27_30
| ~ spl27_166 ),
inference(superposition,[],[f1122,f2890]) ).
fof(f6534,plain,
( k2_lattices(k11_group_4(sK0),sK4,sK3) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3)
| spl27_28
| spl27_30
| ~ spl27_165
| ~ spl27_166 ),
inference(forward_demodulation,[],[f6504,f2879]) ).
fof(f6883,plain,
( m1_relset_1(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_95
| ~ spl27_165 ),
inference(forward_demodulation,[],[f1965,f2879]) ).
fof(f6884,plain,
( m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ spl27_95
| ~ spl27_165
| ~ spl27_166 ),
inference(forward_demodulation,[],[f6883,f2890]) ).
fof(f6885,plain,
( $false
| spl27_39
| ~ spl27_95
| ~ spl27_165
| ~ spl27_166 ),
inference(forward_subsumption_resolution,[],[f6884,f898]) ).
fof(f6886,plain,
( spl27_39
| ~ spl27_95
| ~ spl27_165
| ~ spl27_166 ),
inference(avatar_contradiction_clause,[],[f6885]) ).
fof(f7030,plain,
( ~ v1_funct_2(u1_lattices(k11_group_4(sK0)),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_100
| ~ spl27_165 ),
inference(forward_demodulation,[],[f1985,f2879]) ).
fof(f7031,plain,
( ~ v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| spl27_100
| ~ spl27_165
| ~ spl27_166 ),
inference(forward_demodulation,[],[f7030,f2890]) ).
fof(f7032,plain,
( $false
| ~ spl27_44
| spl27_100
| ~ spl27_165
| ~ spl27_166 ),
inference(forward_subsumption_resolution,[],[f7031,f918]) ).
fof(f7033,plain,
( ~ spl27_44
| spl27_100
| ~ spl27_165
| ~ spl27_166 ),
inference(avatar_contradiction_clause,[],[f7032]) ).
fof(f7574,plain,
( ! [X0,X1] :
( r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(X1,X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(k2_lattices(k11_group_4(sK0),sK3,sK3),sK0)
| k9_group_2(sK0,X1,k2_lattices(k11_group_4(sK0),sK3,sK3)) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X1,k2_lattices(k11_group_4(sK0),sK3,sK3)) )
| ~ spl27_120
| ~ spl27_165 ),
inference(resolution,[],[f6000,f1331]) ).
fof(f9738,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X1) = X0
| r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_demodulation,[],[f2355,f2879]) ).
fof(f9739,plain,
( ! [X0,X1] :
( r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X1) = X0
| ~ m1_subset_1(X1,k1_group_3(sK0)) )
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_demodulation,[],[f9738,f2879]) ).
fof(f9752,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| ~ spl27_132
| ~ spl27_165 ),
inference(resolution,[],[f9739,f478]) ).
fof(f9754,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| ~ spl27_132
| ~ spl27_165 ),
inference(duplicate_literal_removal,[],[f9752]) ).
fof(f9755,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_45
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f9754,f923]) ).
fof(f9758,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_45
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f9755,f2351]) ).
fof(f9761,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f9758,f2347]) ).
fof(f9763,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f9761,f765]) ).
fof(f9765,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f9763,f761]) ).
fof(f9768,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_demodulation,[],[f9765,f2879]) ).
fof(f9769,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0))) )
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(duplicate_literal_removal,[],[f9768]) ).
fof(f9772,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0 )
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(forward_demodulation,[],[f9769,f2879]) ).
fof(f9774,definition,
( spl27_497
<=> ! [X0] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl27_497])],[avatar_definition]) ).
fof(f9775,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| k2_lattices(k11_group_4(sK0),X0,X0) = X0 )
| ~ spl27_497 ),
inference(avatar_component_clause,[],[f9774]) ).
fof(f9776,plain,
( spl27_497
| spl27_207
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165 ),
inference(avatar_split_clause,[],[f9772,f2877,f2354,f2350,f2346,f921,f764,f760,f3589,f9774]) ).
fof(f9792,plain,
( m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK0)
| ~ spl27_2 ),
inference(resolution,[],[f505,f690]) ).
fof(f9794,plain,
( m1_group_2(sK3,sK4)
| ~ spl27_2 ),
inference(forward_subsumption_resolution,[],[f9792,f360]) ).
fof(f9796,plain,
( ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1 ),
inference(resolution,[],[f500,f475]) ).
fof(f9797,plain,
( l3_lattices(k11_group_4(sK0))
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1 ),
inference(forward_subsumption_resolution,[],[f9796,f222]) ).
fof(f9799,plain,
( v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1
| spl27_45 ),
inference(forward_subsumption_resolution,[],[f9797,f923]) ).
fof(f9801,plain,
( ~ v8_lattices(k11_group_4(sK0))
| v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1
| spl27_45
| spl27_131 ),
inference(forward_subsumption_resolution,[],[f9799,f2351]) ).
fof(f9803,plain,
( v6_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1
| spl27_45
| ~ spl27_130
| spl27_131 ),
inference(forward_subsumption_resolution,[],[f9801,f2347]) ).
fof(f9805,plain,
( v3_struct_0(k11_group_4(sK0))
| ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131 ),
inference(forward_subsumption_resolution,[],[f9803,f765]) ).
fof(f9807,plain,
( ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ spl27_1
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131 ),
inference(forward_subsumption_resolution,[],[f9805,f761]) ).
fof(f9809,plain,
( ~ r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_1
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131 ),
inference(forward_subsumption_resolution,[],[f9807,f219]) ).
fof(f9812,plain,
( v1_group_1(sK3)
| ~ m1_group_2(sK3,sK0)
| sK3 = k9_group_2(sK0,sK3,sK4)
| ~ spl27_2 ),
inference(resolution,[],[f9794,f2140]) ).
fof(f10388,plain,
( l1_group_1(sK3)
| spl27_125 ),
inference(resolution,[],[f2310,f424]) ).
fof(f10389,plain,
( $false
| spl27_7
| spl27_125 ),
inference(forward_subsumption_resolution,[],[f10388,f582]) ).
fof(f10390,plain,
( spl27_7
| spl27_125 ),
inference(avatar_contradiction_clause,[],[f10389]) ).
fof(f10391,plain,
( ~ m2_relset_1(u1_group_1(sK3),k2_zfmisc_1(u1_struct_0(sK3),u1_struct_0(sK3)),u1_struct_0(sK3))
| ~ spl27_123 ),
inference(resolution,[],[f2302,f470]) ).
fof(f11317,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| r3_lattices(k11_group_4(sK0),X0,X1) )
| ~ spl27_165 ),
inference(forward_demodulation,[],[f2871,f2879]) ).
fof(f11318,plain,
( ! [X0,X1] :
( r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X0,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0)
| m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_subset_1(X1,k1_group_3(sK0)) )
| ~ spl27_165 ),
inference(forward_demodulation,[],[f11317,f2879]) ).
fof(f12969,plain,
( l1_group_1(sK3)
| ~ spl27_123 ),
inference(resolution,[],[f10391,f425]) ).
fof(f12971,plain,
( $false
| spl27_7
| ~ spl27_123 ),
inference(forward_subsumption_resolution,[],[f12969,f582]) ).
fof(f12972,plain,
( spl27_7
| ~ spl27_123 ),
inference(avatar_contradiction_clause,[],[f12971]) ).
fof(f12973,plain,
( v1_group_1(sK3)
| sK3 = k9_group_2(sK0,sK3,sK4)
| ~ spl27_2 ),
inference(forward_subsumption_resolution,[],[f9812,f359]) ).
fof(f12992,definition,
( spl27_626
<=> sK3 = k9_group_2(sK0,sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl27_626])],[avatar_definition]) ).
fof(f12994,plain,
( sK3 = k9_group_2(sK0,sK3,sK4)
| ~ spl27_626 ),
inference(avatar_component_clause,[],[f12992]) ).
fof(f13140,plain,
( ~ m1_subset_1(sK3,k1_group_3(sK0))
| ~ m1_group_2(sK3,sK0)
| m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK0)
| ~ m1_subset_1(sK4,k1_group_3(sK0))
| spl27_1
| ~ spl27_165 ),
inference(resolution,[],[f501,f11318]) ).
fof(f13143,plain,
( ~ m1_group_2(sK3,sK0)
| m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK0)
| ~ m1_subset_1(sK4,k1_group_3(sK0))
| spl27_1
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f13140,f5939]) ).
fof(f13145,plain,
( m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK0)
| ~ m1_subset_1(sK4,k1_group_3(sK0))
| spl27_1
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f13143,f359]) ).
fof(f13146,plain,
( m1_group_2(sK3,sK4)
| ~ m1_subset_1(sK4,k1_group_3(sK0))
| spl27_1
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f13145,f360]) ).
fof(f13147,plain,
( m1_group_2(sK3,sK4)
| spl27_1
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f13146,f5938]) ).
fof(f13308,plain,
( m1_group_6(sK3,sK0,sK4)
| spl27_1
| ~ spl27_165 ),
inference(resolution,[],[f13147,f1019]) ).
fof(f13310,plain,
( $false
| spl27_1
| spl27_2
| ~ spl27_165 ),
inference(forward_subsumption_resolution,[],[f13308,f504]) ).
fof(f13311,plain,
( spl27_1
| spl27_2
| ~ spl27_165 ),
inference(avatar_contradiction_clause,[],[f13310]) ).
fof(f13321,plain,
( sK3 = k9_group_2(sK0,sK3,sK4)
| ~ spl27_2
| spl27_126 ),
inference(forward_subsumption_resolution,[],[f12973,f2314]) ).
fof(f13327,plain,
( spl27_626
| ~ spl27_2
| spl27_126 ),
inference(avatar_split_clause,[],[f13321,f2312,f503,f12992]) ).
fof(f15261,definition,
( spl27_762
<=> ! [X0] :
( r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(sK4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_762])],[avatar_definition]) ).
fof(f15262,plain,
( ! [X0] :
( r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(sK4,X0) )
| ~ spl27_762 ),
inference(avatar_component_clause,[],[f15261]) ).
fof(f16732,definition,
( spl27_851
<=> ! [X0,X1] :
( r2_hidden(X0,X1)
| k9_group_2(sK0,X0,sK3) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,sK3)
| r1_tarski(X1,k1_group_3(sK0))
| ~ m1_group_2(X0,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl27_851])],[avatar_definition]) ).
fof(f16733,plain,
( ! [X0,X1] :
( ~ m1_group_2(X0,sK0)
| k9_group_2(sK0,X0,sK3) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,sK3)
| r1_tarski(X1,k1_group_3(sK0))
| r2_hidden(X0,X1) )
| ~ spl27_851 ),
inference(avatar_component_clause,[],[f16732]) ).
fof(f65486,plain,
( sK3 = k2_lattices(k11_group_4(sK0),sK3,sK3)
| ~ spl27_165
| ~ spl27_497 ),
inference(resolution,[],[f9775,f5939]) ).
fof(f65523,plain,
( ! [X0,X1] :
( ~ m1_group_2(sK3,sK0)
| r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(X1,X0)
| ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X1,k2_lattices(k11_group_4(sK0),sK3,sK3)) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X1,k2_lattices(k11_group_4(sK0),sK3,sK3)) )
| ~ spl27_120
| ~ spl27_165
| ~ spl27_497 ),
inference(forward_demodulation,[],[f7574,f65486]) ).
fof(f65530,plain,
( ! [X0,X1] :
( r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(X1,X0)
| ~ m1_group_2(X1,sK0)
| k9_group_2(sK0,X1,k2_lattices(k11_group_4(sK0),sK3,sK3)) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X1,k2_lattices(k11_group_4(sK0),sK3,sK3)) )
| ~ spl27_120
| ~ spl27_165
| ~ spl27_497 ),
inference(forward_subsumption_resolution,[],[f65523,f359]) ).
fof(f65536,plain,
( ! [X0,X1] :
( k9_group_2(sK0,X1,sK3) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X1,sK3)
| r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(X1,X0)
| ~ m1_group_2(X1,sK0) )
| ~ spl27_120
| ~ spl27_165
| ~ spl27_497 ),
inference(forward_demodulation,[],[f65530,f65486]) ).
fof(f65541,plain,
( spl27_851
| ~ spl27_120
| ~ spl27_165
| ~ spl27_497 ),
inference(avatar_split_clause,[],[f65536,f9774,f2877,f2243,f16732]) ).
fof(f79621,plain,
( k2_lattices(k11_group_4(sK0),sK3,sK4) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3)
| spl27_28
| spl27_30
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34
| ~ spl27_165
| ~ spl27_166 ),
inference(forward_demodulation,[],[f6534,f1893]) ).
fof(f107434,definition,
( spl27_3507
<=> sK3 = k2_lattices(k11_group_4(sK0),sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl27_3507])],[avatar_definition]) ).
fof(f107436,plain,
( sK3 = k2_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_3507 ),
inference(avatar_component_clause,[],[f107434]) ).
fof(f107473,plain,
( ! [X0] :
( k9_group_2(sK0,sK4,sK3) = k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3)
| r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(sK4,X0) )
| ~ spl27_851 ),
inference(resolution,[],[f16733,f360]) ).
fof(f107523,plain,
( ! [X0] :
( k2_lattices(k11_group_4(sK0),sK3,sK4) = k9_group_2(sK0,sK4,sK3)
| r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(sK4,X0) )
| spl27_28
| spl27_30
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34
| ~ spl27_165
| ~ spl27_166
| ~ spl27_851 ),
inference(forward_demodulation,[],[f107473,f79621]) ).
fof(f107543,plain,
( ! [X0] :
( k2_lattices(k11_group_4(sK0),sK3,sK4) = k9_group_2(sK0,sK3,sK4)
| r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(sK4,X0) )
| spl27_28
| spl27_30
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34
| ~ spl27_165
| ~ spl27_166
| ~ spl27_851 ),
inference(forward_demodulation,[],[f107523,f1898]) ).
fof(f107547,plain,
( ! [X0] :
( sK3 = k2_lattices(k11_group_4(sK0),sK3,sK4)
| r1_tarski(X0,k1_group_3(sK0))
| r2_hidden(sK4,X0) )
| spl27_28
| spl27_30
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34
| ~ spl27_165
| ~ spl27_166
| ~ spl27_626
| ~ spl27_851 ),
inference(forward_demodulation,[],[f107543,f12994]) ).
fof(f107550,plain,
( spl27_762
| spl27_3507
| spl27_28
| spl27_30
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34
| ~ spl27_165
| ~ spl27_166
| ~ spl27_626
| ~ spl27_851 ),
inference(avatar_split_clause,[],[f107547,f16732,f12992,f2888,f2877,f795,f791,f772,f768,f760,f107434,f15261]) ).
fof(f108869,plain,
( sK3 != sK3
| v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_3507 ),
inference(superposition,[],[f484,f107436]) ).
fof(f108871,plain,
( v9_lattices(k11_group_4(sK0))
| ~ v8_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_3507 ),
inference(trivial_inequality_removal,[],[f108869]) ).
fof(f108872,plain,
( ~ v8_lattices(k11_group_4(sK0))
| v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108871,f2351]) ).
fof(f108891,plain,
( v3_struct_0(k11_group_4(sK0))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108872,f2347]) ).
fof(f108895,plain,
( ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| spl27_28
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108891,f761]) ).
fof(f108896,plain,
( ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| spl27_28
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108895,f222]) ).
fof(f108897,plain,
( l3_lattices(k11_group_4(sK0))
| r1_lattices(k11_group_4(sK0),sK3,sK4)
| spl27_28
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108896,f219]) ).
fof(f108898,plain,
( r1_lattices(k11_group_4(sK0),sK3,sK4)
| spl27_28
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108897,f923]) ).
fof(f108899,plain,
( $false
| ~ spl27_1
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(forward_subsumption_resolution,[],[f108898,f9809]) ).
fof(f108900,plain,
( ~ spl27_1
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(avatar_contradiction_clause,[],[f108899]) ).
fof(f108901,plain,
( r2_hidden(sK4,k1_group_3(sK0))
| ~ spl27_762 ),
inference(resolution,[],[f15262,f477]) ).
fof(f108914,plain,
( ~ m1_subset_1(sK4,k1_group_3(sK0))
| ~ v1_xboole_0(k1_group_3(sK0))
| ~ spl27_762 ),
inference(resolution,[],[f108901,f486]) ).
fof(f108915,plain,
( ~ v1_xboole_0(k1_group_3(sK0))
| ~ spl27_165
| ~ spl27_762 ),
inference(forward_subsumption_resolution,[],[f108914,f5938]) ).
fof(f108916,plain,
( $false
| ~ spl27_107
| ~ spl27_165
| ~ spl27_762 ),
inference(forward_subsumption_resolution,[],[f108915,f2070]) ).
fof(f108917,plain,
( ~ spl27_107
| ~ spl27_165
| ~ spl27_762 ),
inference(avatar_contradiction_clause,[],[f108916]) ).
cnf(s1,plain,
( ~ spl27_1
| spl27_2 ),
inference(sat_conversion,[],[f506]) ).
cnf(s2,plain,
( spl27_1
| ~ spl27_2 ),
inference(sat_conversion,[],[f507]) ).
cnf(s18,plain,
( spl27_28
| spl27_29
| spl27_30
| spl27_31 ),
inference(sat_conversion,[],[f774]) ).
cnf(s20,plain,
( spl27_28
| spl27_29
| spl27_30
| spl27_33 ),
inference(sat_conversion,[],[f793]) ).
cnf(s21,plain,
( spl27_28
| spl27_29
| spl27_30
| spl27_34 ),
inference(sat_conversion,[],[f797]) ).
cnf(s22,plain,
~ spl27_30,
inference(sat_conversion,[],[f808]) ).
cnf(s23,plain,
~ spl27_29,
inference(sat_conversion,[],[f814]) ).
cnf(s24,plain,
~ spl27_28,
inference(sat_conversion,[],[f823]) ).
cnf(s25,plain,
~ spl27_7,
inference(sat_conversion,[],[f836]) ).
cnf(s28,plain,
( spl27_39
| ~ spl27_40
| ~ spl27_41
| spl27_42
| ~ spl27_43
| ~ spl27_44
| ~ spl27_45 ),
inference(sat_conversion,[],[f924]) ).
cnf(s29,plain,
spl27_40,
inference(sat_conversion,[],[f930]) ).
cnf(s30,plain,
( spl27_39
| ~ spl27_40
| ~ spl27_41
| spl27_42
| ~ spl27_43
| ~ spl27_44
| spl27_46 ),
inference(sat_conversion,[],[f982]) ).
cnf(s32,plain,
( spl27_39
| ~ spl27_40
| ~ spl27_41
| spl27_42
| ~ spl27_43
| ~ spl27_44
| spl27_48 ),
inference(sat_conversion,[],[f998]) ).
cnf(s66,plain,
spl27_44,
inference(sat_conversion,[],[f1860]) ).
cnf(s81,plain,
( spl27_30
| spl27_99 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s85,plain,
( spl27_28
| spl27_30
| spl27_95
| ~ spl27_99
| ~ spl27_100
| ~ spl27_115
| spl27_120 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s88,plain,
( spl27_123
| ~ spl27_124
| ~ spl27_125
| ~ spl27_126 ),
inference(sat_conversion,[],[f2315]) ).
cnf(s94,plain,
( spl27_7
| spl27_124 ),
inference(sat_conversion,[],[f2340]) ).
cnf(s95,plain,
( spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| spl27_132 ),
inference(sat_conversion,[],[f2356]) ).
cnf(s96,plain,
spl27_130,
inference(sat_conversion,[],[f2362]) ).
cnf(s97,plain,
~ spl27_131,
inference(sat_conversion,[],[f2387]) ).
cnf(s150,plain,
( spl27_28
| spl27_115
| spl27_171 ),
inference(sat_conversion,[],[f3215]) ).
cnf(s166,plain,
spl27_107,
inference(sat_conversion,[],[f3569]) ).
cnf(s169,plain,
~ spl27_207,
inference(sat_conversion,[],[f3640]) ).
cnf(s229,plain,
( ~ spl27_39
| ~ spl27_213 ),
inference(sat_conversion,[],[f5334]) ).
cnf(s234,plain,
spl27_213,
inference(sat_conversion,[],[f5459]) ).
cnf(s246,plain,
spl27_43,
inference(sat_conversion,[],[f5526]) ).
cnf(s285,plain,
( ~ spl27_42
| ~ spl27_263 ),
inference(sat_conversion,[],[f5741]) ).
cnf(s293,plain,
spl27_263,
inference(sat_conversion,[],[f5848]) ).
cnf(s295,plain,
spl27_41,
inference(sat_conversion,[],[f5864]) ).
cnf(s303,plain,
( ~ spl27_46
| spl27_165 ),
inference(sat_conversion,[],[f5931]) ).
cnf(s305,plain,
( ~ spl27_48
| spl27_166 ),
inference(sat_conversion,[],[f5937]) ).
cnf(s338,plain,
( spl27_45
| ~ spl27_171 ),
inference(sat_conversion,[],[f6503]) ).
cnf(s357,plain,
( spl27_39
| ~ spl27_95
| ~ spl27_165
| ~ spl27_166 ),
inference(sat_conversion,[],[f6886]) ).
cnf(s362,plain,
( ~ spl27_44
| spl27_100
| ~ spl27_165
| ~ spl27_166 ),
inference(sat_conversion,[],[f7033]) ).
cnf(s529,plain,
( spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_132
| ~ spl27_165
| spl27_207
| spl27_497 ),
inference(sat_conversion,[],[f9776]) ).
cnf(s558,plain,
( spl27_7
| spl27_125 ),
inference(sat_conversion,[],[f10390]) ).
cnf(s704,plain,
( spl27_7
| ~ spl27_123 ),
inference(sat_conversion,[],[f12972]) ).
cnf(s725,plain,
( spl27_1
| spl27_2
| ~ spl27_165 ),
inference(sat_conversion,[],[f13311]) ).
cnf(s727,plain,
( ~ spl27_2
| spl27_126
| spl27_626 ),
inference(sat_conversion,[],[f13327]) ).
cnf(s2912,plain,
( ~ spl27_120
| ~ spl27_165
| ~ spl27_497
| spl27_851 ),
inference(sat_conversion,[],[f65541]) ).
cnf(s6686,plain,
( spl27_28
| spl27_30
| ~ spl27_31
| ~ spl27_33
| ~ spl27_34
| ~ spl27_165
| ~ spl27_166
| ~ spl27_626
| spl27_762
| ~ spl27_851
| spl27_3507 ),
inference(sat_conversion,[],[f107550]) ).
cnf(s6704,plain,
( ~ spl27_1
| spl27_28
| spl27_29
| spl27_45
| ~ spl27_130
| spl27_131
| ~ spl27_3507 ),
inference(sat_conversion,[],[f108900]) ).
cnf(s6705,plain,
( ~ spl27_107
| ~ spl27_165
| ~ spl27_762 ),
inference(sat_conversion,[],[f108917]) ).
cnf(s6877,plain,
~ spl27_42,
inference(rat,[],[s285,s293]) ).
cnf(s6890,plain,
~ spl27_39,
inference(rat,[],[s229,s234]) ).
cnf(s6954,plain,
( spl27_28
| spl27_29
| spl27_45
| spl27_132 ),
inference(rat,[],[s95,s97,s96]) ).
cnf(s6977,plain,
( ~ spl27_40
| spl27_48 ),
inference(rat,[],[s32,s66,s246,s6877,s295,s6890]) ).
cnf(s6979,plain,
( ~ spl27_40
| spl27_46 ),
inference(rat,[],[s30,s66,s246,s6877,s295,s6890]) ).
cnf(s6983,plain,
spl27_48,
inference(rat,[],[s6977,s29]) ).
cnf(s6985,plain,
spl27_46,
inference(rat,[],[s6979,s29]) ).
cnf(s6988,plain,
spl27_166,
inference(rat,[],[s305,s6983]) ).
cnf(s6990,plain,
spl27_165,
inference(rat,[],[s303,s6985]) ).
cnf(s6993,plain,
~ spl27_762,
inference(rat,[],[s6705,s166,s6990]) ).
cnf(s7001,plain,
~ spl27_95,
inference(rat,[],[s357,s6988,s6890,s6990]) ).
cnf(s7002,plain,
spl27_100,
inference(rat,[],[s362,s6988,s66,s6990]) ).
cnf(s7004,plain,
~ spl27_45,
inference(rat,[],[s28,s66,s246,s6877,s295,s29,s6890]) ).
cnf(s7005,plain,
~ spl27_171,
inference(rat,[],[s338,s7004]) ).
cnf(s7017,plain,
~ spl27_123,
inference(rat,[],[s704,s25]) ).
cnf(s7018,plain,
spl27_125,
inference(rat,[],[s558,s25]) ).
cnf(s7019,plain,
spl27_124,
inference(rat,[],[s94,s25]) ).
cnf(s7023,plain,
~ spl27_126,
inference(rat,[],[s88,s7017,s7018,s7019]) ).
cnf(s7040,plain,
spl27_115,
inference(rat,[],[s150,s7005,s24]) ).
cnf(s7045,plain,
spl27_132,
inference(rat,[],[s6954,s24,s7004,s23]) ).
cnf(s7046,plain,
spl27_497,
inference(rat,[],[s529,s23,s169,s6990,s24,s97,s96,s7004,s7045]) ).
cnf(s7077,plain,
spl27_99,
inference(rat,[],[s81,s22]) ).
cnf(s7097,plain,
spl27_120,
inference(rat,[],[s85,s22,s7040,s7002,s24,s7001,s7077]) ).
cnf(s7113,plain,
spl27_851,
inference(rat,[],[s2912,s7046,s6990,s7097]) ).
cnf(s7123,plain,
spl27_34,
inference(rat,[],[s21,s22,s23,s24]) ).
cnf(s7136,plain,
spl27_33,
inference(rat,[],[s20,s22,s23,s24]) ).
cnf(s7162,plain,
spl27_31,
inference(rat,[],[s18,s22,s23,s24]) ).
cnf(s7207,plain,
spl27_1,
inference(rat,[],[s2,s725,s6990]) ).
cnf(s7208,plain,
~ spl27_3507,
inference(rat,[],[s6704,s23,s97,s96,s7004,s24,s7207]) ).
cnf(s7212,plain,
spl27_2,
inference(rat,[],[s1,s7207]) ).
cnf(s7213,plain,
~ spl27_626,
inference(rat,[],[s6686,s7162,s7113,s6993,s7136,s6988,s6990,s7123,s22,s24,s7208]) ).
cnf(s7214,plain,
$false,
inference(rat,[],[s727,s7023,s7213,s7212]) ).
fof(f108918,plain,
$false,
inference(avatar_sat_refutation,[],[s7214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP648+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/0.47 % Computer : n003.cluster.edu
% 0.21/0.47 % Model : x86_64 x86_64
% 0.21/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.47 % Memory : 8046.5625MB
% 0.21/0.47 % OS : Linux 6.8.0-71-generic
% 0.21/0.47 % CPULimit : 300
% 0.21/0.47 % WCLimit : 300
% 0.21/0.47 % DateTime : Sun Sep 27 10:28:41 UTC 2026
% 0.21/0.47 % CPUTime :
% 0.21/0.47 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.52 Running first-order model finding
% 0.24/0.52 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.06/2.87 % (315261)Will run a generic schedule for satisfiability detection.
% 15.06/2.87 % (315269)dis+10_1_sil=32000:sp=arity:random_seed=3323013390:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.06/2.87 % (315267)% WARNING: option uhcvi not known.
% 15.06/2.87 % (315268)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3642033189:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.06/2.87 % (315266)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=654971300_2999 on theBenchmark for (2999ds/0Mi)
% 15.06/2.87 % (315270)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2460980884:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.06/2.87 % (315267)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3832159832:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.06/2.87 % (315272)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=609647077:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.06/2.87 % (315271)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1334087248:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.06/2.87 % TRYING [1]
% 15.06/2.87 % TRYING [2]
% 15.06/2.87 % (315269)Instruction limit reached!
% 15.06/2.87 % (315269)------------------------------
% 15.06/2.87 % (315269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.06/2.87 % (315269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.87 % (315269)CaDiCaL version: 2.1.3
% 15.06/2.87 % (315269)Termination reason: Instruction limit
% 15.06/2.87 % (315269)Termination phase: Saturation
% 15.06/2.87 % (315269)Time elapsed: 0.056 s
% 15.06/2.87 % (315269)Peak memory usage: 13 MB
% 15.06/2.87 % (315269)Instructions burned: 104 (million)
% 15.06/2.87 % TRYING [3]
% 15.06/2.87 % (315280)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1426525987:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.06/2.87 % TRYING [1]
% 15.06/2.87 % TRYING [2]
% 15.06/2.87 % TRYING [3]
% 15.06/2.87 % (315270)Instruction limit reached!
% 15.06/2.87 % (315270)------------------------------
% 15.06/2.87 % (315270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.06/2.87 % (315270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.87 % (315270)CaDiCaL version: 2.1.3
% 15.06/2.87 % (315270)Termination reason: Instruction limit
% 15.06/2.87 % (315270)Termination phase: Saturation
% 15.06/2.87 % (315270)Time elapsed: 0.120 s
% 15.06/2.87 % (315270)Peak memory usage: 13 MB
% 15.06/2.87 % (315270)Instructions burned: 116 (million)
% 15.06/2.87 % (315271)Instruction limit reached!
% 15.06/2.87 % (315271)------------------------------
% 15.06/2.87 % (315271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.06/2.87 % (315271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.87 % (315271)CaDiCaL version: 2.1.3
% 15.06/2.87 % (315271)Termination reason: Instruction limit
% 15.06/2.87 % (315271)Termination phase: Saturation
% 15.06/2.87 % (315271)Time elapsed: 0.123 s
% 15.06/2.87 % (315271)Peak memory usage: 14 MB
% 15.06/2.87 % (315271)Instructions burned: 131 (million)
% 15.06/2.87 % (315282)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=607117441:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.06/2.87 % (315283)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3162937664:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.06/2.87 % (315272)Instruction limit reached!
% 15.06/2.87 % (315272)------------------------------
% 15.06/2.87 % (315272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.06/2.87 % (315272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.06/2.87 % (315272)CaDiCaL version: 2.1.3
% 15.06/2.87 % (315272)Termination reason: Instruction limit
% 15.06/2.87 % (315272)Termination phase: Saturation
% 15.06/2.87 % (315272)Time elapsed: 0.163 s
% 15.06/2.87 % (315272)Peak memory usage: 14 MB
% 15.06/2.87 % (315272)Instructions burned: 159 (million)
% 15.06/2.87 % TRYING [4]
% 15.06/2.87 % (315286)ott-21_1_sil=16000:fs=off:random_seed=1070034051:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 15.06/2.87 % TRYING [4]
% 15.06/2.87 % (315282)Instruction limit reached!
% 15.06/2.87 % (315282)------------------------------
% 15.06/2.87 % (315282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.06/2.87 % (315282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315282)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315282)Termination reason: Instruction limit
% 39.40/8.71 % (315282)Termination phase: Saturation
% 39.40/8.71 % (315282)Time elapsed: 0.133 s
% 39.40/8.71 % (315282)Peak memory usage: 14 MB
% 39.40/8.71 % (315282)Instructions burned: 131 (million)
% 39.40/8.71 % (315280)Instruction limit reached!
% 39.40/8.71 % (315280)------------------------------
% 39.40/8.71 % (315280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315280)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315280)Termination reason: Instruction limit
% 39.40/8.71 % (315280)Termination phase: Finite model building constraint generation
% 39.40/8.71 % (315280)Time elapsed: 0.244 s
% 39.40/8.71 % (315280)Peak memory usage: 25 MB
% 39.40/8.71 % (315280)Instructions burned: 716 (million)
% 39.40/8.71 % (315288)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3698472968:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 39.40/8.71 % (315289)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1600580388:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 39.40/8.71 % TRYING [1]
% 39.40/8.71 % TRYING [2]
% 39.40/8.71 % TRYING [3]
% 39.40/8.71 % (315286)Instruction limit reached!
% 39.40/8.71 % (315286)------------------------------
% 39.40/8.71 % (315286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315286)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315286)Termination reason: Instruction limit
% 39.40/8.71 % (315286)Termination phase: Saturation
% 39.40/8.71 % (315286)Time elapsed: 0.170 s
% 39.40/8.71 % (315286)Peak memory usage: 13 MB
% 39.40/8.71 % (315286)Instructions burned: 180 (million)
% 39.40/8.71 % (315292)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2504993687:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 39.40/8.71 % TRYING [4]
% 39.40/8.71 % (315289)Instruction limit reached!
% 39.40/8.71 % (315289)------------------------------
% 39.40/8.71 % (315289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315289)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315289)Termination reason: Instruction limit
% 39.40/8.71 % (315289)Termination phase: Finite model building constraint generation
% 39.40/8.71 % (315289)Time elapsed: 0.308 s
% 39.40/8.71 % (315289)Peak memory usage: 24 MB
% 39.40/8.71 % (315289)Instructions burned: 867 (million)
% 39.40/8.71 % (315294)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3025582040:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 39.40/8.71 % (315283)Instruction limit reached!
% 39.40/8.71 % (315283)------------------------------
% 39.40/8.71 % (315283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315283)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315283)Termination reason: Instruction limit
% 39.40/8.71 % (315283)Termination phase: Saturation
% 39.40/8.71 % (315283)Time elapsed: 0.692 s
% 39.40/8.71 % (315283)Peak memory usage: 20 MB
% 39.40/8.71 % (315283)Instructions burned: 684 (million)
% 39.40/8.71 % (315288)Instruction limit reached!
% 39.40/8.71 % (315288)------------------------------
% 39.40/8.71 % (315288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315288)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315288)Termination reason: Instruction limit
% 39.40/8.71 % (315288)Termination phase: Saturation
% 39.40/8.71 % (315288)Time elapsed: 0.528 s
% 39.40/8.71 % (315288)Peak memory usage: 15 MB
% 39.40/8.71 % (315288)Instructions burned: 478 (million)
% 39.40/8.71 % (315296)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3329829868:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 39.40/8.71 % (315297)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=841628736:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 39.40/8.71 % (315294)Instruction limit reached!
% 39.40/8.71 % (315294)------------------------------
% 39.40/8.71 % (315294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315294)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315294)Termination reason: Instruction limit
% 39.40/8.71 % (315294)Termination phase: Finite model building constraint generation
% 39.40/8.71 % (315294)Time elapsed: 0.449 s
% 39.40/8.71 % (315294)Peak memory usage: 106 MB
% 39.40/8.71 % (315294)Instructions burned: 890 (million)
% 39.40/8.71 % (315300)fmb+10_1_sil=64000:random_seed=3103236851:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 39.40/8.71 % TRYING [1]
% 39.40/8.71 % TRYING [2]
% 39.40/8.71 % TRYING [3]
% 39.40/8.71 % TRYING [4]
% 39.40/8.71 % (315292)Instruction limit reached!
% 39.40/8.71 % (315292)------------------------------
% 39.40/8.71 % (315292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315292)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315292)Termination reason: Instruction limit
% 39.40/8.71 % (315292)Termination phase: Saturation
% 39.40/8.71 % (315292)Time elapsed: 1.085 s
% 39.40/8.71 % (315292)Peak memory usage: 27 MB
% 39.40/8.71 % (315292)Instructions burned: 1179 (million)
% 39.40/8.71 % TRYING [5]
% 39.40/8.71 % (315296)Instruction limit reached!
% 39.40/8.71 % (315296)------------------------------
% 39.40/8.71 % (315296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315296)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315296)Termination reason: Instruction limit
% 39.40/8.71 % (315296)Termination phase: Saturation
% 39.40/8.71 % (315296)Time elapsed: 0.664 s
% 39.40/8.71 % (315296)Peak memory usage: 21 MB
% 39.40/8.71 % (315296)Instructions burned: 692 (million)
% 39.40/8.71 % (315302)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1098252434:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 39.40/8.71 % (315302)Cannot represent all propositional literals internally
% 39.40/8.71 % (315302)Refutation not found, incomplete strategy
% 39.40/8.71 % (315302)------------------------------
% 39.40/8.71 % (315302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315302)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315302)Termination reason: Refutation not found, incomplete strategy
% 39.40/8.71 % (315302)Time elapsed: 0.020 s
% 39.40/8.71 % (315302)Peak memory usage: 11 MB
% 39.40/8.71 % (315302)Instructions burned: 23 (million)
% 39.40/8.71 % (315302)------------------------------
% 39.40/8.71 % (315302)------------------------------
% 39.40/8.71 % (315303)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1183591669:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 39.40/8.71 % (315305)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3732443325:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 39.40/8.71 % TRYING [8]
% 39.40/8.71 % (315297)Instruction limit reached!
% 39.40/8.71 % (315297)------------------------------
% 39.40/8.71 % (315297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315297)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315297)Termination reason: Instruction limit
% 39.40/8.71 % (315297)Termination phase: Saturation
% 39.40/8.71 % (315297)Time elapsed: 0.832 s
% 39.40/8.71 % (315297)Peak memory usage: 20 MB
% 39.40/8.71 % (315297)Instructions burned: 879 (million)
% 39.40/8.71 % (315308)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=761368782:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 39.40/8.71 % (315303)Instruction limit reached!
% 39.40/8.71 % (315303)------------------------------
% 39.40/8.71 % (315303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315303)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315303)Termination reason: Instruction limit
% 39.40/8.71 % (315303)Termination phase: Finite model building constraint generation
% 39.40/8.71 % (315303)Time elapsed: 0.587 s
% 39.40/8.71 % (315303)Peak memory usage: 50 MB
% 39.40/8.71 % (315303)Instructions burned: 920 (million)
% 39.40/8.71 % (315310)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3162791161:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 39.40/8.71 % (315310)Cannot represent all propositional literals internally
% 39.40/8.71 % (315310)Refutation not found, incomplete strategy
% 39.40/8.71 % (315310)------------------------------
% 39.40/8.71 % (315310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315310)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315310)Termination reason: Refutation not found, incomplete strategy
% 39.40/8.71 % (315310)Time elapsed: 0.030 s
% 39.40/8.71 % (315310)Peak memory usage: 11 MB
% 39.40/8.71 % (315310)Instructions burned: 34 (million)
% 39.40/8.71 % (315310)------------------------------
% 39.40/8.71 % (315310)------------------------------
% 39.40/8.71 % (315312)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3775346196:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 39.40/8.71 % TRYING [16]
% 39.40/8.71 % TRYING [5]
% 39.40/8.71 % (315308)Instruction limit reached!
% 39.40/8.71 % (315308)------------------------------
% 39.40/8.71 % (315308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315308)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315308)Termination reason: Instruction limit
% 39.40/8.71 % (315308)Termination phase: Saturation
% 39.40/8.71 % (315308)Time elapsed: 1.354 s
% 39.40/8.71 % (315308)Peak memory usage: 26 MB
% 39.40/8.71 % (315308)Instructions burned: 1473 (million)
% 39.40/8.71 % (315314)ott-2_1_sil=16000:newcnf=on:random_seed=1771530185:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 39.40/8.71 % (315312)Instruction limit reached!
% 39.40/8.71 % (315312)------------------------------
% 39.40/8.71 % (315312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315312)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315312)Termination reason: Instruction limit
% 39.40/8.71 % (315312)Termination phase: Finite model building constraint generation
% 39.40/8.71 % (315312)Time elapsed: 1.558 s
% 39.40/8.71 % (315312)Peak memory usage: 135 MB
% 39.40/8.71 % (315312)Instructions burned: 2174 (million)
% 39.40/8.71 % (315316)ott+10_1_sil=32000:tgt=ground:random_seed=1764006342:i=5114:av=off_2960 on theBenchmark for (2960ds/5114Mi)
% 39.40/8.71 % (315314)Instruction limit reached!
% 39.40/8.71 % (315314)------------------------------
% 39.40/8.71 % (315314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315314)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315314)Termination reason: Instruction limit
% 39.40/8.71 % (315314)Termination phase: Saturation
% 39.40/8.71 % (315314)Time elapsed: 0.852 s
% 39.40/8.71 % (315314)Peak memory usage: 20 MB
% 39.40/8.71 % (315314)Instructions burned: 870 (million)
% 39.40/8.71 % (315318)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=453660537:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 39.40/8.71 % TRYING [1]
% 39.40/8.71 % TRYING [2]
% 39.40/8.71 % TRYING [3]
% 39.40/8.71 % TRYING [4]
% 39.40/8.71 % TRYING [5]
% 39.40/8.71 % (315305)Instruction limit reached!
% 39.40/8.71 % (315305)------------------------------
% 39.40/8.71 % (315305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.71 % (315305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.71 % (315305)CaDiCaL version: 2.1.3
% 39.40/8.71 % (315305)Termination reason: Instruction limit
% 39.40/8.71 % (315305)Termination phase: Saturation
% 39.40/8.71 % (315305)Time elapsed: 4.614 s
% 39.40/8.71 % (315305)Peak memory usage: 40 MB
% 39.40/8.71 % (315305)Instructions burned: 5132 (million)
% 39.40/8.71 % (315320)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3341765667:i=3512:aac=none_2936 on theBenchmark for (2936ds/3512Mi)
% 39.40/8.71 % (315267) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-315261-315267"...
% 39.40/8.71 % (315267)...printing done.
% 39.40/8.71 % (315267)Refutation found. Thanks to Tanya!
% 39.40/8.71 % SZS status Theorem for theBenchmark
% 39.40/8.71 % SZS output start Proof for theBenchmark
% See solution above
% 39.40/8.73 % (315267)------------------------------
% 39.40/8.73 % (315267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.40/8.73 % (315267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.40/8.73 % (315267)CaDiCaL version: 2.1.3
% 39.40/8.73 % (315267)Termination reason: Refutation
% 39.40/8.73 % (315267)Time elapsed: 7.974 s
% 39.40/8.73 % (315267)Peak memory usage: 58 MB
% 39.40/8.73 % (315267)Instructions burned: 8343 (million)
% 39.40/8.73 % (315261)Success in time 8.176 s
% 39.40/8.73 % Vampire exiting
%------------------------------------------------------------------------------