%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP648+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n016.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 : Fri Sep 25 01:35:02 PM UTC 2026
% Result : Theorem 77.31s 11.41s
% Output : CNFRefutation 77.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 25
% Syntax : Number of formulae : 388 ( 56 unt; 0 def)
% Number of atoms : 2248 ( 270 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 3181 (1321 ~;1466 |; 299 &)
% ( 24 <=>; 69 =>; 0 <=; 2 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 32 ( 30 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-6 aty)
% Number of variables : 690 ( 0 sgn 662 !; 28 ?; 303 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
=> ( ( X4 = X2
& X3 = X1 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> m1_group_6(X1,X0,X2) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t31_latsubgr) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
=> ( ( X4 = X2
& X3 = X1 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> m1_group_6(X1,X0,X2) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
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/sandbox/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k4_lattices) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k9_group_2) ).
fof(f12,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( 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) )
=> ( 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)
=> ( ( 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) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_group_4) ).
fof(f13,axiom,
! [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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_group_4) ).
fof(f14,axiom,
! [X0] :
( ( l1_lattices(X0)
& ~ v3_struct_0(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/sandbox/benchmark/theBenchmark.p',d2_lattices) ).
fof(f17,axiom,
! [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))
& 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)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k10_group_4) ).
fof(f18,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( l3_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_group_4) ).
fof(f28,axiom,
! [X0,X1,X2] :
( ( 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)
& v1_group_1(k9_group_2(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_group_2) ).
fof(f29,axiom,
! [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))
& v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& v1_funct_1(k9_group_4(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k9_group_4) ).
fof(f34,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l2_lattices(X0)
& l1_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f36,axiom,
! [X0,X1] :
( ( m1_group_2(X1,X0)
& l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X2] :
( m1_group_6(X2,X0,X1)
=> m1_group_2(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_group_6) ).
fof(f55,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v15_lattices(k11_group_4(X0))
& v14_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_group_4) ).
fof(f61,axiom,
! [X0,X1,X2] :
( ( 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) )
=> ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) = g3_lattices(X3,X4,X5)
=> ( X2 = X5
& X1 = X4
& X0 = X3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(f71,axiom,
! [X0,X1,X2] :
( ( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_lattices) ).
fof(f73,axiom,
! [X0,X1] :
( ( m1_group_2(X1,X0)
& l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f75,axiom,
! [X0,X1,X2] :
( ( 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) )
=> ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_group_2) ).
fof(f76,axiom,
! [X0,X1,X2] :
( ( 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,X2)
<=> r1_lattices(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f81,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ! [X2] :
( ( m1_group_2(X2,X0)
& v1_group_1(X2) )
=> ( m1_group_2(X2,X1)
<=> r1_group_2(X0,k9_group_2(X0,X2,X1),X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t107_group_2) ).
fof(f83,axiom,
! [X0] :
( ( l3_lattices(X0)
& v9_lattices(X0)
& v8_lattices(X0)
& ~ v3_struct_0(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/sandbox/benchmark/theBenchmark.p',t21_lattices) ).
fof(f84,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
=> ! [X2] :
( m1_group_2(X2,X0)
=> ( X1 = X2
=> ( m1_group_2(X2,X0)
& v1_group_1(X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t29_latsubgr) ).
fof(f86,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
=> ( ( X4 = X2
& X3 = X1 )
=> ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_latsubgr) ).
fof(f90,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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/sandbox/benchmark/theBenchmark.p',t66_group_2) ).
fof(f95,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v14_lattices(k11_group_4(X0))
& v13_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f55]) ).
fof(f96,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v13_lattices(k11_group_4(X0))
& v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f95]) ).
fof(f97,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v7_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v5_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f97]) ).
fof(f99,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v4_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f98]) ).
fof(f100,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v10_lattices(k11_group_4(X0))
& v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f99]) ).
fof(f101,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( l3_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f18]) ).
fof(f102,plain,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(pure_predicate_removal,[],[f100]) ).
fof(f106,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
& X4 = X2
& X3 = X1
& ( r3_lattices(k11_group_4(X0),X3,X4)
<~> m1_group_6(X1,X0,X2) ) ) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f107,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
& X4 = X2
& X3 = X1
& ( r3_lattices(k11_group_4(X0),X3,X4)
<~> m1_group_6(X1,X0,X2) ) ) ) ) ) ),
inference(flattening,[],[f106]) ).
fof(f110,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_lattices(X0)
| X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f111,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v3_lattices(X0)
| X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
inference(flattening,[],[f110]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ~ 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(ennf_transformation,[],[f10]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ~ 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(flattening,[],[f119]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ~ 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(ennf_transformation,[],[f11]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ~ 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(flattening,[],[f121]) ).
fof(f123,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ 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)
| ( 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)
| 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) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f124,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ 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)
| ( 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)
| 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) ) ) ) ) ) ) ),
inference(flattening,[],[f123]) ).
fof(f125,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(ennf_transformation,[],[f13]) ).
fof(f126,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(flattening,[],[f125]) ).
fof(f127,plain,
! [X0] :
( ~ l1_lattices(X0)
| v3_struct_0(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) ) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f128,plain,
! [X0] :
( ~ l1_lattices(X0)
| v3_struct_0(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) ) ) ),
inference(flattening,[],[f127]) ).
fof(f133,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))
& 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)) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f134,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))
& 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)) ) ),
inference(flattening,[],[f133]) ).
fof(f135,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( l3_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(ennf_transformation,[],[f101]) ).
fof(f136,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( l3_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(flattening,[],[f135]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ~ 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)
& v1_group_1(k9_group_2(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f28]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ~ 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)
& v1_group_1(k9_group_2(X0,X1,X2)) ) ),
inference(flattening,[],[f145]) ).
fof(f147,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))
& v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& v1_funct_1(k9_group_4(X0)) ) ),
inference(ennf_transformation,[],[f29]) ).
fof(f148,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))
& v1_funct_2(k9_group_4(X0),k2_zfmisc_1(k1_group_3(X0),k1_group_3(X0)),k1_group_3(X0))
& v1_funct_1(k9_group_4(X0)) ) ),
inference(flattening,[],[f147]) ).
fof(f152,plain,
! [X0] :
( ~ l3_lattices(X0)
| ( l2_lattices(X0)
& l1_lattices(X0) ) ),
inference(ennf_transformation,[],[f34]) ).
fof(f155,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( ~ m1_group_6(X2,X0,X1)
| m1_group_2(X2,X0) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f156,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( ~ m1_group_6(X2,X0,X1)
| m1_group_2(X2,X0) ) ),
inference(flattening,[],[f155]) ).
fof(f167,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(ennf_transformation,[],[f102]) ).
fof(f168,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( v9_lattices(k11_group_4(X0))
& v8_lattices(k11_group_4(X0))
& v6_lattices(k11_group_4(X0))
& v3_lattices(k11_group_4(X0))
& ~ v3_struct_0(k11_group_4(X0)) ) ),
inference(flattening,[],[f167]) ).
fof(f175,plain,
! [X0,X1,X2] :
( ~ 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)
| ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ( X2 = X5
& X1 = X4
& X0 = X3 ) ) ),
inference(ennf_transformation,[],[f61]) ).
fof(f176,plain,
! [X0,X1,X2] :
( ~ 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)
| ! [X3,X4,X5] :
( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5)
| ( X2 = X5
& X1 = X4
& X0 = X3 ) ) ),
inference(flattening,[],[f175]) ).
fof(f182,plain,
! [X0,X1,X2] :
( ~ 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(ennf_transformation,[],[f71]) ).
fof(f183,plain,
! [X0,X1,X2] :
( ~ 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(flattening,[],[f182]) ).
fof(f186,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
inference(ennf_transformation,[],[f73]) ).
fof(f187,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( m1_group_6(X2,X0,X1)
<=> m1_group_2(X2,X1) ) ),
inference(flattening,[],[f186]) ).
fof(f188,plain,
! [X0,X1,X2] :
( ~ 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)
| ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
inference(ennf_transformation,[],[f75]) ).
fof(f189,plain,
! [X0,X1,X2] :
( ~ 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)
| ( r1_group_2(X0,X1,X2)
<=> X1 = X2 ) ),
inference(flattening,[],[f188]) ).
fof(f190,plain,
! [X0,X1,X2] :
( ~ 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,X2)
<=> r1_lattices(X0,X1,X2) ) ),
inference(ennf_transformation,[],[f76]) ).
fof(f191,plain,
! [X0,X1,X2] :
( ~ 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,X2)
<=> r1_lattices(X0,X1,X2) ) ),
inference(flattening,[],[f190]) ).
fof(f198,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ( m1_group_2(X2,X1)
<=> r1_group_2(X0,k9_group_2(X0,X2,X1),X2) ) ) ) ),
inference(ennf_transformation,[],[f81]) ).
fof(f199,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ( m1_group_2(X2,X1)
<=> r1_group_2(X0,k9_group_2(X0,X2,X1),X2) ) ) ) ),
inference(flattening,[],[f198]) ).
fof(f201,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| v3_struct_0(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 ) ) ) ),
inference(ennf_transformation,[],[f83]) ).
fof(f202,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| v3_struct_0(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 ) ) ) ),
inference(flattening,[],[f201]) ).
fof(f203,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ! [X2] :
( ~ m1_group_2(X2,X0)
| X1 != X2
| ( m1_group_2(X2,X0)
& v1_group_1(X2) ) ) ) ),
inference(ennf_transformation,[],[f84]) ).
fof(f204,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ! [X2] :
( ~ m1_group_2(X2,X0)
| X1 != X2
| ( m1_group_2(X2,X0)
& v1_group_1(X2) ) ) ) ),
inference(flattening,[],[f203]) ).
fof(f207,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(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)))
| X2 != X4
| X1 != X3
| ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ) ) ) ) ) ),
inference(ennf_transformation,[],[f86]) ).
fof(f208,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(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)))
| X2 != X4
| X1 != X3
| ( r3_lattices(k11_group_4(X0),X3,X4)
<=> r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ) ) ) ) ) ),
inference(flattening,[],[f207]) ).
fof(f212,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(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) ) ) ),
inference(ennf_transformation,[],[f90]) ).
fof(f213,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(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) ) ) ),
inference(flattening,[],[f212]) ).
fof(f217,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
& X4 = X2
& X3 = X1
& ( r3_lattices(k11_group_4(X0),X3,X4)
| m1_group_6(X1,X0,X2) )
& ( ~ r3_lattices(k11_group_4(X0),X3,X4)
| ~ m1_group_6(X1,X0,X2) ) ) ) ) ) ),
inference(nnf_transformation,[],[f107]) ).
fof(f218,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(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)))
& X4 = X2
& X3 = X1
& ( r3_lattices(k11_group_4(X0),X3,X4)
| m1_group_6(X1,X0,X2) )
& ( ~ r3_lattices(k11_group_4(X0),X3,X4)
| ~ m1_group_6(X1,X0,X2) ) ) ) ) ) ),
inference(flattening,[],[f217]) ).
fof(f219,plain,
( l1_group_1(sK0)
& v4_group_1(sK0)
& v3_group_1(sK0)
& ~ v3_struct_0(sK0)
& m1_group_2(sK1,sK0)
& m1_group_2(sK2,sK0)
& m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
& m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
& sK2 = sK4
& sK1 = sK3
& ( r3_lattices(k11_group_4(sK0),sK3,sK4)
| m1_group_6(sK1,sK0,sK2) )
& ( ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_group_6(sK1,sK0,sK2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f218]) ).
fof(f220,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ 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)
| ( ( k10_group_4(X0) != X1
| ! [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)
| 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) ) ) ) ) )
& ( ? [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)
& 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) ) ) ) )
| X1 = k10_group_4(X0) ) ) ) ),
inference(nnf_transformation,[],[f124]) ).
fof(f221,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ 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)
| ( ( k10_group_4(X0) != X1
| ! [X6] :
( ~ m1_subset_1(X6,k1_group_3(X0))
| ! [X7] :
( ~ m1_subset_1(X7,k1_group_3(X0))
| ! [X8] :
( ~ m1_group_2(X8,X0)
| ! [X9] :
( ~ m1_group_2(X9,X0)
| X7 != X9
| X6 != X8
| k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X6,X7) = k9_group_2(X0,X8,X9) ) ) ) ) )
& ( ? [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)
& 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) ) ) ) )
| X1 = k10_group_4(X0) ) ) ) ),
inference(rectify,[],[f220]) ).
fof(f222,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ 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)
| ( ( k10_group_4(X0) != X1
| ! [X6] :
( ~ m1_subset_1(X6,k1_group_3(X0))
| ! [X7] :
( ~ m1_subset_1(X7,k1_group_3(X0))
| ! [X8] :
( ~ m1_group_2(X8,X0)
| ! [X9] :
( ~ m1_group_2(X9,X0)
| X7 != X9
| X6 != X8
| k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X6,X7) = k9_group_2(X0,X8,X9) ) ) ) ) )
& ( ( m1_subset_1(sK5(X0,X1),k1_group_3(X0))
& m1_subset_1(sK6(X0,X1),k1_group_3(X0))
& m1_group_2(sK7(X0,X1),X0)
& m1_group_2(sK8(X0,X1),X0)
& sK6(X0,X1) = sK8(X0,X1)
& sK5(X0,X1) = sK7(X0,X1)
& k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,sK5(X0,X1),sK6(X0,X1)) != k9_group_2(X0,sK7(X0,X1),sK8(X0,X1)) )
| X1 = k10_group_4(X0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8]),skolemize(X2,sK5(X0,X1)),skolemize(X3,sK6(X0,X1)),skolemize(X4,sK7(X0,X1)),skolemize(X5,sK8(X0,X1))],[f221]) ).
fof(f241,plain,
! [X0,X1] :
( ~ m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X2] :
( ( ~ m1_group_6(X2,X0,X1)
| m1_group_2(X2,X1) )
& ( ~ m1_group_2(X2,X1)
| m1_group_6(X2,X0,X1) ) ) ),
inference(nnf_transformation,[],[f187]) ).
fof(f242,plain,
! [X0,X1,X2] :
( ( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) )
& ( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f243,plain,
! [X0,X1,X2] :
( ~ 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)
| ( ( ~ r1_group_2(X0,X1,X2)
| X1 = X2 )
& ( X1 != X2
| r1_group_2(X0,X1,X2) ) ) ),
inference(nnf_transformation,[],[f189]) ).
fof(f244,plain,
! [X0,X1,X2] :
( ~ 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,X2)
| r1_lattices(X0,X1,X2) )
& ( ~ r1_lattices(X0,X1,X2)
| r3_lattices(X0,X1,X2) ) ) ),
inference(nnf_transformation,[],[f191]) ).
fof(f245,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ( ( ~ m1_group_2(X2,X1)
| r1_group_2(X0,k9_group_2(X0,X2,X1),X2) )
& ( ~ r1_group_2(X0,k9_group_2(X0,X2,X1),X2)
| m1_group_2(X2,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f199]) ).
fof(f246,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| v3_struct_0(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 )
& ( k2_lattices(X0,X1,X2) != X1
| r1_lattices(X0,X1,X2) ) ) ) ) ),
inference(nnf_transformation,[],[f202]) ).
fof(f247,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(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)))
| X2 != X4
| X1 != X3
| ( ( ~ r3_lattices(k11_group_4(X0),X3,X4)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) )
& ( ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| r3_lattices(k11_group_4(X0),X3,X4) ) ) ) ) ) ) ),
inference(nnf_transformation,[],[f208]) ).
fof(f249,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f250,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f251,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f252,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f253,plain,
m1_group_2(sK1,sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f254,plain,
m1_group_2(sK2,sK0),
inference(cnf_transformation,[],[f219]) ).
fof(f255,plain,
m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0))),
inference(cnf_transformation,[],[f219]) ).
fof(f256,plain,
m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0))),
inference(cnf_transformation,[],[f219]) ).
fof(f257,plain,
sK2 = sK4,
inference(cnf_transformation,[],[f219]) ).
fof(f258,plain,
sK1 = sK3,
inference(cnf_transformation,[],[f219]) ).
fof(f259,plain,
( r3_lattices(k11_group_4(sK0),sK3,sK4)
| m1_group_6(sK1,sK0,sK2) ),
inference(cnf_transformation,[],[f219]) ).
fof(f260,plain,
( ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_group_6(sK1,sK0,sK2) ),
inference(cnf_transformation,[],[f219]) ).
fof(f262,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(f273,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(f274,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(f275,plain,
! [X0,X1,X8,X6,X9,X7] :
( ~ 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)
| k10_group_4(X0) != X1
| ~ m1_subset_1(X6,k1_group_3(X0))
| ~ m1_subset_1(X7,k1_group_3(X0))
| ~ m1_group_2(X8,X0)
| ~ m1_group_2(X9,X0)
| X7 != X9
| X6 != X8
| k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X6,X7) = k9_group_2(X0,X8,X9) ),
inference(cnf_transformation,[],[f222]) ).
fof(f283,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(f284,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(f289,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(f290,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(f291,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(f292,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(f293,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(f294,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(f300,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(f301,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(f302,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(f303,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(f304,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(f309,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f313,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_6(X2,X0,X1)
| m1_group_2(X2,X0) ),
inference(cnf_transformation,[],[f156]) ).
fof(f335,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(f336,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(f337,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(f338,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,[],[f168]) ).
fof(f339,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,[],[f168]) ).
fof(f346,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(f348,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(f365,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(f367,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_6(X2,X0,X1)
| m1_group_2(X2,X1) ),
inference(cnf_transformation,[],[f241]) ).
fof(f368,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,[],[f241]) ).
fof(f369,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f242]) ).
fof(f371,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)
| ~ r1_group_2(X0,X1,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f243]) ).
fof(f374,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,[],[f244]) ).
fof(f379,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)
| ~ m1_group_2(X2,X1)
| r1_group_2(X0,k9_group_2(X0,X2,X1),X2) ),
inference(cnf_transformation,[],[f245]) ).
fof(f383,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,[],[f246]) ).
fof(f385,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(f387,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
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f247]) ).
fof(f393,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(f397,plain,
( ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_group_6(sK3,sK0,sK4) ),
inference(definition_unfolding,[],[f260,f258,f257]) ).
fof(f398,plain,
( r3_lattices(k11_group_4(sK0),sK3,sK4)
| m1_group_6(sK3,sK0,sK4) ),
inference(definition_unfolding,[],[f259,f258,f257]) ).
fof(f399,plain,
m1_group_2(sK4,sK0),
inference(definition_unfolding,[],[f254,f257]) ).
fof(f400,plain,
m1_group_2(sK3,sK0),
inference(definition_unfolding,[],[f253,f258]) ).
fof(f401,plain,
! [X0,X1,X8,X9,X7] :
( ~ 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)
| k10_group_4(X0) != X1
| ~ m1_subset_1(X8,k1_group_3(X0))
| ~ m1_subset_1(X7,k1_group_3(X0))
| ~ m1_group_2(X8,X0)
| ~ m1_group_2(X9,X0)
| X7 != X9
| k9_group_2(X0,X8,X9) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X8,X7) ),
inference(equality_resolution,[],[f275]) ).
fof(f402,plain,
! [X0,X1,X8,X9] :
( ~ 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)
| k10_group_4(X0) != X1
| ~ m1_subset_1(X8,k1_group_3(X0))
| ~ m1_subset_1(X9,k1_group_3(X0))
| ~ m1_group_2(X8,X0)
| ~ m1_group_2(X9,X0)
| k9_group_2(X0,X8,X9) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),X1,X8,X9) ),
inference(equality_resolution,[],[f401]) ).
fof(f403,plain,
! [X0,X8,X9] :
( ~ 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(X8,k1_group_3(X0))
| ~ m1_subset_1(X9,k1_group_3(X0))
| ~ m1_group_2(X8,X0)
| ~ m1_group_2(X9,X0)
| k9_group_2(X0,X8,X9) = k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X8,X9) ),
inference(equality_resolution,[],[f402]) ).
fof(f405,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,[],[f385]) ).
fof(f409,plain,
! [X2,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(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
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| r1_tarski(u1_struct_0(X3),u1_struct_0(X2)) ),
inference(equality_resolution,[],[f387]) ).
fof(f410,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)))
| ~ r3_lattices(k11_group_4(X0),X3,X4)
| r1_tarski(u1_struct_0(X3),u1_struct_0(X4)) ),
inference(equality_resolution,[],[f409]) ).
tcf(c_49,negated_conjecture,
( ~ m1_group_6(sK3,sK0,sK4)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(cnf_transformation,[],[f397]) ).
tcf(c_50,negated_conjecture,
( m1_group_6(sK3,sK0,sK4)
| r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(cnf_transformation,[],[f398]) ).
tcf(c_51,negated_conjecture,
m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0))),
inference(cnf_transformation,[],[f256]) ).
tcf(c_52,negated_conjecture,
m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0))),
inference(cnf_transformation,[],[f255]) ).
tcf(c_53,negated_conjecture,
m1_group_2(sK4,sK0),
inference(cnf_transformation,[],[f399]) ).
tcf(c_54,negated_conjecture,
m1_group_2(sK3,sK0),
inference(cnf_transformation,[],[f400]) ).
tcf(c_55,negated_conjecture,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f252]) ).
tcf(c_56,negated_conjecture,
v3_group_1(sK0),
inference(cnf_transformation,[],[f251]) ).
tcf(c_57,negated_conjecture,
v4_group_1(sK0),
inference(cnf_transformation,[],[f250]) ).
tcf(c_58,negated_conjecture,
l1_group_1(sK0),
inference(cnf_transformation,[],[f249]) ).
tcf(c_60,plain,
! [X0: $i] :
( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = X0 )
| ~ l3_lattices(X0)
| ~ v3_lattices(X0) ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| ( k4_lattices(X1,X0,X2) = k4_lattices(X1,X2,X0) )
| ~ l1_lattices(X1)
| ~ v6_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| ( k9_group_2(X1,X0,X2) = k9_group_2(X1,X2,X0) )
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X1,X2) = k9_group_2(X0,X1,X2) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_funct_1(k10_group_4(X0))
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,k1_group_3(X0))
| ~ m1_subset_1(X1,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))
| ~ 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,[],[f403]) ).
tcf(c_76,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0)) = k11_group_4(X0) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| ( k2_binop_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1),u1_lattices(X1),X0,X2) = k2_lattices(X1,X0,X2) )
| ~ l1_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_82,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_1(k10_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_83,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_84,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_85,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v3_struct_0(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_86,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_87,plain,
! [X0: $i] :
( v3_struct_0(X0)
| l3_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| v1_group_1(k9_group_2(X1,X0,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| m1_group_2(k9_group_2(X1,X0,X2),X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_95,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_1(k9_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_96,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_97,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_101,plain,
! [X0: $i] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_6(X0,X1,X2) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_128,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v3_struct_0(k11_group_4(X0)) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_129,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_130,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v6_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_131,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v8_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f336]) ).
tcf(c_132,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v9_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X0 = X3 )
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) ) ),
inference(cnf_transformation,[],[f348]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X2 = X5 )
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ( g3_lattices(X0,X1,X2) != g3_lattices(X3,X4,X5) ) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| ( k4_lattices(X1,X0,X2) = k2_lattices(X1,X0,X2) )
| ~ l1_lattices(X1)
| ~ v6_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f365]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| m1_group_6(X2,X1,X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f368]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| m1_group_2(X0,X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_6(X0,X1,X2) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_165,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( X1 = X2 )
| ~ v1_group_1(X2)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ r1_group_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f371]) ).
tcf(c_166,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r3_lattices(X0,X1,X2)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r1_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| r1_group_2(X1,k9_group_2(X1,X2,X0),X2)
| ~ v1_group_1(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f379]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_lattices(X0,X1,X2)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( k2_lattices(X0,X1,X2) != X1 ) ),
inference(cnf_transformation,[],[f383]) ).
tcf(c_177,plain,
! [X0: $i,X1: $i] :
( v1_group_1(X0)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(X1))) ),
inference(cnf_transformation,[],[f405]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ r3_lattices(k11_group_4(X0),X1,X2) ),
inference(cnf_transformation,[],[f410]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| m1_group_2(X0,X1)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X2)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f393]) ).
tcf(c_234,plain,
( v3_struct_0(sK0)
| v6_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_235,plain,
( v3_struct_0(sK0)
| v3_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_236,plain,
( v3_struct_0(sK0)
| v1_funct_1(k9_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_237,plain,
( v3_struct_0(sK0)
| l3_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_238,plain,
( v3_struct_0(sK0)
| v1_funct_1(k10_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_240,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(k11_group_4(sK0)) ),
inference(instantiation,[status(thm)],[c_128]) ).
tcf(c_246,plain,
( v3_struct_0(sK0)
| m2_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_247,plain,
( v3_struct_0(sK0)
| v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_248,plain,
( v3_struct_0(sK0)
| m2_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_249,plain,
( v3_struct_0(sK0)
| v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_254,plain,
( v3_struct_0(sK0)
| ( g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)) = k11_group_4(sK0) )
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_293,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X1,X2) = k9_group_2(X0,X1,X2) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X1,k1_group_3(X0))
| ~ m1_subset_1(X2,k1_group_3(X0))
| ~ m1_group_2(X1,X0)
| ~ m1_group_2(X2,X0) ),
inference(global_subsumption_just,[status(thm)],[c_75,c_82,c_84,c_83,c_75]) ).
tcf(c_294,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| ( k2_binop_1(k1_group_3(X1),k1_group_3(X1),k1_group_3(X1),k10_group_4(X1),X0,X2) = k9_group_2(X1,X0,X2) )
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X1)
| ~ m1_subset_1(X2,k1_group_3(X1))
| ~ m1_subset_1(X0,k1_group_3(X1)) ),
inference(renaming,[status(thm)],[c_293]) ).
tcf(c_296,plain,
( ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_group_6(sK3,sK0,sK4) ),
inference(prop_impl_just,[status(thm)],[c_49]) ).
tcf(c_297,plain,
( ~ m1_group_6(sK3,sK0,sK4)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(renaming,[status(thm)],[c_296]) ).
tcf(c_298,plain,
( r3_lattices(k11_group_4(sK0),sK3,sK4)
| m1_group_6(sK3,sK0,sK4) ),
inference(prop_impl_just,[status(thm)],[c_50]) ).
tcf(c_299,plain,
( m1_group_6(sK3,sK0,sK4)
| r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(renaming,[status(thm)],[c_298]) ).
tcf(c_316,plain,
! [X0: $i] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(prop_impl_just,[status(thm)],[c_101]) ).
tcf(c_2751,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X3)
| v3_struct_0(X0)
| r1_lattices(X0,X1,X2)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ l1_group_1(X3)
| ~ v4_group_1(X3)
| ~ v3_group_1(X3)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( k11_group_4(X3) != X0 )
| ( k2_lattices(X0,X1,X2) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_131,c_175]) ).
tcf(c_2752,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v3_struct_0(k11_group_4(X0))
| r1_lattices(k11_group_4(X0),X1,X2)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v9_lattices(k11_group_4(X0))
| ~ l3_lattices(k11_group_4(X0))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ( k2_lattices(k11_group_4(X0),X1,X2) != X1 ) ),
inference(unflattening,[status(thm)],[c_2751]) ).
tcf(c_2754,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k2_lattices(k11_group_4(X0),X1,X2) != X1 )
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| r1_lattices(k11_group_4(X0),X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_2752,c_132,c_87,c_128,c_2752]) ).
tcf(c_2755,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_lattices(k11_group_4(X0),X1,X2)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ( k2_lattices(k11_group_4(X0),X1,X2) != X1 ) ),
inference(renaming,[status(thm)],[c_2754]) ).
tcf(c_2811,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r3_lattices(X1,X2,X3)
| ~ v9_lattices(X1)
| ~ v6_lattices(X1)
| ~ l3_lattices(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ r1_lattices(X1,X2,X3)
| ( k11_group_4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_131,c_166]) ).
tcf(c_2812,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v3_struct_0(k11_group_4(X0))
| r3_lattices(k11_group_4(X0),X1,X2)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v9_lattices(k11_group_4(X0))
| ~ v6_lattices(k11_group_4(X0))
| ~ l3_lattices(k11_group_4(X0))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ r1_lattices(k11_group_4(X0),X1,X2) ),
inference(unflattening,[status(thm)],[c_2811]) ).
tcf(c_2814,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ r1_lattices(k11_group_4(X0),X1,X2)
| ~ v3_group_1(X0)
| ~ v4_group_1(X0)
| ~ l1_group_1(X0)
| r3_lattices(k11_group_4(X0),X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_2812,c_132,c_130,c_87,c_128,c_2812]) ).
tcf(c_2815,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r3_lattices(k11_group_4(X0),X1,X2)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ r1_lattices(k11_group_4(X0),X1,X2) ),
inference(renaming,[status(thm)],[c_2814]) ).
tcf(c_3514,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| m1_group_2(X0,X2)
| r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ( X2 != sK4 )
| ( X1 != sK0 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_299,c_161]) ).
tcf(c_3515,plain,
( v3_struct_0(sK0)
| m1_group_2(sK3,sK4)
| r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(sK4,sK0) ),
inference(unflattening,[status(thm)],[c_3514]) ).
tcf(c_3516,plain,
( r3_lattices(k11_group_4(sK0),sK3,sK4)
| m1_group_2(sK3,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3515,c_58,c_57,c_56,c_55,c_53,c_3515]) ).
tcf(c_3517,plain,
( m1_group_2(sK3,sK4)
| r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(renaming,[status(thm)],[c_3516]) ).
tcf(c_3536,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X2)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| ( X2 != sK4 )
| ( X1 != sK0 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_297,c_160]) ).
tcf(c_3537,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK3,sK4)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(unflattening,[status(thm)],[c_3536]) ).
tcf(c_3538,plain,
( ~ r3_lattices(k11_group_4(sK0),sK3,sK4)
| ~ m1_group_2(sK3,sK4) ),
inference(global_subsumption_just,[status(thm)],[c_3537,c_58,c_57,c_56,c_55,c_53,c_3537]) ).
tcf(c_3539,plain,
( ~ m1_group_2(sK3,sK4)
| ~ r3_lattices(k11_group_4(sK0),sK3,sK4) ),
inference(renaming,[status(thm)],[c_3538]) ).
tcf(c_3589,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( v3_struct_0(X3)
| v3_struct_0(X2)
| m1_group_2(X0,X2)
| ~ l1_group_1(X3)
| ~ l1_group_1(X2)
| ~ v4_group_1(X3)
| ~ v4_group_1(X2)
| ~ v3_group_1(X3)
| ~ v3_group_1(X2)
| ~ m1_group_2(X5,X3)
| ~ m1_group_2(X4,X2)
| ~ m1_group_2(X1,X5)
| ( X4 != X5 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_106,c_160]) ).
tcf(c_3590,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| m1_group_2(X0,X2)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2)
| ~ m1_group_2(X1,X2)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_3589]) ).
tcf(c_3636,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| r1_group_2(X1,k9_group_2(X1,X2,X0),X2)
| ~ v1_group_1(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_173,c_3590]) ).
tcf(c_3856,plain,
! [X0: $i,X1: $i] :
( l1_lattices(X1)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ( k11_group_4(X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_316,c_87]) ).
tcf(c_3857,plain,
! [X0: $i] :
( v3_struct_0(X0)
| l1_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(unflattening,[status(thm)],[c_3856]) ).
tcf(c_3858,plain,
( v3_struct_0(sK0)
| l1_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_3857]) ).
tcf(c_4979,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r3_lattices(k11_group_4(X0),X1,X2)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ r1_lattices(k11_group_4(X0),X1,X2)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_2815]) ).
tcf(c_4980,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| r3_lattices(k11_group_4(sK0),X0,X1)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ r1_lattices(k11_group_4(sK0),X0,X1) ),
inference(unflattening,[status(thm)],[c_4979]) ).
tcf(c_4982,plain,
! [X0: $i,X1: $i] :
( ~ r1_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)))
| r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_4980,c_58,c_56,c_55,c_4980]) ).
tcf(c_4983,plain,
! [X0: $i,X1: $i] :
( r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ r1_lattices(k11_group_4(sK0),X0,X1) ),
inference(renaming,[status(thm)],[c_4982]) ).
tcf(c_5015,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_lattices(k11_group_4(X0),X1,X2)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ( X0 != sK0 )
| ( k2_lattices(k11_group_4(X0),X1,X2) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_2755]) ).
tcf(c_5016,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| r1_lattices(k11_group_4(sK0),X0,X1)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( k2_lattices(k11_group_4(sK0),X0,X1) != X0 ) ),
inference(unflattening,[status(thm)],[c_5015]) ).
tcf(c_5018,plain,
! [X0: $i,X1: $i] :
( ( k2_lattices(k11_group_4(sK0),X0,X1) != X0 )
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| r1_lattices(k11_group_4(sK0),X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5016,c_58,c_56,c_55,c_5016]) ).
tcf(c_5019,plain,
! [X0: $i,X1: $i] :
( r1_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( k2_lattices(k11_group_4(sK0),X0,X1) != X0 ) ),
inference(renaming,[status(thm)],[c_5018]) ).
tcf(c_5051,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ~ r3_lattices(k11_group_4(X0),X1,X2)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_180]) ).
tcf(c_5052,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(unflattening,[status(thm)],[c_5051]) ).
tcf(c_5054,plain,
! [X0: $i,X1: $i] :
( ~ 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)))
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_5052,c_58,c_56,c_55,c_5052]) ).
tcf(c_5055,plain,
! [X0: $i,X1: $i] :
( r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ r3_lattices(k11_group_4(sK0),X0,X1) ),
inference(renaming,[status(thm)],[c_5054]) ).
tcf(c_5116,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( X1 = X2 )
| ~ v1_group_1(X2)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ r1_group_2(X0,X1,X2)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_165]) ).
tcf(c_5117,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| ( X0 = X1 )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(X1)
| ~ v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_group_2(sK0,X0,X1) ),
inference(unflattening,[status(thm)],[c_5116]) ).
tcf(c_5119,plain,
! [X0: $i,X1: $i] :
( ~ r1_group_2(sK0,X0,X1)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ v1_group_1(X0)
| ~ v1_group_1(X1)
| ( X0 = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_5117,c_58,c_56,c_55,c_5117]) ).
tcf(c_5120,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ v1_group_1(X1)
| ~ v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_group_2(sK0,X0,X1) ),
inference(renaming,[status(thm)],[c_5119]) ).
tcf(c_5140,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v6_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_130]) ).
tcf(c_5141,plain,
( v3_struct_0(sK0)
| v6_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5140]) ).
tcf(c_5142,plain,
v6_lattices(k11_group_4(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5141,c_58,c_57,c_56,c_55,c_234]) ).
tcf(c_5154,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_97]) ).
tcf(c_5155,plain,
( v3_struct_0(sK0)
| m2_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5154]) ).
tcf(c_5156,plain,
m2_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5155,c_58,c_57,c_56,c_55,c_246]) ).
tcf(c_5161,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_96]) ).
tcf(c_5162,plain,
( v3_struct_0(sK0)
| v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5161]) ).
tcf(c_5163,plain,
v1_funct_2(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5162,c_58,c_57,c_56,c_55,c_247]) ).
tcf(c_5168,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_1(k9_group_4(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_95]) ).
tcf(c_5169,plain,
( v3_struct_0(sK0)
| v1_funct_1(k9_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5168]) ).
tcf(c_5170,plain,
v1_funct_1(k9_group_4(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5169,c_58,c_57,c_56,c_55,c_236]) ).
tcf(c_5175,plain,
! [X0: $i] :
( v3_struct_0(X0)
| l3_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_87]) ).
tcf(c_5176,plain,
( v3_struct_0(sK0)
| l3_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5175]) ).
tcf(c_5177,plain,
l3_lattices(k11_group_4(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5176,c_58,c_57,c_56,c_55,c_237]) ).
tcf(c_5182,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_lattices(k11_group_4(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_86]) ).
tcf(c_5183,plain,
( v3_struct_0(sK0)
| v3_lattices(k11_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5182]) ).
tcf(c_5184,plain,
v3_lattices(k11_group_4(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5183,c_58,c_57,c_56,c_55,c_235]) ).
tcf(c_5189,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v3_struct_0(k11_group_4(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_85]) ).
tcf(c_5190,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(k11_group_4(sK0)) ),
inference(unflattening,[status(thm)],[c_5189]) ).
tcf(c_5191,plain,
~ v3_struct_0(k11_group_4(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5190,c_58,c_57,c_56,c_55,c_240]) ).
tcf(c_5196,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_84]) ).
tcf(c_5197,plain,
( v3_struct_0(sK0)
| m2_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5196]) ).
tcf(c_5198,plain,
m2_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5197,c_58,c_57,c_56,c_55,c_248]) ).
tcf(c_5203,plain,
! [X0: $i] :
( 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))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_83]) ).
tcf(c_5204,plain,
( v3_struct_0(sK0)
| v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5203]) ).
tcf(c_5205,plain,
v1_funct_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5204,c_58,c_57,c_56,c_55,c_249]) ).
tcf(c_5210,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_1(k10_group_4(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_82]) ).
tcf(c_5211,plain,
( v3_struct_0(sK0)
| v1_funct_1(k10_group_4(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5210]) ).
tcf(c_5212,plain,
v1_funct_1(k10_group_4(sK0)),
inference(global_subsumption_just,[status(thm)],[c_5211,c_58,c_57,c_56,c_55,c_238]) ).
tcf(c_5217,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( g3_lattices(k1_group_3(X0),k9_group_4(X0),k10_group_4(X0)) = k11_group_4(X0) )
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_76]) ).
tcf(c_5218,plain,
( v3_struct_0(sK0)
| ( g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)) = k11_group_4(sK0) )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_5217]) ).
tcf(c_5219,plain,
g3_lattices(k1_group_3(sK0),k9_group_4(sK0),k10_group_4(sK0)) = k11_group_4(sK0),
inference(global_subsumption_just,[status(thm)],[c_5218,c_58,c_57,c_56,c_55,c_254]) ).
tcf(c_5245,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r1_group_2(X0,k9_group_2(X0,X2,X1),X2)
| ~ v1_group_1(X2)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_3636]) ).
tcf(c_5246,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| r1_group_2(sK0,k9_group_2(sK0,X0,X1),X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_5245]) ).
tcf(c_5248,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ v1_group_1(X0)
| r1_group_2(sK0,k9_group_2(sK0,X0,X1),X0) ),
inference(global_subsumption_just,[status(thm)],[c_5246,c_58,c_56,c_55,c_5246]) ).
tcf(c_5249,plain,
! [X0: $i,X1: $i] :
( r1_group_2(sK0,k9_group_2(sK0,X0,X1),X0)
| ~ v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_5248]) ).
tcf(c_5300,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k2_binop_1(k1_group_3(X0),k1_group_3(X0),k1_group_3(X0),k10_group_4(X0),X1,X2) = k9_group_2(X0,X1,X2) )
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X2,k1_group_3(X0))
| ~ m1_subset_1(X1,k1_group_3(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_294]) ).
tcf(c_5301,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| ( k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) = k9_group_2(sK0,X0,X1) )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_subset_1(X0,k1_group_3(sK0)) ),
inference(unflattening,[status(thm)],[c_5300]) ).
tcf(c_5303,plain,
! [X0: $i,X1: $i] :
( ~ 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)
| ( k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) = k9_group_2(sK0,X0,X1) ) ),
inference(global_subsumption_just,[status(thm)],[c_5301,c_58,c_56,c_55,c_5301]) ).
tcf(c_5304,plain,
! [X0: $i,X1: $i] :
( ( k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,X1) = k9_group_2(sK0,X0,X1) )
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X1,k1_group_3(sK0))
| ~ m1_subset_1(X0,k1_group_3(sK0)) ),
inference(renaming,[status(thm)],[c_5303]) ).
tcf(c_5345,plain,
! [X0: $i,X1: $i] :
( v1_group_1(X1)
| v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X0)))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_177]) ).
tcf(c_5346,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v1_group_1(X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(unflattening,[status(thm)],[c_5345]) ).
tcf(c_5348,plain,
! [X0: $i] :
( ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ~ m1_group_2(X0,sK0)
| v1_group_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5346,c_58,c_56,c_55,c_5346]) ).
tcf(c_5349,plain,
! [X0: $i] :
( v1_group_1(X0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(renaming,[status(thm)],[c_5348]) ).
tcf(c_5390,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| m1_group_2(k9_group_2(X0,X1,X2),X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_94]) ).
tcf(c_5391,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| m1_group_2(k9_group_2(sK0,X0,X1),sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_5390]) ).
tcf(c_5393,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| m1_group_2(k9_group_2(sK0,X0,X1),sK0) ),
inference(global_subsumption_just,[status(thm)],[c_5391,c_58,c_56,c_55,c_5391]) ).
tcf(c_5394,plain,
! [X0: $i,X1: $i] :
( m1_group_2(k9_group_2(sK0,X0,X1),sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_5393]) ).
tcf(c_5405,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v1_group_1(k9_group_2(X0,X1,X2))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_93]) ).
tcf(c_5406,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v1_group_1(k9_group_2(sK0,X0,X1))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_5405]) ).
tcf(c_5408,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| v1_group_1(k9_group_2(sK0,X0,X1)) ),
inference(global_subsumption_just,[status(thm)],[c_5406,c_58,c_56,c_55,c_5406]) ).
tcf(c_5409,plain,
! [X0: $i,X1: $i] :
( v1_group_1(k9_group_2(sK0,X0,X1))
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_5408]) ).
tcf(c_5576,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k9_group_2(X0,X1,X2) = k9_group_2(X0,X2,X1) )
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_67]) ).
tcf(c_5577,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| ( k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_5576]) ).
tcf(c_5579,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ( k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_5577,c_58,c_56,c_55,c_5577]) ).
tcf(c_5580,plain,
! [X0: $i,X1: $i] :
( ( k9_group_2(sK0,X0,X1) = k9_group_2(sK0,X1,X0) )
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_5579]) ).
tcf(c_5591,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| m1_group_2(X1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X2)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_3590]) ).
tcf(c_5592,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| m1_group_2(X0,sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_5591]) ).
tcf(c_5593,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| m1_group_2(X0,sK0) ),
inference(global_subsumption_just,[status(thm)],[c_5592,c_58,c_56,c_55,c_5592]) ).
tcf(c_5594,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_5593]) ).
tcf(c_5604,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| m1_group_2(X1,X2)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X0)
| ~ m1_group_2(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X2))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_57,c_185]) ).
tcf(c_5605,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(unflattening,[status(thm)],[c_5604]) ).
tcf(c_5606,plain,
! [X0: $i,X1: $i] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| m1_group_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_5605,c_58,c_56,c_55,c_5605]) ).
tcf(c_5607,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(renaming,[status(thm)],[c_5606]) ).
tcf(c_5799,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2) )
| ~ l1_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( k11_group_4(sK0) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_158,c_5142]) ).
tcf(c_5800,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(k11_group_4(sK0))
| ( k4_lattices(k11_group_4(sK0),X0,X1) = k2_lattices(k11_group_4(sK0),X0,X1) )
| ~ l1_lattices(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(unflattening,[status(thm)],[c_5799]) ).
tcf(c_5802,plain,
! [X0: $i,X1: $i] :
( ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( k4_lattices(k11_group_4(sK0),X0,X1) = k2_lattices(k11_group_4(sK0),X0,X1) ) ),
inference(global_subsumption_just,[status(thm)],[c_5800,c_58,c_57,c_56,c_55,c_240,c_3858,c_5800]) ).
tcf(c_5803,plain,
! [X0: $i,X1: $i] :
( ( k4_lattices(k11_group_4(sK0),X0,X1) = k2_lattices(k11_group_4(sK0),X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(renaming,[status(thm)],[c_5802]) ).
tcf(c_5829,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ( k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1) )
| ~ l1_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( k11_group_4(sK0) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_5142]) ).
tcf(c_5830,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(k11_group_4(sK0))
| ( k4_lattices(k11_group_4(sK0),X0,X1) = k4_lattices(k11_group_4(sK0),X1,X0) )
| ~ l1_lattices(k11_group_4(sK0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(unflattening,[status(thm)],[c_5829]) ).
tcf(c_5832,plain,
! [X0: $i,X1: $i] :
( ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( k4_lattices(k11_group_4(sK0),X0,X1) = k4_lattices(k11_group_4(sK0),X1,X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_5830,c_58,c_57,c_56,c_55,c_240,c_3858,c_5830]) ).
tcf(c_5833,plain,
! [X0: $i,X1: $i] :
( ( k4_lattices(k11_group_4(sK0),X0,X1) = k4_lattices(k11_group_4(sK0),X1,X0) )
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(renaming,[status(thm)],[c_5832]) ).
tcf(c_5855,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r3_lattices(k11_group_4(sK0),X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( X1 != X3 )
| ( X0 != X2 )
| ( k11_group_4(sK0) != k11_group_4(sK0) )
| ( k2_lattices(k11_group_4(sK0),X0,X1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_5019,c_4983]) ).
tcf(c_5856,plain,
! [X0: $i,X1: $i] :
( r3_lattices(k11_group_4(sK0),X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( k2_lattices(k11_group_4(sK0),X0,X1) != X0 ) ),
inference(unflattening,[status(thm)],[c_5855]) ).
tcf(c_6649,plain,
! [X0: $i,X1: $i] :
( m1_group_2(sK3,sK4)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( X1 != sK4 )
| ( X0 != sK3 )
| ( k11_group_4(sK0) != k11_group_4(sK0) ) ),
inference(resolution_lifted,[status(thm)],[c_3517,c_5055]) ).
tcf(c_6650,plain,
( m1_group_2(sK3,sK4)
| r1_tarski(u1_struct_0(sK3),u1_struct_0(sK4))
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK3,sK0)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0))) ),
inference(unflattening,[status(thm)],[c_6649]) ).
tcf(c_6651,plain,
( m1_group_2(sK3,sK4)
| r1_tarski(u1_struct_0(sK3),u1_struct_0(sK4)) ),
inference(global_subsumption_just,[status(thm)],[c_6650,c_54,c_53,c_52,c_51,c_6650]) ).
tcf(c_6659,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(sK3,sK4)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0)))
| ( X1 != sK4 )
| ( X0 != sK3 )
| ( k11_group_4(sK0) != k11_group_4(sK0) )
| ( k2_lattices(k11_group_4(sK0),X0,X1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_3539,c_5856]) ).
tcf(c_6660,plain,
( ~ m1_group_2(sK3,sK4)
| ~ m1_subset_1(sK4,u1_struct_0(k11_group_4(sK0)))
| ~ m1_subset_1(sK3,u1_struct_0(k11_group_4(sK0)))
| ( k2_lattices(k11_group_4(sK0),sK3,sK4) != sK3 ) ),
inference(unflattening,[status(thm)],[c_6659]) ).
tcf(c_12638,plain,
( r1_tarski(u1_struct_0(sK3),u1_struct_0(sK4))
| m1_group_2(sK3,sK4) ),
inference(prop_impl_just,[status(thm)],[c_6651]) ).
tcf(c_12639,plain,
( m1_group_2(sK3,sK4)
| r1_tarski(u1_struct_0(sK3),u1_struct_0(sK4)) ),
inference(renaming,[status(thm)],[c_12638]) ).
tcf(c_12640,plain,
( ( k2_lattices(k11_group_4(sK0),sK3,sK4) != sK3 )
| ~ m1_group_2(sK3,sK4) ),
inference(prop_impl_just,[status(thm)],[c_52,c_51,c_6660]) ).
tcf(c_12641,plain,
( ~ m1_group_2(sK3,sK4)
| ( k2_lattices(k11_group_4(sK0),sK3,sK4) != sK3 ) ),
inference(renaming,[status(thm)],[c_12640]) ).
tcf(c_27560,plain,
! [X0: $i] :
( v3_struct_0(k11_group_4(sK0))
| ( 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,X0) = k2_lattices(k11_group_4(sK0),sK4,X0) )
| ~ l1_lattices(k11_group_4(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(superposition,[status(thm)],[c_51,c_77]) ).
tcf(c_27564,plain,
! [X0: $i] :
( ( 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,X0) = k2_lattices(k11_group_4(sK0),sK4,X0) )
| ~ l1_lattices(k11_group_4(sK0))
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27560,c_5191]) ).
tcf(c_27663,plain,
( ( g3_lattices(u1_struct_0(k11_group_4(sK0)),u2_lattices(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0))) = k11_group_4(sK0) )
| ~ l3_lattices(k11_group_4(sK0)) ),
inference(superposition,[status(thm)],[c_5184,c_60]) ).
tcf(c_27741,plain,
l1_lattices(k11_group_4(sK0)),
inference(superposition,[status(thm)],[c_5177,c_101]) ).
tcf(c_27955,plain,
m1_relset_1(k9_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)),
inference(superposition,[status(thm)],[c_5156,c_163]) ).
tcf(c_27966,plain,
m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)),
inference(superposition,[status(thm)],[c_5198,c_163]) ).
tcf(c_27977,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k10_group_4(sK0) = X2 )
| ~ v1_funct_1(k9_group_4(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))
| ~ m1_relset_1(k10_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_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ( g3_lattices(X0,X1,X2) != k11_group_4(sK0) ) ),
inference(superposition,[status(thm)],[c_5219,c_141]) ).
tcf(c_27979,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k1_group_3(sK0) = X0 )
| ~ v1_funct_1(k9_group_4(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))
| ~ m1_relset_1(k10_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_2(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0))
| ( g3_lattices(X0,X1,X2) != k11_group_4(sK0) ) ),
inference(superposition,[status(thm)],[c_5219,c_139]) ).
tcf(c_27983,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k1_group_3(sK0) = X0 )
| ~ m1_relset_1(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))
| ( g3_lattices(X0,X1,X2) != k11_group_4(sK0) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27979,c_5170,c_5212,c_5163,c_5205]) ).
tcf(c_27985,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k10_group_4(sK0) = X2 )
| ~ m1_relset_1(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))
| ( g3_lattices(X0,X1,X2) != k11_group_4(sK0) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27977,c_5170,c_5212,c_5163,c_5205]) ).
tcf(c_27996,plain,
! [X0: $i,X1: $i] :
( ( k9_group_2(sK0,X0,X1) = X0 )
| ~ v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,X1)
| ~ v1_group_1(k9_group_2(sK0,X0,X1))
| ~ m1_group_2(k9_group_2(sK0,X0,X1),sK0) ),
inference(superposition,[status(thm)],[c_5249,c_5120]) ).
tcf(c_28002,plain,
( v1_group_1(sK3)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_52,c_5349]) ).
tcf(c_28007,plain,
v1_group_1(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_28002,c_54]) ).
tcf(c_28112,plain,
! [X0: $i] :
( ( k9_group_2(sK0,X0,sK4) = k9_group_2(sK0,sK4,X0) )
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_53,c_5580]) ).
tcf(c_28203,plain,
! [X0: $i] :
( ( k4_lattices(k11_group_4(sK0),X0,sK4) = k2_lattices(k11_group_4(sK0),X0,sK4) )
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(superposition,[status(thm)],[c_51,c_5803]) ).
tcf(c_28204,plain,
! [X0: $i] :
( ( k4_lattices(k11_group_4(sK0),X0,sK3) = k2_lattices(k11_group_4(sK0),X0,sK3) )
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(superposition,[status(thm)],[c_52,c_5803]) ).
tcf(c_28213,plain,
! [X0: $i] :
( ( k4_lattices(k11_group_4(sK0),X0,sK4) = k4_lattices(k11_group_4(sK0),sK4,X0) )
| ~ m1_subset_1(X0,u1_struct_0(k11_group_4(sK0))) ),
inference(superposition,[status(thm)],[c_51,c_5833]) ).
tcf(c_28238,plain,
( m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_12639,c_5607]) ).
tcf(c_28240,plain,
m1_group_2(sK3,sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_28238,c_53,c_54]) ).
tcf(c_28329,plain,
( ( 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) = k2_lattices(k11_group_4(sK0),sK4,sK3) )
| ~ l1_lattices(k11_group_4(sK0)) ),
inference(superposition,[status(thm)],[c_52,c_27564]) ).
tcf(c_28334,plain,
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) = k2_lattices(k11_group_4(sK0),sK4,sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_28329,c_27741]) ).
tcf(c_28392,plain,
g3_lattices(u1_struct_0(k11_group_4(sK0)),u2_lattices(k11_group_4(sK0)),u1_lattices(k11_group_4(sK0))) = k11_group_4(sK0),
inference(superposition,[status(thm)],[c_5177,c_27663]) ).
tcf(c_29021,plain,
! [X0: $i,X1: $i] :
( ( k9_group_2(sK0,X0,X1) = X0 )
| ~ v1_group_1(X0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_27996,c_5594,c_5409,c_5394]) ).
tcf(c_29034,plain,
( ( k9_group_2(sK0,sK3,sK4) = sK3 )
| ~ v1_group_1(sK3)
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_28240,c_29021]) ).
tcf(c_29050,plain,
k9_group_2(sK0,sK3,sK4) = sK3,
inference(forward_subsumption_resolution,[status(thm)],[c_29034,c_28007,c_53]) ).
tcf(c_29395,plain,
k9_group_2(sK0,sK3,sK4) = k9_group_2(sK0,sK4,sK3),
inference(superposition,[status(thm)],[c_54,c_28112]) ).
tcf(c_29404,plain,
k9_group_2(sK0,sK4,sK3) = sK3,
inference(demodulation,[status(thm)],[c_29395,c_29050]) ).
tcf(c_29586,plain,
k4_lattices(k11_group_4(sK0),sK3,sK4) = k2_lattices(k11_group_4(sK0),sK3,sK4),
inference(superposition,[status(thm)],[c_52,c_28203]) ).
tcf(c_29596,plain,
k4_lattices(k11_group_4(sK0),sK4,sK3) = k2_lattices(k11_group_4(sK0),sK4,sK3),
inference(superposition,[status(thm)],[c_51,c_28204]) ).
tcf(c_29661,plain,
k4_lattices(k11_group_4(sK0),sK3,sK4) = k4_lattices(k11_group_4(sK0),sK4,sK3),
inference(superposition,[status(thm)],[c_52,c_28213]) ).
tcf(c_29667,plain,
k2_lattices(k11_group_4(sK0),sK3,sK4) = k2_lattices(k11_group_4(sK0),sK4,sK3),
inference(demodulation,[status(thm)],[c_29661,c_29586,c_29596]) ).
tcf(c_30260,plain,
( ( u1_lattices(k11_group_4(sK0)) = 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))
| ~ m1_relset_1(k10_group_4(sK0),k2_zfmisc_1(k1_group_3(sK0),k1_group_3(sK0)),k1_group_3(sK0)) ),
inference(superposition,[status(thm)],[c_28392,c_27985]) ).
tcf(c_30262,plain,
( ( u1_struct_0(k11_group_4(sK0)) = k1_group_3(sK0) )
| ~ m1_relset_1(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)) ),
inference(superposition,[status(thm)],[c_28392,c_27983]) ).
tcf(c_30272,plain,
u1_struct_0(k11_group_4(sK0)) = k1_group_3(sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_30262,c_27955,c_27966]) ).
tcf(c_30274,plain,
u1_lattices(k11_group_4(sK0)) = k10_group_4(sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_30260,c_27955,c_27966]) ).
tcf(c_30404,plain,
k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),u1_lattices(k11_group_4(sK0)),sK4,sK3) = k2_lattices(k11_group_4(sK0),sK4,sK3),
inference(superposition,[status(thm)],[c_30272,c_28334]) ).
tcf(c_30441,plain,
m1_subset_1(sK3,k1_group_3(sK0)),
inference(superposition,[status(thm)],[c_30272,c_52]) ).
tcf(c_30442,plain,
m1_subset_1(sK4,k1_group_3(sK0)),
inference(superposition,[status(thm)],[c_30272,c_51]) ).
tcf(c_30529,plain,
k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3) = k2_lattices(k11_group_4(sK0),sK4,sK3),
inference(demodulation,[status(thm)],[c_30404,c_30274]) ).
tcf(c_30611,plain,
! [X0: $i] :
( ( k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,sK3) = k9_group_2(sK0,X0,sK3) )
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X0,k1_group_3(sK0)) ),
inference(superposition,[status(thm)],[c_30441,c_5304]) ).
tcf(c_30612,plain,
! [X0: $i] :
( ( k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),X0,sK3) = k9_group_2(sK0,X0,sK3) )
| ~ m1_group_2(X0,sK0)
| ~ m1_subset_1(X0,k1_group_3(sK0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30611,c_54]) ).
tcf(c_36277,plain,
( ~ m1_group_2(sK3,sK4)
| ( k2_lattices(k11_group_4(sK0),sK4,sK3) != sK3 ) ),
inference(superposition,[status(thm)],[c_29667,c_12641]) ).
tcf(c_36278,plain,
k2_lattices(k11_group_4(sK0),sK4,sK3) != sK3,
inference(forward_subsumption_resolution,[status(thm)],[c_36277,c_28240]) ).
tcf(c_54775,plain,
( ( k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3) = k9_group_2(sK0,sK4,sK3) )
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_30442,c_30612]) ).
tcf(c_54787,plain,
k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3) = k9_group_2(sK0,sK4,sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_54775,c_53]) ).
tcf(c_54788,plain,
k2_binop_1(k1_group_3(sK0),k1_group_3(sK0),k1_group_3(sK0),k10_group_4(sK0),sK4,sK3) = sK3,
inference(demodulation,[status(thm)],[c_54787,c_29404]) ).
tcf(c_55589,plain,
k2_lattices(k11_group_4(sK0),sK4,sK3) = sK3,
inference(superposition,[status(thm)],[c_54788,c_30529]) ).
tcf(c_55592,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_55589,c_36278]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP648+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 15:32:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 77.31/11.41 % SZS status Started for theBenchmark.p
% 77.31/11.41 % SZS status Theorem for theBenchmark.p
% 77.31/11.41
% 77.31/11.41 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 77.31/11.41
% 77.31/11.41 % ------ iProver source info
% 77.31/11.41
% 77.31/11.41 % git: date: 2026-07-19 20:42:38 +0200
% 77.31/11.41 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 77.31/11.41 % git: non_committed_changes: false
% 77.31/11.41
% 77.31/11.41 % ------ Parsing...
% 77.31/11.41 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 77.31/11.41
% 77.31/11.41 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 8 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 8 0s sf_e pe_s pe_e %
% 77.31/11.41
% 77.31/11.41 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 77.31/11.41
% 77.31/11.41 % ------ Preprocessing... sf_s rm: 2 0s sf_e sf_s rm: 0 0s sf_e
% 77.31/11.41 % ------ Proving...
% 77.31/11.41 % ------ Problem Properties
% 77.31/11.41
% 77.31/11.41 %
% 77.31/11.41 % clauses 134
% 77.31/11.41 % conjectures 7
% 77.31/11.41 % EPR 40
% 77.31/11.41 % Horn 113
% 77.31/11.41 % unary 43
% 77.31/11.41 % binary 33
% 77.31/11.41 % lits 368
% 77.31/11.41 % lits eq 42
% 77.31/11.41 % fd_pure 0
% 77.31/11.41 % fd_pseudo 0
% 77.31/11.41 % fd_cond 8
% 77.31/11.41 % fd_pseudo_cond 7
% 77.31/11.41 % AC symbols 0
% 77.31/11.41
% 77.31/11.41 % ------ Input Options Time Limit: Unbounded
% 77.31/11.41
% 77.31/11.41
% 77.31/11.41 % ------
% 77.31/11.41 % Current options:
% 77.31/11.41 % ------
% 77.31/11.41
% 77.31/11.41
% 77.31/11.41 %
% 77.31/11.41
% 77.31/11.41 % ------ Proving...
% 77.31/11.41 %
% 77.31/11.41
% 77.31/11.41 % SZS status Theorem for theBenchmark.p
% 77.31/11.41
% 77.31/11.41 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 77.31/11.42
% 77.31/11.42
%------------------------------------------------------------------------------