%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP637+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 : n008.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:34:57 PM UTC 2026
% Result : Theorem 3.89s 1.73s
% Output : CNFRefutation 3.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 57
% Syntax : Number of formulae : 801 ( 233 unt; 13 def)
% Number of atoms : 2943 ( 230 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 3086 (1379 ~;1468 |; 174 &)
% ( 8 <=>; 57 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 33 ( 31 usr; 14 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 13 con; 0-4 aty)
% Number of variables : 917 ( 1 sgn 881 !; 36 ?; 549 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_group_1(X1)
& v4_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( m1_group_6(X3,X0,X4)
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_latsubgr) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_group_1(X1)
& v4_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_group_6(X2,X0,X1)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( m1_group_6(X3,X0,X4)
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(f5,axiom,
! [X0,X1,X2] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
=> v1_relat_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f7,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X0) )
=> ! [X2] :
( m1_relset_1(X2,X0,X1)
=> ( ( v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> ( v1_funct_2(X2,X0,X1)
& v1_partfun1(X2,X0,X1)
& ~ v1_xboole_0(X2)
& v1_funct_1(X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc6_funct_2) ).
fof(f8,axiom,
! [X0] :
( ( l1_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) )
=> ( m1_group_2(X1,X0)
<=> ( u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_group_2) ).
fof(f12,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,X0,X1)
& v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_funct_2) ).
fof(f15,axiom,
! [X0] :
( l1_group_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_group_1) ).
fof(f17,axiom,
! [X0] :
( ( l1_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> ( l1_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_group_2) ).
fof(f18,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(f21,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
=> m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f22,axiom,
! [X0] :
( l1_group_1(X0)
=> ( m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_funct_1(u1_group_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_group_1) ).
fof(f24,axiom,
? [X0] : l1_group_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_l1_group_1) ).
fof(f25,axiom,
? [X0] : l1_struct_0(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_l1_struct_0) ).
fof(f26,axiom,
! [X0] :
( ( l1_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ? [X1] : m1_group_2(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_group_2) ).
fof(f27,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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_group_6) ).
fof(f28,axiom,
! [X0,X1] :
? [X2] : m1_relset_1(X2,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_relset_1) ).
fof(f29,axiom,
! [X0] :
? [X1] : m1_subset_1(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f30,axiom,
! [X0,X1] :
? [X2] : m2_relset_1(X2,X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m2_relset_1) ).
fof(f31,axiom,
! [X0] :
( ( l1_struct_0(X0)
& ~ v3_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f32,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f33,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f34,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X0) )
=> ~ v1_xboole_0(k2_zfmisc_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_subset_1) ).
fof(f35,axiom,
! [X0,X1] :
? [X2] :
( v1_funct_2(X2,X0,X1)
& v1_funct_1(X2)
& v1_relat_1(X2)
& m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_funct_2) ).
fof(f36,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ? [X1] :
( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(f37,axiom,
? [X0] : v1_xboole_0(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(f38,axiom,
! [X0,X1] :
? [X2] :
( v1_funct_1(X2)
& v1_relat_1(X2)
& m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_partfun1) ).
fof(f39,axiom,
! [X0] :
? [X1] :
( v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(f40,axiom,
? [X0] : ~ v1_xboole_0(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(f41,axiom,
? [X0] :
( ~ v3_struct_0(X0)
& l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(f42,axiom,
! [X0] :
( ( l1_struct_0(X0)
& ~ v3_struct_0(X0) )
=> ? [X1] :
( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc5_struct_0) ).
fof(f43,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,X0,X1)
& v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f44,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(f45,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(f46,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f47,axiom,
! [X0,X1,X2] :
( v1_relat_1(X2)
=> ( r1_tarski(X0,X1)
=> r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t156_relat_1) ).
fof(f48,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f49,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( r2_hidden(X0,X1)
| v1_xboole_0(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f50,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f51,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X2))
& r2_hidden(X0,X1) )
=> m1_subset_1(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(f52,axiom,
! [X0,X1,X2] :
~ ( v1_xboole_0(X2)
& m1_subset_1(X1,k1_zfmisc_1(X2))
& r2_hidden(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(f53,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(f54,axiom,
! [X0] :
( v1_xboole_0(X0)
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(f55,axiom,
! [X0,X1] :
~ ( v1_xboole_0(X1)
& r2_hidden(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f56,axiom,
! [X0,X1] :
~ ( v1_xboole_0(X1)
& X0 != X1
& v1_xboole_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(f57,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f46]) ).
fof(f58,plain,
~ ! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_group_1(X1)
& v4_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2) )
=> ! [X3] :
( m1_group_2(X3,X0)
=> ! [X4] :
( m1_group_2(X4,X0)
=> ! [X5] :
( m1_group_2(X5,X1)
=> ! [X6] :
( m1_group_2(X6,X1)
=> ( ( m1_group_6(X3,X0,X4)
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
=> m1_group_6(X5,X1,X6) ) ) ) ) ) ) ) ),
inference(pure_predicate_removal,[],[f2]) ).
fof(f59,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_group_1(X1)
& v4_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& ? [X3] :
( m1_group_2(X3,X0)
& ? [X4] :
( m1_group_2(X4,X0)
& ? [X5] :
( m1_group_2(X5,X1)
& ? [X6] :
( m1_group_2(X6,X1)
& m1_group_6(X3,X0,X4)
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& ~ m1_group_6(X5,X1,X6) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f58]) ).
fof(f60,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_group_1(X1)
& v4_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X2)
& ? [X3] :
( m1_group_2(X3,X0)
& ? [X4] :
( m1_group_2(X4,X0)
& ? [X5] :
( m1_group_2(X5,X1)
& ? [X6] :
( m1_group_2(X6,X1)
& m1_group_6(X3,X0,X4)
& u1_struct_0(X6) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k2_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& ~ m1_group_6(X5,X1,X6) ) ) ) ) ) ) ),
inference(flattening,[],[f59]) ).
fof(f61,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X1,X0) ),
inference(ennf_transformation,[],[f3]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ! [X2] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ( v1_funct_2(X2,X0,X1)
& v1_partfun1(X2,X0,X1)
& ~ v1_xboole_0(X2)
& v1_funct_1(X2) ) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f68,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ! [X2] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ( v1_funct_2(X2,X0,X1)
& v1_partfun1(X2,X0,X1)
& ~ v1_xboole_0(X2)
& v1_funct_1(X2) ) ) ),
inference(flattening,[],[f67]) ).
fof(f69,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ( m1_group_2(X1,X0)
<=> ( u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
inference(ennf_transformation,[],[f8]) ).
fof(f70,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ( m1_group_2(X1,X0)
<=> ( u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) ) ) ),
inference(flattening,[],[f69]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f12]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(flattening,[],[f71]) ).
fof(f73,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f74,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ( l1_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) ) ) ),
inference(ennf_transformation,[],[f17]) ).
fof(f75,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ( l1_group_1(X1)
& v3_group_1(X1)
& ~ v3_struct_0(X1) ) ) ),
inference(flattening,[],[f74]) ).
fof(f76,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,[],[f18]) ).
fof(f77,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,[],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(ennf_transformation,[],[f21]) ).
fof(f79,plain,
! [X0] :
( ~ l1_group_1(X0)
| ( m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
& v1_funct_1(u1_group_1(X0)) ) ),
inference(ennf_transformation,[],[f22]) ).
fof(f80,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ? [X1] : m1_group_2(X1,X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f81,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ? [X1] : m1_group_2(X1,X0) ),
inference(flattening,[],[f80]) ).
fof(f82,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) ),
inference(ennf_transformation,[],[f27]) ).
fof(f83,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) ),
inference(flattening,[],[f82]) ).
fof(f84,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f31]) ).
fof(f85,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(flattening,[],[f84]) ).
fof(f86,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(k2_zfmisc_1(X0,X1)) ),
inference(ennf_transformation,[],[f34]) ).
fof(f87,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(k2_zfmisc_1(X0,X1)) ),
inference(flattening,[],[f86]) ).
fof(f88,plain,
! [X0] :
( v1_xboole_0(X0)
| ? [X1] :
( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) ) ),
inference(ennf_transformation,[],[f36]) ).
fof(f89,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ? [X1] :
( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
inference(ennf_transformation,[],[f42]) ).
fof(f90,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ? [X1] :
( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
inference(flattening,[],[f89]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(flattening,[],[f91]) ).
fof(f93,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,[],[f44]) ).
fof(f94,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,[],[f93]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(ennf_transformation,[],[f47]) ).
fof(f96,plain,
! [X0,X1,X2] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(flattening,[],[f95]) ).
fof(f97,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f48]) ).
fof(f98,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f49]) ).
fof(f99,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(flattening,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(ennf_transformation,[],[f51]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f52]) ).
fof(f103,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,[],[f53]) ).
fof(f104,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,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| X0 = k1_xboole_0 ),
inference(ennf_transformation,[],[f54]) ).
fof(f106,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f55]) ).
fof(f107,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| X0 = X1
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f56]) ).
fof(f108,plain,
( l1_group_1(sK0)
& v4_group_1(sK0)
& v3_group_1(sK0)
& ~ v3_struct_0(sK0)
& l1_group_1(sK1)
& v4_group_1(sK1)
& v3_group_1(sK1)
& ~ v3_struct_0(sK1)
& m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
& v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1))
& v1_funct_1(sK2)
& m1_group_2(sK3,sK0)
& m1_group_2(sK4,sK0)
& m1_group_2(sK5,sK1)
& m1_group_2(sK6,sK1)
& m1_group_6(sK3,sK0,sK4)
& u1_struct_0(sK6) = k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK4))
& u1_struct_0(sK5) = k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK3))
& ~ m1_group_6(sK5,sK1,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6)],[f60]) ).
fof(f109,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ( ( ~ m1_group_2(X1,X0)
| ( u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( u1_group_1(X1) != k1_realset1(u1_group_1(X0),u1_struct_0(X1))
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| m1_group_2(X1,X0) ) ) ) ),
inference(nnf_transformation,[],[f70]) ).
fof(f110,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ( ( ~ m1_group_2(X1,X0)
| ( u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1))
& r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ) )
& ( u1_group_1(X1) != k1_realset1(u1_group_1(X0),u1_struct_0(X1))
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| m1_group_2(X1,X0) ) ) ) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
l1_group_1(sK7),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7)],[f24]) ).
fof(f112,plain,
l1_struct_0(sK8),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X0,sK8)],[f25]) ).
fof(f113,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(sK9(X0),X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X1,sK9(X0))],[f81]) ).
fof(f114,plain,
! [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(sK10(X0,X1),X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X2,sK10(X0,X1))],[f83]) ).
fof(f115,plain,
! [X0,X1] : m1_relset_1(sK11(X0,X1),X0,X1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f28]) ).
fof(f116,plain,
! [X0] : m1_subset_1(sK12(X0),X0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X1,sK12(X0))],[f29]) ).
fof(f117,plain,
! [X0,X1] : m2_relset_1(sK13(X0,X1),X0,X1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X2,sK13(X0,X1))],[f30]) ).
fof(f118,plain,
! [X0,X1] :
( v1_funct_2(sK14(X0,X1),X0,X1)
& v1_funct_1(sK14(X0,X1))
& v1_relat_1(sK14(X0,X1))
& m1_relset_1(sK14(X0,X1),X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0,X1))],[f35]) ).
fof(f119,plain,
! [X0] :
( v1_xboole_0(X0)
| ( ~ v1_xboole_0(sK15(X0))
& m1_subset_1(sK15(X0),k1_zfmisc_1(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(X1,sK15(X0))],[f88]) ).
fof(f120,plain,
v1_xboole_0(sK16),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(X0,sK16)],[f37]) ).
fof(f121,plain,
! [X0,X1] :
( v1_funct_1(sK17(X0,X1))
& v1_relat_1(sK17(X0,X1))
& m1_relset_1(sK17(X0,X1),X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X2,sK17(X0,X1))],[f38]) ).
fof(f122,plain,
! [X0] :
( v1_xboole_0(sK18(X0))
& m1_subset_1(sK18(X0),k1_zfmisc_1(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X1,sK18(X0))],[f39]) ).
fof(f123,plain,
~ v1_xboole_0(sK19),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X0,sK19)],[f40]) ).
fof(f124,plain,
( ~ v3_struct_0(sK20)
& l1_struct_0(sK20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X0,sK20)],[f41]) ).
fof(f125,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ( ~ v1_xboole_0(sK21(X0))
& m1_subset_1(sK21(X0),k1_zfmisc_1(u1_struct_0(X0))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X1,sK21(X0))],[f90]) ).
fof(f126,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,[],[f94]) ).
fof(f127,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,[],[f45]) ).
fof(f128,plain,
! [X0,X1] :
( ( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) )
& ( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f50]) ).
fof(f129,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f130,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f131,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f132,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f133,plain,
l1_group_1(sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f134,plain,
v4_group_1(sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f135,plain,
v3_group_1(sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f136,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f137,plain,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f108]) ).
fof(f138,plain,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f108]) ).
fof(f139,plain,
v1_funct_1(sK2),
inference(cnf_transformation,[],[f108]) ).
fof(f140,plain,
m1_group_2(sK3,sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f141,plain,
m1_group_2(sK4,sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f142,plain,
m1_group_2(sK5,sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f143,plain,
m1_group_2(sK6,sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f144,plain,
m1_group_6(sK3,sK0,sK4),
inference(cnf_transformation,[],[f108]) ).
fof(f145,plain,
u1_struct_0(sK6) = k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK4)),
inference(cnf_transformation,[],[f108]) ).
fof(f146,plain,
u1_struct_0(sK5) = k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK3)),
inference(cnf_transformation,[],[f108]) ).
fof(f147,plain,
~ m1_group_6(sK5,sK1,sK6),
inference(cnf_transformation,[],[f108]) ).
fof(f148,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ r2_hidden(X1,X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f64]) ).
fof(f157,plain,
! [X2,X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| ~ v1_xboole_0(X2) ),
inference(cnf_transformation,[],[f68]) ).
fof(f159,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| u1_group_1(X1) = k1_realset1(u1_group_1(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f110]) ).
fof(f160,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| ~ m1_group_2(X1,X0)
| r1_tarski(u1_struct_0(X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f110]) ).
fof(f161,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| v3_struct_0(X1)
| u1_group_1(X1) != k1_realset1(u1_group_1(X0),u1_struct_0(X1))
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| m1_group_2(X1,X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f162,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f72]) ).
fof(f163,plain,
! [X0] :
( ~ l1_group_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f73]) ).
fof(f164,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| l1_group_1(X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f165,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| v3_group_1(X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f166,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ v3_struct_0(X1) ),
inference(cnf_transformation,[],[f75]) ).
fof(f167,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,[],[f77]) ).
fof(f168,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1))) ),
inference(cnf_transformation,[],[f78]) ).
fof(f169,plain,
! [X0] :
( ~ l1_group_1(X0)
| m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f170,plain,
! [X0] :
( ~ l1_group_1(X0)
| v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f171,plain,
! [X0] :
( ~ l1_group_1(X0)
| v1_funct_1(u1_group_1(X0)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f172,plain,
l1_group_1(sK7),
inference(cnf_transformation,[],[f111]) ).
fof(f173,plain,
l1_struct_0(sK8),
inference(cnf_transformation,[],[f112]) ).
fof(f174,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(sK9(X0),X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f175,plain,
! [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(sK10(X0,X1),X0,X1) ),
inference(cnf_transformation,[],[f114]) ).
fof(f176,plain,
! [X0,X1] : m1_relset_1(sK11(X0,X1),X0,X1),
inference(cnf_transformation,[],[f115]) ).
fof(f177,plain,
! [X0] : m1_subset_1(sK12(X0),X0),
inference(cnf_transformation,[],[f116]) ).
fof(f178,plain,
! [X0,X1] : m2_relset_1(sK13(X0,X1),X0,X1),
inference(cnf_transformation,[],[f117]) ).
fof(f179,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f85]) ).
fof(f180,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f32]) ).
fof(f181,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f33]) ).
fof(f182,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(k2_zfmisc_1(X0,X1)) ),
inference(cnf_transformation,[],[f87]) ).
fof(f183,plain,
! [X0,X1] : v1_funct_2(sK14(X0,X1),X0,X1),
inference(cnf_transformation,[],[f118]) ).
fof(f184,plain,
! [X0,X1] : v1_funct_1(sK14(X0,X1)),
inference(cnf_transformation,[],[f118]) ).
fof(f185,plain,
! [X0,X1] : v1_relat_1(sK14(X0,X1)),
inference(cnf_transformation,[],[f118]) ).
fof(f186,plain,
! [X0,X1] : m1_relset_1(sK14(X0,X1),X0,X1),
inference(cnf_transformation,[],[f118]) ).
fof(f187,plain,
! [X0] :
( v1_xboole_0(X0)
| ~ v1_xboole_0(sK15(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f188,plain,
! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK15(X0),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f189,plain,
v1_xboole_0(sK16),
inference(cnf_transformation,[],[f120]) ).
fof(f191,plain,
! [X0,X1] : v1_relat_1(sK17(X0,X1)),
inference(cnf_transformation,[],[f121]) ).
fof(f192,plain,
! [X0,X1] : m1_relset_1(sK17(X0,X1),X0,X1),
inference(cnf_transformation,[],[f121]) ).
fof(f193,plain,
! [X0] : v1_xboole_0(sK18(X0)),
inference(cnf_transformation,[],[f122]) ).
fof(f194,plain,
! [X0] : m1_subset_1(sK18(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f122]) ).
fof(f195,plain,
~ v1_xboole_0(sK19),
inference(cnf_transformation,[],[f123]) ).
fof(f196,plain,
~ v3_struct_0(sK20),
inference(cnf_transformation,[],[f124]) ).
fof(f197,plain,
l1_struct_0(sK20),
inference(cnf_transformation,[],[f124]) ).
fof(f198,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(sK21(X0)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f199,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| m1_subset_1(sK21(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f125]) ).
fof(f200,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f92]) ).
fof(f201,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,[],[f126]) ).
fof(f202,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,[],[f126]) ).
fof(f203,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f204,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f127]) ).
fof(f205,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f57]) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f207,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f97]) ).
fof(f208,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f99]) ).
fof(f209,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
fof(f210,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f128]) ).
fof(f211,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f101]) ).
fof(f212,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f213,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,[],[f104]) ).
fof(f214,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f105]) ).
fof(f215,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f216,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| X0 = X1
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_49,negated_conjecture,
~ m1_group_6(sK5,sK1,sK6),
inference(cnf_transformation,[],[f147]) ).
tcf(c_50,negated_conjecture,
k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK3)) = u1_struct_0(sK5),
inference(cnf_transformation,[],[f146]) ).
tcf(c_51,negated_conjecture,
k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK4)) = u1_struct_0(sK6),
inference(cnf_transformation,[],[f145]) ).
tcf(c_52,negated_conjecture,
m1_group_6(sK3,sK0,sK4),
inference(cnf_transformation,[],[f144]) ).
tcf(c_53,negated_conjecture,
m1_group_2(sK6,sK1),
inference(cnf_transformation,[],[f143]) ).
tcf(c_54,negated_conjecture,
m1_group_2(sK5,sK1),
inference(cnf_transformation,[],[f142]) ).
tcf(c_55,negated_conjecture,
m1_group_2(sK4,sK0),
inference(cnf_transformation,[],[f141]) ).
tcf(c_56,negated_conjecture,
m1_group_2(sK3,sK0),
inference(cnf_transformation,[],[f140]) ).
tcf(c_57,negated_conjecture,
v1_funct_1(sK2),
inference(cnf_transformation,[],[f139]) ).
tcf(c_58,negated_conjecture,
v1_funct_2(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f138]) ).
tcf(c_59,negated_conjecture,
m2_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f137]) ).
tcf(c_60,negated_conjecture,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f136]) ).
tcf(c_61,negated_conjecture,
v3_group_1(sK1),
inference(cnf_transformation,[],[f135]) ).
tcf(c_62,negated_conjecture,
v4_group_1(sK1),
inference(cnf_transformation,[],[f134]) ).
tcf(c_63,negated_conjecture,
l1_group_1(sK1),
inference(cnf_transformation,[],[f133]) ).
tcf(c_64,negated_conjecture,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f132]) ).
tcf(c_65,negated_conjecture,
v3_group_1(sK0),
inference(cnf_transformation,[],[f131]) ).
tcf(c_66,negated_conjecture,
v4_group_1(sK0),
inference(cnf_transformation,[],[f130]) ).
tcf(c_67,negated_conjecture,
l1_group_1(sK0),
inference(cnf_transformation,[],[f129]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i] :
( ~ r2_hidden(X1,X0)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_xboole_0(X2)
| v1_xboole_0(X1)
| ~ v1_xboole_0(X0)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| m1_group_2(X1,X0)
| ~ l1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X1)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),u1_struct_0(X1)) != u1_group_1(X1) ) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X1)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| ( k1_realset1(u1_group_1(X1),u1_struct_0(X0)) = u1_group_1(X0) )
| ~ l1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X1)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k2_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X2))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_78,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ v3_struct_0(X0)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f166]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( v3_group_1(X0)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( l1_group_1(X0)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f164]) ).
tcf(c_82,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,[],[f167]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_84,plain,
! [X0: $i] :
( v1_funct_1(u1_group_1(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_85,plain,
! [X0: $i] :
( v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f170]) ).
tcf(c_86,plain,
! [X0: $i] :
( m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(cnf_transformation,[],[f169]) ).
tcf(c_87,plain,
l1_group_1(sK7),
inference(cnf_transformation,[],[f172]) ).
tcf(c_88,plain,
l1_struct_0(sK8),
inference(cnf_transformation,[],[f173]) ).
tcf(c_89,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK9(X0),X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f174]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m1_group_6(sK10(X1,X0),X1,X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] : m1_relset_1(sK11(X0,X1),X0,X1),
inference(cnf_transformation,[],[f176]) ).
tcf(c_92,plain,
! [X0: $i] : m1_subset_1(sK12(X0),X0),
inference(cnf_transformation,[],[f177]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] : m2_relset_1(sK13(X0,X1),X0,X1),
inference(cnf_transformation,[],[f178]) ).
tcf(c_94,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_95,plain,
! [X0: $i] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f180]) ).
tcf(c_96,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f181]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(k2_zfmisc_1(X0,X1)) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] : m1_relset_1(sK14(X0,X1),X0,X1),
inference(cnf_transformation,[],[f186]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i] : v1_relat_1(sK14(X0,X1)),
inference(cnf_transformation,[],[f185]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] : v1_funct_1(sK14(X0,X1)),
inference(cnf_transformation,[],[f184]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] : v1_funct_2(sK14(X0,X1),X0,X1),
inference(cnf_transformation,[],[f183]) ).
tcf(c_102,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| m1_subset_1(sK15(X0),k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_103,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ v1_xboole_0(sK15(X0)) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_104,plain,
v1_xboole_0(sK16),
inference(cnf_transformation,[],[f189]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i] : m1_relset_1(sK17(X0,X1),X0,X1),
inference(cnf_transformation,[],[f192]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i] : v1_relat_1(sK17(X0,X1)),
inference(cnf_transformation,[],[f191]) ).
tcf(c_108,plain,
! [X0: $i] : m1_subset_1(sK18(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f194]) ).
tcf(c_109,plain,
! [X0: $i] : v1_xboole_0(sK18(X0)),
inference(cnf_transformation,[],[f193]) ).
tcf(c_110,plain,
~ v1_xboole_0(sK19),
inference(cnf_transformation,[],[f195]) ).
tcf(c_111,plain,
l1_struct_0(sK20),
inference(cnf_transformation,[],[f197]) ).
tcf(c_112,plain,
~ v3_struct_0(sK20),
inference(cnf_transformation,[],[f196]) ).
tcf(c_113,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_subset_1(sK21(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_114,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ v1_xboole_0(sK21(X0)) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_116,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,[],[f202]) ).
tcf(c_117,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,[],[f201]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(X0,X1,X2)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_120,plain,
! [X0: $i] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f205]) ).
tcf(c_121,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(k9_relat_1(X2,X0),k9_relat_1(X2,X1))
| ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X2,X1)
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_128,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,[],[f213]) ).
tcf(c_129,plain,
! [X0: $i] :
( ( X0 = k1_xboole_0 )
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_141,plain,
( l1_struct_0(sK0)
| ~ l1_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_160,plain,
( v3_struct_0(sK0)
| ~ l1_struct_0(sK0)
| ~ v1_xboole_0(u1_struct_0(sK0)) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_180,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_75,c_81,c_80,c_79,c_75]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_180]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1)
| ~ l1_group_1(X1)
| ( k1_realset1(u1_group_1(X1),u1_struct_0(X0)) = u1_group_1(X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_76,c_81,c_80,c_79,c_76]) ).
tcf(c_183,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ( k1_realset1(u1_group_1(X1),u1_struct_0(X0)) = u1_group_1(X0) )
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_182]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m2_relset_1(X0,X1,X2)
| m1_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_119]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(renaming,[status(thm)],[c_184]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_124]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_118,c_83]) ).
tcf(c_214,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_group_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_78]) ).
tcf(c_218,plain,
! [X0: $i] :
( v1_funct_2(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_85]) ).
tcf(c_220,plain,
! [X0: $i] :
( m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(prop_impl_just,[status(thm)],[c_86]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,X2)
| ~ r1_tarski(X1,X2)
| ~ r2_hidden(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_126,c_190]) ).
tcf(c_361,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ v1_xboole_0(X2)
| ~ r1_tarski(X1,X2)
| ~ r2_hidden(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_127,c_190]) ).
tcf(c_1086,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X2,X1,X0)
| ( X2 != sK2 )
| ( u1_struct_0(sK0) != X1 )
| ( u1_struct_0(sK1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_185]) ).
tcf(c_1087,plain,
m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(unflattening,[status(thm)],[c_1086]) ).
tcf(c_1091,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_relset_1(X1,X2,X3)
| ~ l1_group_1(X0)
| ( u1_group_1(X0) != X1 )
| ( u1_struct_0(X0) != X3 )
| ( k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_185,c_220]) ).
tcf(c_1092,plain,
! [X0: $i] :
( m1_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_group_1(X0) ),
inference(unflattening,[status(thm)],[c_1091]) ).
tcf(c_1100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_relset_1(X2,X3,X4)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK13(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_185,c_93]) ).
tcf(c_1101,plain,
! [X0: $i,X1: $i] : m1_relset_1(sK13(X0,X1),X0,X1),
inference(unflattening,[status(thm)],[c_1100]) ).
tcf(c_1149,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v1_xboole_0(sK21(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_214,c_114]) ).
tcf(c_1150,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v1_xboole_0(sK21(X0)) ),
inference(unflattening,[status(thm)],[c_1149]) ).
tcf(c_1161,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m1_subset_1(sK21(X1),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_group_1(X0)
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_214,c_113]) ).
tcf(c_1162,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_subset_1(sK21(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0) ),
inference(unflattening,[status(thm)],[c_1161]) ).
tcf(c_1173,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ~ l1_group_1(X0)
| ~ v1_xboole_0(u1_struct_0(X1))
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_214,c_94]) ).
tcf(c_1174,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(unflattening,[status(thm)],[c_1173]) ).
tcf(c_1185,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ v1_xboole_0(sK21(X0))
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_114,c_88]) ).
tcf(c_1186,plain,
( v3_struct_0(sK8)
| ~ v1_xboole_0(sK21(sK8)) ),
inference(unflattening,[status(thm)],[c_1185]) ).
tcf(c_1193,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_subset_1(sK21(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_113,c_88]) ).
tcf(c_1194,plain,
( v3_struct_0(sK8)
| m1_subset_1(sK21(sK8),k1_zfmisc_1(u1_struct_0(sK8))) ),
inference(unflattening,[status(thm)],[c_1193]) ).
tcf(c_1201,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0))
| ( X0 != sK8 ) ),
inference(resolution_lifted,[status(thm)],[c_94,c_88]) ).
tcf(c_1202,plain,
( v3_struct_0(sK8)
| ~ v1_xboole_0(u1_struct_0(sK8)) ),
inference(unflattening,[status(thm)],[c_1201]) ).
tcf(c_1209,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ v1_xboole_0(sK21(X0))
| ( X0 != sK20 ) ),
inference(resolution_lifted,[status(thm)],[c_114,c_111]) ).
tcf(c_1210,plain,
( v3_struct_0(sK20)
| ~ v1_xboole_0(sK21(sK20)) ),
inference(unflattening,[status(thm)],[c_1209]) ).
tcf(c_1211,plain,
~ v1_xboole_0(sK21(sK20)),
inference(global_subsumption_just,[status(thm)],[c_1210,c_112,c_1210]) ).
tcf(c_1216,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_subset_1(sK21(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ( X0 != sK20 ) ),
inference(resolution_lifted,[status(thm)],[c_113,c_111]) ).
tcf(c_1217,plain,
( v3_struct_0(sK20)
| m1_subset_1(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))) ),
inference(unflattening,[status(thm)],[c_1216]) ).
tcf(c_1218,plain,
m1_subset_1(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))),
inference(global_subsumption_just,[status(thm)],[c_1217,c_112,c_1217]) ).
tcf(c_1223,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0))
| ( X0 != sK20 ) ),
inference(resolution_lifted,[status(thm)],[c_94,c_111]) ).
tcf(c_1224,plain,
( v3_struct_0(sK20)
| ~ v1_xboole_0(u1_struct_0(sK20)) ),
inference(unflattening,[status(thm)],[c_1223]) ).
tcf(c_1225,plain,
~ v1_xboole_0(u1_struct_0(sK20)),
inference(global_subsumption_just,[status(thm)],[c_1224,c_112,c_1224]) ).
tcf(c_1248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X0,X2,X3) = k9_relat_1(X2,X3) )
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X1,X0)
| ( X2 != sK2 )
| ( u1_struct_0(sK0) != X1 )
| ( u1_struct_0(sK1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_115]) ).
tcf(c_1249,plain,
! [X0: $i] :
( ( k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,X0) = k9_relat_1(sK2,X0) )
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(unflattening,[status(thm)],[c_1248]) ).
tcf(c_1251,plain,
! [X0: $i] : k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,X0) = k9_relat_1(sK2,X0),
inference(global_subsumption_just,[status(thm)],[c_1249,c_57,c_1087,c_1249]) ).
tcf(c_1257,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k2_funct_2(X1,X0,X2,X3),k1_zfmisc_1(X0))
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X1,X0)
| ( X2 != sK2 )
| ( u1_struct_0(sK0) != X1 )
| ( u1_struct_0(sK1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_77]) ).
tcf(c_1258,plain,
! [X0: $i] :
( m1_subset_1(k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,X0),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(unflattening,[status(thm)],[c_1257]) ).
tcf(c_1260,plain,
! [X0: $i] : m1_subset_1(k2_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,X0),k1_zfmisc_1(u1_struct_0(sK1))),
inference(global_subsumption_just,[status(thm)],[c_1258,c_57,c_1087,c_1258]) ).
tcf(c_1266,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(X2)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X1,X0)
| ( X2 != sK2 )
| ( u1_struct_0(sK0) != X1 )
| ( u1_struct_0(sK1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_72]) ).
tcf(c_1267,plain,
( v1_xboole_0(u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK1))
| ~ v1_xboole_0(sK2)
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(unflattening,[status(thm)],[c_1266]) ).
tcf(c_1268,plain,
( ~ v1_xboole_0(sK2)
| v1_xboole_0(u1_struct_0(sK1)) ),
inference(global_subsumption_just,[status(thm)],[c_1267,c_67,c_57,c_64,c_141,c_160,c_1087,c_1267]) ).
tcf(c_1269,plain,
( v1_xboole_0(u1_struct_0(sK1))
| ~ v1_xboole_0(sK2) ),
inference(renaming,[status(thm)],[c_1268]) ).
tcf(c_1276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( k2_funct_2(X2,X3,X1,X4) = k9_relat_1(X1,X4) )
| ~ l1_group_1(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,X2,X3)
| ( u1_group_1(X0) != X1 )
| ( u1_struct_0(X0) != X3 )
| ( k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_218]) ).
tcf(c_1277,plain,
! [X0: $i,X1: $i] :
( ( k2_funct_2(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0),u1_group_1(X0),X1) = k9_relat_1(u1_group_1(X0),X1) )
| ~ l1_group_1(X0)
| ~ v1_funct_1(u1_group_1(X0))
| ~ m1_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(unflattening,[status(thm)],[c_1276]) ).
tcf(c_1279,plain,
! [X0: $i,X1: $i] :
( ( k2_funct_2(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0),u1_group_1(X0),X1) = k9_relat_1(u1_group_1(X0),X1) )
| ~ l1_group_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_1277,c_84,c_1092,c_1277]) ).
tcf(c_1288,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_subset_1(k2_funct_2(X2,X3,X1,X4),k1_zfmisc_1(X3))
| ~ l1_group_1(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,X2,X3)
| ( u1_group_1(X0) != X1 )
| ( u1_struct_0(X0) != X3 )
| ( k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_77,c_218]) ).
tcf(c_1289,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k2_funct_2(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0),u1_group_1(X0),X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v1_funct_1(u1_group_1(X0))
| ~ m1_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(unflattening,[status(thm)],[c_1288]) ).
tcf(c_1291,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k2_funct_2(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0),u1_group_1(X0),X1),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_1289,c_84,c_1092,c_1289]) ).
tcf(c_1300,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v1_xboole_0(X3)
| v1_xboole_0(X2)
| ~ v1_xboole_0(X1)
| ~ l1_group_1(X0)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X1,X2,X3)
| ( u1_group_1(X0) != X1 )
| ( u1_struct_0(X0) != X3 )
| ( k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_72,c_218]) ).
tcf(c_1301,plain,
! [X0: $i] :
( v1_xboole_0(u1_struct_0(X0))
| v1_xboole_0(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v1_xboole_0(u1_group_1(X0))
| ~ v1_funct_1(u1_group_1(X0))
| ~ m1_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(unflattening,[status(thm)],[c_1300]) ).
tcf(c_1303,plain,
! [X0: $i] :
( v1_xboole_0(u1_struct_0(X0))
| v1_xboole_0(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v1_xboole_0(u1_group_1(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1301,c_84,c_1092,c_1301]) ).
tcf(c_1318,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( k2_funct_2(X3,X4,X2,X5) = k9_relat_1(X2,X5) )
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X3,X4)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK14(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_115,c_101]) ).
tcf(c_1319,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k2_funct_2(X0,X1,sK14(X0,X1),X2) = k9_relat_1(sK14(X0,X1),X2) )
| ~ v1_funct_1(sK14(X0,X1))
| ~ m1_relset_1(sK14(X0,X1),X0,X1) ),
inference(unflattening,[status(thm)],[c_1318]) ).
tcf(c_1321,plain,
! [X0: $i,X1: $i,X2: $i] : k2_funct_2(X0,X1,sK14(X0,X1),X2) = k9_relat_1(sK14(X0,X1),X2),
inference(global_subsumption_just,[status(thm)],[c_1319,c_100,c_98,c_1319]) ).
tcf(c_1327,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( m1_subset_1(k2_funct_2(X3,X4,X2,X5),k1_zfmisc_1(X4))
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X3,X4)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK14(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_77,c_101]) ).
tcf(c_1328,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k2_funct_2(X0,X1,sK14(X0,X1),X2),k1_zfmisc_1(X1))
| ~ v1_funct_1(sK14(X0,X1))
| ~ m1_relset_1(sK14(X0,X1),X0,X1) ),
inference(unflattening,[status(thm)],[c_1327]) ).
tcf(c_1330,plain,
! [X0: $i,X1: $i,X2: $i] : m1_subset_1(k2_funct_2(X0,X1,sK14(X0,X1),X2),k1_zfmisc_1(X1)),
inference(global_subsumption_just,[status(thm)],[c_1328,c_100,c_98,c_1328]) ).
tcf(c_1336,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(X4)
| v1_xboole_0(X3)
| ~ v1_xboole_0(X2)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X2,X3,X4)
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK14(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_72,c_101]) ).
tcf(c_1337,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(sK14(X0,X1))
| ~ v1_funct_1(sK14(X0,X1))
| ~ m1_relset_1(sK14(X0,X1),X0,X1) ),
inference(unflattening,[status(thm)],[c_1336]) ).
tcf(c_1339,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| v1_xboole_0(X0)
| ~ v1_xboole_0(sK14(X0,X1)) ),
inference(global_subsumption_just,[status(thm)],[c_1337,c_100,c_98,c_1337]) ).
tcf(c_1368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK11(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_200,c_91]) ).
tcf(c_1369,plain,
! [X0: $i,X1: $i] : m1_subset_1(sK11(X0,X1),k1_zfmisc_1(k2_zfmisc_1(X0,X1))),
inference(unflattening,[status(thm)],[c_1368]) ).
tcf(c_1374,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK14(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_200,c_98]) ).
tcf(c_1375,plain,
! [X0: $i,X1: $i] : m1_subset_1(sK14(X0,X1),k1_zfmisc_1(k2_zfmisc_1(X0,X1))),
inference(unflattening,[status(thm)],[c_1374]) ).
tcf(c_1380,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK17(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_200,c_105]) ).
tcf(c_1381,plain,
! [X0: $i,X1: $i] : m1_subset_1(sK17(X0,X1),k1_zfmisc_1(k2_zfmisc_1(X0,X1))),
inference(unflattening,[status(thm)],[c_1380]) ).
tcf(c_1386,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ( X0 != sK2 )
| ( u1_struct_0(sK0) != X1 )
| ( u1_struct_0(sK1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_200,c_1087]) ).
tcf(c_1387,plain,
m1_subset_1(sK2,k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK1)))),
inference(unflattening,[status(thm)],[c_1386]) ).
tcf(c_1391,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ l1_group_1(X0)
| ( u1_group_1(X0) != X1 )
| ( u1_struct_0(X0) != X3 )
| ( k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_200,c_1092]) ).
tcf(c_1392,plain,
! [X0: $i] :
( m1_subset_1(u1_group_1(X0),k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))))
| ~ l1_group_1(X0) ),
inference(unflattening,[status(thm)],[c_1391]) ).
tcf(c_1400,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X3,X4)))
| ( X1 != X4 )
| ( X0 != X3 )
| ( sK13(X0,X1) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_200,c_1101]) ).
tcf(c_1401,plain,
! [X0: $i,X1: $i] : m1_subset_1(sK13(X0,X1),k1_zfmisc_1(k2_zfmisc_1(X0,X1))),
inference(unflattening,[status(thm)],[c_1400]) ).
tcf(c_1413,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_6(X1,X0,X2)
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_117]) ).
tcf(c_1414,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_6(X0,sK1,X1) ),
inference(unflattening,[status(thm)],[c_1413]) ).
tcf(c_1416,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_6(X0,sK1,X1)
| ~ m1_group_2(X1,sK1)
| m1_group_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_1414,c_63,c_61,c_60,c_1414]) ).
tcf(c_1417,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_6(X0,sK1,X1) ),
inference(renaming,[status(thm)],[c_1416]) ).
tcf(c_1428,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| m1_group_6(X2,X0,X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X1,X0)
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_116]) ).
tcf(c_1429,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| m1_group_6(X0,sK1,X1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_1428]) ).
tcf(c_1431,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK1)
| m1_group_6(X0,sK1,X1) ),
inference(global_subsumption_just,[status(thm)],[c_1429,c_63,c_61,c_60,c_1429]) ).
tcf(c_1432,plain,
! [X0: $i,X1: $i] :
( m1_group_6(X0,sK1,X1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_1431]) ).
tcf(c_1443,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| m1_group_6(sK10(X0,X1),X0,X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_90]) ).
tcf(c_1444,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| m1_group_6(sK10(sK1,X0),sK1,X0)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X0,sK1) ),
inference(unflattening,[status(thm)],[c_1443]) ).
tcf(c_1446,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| m1_group_6(sK10(sK1,X0),sK1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1444,c_63,c_61,c_60,c_1444]) ).
tcf(c_1447,plain,
! [X0: $i] :
( m1_group_6(sK10(sK1,X0),sK1,X0)
| ~ m1_group_2(X0,sK1) ),
inference(renaming,[status(thm)],[c_1446]) ).
tcf(c_1455,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_6(X1,X0,X2)
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_82]) ).
tcf(c_1456,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| m1_group_2(X0,sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_6(X0,sK1,X1) ),
inference(unflattening,[status(thm)],[c_1455]) ).
tcf(c_1457,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_6(X0,sK1,X1)
| ~ m1_group_2(X1,sK1)
| m1_group_2(X0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_1456,c_63,c_61,c_60,c_1456]) ).
tcf(c_1458,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_6(X0,sK1,X1) ),
inference(renaming,[status(thm)],[c_1457]) ).
tcf(c_1468,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 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_62,c_128]) ).
tcf(c_1469,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK1)
| m1_group_2(X0,X1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(unflattening,[status(thm)],[c_1468]) ).
tcf(c_1471,plain,
! [X0: $i,X1: $i] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X1,sK1)
| m1_group_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_1469,c_63,c_61,c_60,c_1469]) ).
tcf(c_1472,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(renaming,[status(thm)],[c_1471]) ).
tcf(c_1486,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_6(X1,X0,X2)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_117]) ).
tcf(c_1487,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_6(X0,sK0,X1) ),
inference(unflattening,[status(thm)],[c_1486]) ).
tcf(c_1488,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_6(X0,sK0,X1)
| ~ m1_group_2(X1,sK0)
| m1_group_2(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_1487,c_67,c_65,c_64,c_1487]) ).
tcf(c_1489,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_6(X0,sK0,X1) ),
inference(renaming,[status(thm)],[c_1488]) ).
tcf(c_1499,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| m1_group_6(X2,X0,X1)
| ~ 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_66,c_116]) ).
tcf(c_1500,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| m1_group_6(X0,sK0,X1)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_1499]) ).
tcf(c_1502,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| m1_group_6(X0,sK0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_1500,c_67,c_65,c_64,c_1500]) ).
tcf(c_1503,plain,
! [X0: $i,X1: $i] :
( m1_group_6(X0,sK0,X1)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_1502]) ).
tcf(c_1514,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| m1_group_6(sK10(X0,X1),X0,X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_90]) ).
tcf(c_1515,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| m1_group_6(sK10(sK0,X0),sK0,X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_1514]) ).
tcf(c_1517,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| m1_group_6(sK10(sK0,X0),sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1515,c_67,c_65,c_64,c_1515]) ).
tcf(c_1518,plain,
! [X0: $i] :
( m1_group_6(sK10(sK0,X0),sK0,X0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_1517]) ).
tcf(c_1526,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_6(X1,X0,X2)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_66,c_82]) ).
tcf(c_1527,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_6(X0,sK0,X1) ),
inference(unflattening,[status(thm)],[c_1526]) ).
tcf(c_1528,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_6(X0,sK0,X1)
| ~ m1_group_2(X1,sK0)
| m1_group_2(X0,sK0) ),
inference(global_subsumption_just,[status(thm)],[c_1527,c_67,c_65,c_64,c_1527]) ).
tcf(c_1529,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_6(X0,sK0,X1) ),
inference(renaming,[status(thm)],[c_1528]) ).
tcf(c_1539,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_66,c_128]) ).
tcf(c_1540,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_1539]) ).
tcf(c_1541,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_1540,c_67,c_65,c_64,c_1540]) ).
tcf(c_1542,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_1541]) ).
tcf(c_1585,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_group_2(X1,sK1)
| ~ m1_group_2(X3,sK1)
| ~ m1_group_2(X2,sK1)
| ~ m1_group_2(X0,X2)
| ( sK1 != sK1 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1432,c_1458]) ).
tcf(c_1586,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_1585]) ).
tcf(c_1598,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_group_2(X1,sK0)
| ~ m1_group_2(X3,sK0)
| ~ m1_group_2(X2,sK0)
| ~ m1_group_2(X0,X2)
| ( sK0 != sK0 )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1503,c_1529]) ).
tcf(c_1599,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(unflattening,[status(thm)],[c_1598]) ).
tcf(c_1611,plain,
( ( sK6 != sK4 )
| ( sK1 != sK0 )
| ( sK5 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_52]) ).
tcf(c_1621,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,X1)
| ( sK1 != sK1 )
| ( X1 != sK6 )
| ( X0 != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_1432]) ).
tcf(c_1622,plain,
( ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(sK5,sK6) ),
inference(unflattening,[status(thm)],[c_1621]) ).
tcf(c_1623,plain,
~ m1_group_2(sK5,sK6),
inference(global_subsumption_just,[status(thm)],[c_1622,c_53,c_1622]) ).
tcf(c_1628,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| ( sK1 != sK1 )
| ( X0 != sK6 )
| ( sK10(sK1,X0) != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_1447]) ).
tcf(c_1629,plain,
( ~ m1_group_2(sK6,sK1)
| ( sK10(sK1,sK6) != sK5 ) ),
inference(unflattening,[status(thm)],[c_1628]) ).
tcf(c_1630,plain,
sK10(sK1,sK6) != sK5,
inference(global_subsumption_just,[status(thm)],[c_1629,c_53,c_1629]) ).
tcf(c_1637,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| ( sK1 != sK0 )
| ( X0 != sK6 )
| ( sK10(sK0,X0) != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_1518]) ).
tcf(c_1638,plain,
( ~ m1_group_2(sK6,sK0)
| ( sK1 != sK0 )
| ( sK10(sK0,sK6) != sK5 ) ),
inference(unflattening,[status(thm)],[c_1637]) ).
tcf(c_1648,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK1)
| ~ m1_group_2(X1,sK1)
| ( sK1 != sK0 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_1458]) ).
tcf(c_1649,plain,
( m1_group_2(sK3,sK1)
| ~ m1_group_2(sK4,sK1)
| ( sK1 != sK0 ) ),
inference(unflattening,[status(thm)],[c_1648]) ).
tcf(c_1672,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK0)
| ( sK0 != sK0 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_1489]) ).
tcf(c_1673,plain,
( m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK0) ),
inference(unflattening,[status(thm)],[c_1672]) ).
tcf(c_1674,plain,
m1_group_2(sK3,sK4),
inference(global_subsumption_just,[status(thm)],[c_1673,c_55,c_1673]) ).
tcf(c_1679,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,sK1)
| ~ m1_group_2(X2,sK1)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK1 )
| ( X0 != X2 )
| ( sK10(sK1,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1458,c_1447]) ).
tcf(c_1680,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(X0,sK1) ),
inference(unflattening,[status(thm)],[c_1679]) ).
tcf(c_1688,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,X2)
| ~ m1_group_2(X2,sK1)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK1 )
| ( X0 != X2 )
| ( sK10(sK1,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1417,c_1447]) ).
tcf(c_1689,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),X0)
| ~ m1_group_2(X0,sK1) ),
inference(unflattening,[status(thm)],[c_1688]) ).
tcf(c_1709,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,sK1)
| ~ m1_group_2(X2,sK1)
| ~ m1_group_2(X0,sK0)
| ( sK1 != sK0 )
| ( X0 != X2 )
| ( sK10(sK0,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1458,c_1518]) ).
tcf(c_1710,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK0 ) ),
inference(unflattening,[status(thm)],[c_1709]) ).
tcf(c_1739,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,sK0)
| ~ m1_group_2(X2,sK0)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK0 )
| ( X0 != X2 )
| ( sK10(sK1,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1447,c_1529]) ).
tcf(c_1740,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK0 ) ),
inference(unflattening,[status(thm)],[c_1739]) ).
tcf(c_1758,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,sK0)
| ~ m1_group_2(X2,sK0)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK0 )
| ( X0 != X2 )
| ( sK10(sK0,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1529,c_1518]) ).
tcf(c_1759,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_1758]) ).
tcf(c_1767,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,X2)
| ~ m1_group_2(X2,sK0)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK0 )
| ( X0 != X2 )
| ( sK10(sK0,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1489,c_1518]) ).
tcf(c_1768,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),X0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_1767]) ).
tcf(c_2453,definition,
iPr_def_10 = sK10(sK0,sK6),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_2454,definition,
iPr_def_11 = sK10(sK1,sK6),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_2455,definition,
iPr_def_12 = u1_struct_0(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_2456,definition,
iPr_def_13 = u1_struct_0(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_2457,definition,
iPr_def_14 = k2_zfmisc_1(iPr_def_12,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_2458,definition,
iPr_def_15 = k1_zfmisc_1(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_2459,definition,
iPr_def_16 = k1_zfmisc_1(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_2460,definition,
iPr_def_17 = u1_struct_0(sK4),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_2461,definition,
iPr_def_18 = k2_funct_2(iPr_def_12,iPr_def_13,sK2,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_2462,definition,
iPr_def_19 = u1_struct_0(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_2463,definition,
iPr_def_20 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_2464,definition,
iPr_def_21 = k2_funct_2(iPr_def_12,iPr_def_13,sK2,iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_2465,definition,
iPr_def_22 = u1_struct_0(sK5),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_2466,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),X0)
| ~ m1_group_2(X0,sK0) ),
inference(demodulation,[status(thm)],[c_1768]) ).
tcf(c_2467,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK0)
| ~ m1_group_2(X0,sK0) ),
inference(demodulation,[status(thm)],[c_1759]) ).
tcf(c_2468,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK0 ) ),
inference(demodulation,[status(thm)],[c_1740]) ).
tcf(c_2469,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,sK1)
| ( sK1 != sK0 ) ),
inference(demodulation,[status(thm)],[c_1710]) ).
tcf(c_2470,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),X0)
| ~ m1_group_2(X0,sK1) ),
inference(demodulation,[status(thm)],[c_1689]) ).
tcf(c_2471,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(X0,sK1) ),
inference(demodulation,[status(thm)],[c_1680]) ).
tcf(c_2472,plain,
m1_group_2(sK3,sK4),
inference(demodulation,[status(thm)],[c_1674]) ).
tcf(c_2473,plain,
( m1_group_2(sK3,sK1)
| ~ m1_group_2(sK4,sK1)
| ( sK1 != sK0 ) ),
inference(demodulation,[status(thm)],[c_1649]) ).
tcf(c_2474,plain,
( ~ m1_group_2(sK6,sK0)
| ( iPr_def_10 != sK5 )
| ( sK1 != sK0 ) ),
inference(demodulation,[status(thm)],[c_1638,c_2453]) ).
tcf(c_2475,plain,
iPr_def_11 != sK5,
inference(demodulation,[status(thm)],[c_1630,c_2454]) ).
tcf(c_2476,plain,
~ m1_group_2(sK5,sK6),
inference(demodulation,[status(thm)],[c_1623]) ).
tcf(c_2477,plain,
( ( sK6 != sK4 )
| ( sK1 != sK0 )
| ( sK5 != sK3 ) ),
inference(demodulation,[status(thm)],[c_1611]) ).
tcf(c_2478,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1) ),
inference(demodulation,[status(thm)],[c_1599]) ).
tcf(c_2479,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,X1) ),
inference(demodulation,[status(thm)],[c_1586]) ).
tcf(c_2480,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(demodulation,[status(thm)],[c_1542]) ).
tcf(c_2481,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X1)) ),
inference(demodulation,[status(thm)],[c_1472]) ).
tcf(c_2482,plain,
m1_subset_1(sK2,iPr_def_15),
inference(demodulation,[status(thm)],[c_1387,c_2456,c_2455,c_2457,c_2458]) ).
tcf(c_2483,plain,
( v1_xboole_0(iPr_def_13)
| ~ v1_xboole_0(sK2) ),
inference(demodulation,[status(thm)],[c_1269]) ).
tcf(c_2484,plain,
! [X0: $i] : m1_subset_1(k2_funct_2(iPr_def_12,iPr_def_13,sK2,X0),iPr_def_16),
inference(demodulation,[status(thm)],[c_1260,c_2459]) ).
tcf(c_2485,plain,
! [X0: $i] : k2_funct_2(iPr_def_12,iPr_def_13,sK2,X0) = k9_relat_1(sK2,X0),
inference(demodulation,[status(thm)],[c_1251]) ).
tcf(c_2486,negated_conjecture,
l1_group_1(sK0),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_2487,negated_conjecture,
v3_group_1(sK0),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_2488,negated_conjecture,
~ v3_struct_0(sK0),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_2489,negated_conjecture,
l1_group_1(sK1),
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_2490,negated_conjecture,
v3_group_1(sK1),
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_2491,negated_conjecture,
~ v3_struct_0(sK1),
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_2492,negated_conjecture,
m1_group_2(sK3,sK0),
inference(demodulation,[status(thm)],[c_56]) ).
tcf(c_2493,negated_conjecture,
m1_group_2(sK4,sK0),
inference(demodulation,[status(thm)],[c_55]) ).
tcf(c_2494,negated_conjecture,
m1_group_2(sK5,sK1),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_2495,negated_conjecture,
m1_group_2(sK6,sK1),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_2496,negated_conjecture,
iPr_def_18 = iPr_def_19,
inference(demodulation,[status(thm)],[c_51,c_2462,c_2460,c_2461]) ).
tcf(c_2497,negated_conjecture,
iPr_def_21 = iPr_def_22,
inference(demodulation,[status(thm)],[c_50,c_2465,c_2463,c_2464]) ).
tcf(c_4018,plain,
! [X0: $i] : m1_subset_1(k9_relat_1(sK2,X0),iPr_def_16),
inference(light_normalisation,[status(thm)],[c_2484,c_2485]) ).
tcf(c_4045,plain,
! [X0: $i] :
( m1_group_2(X0,X0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_120,c_2480]) ).
tcf(c_4056,plain,
! [X0: $i] :
( m1_group_2(X0,X0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_120,c_2481]) ).
tcf(c_4064,plain,
m1_group_2(sK4,sK4),
inference(superposition,[status(thm)],[c_2493,c_4045]) ).
tcf(c_4065,plain,
m1_group_2(sK3,sK3),
inference(superposition,[status(thm)],[c_2492,c_4045]) ).
tcf(c_4066,plain,
! [X0: $i] :
( m1_group_2(sK0,X0)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_12,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2455,c_2481]) ).
tcf(c_4067,plain,
! [X0: $i] :
( m1_group_2(sK0,X0)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_12,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2455,c_2480]) ).
tcf(c_4068,plain,
! [X0: $i] :
( m1_group_2(X0,sK0)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_2455,c_2481]) ).
tcf(c_4082,plain,
! [X0: $i] :
( m1_group_2(sK1,X0)
| ~ m1_group_2(sK1,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_13,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2456,c_2481]) ).
tcf(c_4083,plain,
! [X0: $i] :
( m1_group_2(sK1,X0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_13,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2456,c_2480]) ).
tcf(c_4085,plain,
! [X0: $i] :
( m1_group_2(X0,sK1)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_2456,c_2480]) ).
tcf(c_4100,plain,
m1_subset_1(sK18(iPr_def_14),iPr_def_15),
inference(superposition,[status(thm)],[c_2458,c_108]) ).
tcf(c_4101,plain,
~ v1_xboole_0(iPr_def_15),
inference(superposition,[status(thm)],[c_2458,c_95]) ).
tcf(c_4102,plain,
m1_subset_1(sK18(iPr_def_13),iPr_def_16),
inference(superposition,[status(thm)],[c_2459,c_108]) ).
tcf(c_4103,plain,
~ v1_xboole_0(iPr_def_16),
inference(superposition,[status(thm)],[c_2459,c_95]) ).
tcf(c_4108,plain,
m1_group_2(sK6,sK6),
inference(superposition,[status(thm)],[c_2495,c_4056]) ).
tcf(c_4109,plain,
m1_group_2(sK5,sK5),
inference(superposition,[status(thm)],[c_2494,c_4056]) ).
tcf(c_4114,plain,
( m1_group_2(iPr_def_10,sK6)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2453,c_2466]) ).
tcf(c_4115,plain,
( m1_group_2(sK10(sK0,sK1),sK10(sK0,sK1))
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2466,c_4056]) ).
tcf(c_4116,plain,
( m1_group_2(sK10(sK0,sK0),sK10(sK0,sK0))
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2466,c_4045]) ).
tcf(c_4127,plain,
( m1_group_2(iPr_def_10,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2453,c_2467]) ).
tcf(c_4128,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK10(sK0,X0))
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2467,c_4045]) ).
tcf(c_4137,plain,
( m1_group_2(iPr_def_11,sK6)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2454,c_2470]) ).
tcf(c_4138,plain,
( m1_group_2(sK10(sK1,sK1),sK10(sK1,sK1))
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2470,c_4056]) ).
tcf(c_4139,plain,
( m1_group_2(sK10(sK1,sK0),sK10(sK1,sK0))
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2470,c_4045]) ).
tcf(c_4140,plain,
m1_group_2(iPr_def_11,sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4137,c_2495]) ).
tcf(c_4149,plain,
( m1_group_2(iPr_def_11,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2454,c_2471]) ).
tcf(c_4150,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK10(sK1,X0))
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2471,c_4056]) ).
tcf(c_4151,plain,
m1_group_2(iPr_def_11,sK1),
inference(forward_subsumption_resolution,[status(thm)],[c_4149,c_2495]) ).
tcf(c_4154,plain,
! [X0: $i] :
( m1_group_2(sK4,X0)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2460,c_2481]) ).
tcf(c_4155,plain,
! [X0: $i] :
( m1_group_2(sK4,X0)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2460,c_2480]) ).
tcf(c_4156,plain,
! [X0: $i] :
( m1_group_2(X0,sK4)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_17) ),
inference(superposition,[status(thm)],[c_2460,c_2481]) ).
tcf(c_4157,plain,
! [X0: $i] :
( m1_group_2(X0,sK4)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_17) ),
inference(superposition,[status(thm)],[c_2460,c_2480]) ).
tcf(c_4158,plain,
! [X0: $i] :
( m1_group_2(X0,sK4)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4157,c_2493]) ).
tcf(c_4166,plain,
! [X0: $i] :
( m1_group_2(sK4,X0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4155,c_2493]) ).
tcf(c_4176,plain,
u1_struct_0(sK6) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_2462,c_2496]) ).
tcf(c_4177,plain,
! [X0: $i] :
( m1_group_2(sK6,X0)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4176,c_2481]) ).
tcf(c_4178,plain,
! [X0: $i] :
( m1_group_2(sK6,X0)
| ~ m1_group_2(sK6,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4176,c_2480]) ).
tcf(c_4179,plain,
! [X0: $i] :
( m1_group_2(X0,sK6)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_18) ),
inference(superposition,[status(thm)],[c_4176,c_2481]) ).
tcf(c_4180,plain,
! [X0: $i] :
( m1_group_2(X0,sK6)
| ~ m1_group_2(sK6,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_18) ),
inference(superposition,[status(thm)],[c_4176,c_2480]) ).
tcf(c_4185,plain,
! [X0: $i] :
( m1_group_2(X0,sK6)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_18) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4179,c_2495]) ).
tcf(c_4193,plain,
! [X0: $i] :
( m1_group_2(sK6,X0)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4177,c_2495]) ).
tcf(c_4200,plain,
! [X0: $i] :
( m1_group_2(sK3,X0)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2463,c_2481]) ).
tcf(c_4201,plain,
! [X0: $i] :
( m1_group_2(sK3,X0)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2463,c_2480]) ).
tcf(c_4202,plain,
! [X0: $i] :
( m1_group_2(X0,sK3)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_20) ),
inference(superposition,[status(thm)],[c_2463,c_2481]) ).
tcf(c_4203,plain,
! [X0: $i] :
( m1_group_2(X0,sK3)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_20) ),
inference(superposition,[status(thm)],[c_2463,c_2480]) ).
tcf(c_4204,plain,
! [X0: $i] :
( m1_group_2(X0,sK3)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4203,c_2492]) ).
tcf(c_4212,plain,
! [X0: $i] :
( m1_group_2(sK3,X0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4201,c_2492]) ).
tcf(c_4222,plain,
u1_struct_0(sK5) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_2465,c_2497]) ).
tcf(c_4223,plain,
! [X0: $i] :
( m1_group_2(sK5,X0)
| ~ m1_group_2(sK5,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4222,c_2481]) ).
tcf(c_4224,plain,
! [X0: $i] :
( m1_group_2(sK5,X0)
| ~ m1_group_2(sK5,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4222,c_2480]) ).
tcf(c_4225,plain,
! [X0: $i] :
( m1_group_2(X0,sK5)
| ~ m1_group_2(sK5,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_21) ),
inference(superposition,[status(thm)],[c_4222,c_2481]) ).
tcf(c_4226,plain,
! [X0: $i] :
( m1_group_2(X0,sK5)
| ~ m1_group_2(sK5,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_21) ),
inference(superposition,[status(thm)],[c_4222,c_2480]) ).
tcf(c_4231,plain,
! [X0: $i] :
( m1_group_2(X0,sK5)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4225,c_2494]) ).
tcf(c_4239,plain,
! [X0: $i] :
( m1_group_2(sK5,X0)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4223,c_2494]) ).
tcf(c_4250,plain,
m1_group_2(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_4151,c_4056]) ).
tcf(c_4261,plain,
( m1_group_2(sK5,sK4)
| ~ r1_tarski(iPr_def_21,iPr_def_17)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_4222,c_4158]) ).
tcf(c_4262,plain,
( m1_group_2(sK0,sK4)
| ~ r1_tarski(iPr_def_12,iPr_def_17)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2455,c_4158]) ).
tcf(c_4263,plain,
( m1_group_2(sK1,sK4)
| ~ r1_tarski(iPr_def_13,iPr_def_17)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4158]) ).
tcf(c_4265,plain,
( m1_group_2(sK6,sK4)
| ~ r1_tarski(iPr_def_18,iPr_def_17)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_4176,c_4158]) ).
tcf(c_4285,plain,
( m1_group_2(sK4,sK5)
| ~ r1_tarski(iPr_def_17,iPr_def_21)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_4222,c_4166]) ).
tcf(c_4287,plain,
( m1_group_2(sK4,sK1)
| ~ r1_tarski(iPr_def_17,iPr_def_13)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4166]) ).
tcf(c_4288,plain,
( m1_group_2(sK4,sK3)
| ~ r1_tarski(iPr_def_17,iPr_def_20)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4166]) ).
tcf(c_4289,plain,
( m1_group_2(sK4,sK6)
| ~ r1_tarski(iPr_def_17,iPr_def_18)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_4176,c_4166]) ).
tcf(c_4294,plain,
( m1_group_2(sK4,sK3)
| ~ r1_tarski(iPr_def_17,iPr_def_20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4288,c_2492]) ).
tcf(c_4313,plain,
( m1_group_2(sK5,sK6)
| ~ r1_tarski(iPr_def_21,iPr_def_18)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_4222,c_4185]) ).
tcf(c_4314,plain,
( m1_group_2(sK0,sK6)
| ~ r1_tarski(iPr_def_12,iPr_def_18)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2455,c_4185]) ).
tcf(c_4315,plain,
( m1_group_2(sK1,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2456,c_4185]) ).
tcf(c_4316,plain,
( m1_group_2(sK3,sK6)
| ~ r1_tarski(iPr_def_20,iPr_def_18)
| ~ m1_group_2(sK3,sK1) ),
inference(superposition,[status(thm)],[c_2463,c_4185]) ).
tcf(c_4318,plain,
( m1_group_2(sK4,sK6)
| ~ r1_tarski(iPr_def_17,iPr_def_18)
| ~ m1_group_2(sK4,sK1) ),
inference(superposition,[status(thm)],[c_2460,c_4185]) ).
tcf(c_4331,plain,
~ r1_tarski(iPr_def_21,iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_4313,c_2476,c_2494]) ).
tcf(c_4338,plain,
( m1_group_2(sK6,sK5)
| ~ r1_tarski(iPr_def_18,iPr_def_21)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_4222,c_4193]) ).
tcf(c_4339,plain,
( m1_group_2(sK6,sK0)
| ~ r1_tarski(iPr_def_18,iPr_def_12)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2455,c_4193]) ).
tcf(c_4341,plain,
( m1_group_2(sK6,sK3)
| ~ r1_tarski(iPr_def_18,iPr_def_20)
| ~ m1_group_2(sK3,sK1) ),
inference(superposition,[status(thm)],[c_2463,c_4193]) ).
tcf(c_4343,plain,
( m1_group_2(sK6,sK4)
| ~ r1_tarski(iPr_def_18,iPr_def_17)
| ~ m1_group_2(sK4,sK1) ),
inference(superposition,[status(thm)],[c_2460,c_4193]) ).
tcf(c_4353,plain,
( m1_group_2(sK6,sK5)
| ~ r1_tarski(iPr_def_18,iPr_def_21) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4338,c_2494]) ).
tcf(c_4366,plain,
( m1_group_2(sK5,sK3)
| ~ r1_tarski(iPr_def_21,iPr_def_20)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_4222,c_4204]) ).
tcf(c_4367,plain,
( m1_group_2(sK0,sK3)
| ~ r1_tarski(iPr_def_12,iPr_def_20)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2455,c_4204]) ).
tcf(c_4368,plain,
( m1_group_2(sK1,sK3)
| ~ r1_tarski(iPr_def_13,iPr_def_20)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4204]) ).
tcf(c_4370,plain,
( m1_group_2(sK6,sK3)
| ~ r1_tarski(iPr_def_18,iPr_def_20)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_4176,c_4204]) ).
tcf(c_4384,plain,
k9_relat_1(sK2,iPr_def_17) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2461,c_2485]) ).
tcf(c_4385,plain,
m1_subset_1(iPr_def_18,iPr_def_16),
inference(superposition,[status(thm)],[c_4384,c_4018]) ).
tcf(c_4390,plain,
( v1_xboole_0(iPr_def_14)
| m1_subset_1(sK15(iPr_def_14),iPr_def_15) ),
inference(superposition,[status(thm)],[c_2458,c_102]) ).
tcf(c_4391,plain,
( v1_xboole_0(iPr_def_13)
| m1_subset_1(sK15(iPr_def_13),iPr_def_16) ),
inference(superposition,[status(thm)],[c_2459,c_102]) ).
tcf(c_4405,plain,
k1_xboole_0 = sK16,
inference(superposition,[status(thm)],[c_104,c_129]) ).
tcf(c_4406,plain,
! [X0: $i] : sK18(X0) = k1_xboole_0,
inference(superposition,[status(thm)],[c_109,c_129]) ).
tcf(c_4408,plain,
! [X0: $i] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(demodulation,[status(thm)],[c_108,c_4406]) ).
tcf(c_4410,plain,
m1_subset_1(k1_xboole_0,iPr_def_16),
inference(demodulation,[status(thm)],[c_4102,c_4406]) ).
tcf(c_4411,plain,
m1_subset_1(k1_xboole_0,iPr_def_15),
inference(demodulation,[status(thm)],[c_4100,c_4406]) ).
tcf(c_4420,plain,
( m1_group_2(sK3,sK5)
| ~ r1_tarski(iPr_def_20,iPr_def_21)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_4222,c_4212]) ).
tcf(c_4422,plain,
( m1_group_2(sK3,sK1)
| ~ r1_tarski(iPr_def_20,iPr_def_13)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4212]) ).
tcf(c_4424,plain,
( m1_group_2(sK3,sK6)
| ~ r1_tarski(iPr_def_20,iPr_def_18)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_4176,c_4212]) ).
tcf(c_4442,plain,
( m1_group_2(sK0,sK5)
| ~ r1_tarski(iPr_def_12,iPr_def_21)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2455,c_4231]) ).
tcf(c_4443,plain,
( m1_group_2(sK1,sK5)
| ~ r1_tarski(iPr_def_13,iPr_def_21)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2456,c_4231]) ).
tcf(c_4444,plain,
( m1_group_2(sK3,sK5)
| ~ r1_tarski(iPr_def_20,iPr_def_21)
| ~ m1_group_2(sK3,sK1) ),
inference(superposition,[status(thm)],[c_2463,c_4231]) ).
tcf(c_4446,plain,
( m1_group_2(sK4,sK5)
| ~ r1_tarski(iPr_def_17,iPr_def_21)
| ~ m1_group_2(sK4,sK1) ),
inference(superposition,[status(thm)],[c_2460,c_4231]) ).
tcf(c_4466,plain,
( m1_group_2(sK5,sK0)
| ~ r1_tarski(iPr_def_21,iPr_def_12)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2455,c_4239]) ).
tcf(c_4468,plain,
( m1_group_2(sK5,sK3)
| ~ r1_tarski(iPr_def_21,iPr_def_20)
| ~ m1_group_2(sK3,sK1) ),
inference(superposition,[status(thm)],[c_2463,c_4239]) ).
tcf(c_4470,plain,
( m1_group_2(sK5,sK4)
| ~ r1_tarski(iPr_def_21,iPr_def_17)
| ~ m1_group_2(sK4,sK1) ),
inference(superposition,[status(thm)],[c_2460,c_4239]) ).
tcf(c_4510,plain,
k9_relat_1(sK2,iPr_def_20) = iPr_def_21,
inference(demodulation,[status(thm)],[c_2464,c_2485]) ).
tcf(c_4511,plain,
m1_subset_1(iPr_def_21,iPr_def_16),
inference(superposition,[status(thm)],[c_4510,c_4018]) ).
tcf(c_4524,plain,
! [X0: $i] :
( m1_subset_1(X0,iPr_def_15)
| ~ r1_tarski(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2458,c_124]) ).
tcf(c_4525,plain,
! [X0: $i] :
( m1_subset_1(X0,iPr_def_16)
| ~ r1_tarski(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_2459,c_124]) ).
tcf(c_4536,plain,
! [X0: $i] : r1_tarski(sK12(k1_zfmisc_1(X0)),X0),
inference(superposition,[status(thm)],[c_92,c_125]) ).
tcf(c_4537,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r1_tarski(sK15(X0),X0) ),
inference(superposition,[status(thm)],[c_102,c_125]) ).
tcf(c_4539,plain,
! [X0: $i] :
( r1_tarski(X0,iPr_def_14)
| ~ m1_subset_1(X0,iPr_def_15) ),
inference(superposition,[status(thm)],[c_2458,c_125]) ).
tcf(c_4540,plain,
! [X0: $i] :
( r1_tarski(X0,iPr_def_13)
| ~ m1_subset_1(X0,iPr_def_16) ),
inference(superposition,[status(thm)],[c_2459,c_125]) ).
tcf(c_4552,plain,
! [X0: $i] : r1_tarski(k1_xboole_0,X0),
inference(superposition,[status(thm)],[c_4408,c_125]) ).
tcf(c_4614,plain,
! [X0: $i,X1: $i] : v1_relat_1(sK12(k1_zfmisc_1(k2_zfmisc_1(X0,X1)))),
inference(superposition,[status(thm)],[c_92,c_70]) ).
tcf(c_4615,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(k2_zfmisc_1(X0,X1))
| v1_relat_1(sK15(k2_zfmisc_1(X0,X1))) ),
inference(superposition,[status(thm)],[c_102,c_70]) ).
tcf(c_4616,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ r1_tarski(X0,k2_zfmisc_1(X1,X2)) ),
inference(superposition,[status(thm)],[c_124,c_70]) ).
tcf(c_4617,plain,
v1_relat_1(k1_xboole_0),
inference(superposition,[status(thm)],[c_4408,c_70]) ).
tcf(c_4618,plain,
! [X0: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(iPr_def_14)) ),
inference(superposition,[status(thm)],[c_2457,c_70]) ).
tcf(c_4619,plain,
! [X0: $i] :
( v1_relat_1(X0)
| ~ m1_subset_1(X0,iPr_def_15) ),
inference(light_normalisation,[status(thm)],[c_4618,c_2458]) ).
tcf(c_4635,plain,
( v1_xboole_0(iPr_def_13)
| v1_xboole_0(iPr_def_12)
| ~ v1_xboole_0(iPr_def_14) ),
inference(superposition,[status(thm)],[c_2457,c_97]) ).
tcf(c_4645,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r2_hidden(sK12(X0),X0) ),
inference(superposition,[status(thm)],[c_92,c_123]) ).
tcf(c_4646,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v1_xboole_0(k1_zfmisc_1(X0))
| r2_hidden(sK15(X0),k1_zfmisc_1(X0)) ),
inference(superposition,[status(thm)],[c_102,c_123]) ).
tcf(c_4647,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(k1_zfmisc_1(X1))
| r2_hidden(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(superposition,[status(thm)],[c_124,c_123]) ).
tcf(c_4648,plain,
( v1_xboole_0(iPr_def_15)
| r2_hidden(sK2,iPr_def_15) ),
inference(superposition,[status(thm)],[c_2482,c_123]) ).
tcf(c_4649,plain,
! [X0: $i] :
( v1_xboole_0(iPr_def_16)
| r2_hidden(k9_relat_1(sK2,X0),iPr_def_16) ),
inference(superposition,[status(thm)],[c_4018,c_123]) ).
tcf(c_4650,plain,
( v1_xboole_0(iPr_def_16)
| r2_hidden(iPr_def_18,iPr_def_16) ),
inference(superposition,[status(thm)],[c_4385,c_123]) ).
tcf(c_4651,plain,
! [X0: $i] :
( v1_xboole_0(k1_zfmisc_1(X0))
| r2_hidden(k1_xboole_0,k1_zfmisc_1(X0)) ),
inference(superposition,[status(thm)],[c_4408,c_123]) ).
tcf(c_4652,plain,
( v1_xboole_0(iPr_def_16)
| r2_hidden(k1_xboole_0,iPr_def_16) ),
inference(superposition,[status(thm)],[c_4410,c_123]) ).
tcf(c_4653,plain,
( v1_xboole_0(iPr_def_15)
| r2_hidden(k1_xboole_0,iPr_def_15) ),
inference(superposition,[status(thm)],[c_4411,c_123]) ).
tcf(c_4654,plain,
( v1_xboole_0(iPr_def_16)
| r2_hidden(iPr_def_21,iPr_def_16) ),
inference(superposition,[status(thm)],[c_4511,c_123]) ).
tcf(c_4655,plain,
r2_hidden(iPr_def_21,iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_4654,c_4103]) ).
tcf(c_4656,plain,
r2_hidden(k1_xboole_0,iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_4653,c_4101]) ).
tcf(c_4657,plain,
r2_hidden(k1_xboole_0,iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_4652,c_4103]) ).
tcf(c_4658,plain,
r2_hidden(iPr_def_18,iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_4650,c_4103]) ).
tcf(c_4659,plain,
r2_hidden(sK2,iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_4648,c_4101]) ).
tcf(c_4662,plain,
! [X0: $i] : r2_hidden(k1_xboole_0,k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_4651,c_95]) ).
tcf(c_4663,plain,
! [X0: $i] : r2_hidden(k9_relat_1(sK2,X0),iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_4649,c_4103]) ).
tcf(c_4664,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r2_hidden(sK15(X0),k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4646,c_95]) ).
tcf(c_4667,plain,
! [X0: $i,X1: $i] :
( r2_hidden(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4647,c_95]) ).
tcf(c_4679,plain,
~ r2_hidden(iPr_def_16,iPr_def_21),
inference(superposition,[status(thm)],[c_4655,c_68]) ).
tcf(c_4684,plain,
~ r2_hidden(iPr_def_15,k1_xboole_0),
inference(superposition,[status(thm)],[c_4656,c_68]) ).
tcf(c_4687,plain,
~ r2_hidden(iPr_def_16,k1_xboole_0),
inference(superposition,[status(thm)],[c_4657,c_68]) ).
tcf(c_4758,plain,
( v3_struct_0(sK1)
| m1_group_2(sK9(sK1),sK9(sK1))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_89,c_4056]) ).
tcf(c_4759,plain,
( v3_struct_0(sK0)
| m1_group_2(sK9(sK0),sK9(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_89,c_4045]) ).
tcf(c_4760,plain,
m1_group_2(sK9(sK0),sK9(sK0)),
inference(forward_subsumption_resolution,[status(thm)],[c_4759,c_2488,c_2486,c_2487]) ).
tcf(c_4761,plain,
m1_group_2(sK9(sK1),sK9(sK1)),
inference(forward_subsumption_resolution,[status(thm)],[c_4758,c_2491,c_2489,c_2490]) ).
tcf(c_4772,plain,
( v3_group_1(sK6)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2495,c_80]) ).
tcf(c_4773,plain,
( v3_group_1(sK5)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2494,c_80]) ).
tcf(c_4774,plain,
( v3_group_1(sK4)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2493,c_80]) ).
tcf(c_4775,plain,
( v3_group_1(sK3)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2492,c_80]) ).
tcf(c_4776,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_group_1(sK9(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ),
inference(superposition,[status(thm)],[c_89,c_80]) ).
tcf(c_4778,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| v3_group_1(sK10(sK1,X0))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2471,c_80]) ).
tcf(c_4780,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_group_1(sK10(sK0,X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2466,c_80]) ).
tcf(c_4781,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_group_1(sK10(sK0,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2467,c_80]) ).
tcf(c_4787,plain,
( v3_group_1(iPr_def_11)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_4151,c_80]) ).
tcf(c_4789,plain,
v3_group_1(iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_4787,c_2491,c_2489,c_2490]) ).
tcf(c_4794,plain,
v3_group_1(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4775,c_2488,c_2486,c_2487]) ).
tcf(c_4795,plain,
v3_group_1(sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_4774,c_2488,c_2486,c_2487]) ).
tcf(c_4796,plain,
v3_group_1(sK5),
inference(forward_subsumption_resolution,[status(thm)],[c_4773,c_2491,c_2489,c_2490]) ).
tcf(c_4797,plain,
v3_group_1(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4772,c_2491,c_2489,c_2490]) ).
tcf(c_4802,plain,
! [X0: $i] :
( v3_group_1(sK10(sK0,X0))
| ~ m1_group_2(X0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4781,c_2488,c_2486,c_2487]) ).
tcf(c_4815,plain,
! [X0: $i] :
( v3_group_1(sK10(sK1,X0))
| ~ m1_group_2(X0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4778,c_2491,c_2489,c_2490]) ).
tcf(c_4837,plain,
( l1_group_1(sK6)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2495,c_81]) ).
tcf(c_4838,plain,
( l1_group_1(sK5)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2494,c_81]) ).
tcf(c_4839,plain,
( l1_group_1(sK4)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2493,c_81]) ).
tcf(c_4840,plain,
( l1_group_1(sK3)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2492,c_81]) ).
tcf(c_4841,plain,
! [X0: $i] :
( v3_struct_0(X0)
| l1_group_1(sK9(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0) ),
inference(superposition,[status(thm)],[c_89,c_81]) ).
tcf(c_4843,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| l1_group_1(sK10(sK1,X0))
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2471,c_81]) ).
tcf(c_4845,plain,
! [X0: $i] :
( v3_struct_0(X0)
| l1_group_1(sK10(sK0,X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2466,c_81]) ).
tcf(c_4846,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| l1_group_1(sK10(sK0,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2467,c_81]) ).
tcf(c_4852,plain,
( l1_group_1(iPr_def_11)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_4151,c_81]) ).
tcf(c_4854,plain,
l1_group_1(iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_4852,c_2491,c_2489,c_2490]) ).
tcf(c_4859,plain,
l1_group_1(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4840,c_2488,c_2486,c_2487]) ).
tcf(c_4860,plain,
l1_group_1(sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_4839,c_2488,c_2486,c_2487]) ).
tcf(c_4861,plain,
l1_group_1(sK5),
inference(forward_subsumption_resolution,[status(thm)],[c_4838,c_2491,c_2489,c_2490]) ).
tcf(c_4862,plain,
l1_group_1(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4837,c_2491,c_2489,c_2490]) ).
tcf(c_4867,plain,
! [X0: $i] :
( l1_group_1(sK10(sK0,X0))
| ~ m1_group_2(X0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4846,c_2488,c_2486,c_2487]) ).
tcf(c_4880,plain,
! [X0: $i] :
( l1_group_1(sK10(sK1,X0))
| ~ m1_group_2(X0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4843,c_2491,c_2489,c_2490]) ).
tcf(c_4902,plain,
! [X0: $i] :
( r1_tarski(iPr_def_18,k9_relat_1(sK2,X0))
| ~ v1_relat_1(sK2)
| ~ r1_tarski(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_4384,c_121]) ).
tcf(c_4903,plain,
! [X0: $i] :
( r1_tarski(iPr_def_21,k9_relat_1(sK2,X0))
| ~ v1_relat_1(sK2)
| ~ r1_tarski(iPr_def_20,X0) ),
inference(superposition,[status(thm)],[c_4510,c_121]) ).
tcf(c_4904,plain,
! [X0: $i] :
( r1_tarski(k9_relat_1(sK2,X0),iPr_def_18)
| ~ v1_relat_1(sK2)
| ~ r1_tarski(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_4384,c_121]) ).
tcf(c_4905,plain,
! [X0: $i] :
( r1_tarski(k9_relat_1(sK2,X0),iPr_def_21)
| ~ v1_relat_1(sK2)
| ~ r1_tarski(X0,iPr_def_20) ),
inference(superposition,[status(thm)],[c_4510,c_121]) ).
tcf(c_4935,plain,
( m1_group_2(sK6,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2495,c_2478]) ).
tcf(c_4936,plain,
( m1_group_2(sK5,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2494,c_2478]) ).
tcf(c_4939,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK9(X0),sK0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_89,c_2478]) ).
tcf(c_4941,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2471,c_2478]) ).
tcf(c_4942,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2470,c_2478]) ).
tcf(c_4944,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK0)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2467,c_2478]) ).
tcf(c_4949,plain,
( m1_group_2(iPr_def_11,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_4140,c_2478]) ).
tcf(c_4950,plain,
( m1_group_2(iPr_def_11,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_4151,c_2478]) ).
tcf(c_5001,plain,
( v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v3_struct_0(sK6) ),
inference(superposition,[status(thm)],[c_2495,c_79]) ).
tcf(c_5002,plain,
( v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v3_struct_0(sK5) ),
inference(superposition,[status(thm)],[c_2494,c_79]) ).
tcf(c_5003,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(sK4) ),
inference(superposition,[status(thm)],[c_2493,c_79]) ).
tcf(c_5004,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(sK3) ),
inference(superposition,[status(thm)],[c_2492,c_79]) ).
tcf(c_5005,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v3_struct_0(sK9(X0)) ),
inference(superposition,[status(thm)],[c_89,c_79]) ).
tcf(c_5006,plain,
( v3_struct_0(sK4)
| ~ l1_group_1(sK4)
| ~ v3_group_1(sK4)
| ~ v3_struct_0(sK3) ),
inference(superposition,[status(thm)],[c_2472,c_79]) ).
tcf(c_5007,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ m1_group_2(X0,sK1)
| ~ v3_struct_0(sK10(sK1,X0)) ),
inference(superposition,[status(thm)],[c_2471,c_79]) ).
tcf(c_5010,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK0)
| ~ v3_struct_0(sK10(sK0,X0)) ),
inference(superposition,[status(thm)],[c_2467,c_79]) ).
tcf(c_5016,plain,
( v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v3_struct_0(iPr_def_11) ),
inference(superposition,[status(thm)],[c_4151,c_79]) ).
tcf(c_5020,plain,
~ v3_struct_0(iPr_def_11),
inference(forward_subsumption_resolution,[status(thm)],[c_5016,c_2491,c_2489,c_2490]) ).
tcf(c_5024,plain,
~ v3_struct_0(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_5004,c_2488,c_2486,c_2487]) ).
tcf(c_5025,plain,
~ v3_struct_0(sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_5003,c_2488,c_2486,c_2487]) ).
tcf(c_5026,plain,
~ v3_struct_0(sK5),
inference(forward_subsumption_resolution,[status(thm)],[c_5002,c_2491,c_2489,c_2490]) ).
tcf(c_5027,plain,
~ v3_struct_0(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_5001,c_2491,c_2489,c_2490]) ).
tcf(c_5032,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| ~ v3_struct_0(sK10(sK0,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5010,c_2488,c_2486,c_2487]) ).
tcf(c_5040,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| ~ v3_struct_0(sK10(sK1,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5007,c_2491,c_2489,c_2490]) ).
tcf(c_5073,plain,
! [X0: $i] :
( v3_struct_0(sK5)
| v3_struct_0(X0)
| m1_group_2(sK5,X0)
| ~ l1_group_1(sK5)
| ~ v3_group_1(sK5)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(sK5),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_21) != u1_group_1(sK5) ) ),
inference(superposition,[status(thm)],[c_4222,c_74]) ).
tcf(c_5074,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_struct_0(X0)
| m1_group_2(sK0,X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(sK0),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_12) != u1_group_1(sK0) ) ),
inference(superposition,[status(thm)],[c_2455,c_74]) ).
tcf(c_5075,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| v3_struct_0(X0)
| m1_group_2(sK1,X0)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(sK1),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_13) != u1_group_1(sK1) ) ),
inference(superposition,[status(thm)],[c_2456,c_74]) ).
tcf(c_5076,plain,
! [X0: $i] :
( v3_struct_0(sK3)
| v3_struct_0(X0)
| m1_group_2(sK3,X0)
| ~ l1_group_1(sK3)
| ~ v3_group_1(sK3)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(sK3),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_20) != u1_group_1(sK3) ) ),
inference(superposition,[status(thm)],[c_2463,c_74]) ).
tcf(c_5077,plain,
! [X0: $i] :
( v3_struct_0(sK6)
| v3_struct_0(X0)
| m1_group_2(sK6,X0)
| ~ l1_group_1(sK6)
| ~ v3_group_1(sK6)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(sK6),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK6) ) ),
inference(superposition,[status(thm)],[c_4176,c_74]) ).
tcf(c_5078,plain,
! [X0: $i] :
( v3_struct_0(sK4)
| v3_struct_0(X0)
| m1_group_2(sK4,X0)
| ~ l1_group_1(sK4)
| ~ v3_group_1(sK4)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(u1_struct_0(sK4),u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK4) ) ),
inference(superposition,[status(thm)],[c_2460,c_74]) ).
tcf(c_5079,plain,
! [X0: $i] :
( v3_struct_0(sK4)
| v3_struct_0(X0)
| m1_group_2(sK4,X0)
| ~ l1_group_1(sK4)
| ~ v3_group_1(sK4)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK4) ) ),
inference(light_normalisation,[status(thm)],[c_5078,c_2460]) ).
tcf(c_5080,plain,
! [X0: $i] :
( v3_struct_0(sK4)
| v3_struct_0(X0)
| m1_group_2(sK4,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK4) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5079,c_4860,c_4795]) ).
tcf(c_5088,plain,
! [X0: $i] :
( v3_struct_0(sK6)
| v3_struct_0(X0)
| m1_group_2(sK6,X0)
| ~ l1_group_1(sK6)
| ~ v3_group_1(sK6)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK6) ) ),
inference(light_normalisation,[status(thm)],[c_5077,c_4176]) ).
tcf(c_5089,plain,
! [X0: $i] :
( v3_struct_0(sK6)
| v3_struct_0(X0)
| m1_group_2(sK6,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK6) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5088,c_4862,c_4797]) ).
tcf(c_5097,plain,
! [X0: $i] :
( v3_struct_0(sK3)
| v3_struct_0(X0)
| m1_group_2(sK3,X0)
| ~ l1_group_1(sK3)
| ~ v3_group_1(sK3)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_20) != u1_group_1(sK3) ) ),
inference(light_normalisation,[status(thm)],[c_5076,c_2463]) ).
tcf(c_5098,plain,
! [X0: $i] :
( v3_struct_0(sK3)
| v3_struct_0(X0)
| m1_group_2(sK3,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_20) != u1_group_1(sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5097,c_4859,c_4794]) ).
tcf(c_5106,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| v3_struct_0(X0)
| m1_group_2(sK1,X0)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_13,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_13) != u1_group_1(sK1) ) ),
inference(light_normalisation,[status(thm)],[c_5075,c_2456]) ).
tcf(c_5107,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK1,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_13,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_13) != u1_group_1(sK1) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5106,c_2491,c_2489,c_2490]) ).
tcf(c_5114,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_struct_0(X0)
| m1_group_2(sK0,X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_12,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_12) != u1_group_1(sK0) ) ),
inference(light_normalisation,[status(thm)],[c_5074,c_2455]) ).
tcf(c_5115,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK0,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_12,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_12) != u1_group_1(sK0) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5114,c_2488,c_2486,c_2487]) ).
tcf(c_5122,plain,
! [X0: $i] :
( v3_struct_0(sK5)
| v3_struct_0(X0)
| m1_group_2(sK5,X0)
| ~ l1_group_1(sK5)
| ~ v3_group_1(sK5)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_21) != u1_group_1(sK5) ) ),
inference(light_normalisation,[status(thm)],[c_5073,c_4222]) ).
tcf(c_5123,plain,
! [X0: $i] :
( v3_struct_0(sK5)
| v3_struct_0(X0)
| m1_group_2(sK5,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_21) != u1_group_1(sK5) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5122,c_4861,c_4796]) ).
tcf(c_5142,plain,
~ r2_hidden(iPr_def_16,iPr_def_18),
inference(superposition,[status(thm)],[c_4658,c_68]) ).
tcf(c_5145,plain,
~ r2_hidden(iPr_def_15,sK2),
inference(superposition,[status(thm)],[c_4659,c_68]) ).
tcf(c_5160,plain,
( v3_group_1(iPr_def_10)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2453,c_4802]) ).
tcf(c_5172,plain,
( l1_group_1(iPr_def_10)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2453,c_4867]) ).
tcf(c_5184,plain,
( ~ v3_struct_0(iPr_def_10)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2453,c_5032]) ).
tcf(c_5195,plain,
( m1_group_2(sK4,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2493,c_2479]) ).
tcf(c_5196,plain,
( m1_group_2(sK3,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2492,c_2479]) ).
tcf(c_5197,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK9(X0),sK1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_89,c_2479]) ).
tcf(c_5198,plain,
( m1_group_2(sK3,sK1)
| ~ m1_group_2(sK4,sK1) ),
inference(superposition,[status(thm)],[c_2472,c_2479]) ).
tcf(c_5199,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(sK1,sK1)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2471,c_2479]) ).
tcf(c_5201,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(X0,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2466,c_2479]) ).
tcf(c_5202,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2467,c_2479]) ).
tcf(c_5245,plain,
! [X0: $i] : ~ r2_hidden(k1_zfmisc_1(X0),k1_xboole_0),
inference(superposition,[status(thm)],[c_4662,c_68]) ).
tcf(c_5249,plain,
r1_tarski(sK12(iPr_def_15),iPr_def_14),
inference(superposition,[status(thm)],[c_2458,c_4536]) ).
tcf(c_5250,plain,
r1_tarski(sK12(iPr_def_16),iPr_def_13),
inference(superposition,[status(thm)],[c_2459,c_4536]) ).
tcf(c_5306,plain,
! [X0: $i] : ~ r2_hidden(iPr_def_16,k9_relat_1(sK2,X0)),
inference(superposition,[status(thm)],[c_4663,c_68]) ).
tcf(c_5316,plain,
( v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK20)))
| r2_hidden(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))) ),
inference(superposition,[status(thm)],[c_1218,c_123]) ).
tcf(c_5317,plain,
r1_tarski(sK21(sK20),u1_struct_0(sK20)),
inference(superposition,[status(thm)],[c_1218,c_125]) ).
tcf(c_5318,plain,
r2_hidden(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))),
inference(forward_subsumption_resolution,[status(thm)],[c_5316,c_95]) ).
tcf(c_5323,plain,
( v1_xboole_0(iPr_def_15)
| v1_xboole_0(iPr_def_14)
| r2_hidden(sK15(iPr_def_14),iPr_def_15) ),
inference(superposition,[status(thm)],[c_4390,c_123]) ).
tcf(c_5324,plain,
( v1_xboole_0(iPr_def_14)
| r2_hidden(sK15(iPr_def_14),iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5323,c_4101]) ).
tcf(c_5343,plain,
( v1_xboole_0(iPr_def_16)
| v1_xboole_0(iPr_def_13)
| r2_hidden(sK15(iPr_def_13),iPr_def_16) ),
inference(superposition,[status(thm)],[c_4391,c_123]) ).
tcf(c_5344,plain,
( v1_xboole_0(iPr_def_13)
| r2_hidden(sK15(iPr_def_13),iPr_def_16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5343,c_4103]) ).
tcf(c_5404,plain,
v1_relat_1(sK12(k1_zfmisc_1(iPr_def_14))),
inference(superposition,[status(thm)],[c_2457,c_4614]) ).
tcf(c_5405,plain,
v1_relat_1(sK12(iPr_def_15)),
inference(light_normalisation,[status(thm)],[c_5404,c_2458]) ).
tcf(c_5411,plain,
v1_relat_1(sK2),
inference(superposition,[status(thm)],[c_2482,c_4619]) ).
tcf(c_5412,plain,
( v1_xboole_0(iPr_def_14)
| v1_relat_1(sK15(iPr_def_14)) ),
inference(superposition,[status(thm)],[c_4390,c_4619]) ).
tcf(c_5424,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ r2_hidden(X0,sK12(X0)) ),
inference(superposition,[status(thm)],[c_4645,c_68]) ).
tcf(c_5449,plain,
( m1_group_2(sK6,sK3)
| ~ r1_tarski(iPr_def_18,iPr_def_20)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4178]) ).
tcf(c_5451,plain,
( m1_group_2(sK6,sK4)
| ~ r1_tarski(iPr_def_18,iPr_def_17)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4178]) ).
tcf(c_5463,plain,
( m1_group_2(sK0,sK6)
| ~ r1_tarski(iPr_def_12,iPr_def_18)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2455,c_4180]) ).
tcf(c_5464,plain,
( m1_group_2(sK1,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK6,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4180]) ).
tcf(c_5465,plain,
( m1_group_2(sK3,sK6)
| ~ r1_tarski(iPr_def_20,iPr_def_18)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4180]) ).
tcf(c_5467,plain,
( m1_group_2(sK4,sK6)
| ~ r1_tarski(iPr_def_17,iPr_def_18)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4180]) ).
tcf(c_5489,plain,
( m1_group_2(sK5,sK3)
| ~ r1_tarski(iPr_def_21,iPr_def_20)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4224]) ).
tcf(c_5491,plain,
( m1_group_2(sK5,sK4)
| ~ r1_tarski(iPr_def_21,iPr_def_17)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4224]) ).
tcf(c_5503,plain,
( m1_group_2(sK0,sK5)
| ~ r1_tarski(iPr_def_12,iPr_def_21)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_2455,c_4226]) ).
tcf(c_5504,plain,
( m1_group_2(sK1,sK5)
| ~ r1_tarski(iPr_def_13,iPr_def_21)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4226]) ).
tcf(c_5505,plain,
( m1_group_2(sK3,sK5)
| ~ r1_tarski(iPr_def_20,iPr_def_21)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4226]) ).
tcf(c_5507,plain,
( m1_group_2(sK4,sK5)
| ~ r1_tarski(iPr_def_17,iPr_def_21)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4226]) ).
tcf(c_5531,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK4) )
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ l1_group_1(X0)
| m1_group_2(sK4,X0)
| v3_struct_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5080,c_5025,c_5080]) ).
tcf(c_5532,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK4,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK4) ) ),
inference(renaming,[status(thm)],[c_5531]) ).
tcf(c_5545,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK6) )
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ l1_group_1(X0)
| m1_group_2(sK6,X0)
| v3_struct_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5089,c_5027,c_5089]) ).
tcf(c_5546,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK6,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK6) ) ),
inference(renaming,[status(thm)],[c_5545]) ).
tcf(c_5560,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_20) != u1_group_1(sK3) )
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ l1_group_1(X0)
| m1_group_2(sK3,X0)
| v3_struct_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5098,c_5024,c_5098]) ).
tcf(c_5561,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK3,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_20,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_20) != u1_group_1(sK3) ) ),
inference(renaming,[status(thm)],[c_5560]) ).
tcf(c_5583,plain,
~ r2_hidden(k1_zfmisc_1(u1_struct_0(sK20)),sK21(sK20)),
inference(superposition,[status(thm)],[c_5318,c_68]) ).
tcf(c_5584,plain,
~ v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK20))),
inference(superposition,[status(thm)],[c_5318,c_130]) ).
tcf(c_5590,plain,
( v1_xboole_0(iPr_def_14)
| ~ r2_hidden(iPr_def_15,sK15(iPr_def_14)) ),
inference(superposition,[status(thm)],[c_5324,c_68]) ).
tcf(c_5599,plain,
( v1_xboole_0(iPr_def_13)
| ~ r2_hidden(iPr_def_16,sK15(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_5344,c_68]) ).
tcf(c_5612,plain,
m1_subset_1(iPr_def_14,iPr_def_15),
inference(superposition,[status(thm)],[c_120,c_4524]) ).
tcf(c_5614,plain,
m1_subset_1(sK12(k1_zfmisc_1(iPr_def_14)),iPr_def_15),
inference(superposition,[status(thm)],[c_4536,c_4524]) ).
tcf(c_5616,plain,
m1_subset_1(sK12(iPr_def_15),iPr_def_15),
inference(superposition,[status(thm)],[c_5249,c_4524]) ).
tcf(c_5618,plain,
( v1_xboole_0(iPr_def_15)
| r2_hidden(iPr_def_14,iPr_def_15) ),
inference(superposition,[status(thm)],[c_5612,c_123]) ).
tcf(c_5619,plain,
v1_relat_1(iPr_def_14),
inference(superposition,[status(thm)],[c_5612,c_4619]) ).
tcf(c_5620,plain,
r2_hidden(iPr_def_14,iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_5618,c_4101]) ).
tcf(c_5621,plain,
~ r2_hidden(iPr_def_15,iPr_def_14),
inference(superposition,[status(thm)],[c_5620,c_68]) ).
tcf(c_5624,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_21) != u1_group_1(sK5) )
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0))
| ~ v3_group_1(X0)
| ~ l1_group_1(X0)
| m1_group_2(sK5,X0)
| v3_struct_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_5123,c_5026,c_5123]) ).
tcf(c_5625,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK5,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_21,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_21) != u1_group_1(sK5) ) ),
inference(renaming,[status(thm)],[c_5624]) ).
tcf(c_5651,plain,
( m1_group_2(sK1,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK1,sK0) ),
inference(global_subsumption_just,[status(thm)],[c_5464,c_4935,c_5464]) ).
tcf(c_5667,plain,
( m1_group_2(sK1,sK5)
| ~ r1_tarski(iPr_def_13,iPr_def_21)
| ~ m1_group_2(sK1,sK0) ),
inference(global_subsumption_just,[status(thm)],[c_5504,c_4936,c_5504]) ).
tcf(c_5687,plain,
( m1_group_2(sK0,sK0)
| ~ r1_tarski(iPr_def_12,iPr_def_12)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2455,c_4066]) ).
tcf(c_5689,plain,
( m1_group_2(sK0,sK3)
| ~ r1_tarski(iPr_def_12,iPr_def_20)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2463,c_4066]) ).
tcf(c_5691,plain,
( m1_group_2(sK0,sK4)
| ~ r1_tarski(iPr_def_12,iPr_def_17)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2460,c_4066]) ).
tcf(c_5692,plain,
( m1_group_2(sK0,sK0)
| ~ m1_group_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5687,c_120]) ).
tcf(c_5716,plain,
( m1_group_2(sK0,sK1)
| ~ r1_tarski(iPr_def_12,iPr_def_13)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4067]) ).
tcf(c_5717,plain,
( m1_group_2(sK0,sK3)
| ~ r1_tarski(iPr_def_12,iPr_def_20)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4067]) ).
tcf(c_5719,plain,
( m1_group_2(sK0,sK4)
| ~ r1_tarski(iPr_def_12,iPr_def_17)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4067]) ).
tcf(c_5732,plain,
( m1_group_2(iPr_def_10,iPr_def_10)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2453,c_4128]) ).
tcf(c_5745,plain,
m1_subset_1(iPr_def_13,iPr_def_16),
inference(superposition,[status(thm)],[c_120,c_4525]) ).
tcf(c_5747,plain,
m1_subset_1(sK12(k1_zfmisc_1(iPr_def_13)),iPr_def_16),
inference(superposition,[status(thm)],[c_4536,c_4525]) ).
tcf(c_5749,plain,
m1_subset_1(sK12(iPr_def_16),iPr_def_16),
inference(superposition,[status(thm)],[c_5250,c_4525]) ).
tcf(c_5751,plain,
( v1_xboole_0(iPr_def_16)
| r2_hidden(iPr_def_13,iPr_def_16) ),
inference(superposition,[status(thm)],[c_5745,c_123]) ).
tcf(c_5752,plain,
r2_hidden(iPr_def_13,iPr_def_16),
inference(forward_subsumption_resolution,[status(thm)],[c_5751,c_4103]) ).
tcf(c_5753,plain,
~ r2_hidden(iPr_def_16,iPr_def_13),
inference(superposition,[status(thm)],[c_5752,c_68]) ).
tcf(c_5774,plain,
r1_tarski(sK2,iPr_def_14),
inference(superposition,[status(thm)],[c_2482,c_4539]) ).
tcf(c_5775,plain,
( v1_xboole_0(iPr_def_14)
| r1_tarski(sK15(iPr_def_14),iPr_def_14) ),
inference(superposition,[status(thm)],[c_4390,c_4539]) ).
tcf(c_5776,plain,
r1_tarski(k1_xboole_0,iPr_def_14),
inference(superposition,[status(thm)],[c_4411,c_4539]) ).
tcf(c_5777,plain,
r1_tarski(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_5612,c_4539]) ).
tcf(c_5791,plain,
( m1_group_2(sK1,sK0)
| ~ r1_tarski(iPr_def_13,iPr_def_12)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2456,c_4068]) ).
tcf(c_5810,plain,
( m1_group_2(sK1,sK3)
| ~ r1_tarski(iPr_def_13,iPr_def_20)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2463,c_4082]) ).
tcf(c_5811,plain,
( m1_group_2(sK1,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_4176,c_4082]) ).
tcf(c_5812,plain,
( m1_group_2(sK1,sK4)
| ~ r1_tarski(iPr_def_13,iPr_def_17)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2460,c_4082]) ).
tcf(c_5832,plain,
( m1_group_2(sK1,sK1)
| ~ r1_tarski(iPr_def_13,iPr_def_13)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2456,c_4083]) ).
tcf(c_5833,plain,
( m1_group_2(sK1,sK3)
| ~ r1_tarski(iPr_def_13,iPr_def_20)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4083]) ).
tcf(c_5835,plain,
( m1_group_2(sK1,sK4)
| ~ r1_tarski(iPr_def_13,iPr_def_17)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4083]) ).
tcf(c_5836,plain,
( m1_group_2(sK1,sK1)
| ~ m1_group_2(sK1,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5832,c_120]) ).
tcf(c_5852,plain,
( m1_group_2(sK3,sK1)
| ~ r1_tarski(iPr_def_20,iPr_def_13)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2463,c_4085]) ).
tcf(c_5854,plain,
( m1_group_2(sK4,sK1)
| ~ r1_tarski(iPr_def_17,iPr_def_13)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2460,c_4085]) ).
tcf(c_5927,plain,
! [X0: $i] : r1_tarski(k9_relat_1(sK2,X0),iPr_def_13),
inference(superposition,[status(thm)],[c_4018,c_4540]) ).
tcf(c_5928,plain,
r1_tarski(iPr_def_18,iPr_def_13),
inference(superposition,[status(thm)],[c_4385,c_4540]) ).
tcf(c_5929,plain,
( v1_xboole_0(iPr_def_13)
| r1_tarski(sK15(iPr_def_13),iPr_def_13) ),
inference(superposition,[status(thm)],[c_4391,c_4540]) ).
tcf(c_5930,plain,
r1_tarski(k1_xboole_0,iPr_def_13),
inference(superposition,[status(thm)],[c_4410,c_4540]) ).
tcf(c_5931,plain,
r1_tarski(iPr_def_21,iPr_def_13),
inference(superposition,[status(thm)],[c_4511,c_4540]) ).
tcf(c_5932,plain,
r1_tarski(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_5745,c_4540]) ).
tcf(c_5952,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ r2_hidden(k1_zfmisc_1(X0),sK15(X0)) ),
inference(superposition,[status(thm)],[c_4664,c_68]) ).
tcf(c_5987,plain,
! [X0: $i] :
( r1_tarski(iPr_def_18,k9_relat_1(sK2,X0))
| ~ r1_tarski(iPr_def_17,X0) ),
inference(global_subsumption_just,[status(thm)],[c_4902,c_4902,c_5411]) ).
tcf(c_5994,plain,
( r1_tarski(iPr_def_18,iPr_def_18)
| ~ r1_tarski(iPr_def_17,iPr_def_17) ),
inference(superposition,[status(thm)],[c_4384,c_5987]) ).
tcf(c_5995,plain,
( r1_tarski(iPr_def_18,iPr_def_21)
| ~ r1_tarski(iPr_def_17,iPr_def_20) ),
inference(superposition,[status(thm)],[c_4510,c_5987]) ).
tcf(c_6002,plain,
! [X0: $i] :
( r1_tarski(iPr_def_21,k9_relat_1(sK2,X0))
| ~ r1_tarski(iPr_def_20,X0) ),
inference(global_subsumption_just,[status(thm)],[c_4903,c_4903,c_5411]) ).
tcf(c_6009,plain,
( r1_tarski(iPr_def_21,iPr_def_18)
| ~ r1_tarski(iPr_def_20,iPr_def_17) ),
inference(superposition,[status(thm)],[c_4384,c_6002]) ).
tcf(c_6010,plain,
( r1_tarski(iPr_def_21,iPr_def_21)
| ~ r1_tarski(iPr_def_20,iPr_def_20) ),
inference(superposition,[status(thm)],[c_4510,c_6002]) ).
tcf(c_6011,plain,
~ r1_tarski(iPr_def_20,iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_6009,c_4331]) ).
tcf(c_6023,plain,
! [X0: $i] :
( r1_tarski(k9_relat_1(sK2,X0),iPr_def_18)
| ~ r1_tarski(X0,iPr_def_17) ),
inference(global_subsumption_just,[status(thm)],[c_4904,c_4904,c_5411]) ).
tcf(c_6032,plain,
! [X0: $i] :
( r1_tarski(k9_relat_1(sK2,X0),iPr_def_21)
| ~ r1_tarski(X0,iPr_def_20) ),
inference(global_subsumption_just,[status(thm)],[c_4905,c_4905,c_5411]) ).
tcf(c_6047,plain,
( m1_group_2(iPr_def_11,sK0)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2454,c_4941]) ).
tcf(c_6048,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_4941,c_2479]) ).
tcf(c_6050,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_4941,c_2478]) ).
tcf(c_6051,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| l1_group_1(sK10(sK1,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_4941,c_81]) ).
tcf(c_6052,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_group_1(sK10(sK1,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_4941,c_80]) ).
tcf(c_6053,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK10(sK1,X0))
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_4941,c_4045]) ).
tcf(c_6066,plain,
! [X0: $i] :
( v3_group_1(sK10(sK1,X0))
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6052,c_2488,c_2486,c_2487]) ).
tcf(c_6070,plain,
! [X0: $i] :
( l1_group_1(sK10(sK1,X0))
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6051,c_2488,c_2486,c_2487]) ).
tcf(c_6100,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_6070,c_6066,c_6053,c_6052,c_6051,c_6050,c_6048,c_6047,c_6032,c_6023,c_6011,c_6010,c_6009,c_6002,c_5995,c_5994,c_5987,c_5952,c_5932,c_5931,c_5930,c_5929,c_5928,c_5927,c_5854,c_5852,c_5836,c_5835,c_5833,c_5832,c_5812,c_5811,c_5810,c_5791,c_5777,c_5776,c_5775,c_5774,c_5753,c_5752,c_5751,c_5749,c_5747,c_5745,c_5732,c_5719,c_5717,c_5716,c_5691,c_5689,c_5687,c_5667,c_5651,c_5625,c_5621,c_5620,c_5619,c_5618,c_5616,c_5614,c_5612,c_5599,c_5590,c_5584,c_5583,c_5561,c_5546,c_5532,c_5507,c_5505,c_5504,c_5503,c_5491,c_5489,c_5467,c_5465,c_5464,c_5463,c_5451,c_5449,c_5424,c_5412,c_5411,c_5405,c_5404,c_5344,c_5343,c_5324,c_5323,c_5317,c_5306,c_5250,c_5249,c_5245,c_5202,c_5201,c_5199,c_5198,c_5197,c_5196,c_5195,c_5184,c_5172,c_5160,c_5145,c_5142,c_5123,c_5122,c_5115,c_5114,c_5107,c_5106,c_5098,c_5097,c_5089,c_5088,c_5080,c_5079,c_5078,c_5077,c_5076,c_5075,c_5074,c_5073,c_5040,c_5032,c_5027,c_5026,c_5025,c_5024,c_5020,c_5016,c_5010,c_5007,c_5006,c_5005,c_5004,c_5003,c_5002,c_5001,c_4950,c_4949,c_4944,c_4942,c_4941,c_4939,c_4936,c_4935,c_4905,c_4904,c_4903,c_4902,c_4880,c_4867,c_4862,c_4861,c_4860,c_4859,c_4854,c_4852,c_4846,c_4845,c_4843,c_4841,c_4840,c_4839,c_4838,c_4837,c_4815,c_4802,c_4797,c_4796,c_4795,c_4794,c_4789,c_4787,c_4781,c_4780,c_4778,c_4776,c_4775,c_4774,c_4773,c_4772,c_4761,c_4760,c_4759,c_4758,c_4687,c_4684,c_4679,c_4663,c_4662,c_4659,c_4658,c_4657,c_4656,c_4655,c_4654,c_4653,c_4652,c_4651,c_4650,c_4649,c_4648,c_4635,c_4619,c_4618,c_4617,c_4616,c_4615,c_4552,c_4540,c_4539,c_4537,c_4525,c_4524,c_4511,c_4510,c_4470,c_4468,c_4466,c_4446,c_4444,c_4443,c_4442,c_4424,c_4422,c_4420,c_4411,c_4410,c_4408,c_4406,c_4405,c_4391,c_4390,c_4385,c_4384,c_4370,c_4368,c_4367,c_4366,c_4353,c_4343,c_4341,c_4339,c_4338,c_4331,c_4318,c_4316,c_4315,c_4314,c_4313,c_4294,c_4289,c_4288,c_4287,c_4285,c_4265,c_4263,c_4262,c_4261,c_4250,c_4239,c_4231,c_4226,c_4225,c_4224,c_4223,c_4222,c_4212,c_4204,c_4203,c_4202,c_4201,c_4200,c_4193,c_4185,c_4180,c_4179,c_4178,c_4177,c_4176,c_4166,c_4158,c_4157,c_4156,c_4155,c_4154,c_4151,c_4150,c_4149,c_4140,c_4139,c_4138,c_4137,c_4128,c_4127,c_4116,c_4115,c_4114,c_4109,c_4108,c_4103,c_4102,c_4101,c_4100,c_4085,c_4083,c_4082,c_4068,c_4067,c_4066,c_4065,c_4064,c_5692,c_4056,c_4045,c_4018,c_2497,c_2496,c_2485,c_2484,c_2483,c_2482,c_2475,c_2474,c_2465,c_2464,c_2463,c_2462,c_2461,c_2460,c_2459,c_2458,c_2457,c_2456,c_2455,c_2454,c_2453,c_5318,c_5316,c_4667,c_4647,c_4664,c_4646,c_4536,c_4645,c_4614,c_2466,c_2467,c_2468,c_2469,c_2470,c_2471,c_2472,c_2473,c_2476,c_2477,c_2478,c_2479,c_2480,c_2481,c_1401,c_1392,c_1381,c_1375,c_1369,c_1339,c_1330,c_1321,c_1303,c_1291,c_1279,c_1225,c_1218,c_1211,c_1202,c_1194,c_1186,c_1174,c_1162,c_1150,c_361,c_360,c_183,c_181,c_131,c_130,c_129,c_125,c_124,c_123,c_122,c_121,c_120,c_112,c_110,c_109,c_108,c_106,c_104,c_103,c_102,c_99,c_97,c_96,c_95,c_92,c_89,c_87,c_81,c_80,c_79,c_74,c_70,c_68,c_2486,c_2487,c_2488,c_2489,c_2490,c_2491,c_2492,c_2493,c_2494,c_2495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP637+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.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 15:22:54 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/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.08/0.41
% 0.08/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.08/0.41
% 0.08/0.41 % Detected problem language: tptp
% 0.08/0.42 % Proving...
% 3.89/1.73 % SZS status Started for theBenchmark.p
% 3.89/1.73 % SZS status Theorem for theBenchmark.p
% 3.89/1.73
% 3.89/1.73 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.89/1.73
% 3.89/1.73 % ------ iProver source info
% 3.89/1.73
% 3.89/1.73 % git: date: 2026-07-19 20:42:38 +0200
% 3.89/1.73 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.89/1.73 % git: non_committed_changes: false
% 3.89/1.73
% 3.89/1.73 % ------ Parsing...
% 3.89/1.73 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.89/1.73
% 3.89/1.73 % ------ 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 %
% 3.89/1.73
% 3.89/1.73 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.89/1.73
% 3.89/1.73 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.89/1.73 % ------ Proving...
% 3.89/1.73 % ------ Problem Properties
% 3.89/1.73
% 3.89/1.73 %
% 3.89/1.73 % clauses 99
% 3.89/1.73 % conjectures 12
% 3.89/1.73 % EPR 39
% 3.89/1.73 % Horn 86
% 3.89/1.73 % unary 52
% 3.89/1.73 % binary 20
% 3.89/1.73 % lits 195
% 3.89/1.73 % lits eq 31
% 3.89/1.73 % fd_pure 0
% 3.89/1.73 % fd_pseudo 0
% 3.89/1.73 % fd_cond 1
% 3.89/1.73 % fd_pseudo_cond 1
% 3.89/1.73 % AC symbols 0
% 3.89/1.73
% 3.89/1.73 % ------ Schedule dynamic 5 is on
% 3.89/1.73
% 3.89/1.73 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.89/1.73
% 3.89/1.73
% 3.89/1.73 % ------
% 3.89/1.73 % Current options:
% 3.89/1.73 % ------
% 3.89/1.73
% 3.89/1.73
% 3.89/1.73 %
% 3.89/1.73
% 3.89/1.73 % ------ Proving...
% 3.89/1.73 %
% 3.89/1.73
% 3.89/1.73 % SZS status Theorem for theBenchmark.p
% 3.89/1.73
% 3.89/1.73 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.89/1.76
% 3.89/1.76
%------------------------------------------------------------------------------