%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP638+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 : n026.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:58 PM UTC 2026
% Result : Theorem 3.75s 1.18s
% Output : CNFRefutation 4.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 54
% Syntax : Number of formulae : 788 ( 216 unt; 10 def)
% Number of atoms : 2837 ( 189 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 3085 (1387 ~;1461 |; 172 &)
% ( 8 <=>; 57 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 30 ( 28 usr; 11 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 13 con; 0-4 aty)
% Number of variables : 944 ( 1 sgn 908 !; 36 ?; 574 :)
% 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,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( m1_group_6(X3,X1,X4)
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
=> m1_group_6(X5,X0,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_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,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( m1_group_6(X3,X1,X4)
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
=> m1_group_6(X5,X0,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(f14,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,X0,X1)
& v1_funct_1(X2) )
=> m1_subset_1(k3_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_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_1(X2) )
=> k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_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(k10_relat_1(X2,X0),k10_relat_1(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t178_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,X1)
=> ! [X4] :
( m1_group_2(X4,X1)
=> ! [X5] :
( m1_group_2(X5,X0)
=> ! [X6] :
( m1_group_2(X6,X0)
=> ( ( m1_group_6(X3,X1,X4)
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3)) )
=> m1_group_6(X5,X0,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,X1)
& ? [X4] :
( m1_group_2(X4,X1)
& ? [X5] :
( m1_group_2(X5,X0)
& ? [X6] :
( m1_group_2(X6,X0)
& m1_group_6(X3,X1,X4)
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& ~ m1_group_6(X5,X0,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,X1)
& ? [X4] :
( m1_group_2(X4,X1)
& ? [X5] :
( m1_group_2(X5,X0)
& ? [X6] :
( m1_group_2(X6,X0)
& m1_group_6(X3,X1,X4)
& u1_struct_0(X6) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X4))
& u1_struct_0(X5) = k3_funct_2(u1_struct_0(X0),u1_struct_0(X1),X2,u1_struct_0(X3))
& ~ m1_group_6(X5,X0,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_1(X2)
| m1_subset_1(k3_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f14]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k3_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X0)) ),
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_1(X2)
| k3_funct_2(X0,X1,X2,X3) = k10_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f43]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_1(X2)
| k3_funct_2(X0,X1,X2,X3) = k10_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(k10_relat_1(X2,X0),k10_relat_1(X2,X1)) ),
inference(ennf_transformation,[],[f47]) ).
fof(f96,plain,
! [X0,X1,X2] :
( ~ v1_relat_1(X2)
| ~ r1_tarski(X0,X1)
| r1_tarski(k10_relat_1(X2,X0),k10_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,sK1)
& m1_group_2(sK4,sK1)
& m1_group_2(sK5,sK0)
& m1_group_2(sK6,sK0)
& m1_group_6(sK3,sK1,sK4)
& u1_struct_0(sK6) = k3_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK4))
& u1_struct_0(sK5) = k3_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),sK2,u1_struct_0(sK3))
& ~ m1_group_6(sK5,sK0,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,sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f141,plain,
m1_group_2(sK4,sK1),
inference(cnf_transformation,[],[f108]) ).
fof(f142,plain,
m1_group_2(sK5,sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f143,plain,
m1_group_2(sK6,sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f144,plain,
m1_group_6(sK3,sK1,sK4),
inference(cnf_transformation,[],[f108]) ).
fof(f145,plain,
u1_struct_0(sK6) = k3_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) = k3_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,sK0,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_1(X2)
| m1_subset_1(k3_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X0)) ),
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(f190,plain,
! [X0,X1] : v1_funct_1(sK17(X0,X1)),
inference(cnf_transformation,[],[f121]) ).
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_1(X2)
| k3_funct_2(X0,X1,X2,X3) = k10_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(k10_relat_1(X2,X0),k10_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,sK0,sK6),
inference(cnf_transformation,[],[f147]) ).
tcf(c_50,negated_conjecture,
k3_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,
k3_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,sK1,sK4),
inference(cnf_transformation,[],[f144]) ).
tcf(c_53,negated_conjecture,
m1_group_2(sK6,sK0),
inference(cnf_transformation,[],[f143]) ).
tcf(c_54,negated_conjecture,
m1_group_2(sK5,sK0),
inference(cnf_transformation,[],[f142]) ).
tcf(c_55,negated_conjecture,
m1_group_2(sK4,sK1),
inference(cnf_transformation,[],[f141]) ).
tcf(c_56,negated_conjecture,
m1_group_2(sK3,sK1),
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(k3_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(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_107,plain,
! [X0: $i,X1: $i] : v1_funct_1(sK17(X0,X1)),
inference(cnf_transformation,[],[f190]) ).
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] :
( ( k3_funct_2(X1,X2,X0,X3) = k10_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(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(k10_relat_1(X2,X0),k10_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_1078,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X2,X0,X1)
| ( X2 != sK2 )
| ( u1_struct_0(sK1) != X1 )
| ( u1_struct_0(sK0) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_59,c_185]) ).
tcf(c_1079,plain,
m1_relset_1(sK2,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(unflattening,[status(thm)],[c_1078]) ).
tcf(c_1083,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_1084,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_1083]) ).
tcf(c_1092,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_1093,plain,
! [X0: $i,X1: $i] : m1_relset_1(sK13(X0,X1),X0,X1),
inference(unflattening,[status(thm)],[c_1092]) ).
tcf(c_1141,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,X0,X1)
| ( X2 != sK2 )
| ( u1_struct_0(sK1) != X1 )
| ( u1_struct_0(sK0) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_58,c_72]) ).
tcf(c_1142,plain,
( v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(u1_struct_0(sK0))
| ~ 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_1141]) ).
tcf(c_1143,plain,
( v1_xboole_0(u1_struct_0(sK1))
| ~ v1_xboole_0(sK2) ),
inference(global_subsumption_just,[status(thm)],[c_1142,c_67,c_57,c_64,c_141,c_160,c_1079,c_1142]) ).
tcf(c_1151,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_1152,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_1151]) ).
tcf(c_1154,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_1152,c_84,c_1084,c_1152]) ).
tcf(c_1169,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_1170,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_1169]) ).
tcf(c_1172,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_1170,c_100,c_98,c_1170]) ).
tcf(c_1289,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_1290,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v1_xboole_0(sK21(X0)) ),
inference(unflattening,[status(thm)],[c_1289]) ).
tcf(c_1301,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_1302,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_1301]) ).
tcf(c_1313,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_1314,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(unflattening,[status(thm)],[c_1313]) ).
tcf(c_1325,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_1326,plain,
( v3_struct_0(sK8)
| ~ v1_xboole_0(sK21(sK8)) ),
inference(unflattening,[status(thm)],[c_1325]) ).
tcf(c_1333,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_1334,plain,
( v3_struct_0(sK8)
| m1_subset_1(sK21(sK8),k1_zfmisc_1(u1_struct_0(sK8))) ),
inference(unflattening,[status(thm)],[c_1333]) ).
tcf(c_1341,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_1342,plain,
( v3_struct_0(sK8)
| ~ v1_xboole_0(u1_struct_0(sK8)) ),
inference(unflattening,[status(thm)],[c_1341]) ).
tcf(c_1349,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_1350,plain,
( v3_struct_0(sK20)
| ~ v1_xboole_0(sK21(sK20)) ),
inference(unflattening,[status(thm)],[c_1349]) ).
tcf(c_1351,plain,
~ v1_xboole_0(sK21(sK20)),
inference(global_subsumption_just,[status(thm)],[c_1350,c_112,c_1350]) ).
tcf(c_1356,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_1357,plain,
( v3_struct_0(sK20)
| m1_subset_1(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))) ),
inference(unflattening,[status(thm)],[c_1356]) ).
tcf(c_1358,plain,
m1_subset_1(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))),
inference(global_subsumption_just,[status(thm)],[c_1357,c_112,c_1357]) ).
tcf(c_1363,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_1364,plain,
( v3_struct_0(sK20)
| ~ v1_xboole_0(u1_struct_0(sK20)) ),
inference(unflattening,[status(thm)],[c_1363]) ).
tcf(c_1365,plain,
~ v1_xboole_0(u1_struct_0(sK20)),
inference(global_subsumption_just,[status(thm)],[c_1364,c_112,c_1364]) ).
tcf(c_1565,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_1566,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_1565]) ).
tcf(c_1568,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_1566,c_63,c_61,c_60,c_1566]) ).
tcf(c_1569,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_1568]) ).
tcf(c_1580,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_1581,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_1580]) ).
tcf(c_1583,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_1581,c_63,c_61,c_60,c_1581]) ).
tcf(c_1584,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_1583]) ).
tcf(c_1595,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_1596,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_1595]) ).
tcf(c_1598,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| m1_group_6(sK10(sK1,X0),sK1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1596,c_63,c_61,c_60,c_1596]) ).
tcf(c_1599,plain,
! [X0: $i] :
( m1_group_6(sK10(sK1,X0),sK1,X0)
| ~ m1_group_2(X0,sK1) ),
inference(renaming,[status(thm)],[c_1598]) ).
tcf(c_1607,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_1608,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_1607]) ).
tcf(c_1609,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_1608,c_63,c_61,c_60,c_1608]) ).
tcf(c_1610,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_1609]) ).
tcf(c_1620,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_1621,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_1620]) ).
tcf(c_1623,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_1621,c_63,c_61,c_60,c_1621]) ).
tcf(c_1624,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_1623]) ).
tcf(c_1638,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_1639,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_1638]) ).
tcf(c_1640,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_1639,c_67,c_65,c_64,c_1639]) ).
tcf(c_1641,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_1640]) ).
tcf(c_1651,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_1652,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_1651]) ).
tcf(c_1654,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_1652,c_67,c_65,c_64,c_1652]) ).
tcf(c_1655,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_1654]) ).
tcf(c_1666,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_1667,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_1666]) ).
tcf(c_1669,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| m1_group_6(sK10(sK0,X0),sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1667,c_67,c_65,c_64,c_1667]) ).
tcf(c_1670,plain,
! [X0: $i] :
( m1_group_6(sK10(sK0,X0),sK0,X0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_1669]) ).
tcf(c_1678,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_1679,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_1678]) ).
tcf(c_1680,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_1679,c_67,c_65,c_64,c_1679]) ).
tcf(c_1681,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_1680]) ).
tcf(c_1691,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_1692,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_1691]) ).
tcf(c_1693,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_1692,c_67,c_65,c_64,c_1692]) ).
tcf(c_1694,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_1693]) ).
tcf(c_1737,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_1584,c_1610]) ).
tcf(c_1738,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_1737]) ).
tcf(c_1750,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_1655,c_1681]) ).
tcf(c_1751,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_1750]) ).
tcf(c_1763,plain,
( ( sK6 != sK4 )
| ( sK0 != sK1 )
| ( sK5 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_52]) ).
tcf(c_1784,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| ( sK0 != sK1 )
| ( X0 != sK6 )
| ( sK10(sK1,X0) != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_1599]) ).
tcf(c_1785,plain,
( ~ m1_group_2(sK6,sK1)
| ( sK0 != sK1 )
| ( sK10(sK1,sK6) != sK5 ) ),
inference(unflattening,[status(thm)],[c_1784]) ).
tcf(c_1795,plain,
! [X0: $i,X1: $i] :
( ~ m1_group_2(X1,sK0)
| ~ m1_group_2(X0,X1)
| ( sK0 != sK0 )
| ( X1 != sK6 )
| ( X0 != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_1655]) ).
tcf(c_1796,plain,
( ~ m1_group_2(sK6,sK0)
| ~ m1_group_2(sK5,sK6) ),
inference(unflattening,[status(thm)],[c_1795]) ).
tcf(c_1797,plain,
~ m1_group_2(sK5,sK6),
inference(global_subsumption_just,[status(thm)],[c_1796,c_53,c_1796]) ).
tcf(c_1802,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| ( sK0 != sK0 )
| ( X0 != sK6 )
| ( sK10(sK0,X0) != sK5 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_1670]) ).
tcf(c_1803,plain,
( ~ m1_group_2(sK6,sK0)
| ( sK10(sK0,sK6) != sK5 ) ),
inference(unflattening,[status(thm)],[c_1802]) ).
tcf(c_1804,plain,
sK10(sK0,sK6) != sK5,
inference(global_subsumption_just,[status(thm)],[c_1803,c_53,c_1803]) ).
tcf(c_1811,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,X1)
| ~ m1_group_2(X1,sK1)
| ( sK1 != sK1 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_1569]) ).
tcf(c_1812,plain,
( m1_group_2(sK3,sK4)
| ~ m1_group_2(sK4,sK1) ),
inference(unflattening,[status(thm)],[c_1811]) ).
tcf(c_1813,plain,
m1_group_2(sK3,sK4),
inference(global_subsumption_just,[status(thm)],[c_1812,c_55,c_1812]) ).
tcf(c_1818,plain,
! [X0: $i,X1: $i] :
( m1_group_2(X0,sK0)
| ~ m1_group_2(X1,sK0)
| ( sK0 != sK1 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_1681]) ).
tcf(c_1819,plain,
( m1_group_2(sK3,sK0)
| ~ m1_group_2(sK4,sK0)
| ( sK0 != sK1 ) ),
inference(unflattening,[status(thm)],[c_1818]) ).
tcf(c_1831,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_1610,c_1599]) ).
tcf(c_1832,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(X0,sK1) ),
inference(unflattening,[status(thm)],[c_1831]) ).
tcf(c_1840,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_1569,c_1599]) ).
tcf(c_1841,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),X0)
| ~ m1_group_2(X0,sK1) ),
inference(unflattening,[status(thm)],[c_1840]) ).
tcf(c_1861,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,sK1)
| ~ m1_group_2(X2,sK1)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK1 )
| ( X0 != X2 )
| ( sK10(sK0,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1610,c_1670]) ).
tcf(c_1862,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK1 ) ),
inference(unflattening,[status(thm)],[c_1861]) ).
tcf(c_1891,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_group_2(X1,sK0)
| ~ m1_group_2(X2,sK0)
| ~ m1_group_2(X0,sK1)
| ( sK0 != sK1 )
| ( X0 != X2 )
| ( sK10(sK1,X0) != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_1599,c_1681]) ).
tcf(c_1892,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK1 ) ),
inference(unflattening,[status(thm)],[c_1891]) ).
tcf(c_1908,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_1681,c_1670]) ).
tcf(c_1909,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_1908]) ).
tcf(c_1917,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_1641,c_1670]) ).
tcf(c_1918,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),X0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_1917]) ).
tcf(c_2403,definition,
iPr_def_10 = sK10(sK0,sK6),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_2404,definition,
iPr_def_11 = sK10(sK1,sK6),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_2405,definition,
iPr_def_12 = u1_struct_0(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_2406,definition,
iPr_def_13 = u1_struct_0(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_2407,definition,
iPr_def_14 = u1_struct_0(sK4),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_2408,definition,
iPr_def_15 = k3_funct_2(iPr_def_13,iPr_def_12,sK2,iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_2409,definition,
iPr_def_16 = u1_struct_0(sK6),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_2410,definition,
iPr_def_17 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_2411,definition,
iPr_def_18 = k3_funct_2(iPr_def_13,iPr_def_12,sK2,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_2412,definition,
iPr_def_19 = u1_struct_0(sK5),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_2413,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),X0)
| ~ m1_group_2(X0,sK0) ),
inference(demodulation,[status(thm)],[c_1918]) ).
tcf(c_2414,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK0)
| ~ m1_group_2(X0,sK0) ),
inference(demodulation,[status(thm)],[c_1909]) ).
tcf(c_2415,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK1 ) ),
inference(demodulation,[status(thm)],[c_1892]) ).
tcf(c_2416,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0)
| ( sK0 != sK1 ) ),
inference(demodulation,[status(thm)],[c_1862]) ).
tcf(c_2417,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),X0)
| ~ m1_group_2(X0,sK1) ),
inference(demodulation,[status(thm)],[c_1841]) ).
tcf(c_2418,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(X0,sK1) ),
inference(demodulation,[status(thm)],[c_1832]) ).
tcf(c_2419,plain,
( m1_group_2(sK3,sK0)
| ~ m1_group_2(sK4,sK0)
| ( sK0 != sK1 ) ),
inference(demodulation,[status(thm)],[c_1819]) ).
tcf(c_2420,plain,
m1_group_2(sK3,sK4),
inference(demodulation,[status(thm)],[c_1813]) ).
tcf(c_2421,plain,
iPr_def_10 != sK5,
inference(demodulation,[status(thm)],[c_1804,c_2403]) ).
tcf(c_2422,plain,
~ m1_group_2(sK5,sK6),
inference(demodulation,[status(thm)],[c_1797]) ).
tcf(c_2423,plain,
( ~ m1_group_2(sK6,sK1)
| ( iPr_def_11 != sK5 )
| ( sK0 != sK1 ) ),
inference(demodulation,[status(thm)],[c_1785,c_2404]) ).
tcf(c_2424,plain,
( ( sK6 != sK4 )
| ( sK0 != sK1 )
| ( sK5 != sK3 ) ),
inference(demodulation,[status(thm)],[c_1763]) ).
tcf(c_2425,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_1751]) ).
tcf(c_2426,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_1738]) ).
tcf(c_2427,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_1694]) ).
tcf(c_2428,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_1624]) ).
tcf(c_2429,plain,
( v1_xboole_0(iPr_def_12)
| ~ v1_xboole_0(sK2) ),
inference(demodulation,[status(thm)],[c_1143,c_2405]) ).
tcf(c_2430,plain,
m1_relset_1(sK2,iPr_def_13,iPr_def_12),
inference(demodulation,[status(thm)],[c_1079,c_2406]) ).
tcf(c_2431,negated_conjecture,
l1_group_1(sK0),
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_2432,negated_conjecture,
v3_group_1(sK0),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_2433,negated_conjecture,
~ v3_struct_0(sK0),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_2434,negated_conjecture,
l1_group_1(sK1),
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_2435,negated_conjecture,
v3_group_1(sK1),
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_2436,negated_conjecture,
~ v3_struct_0(sK1),
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_2437,negated_conjecture,
v1_funct_1(sK2),
inference(demodulation,[status(thm)],[c_57]) ).
tcf(c_2438,negated_conjecture,
m1_group_2(sK3,sK1),
inference(demodulation,[status(thm)],[c_56]) ).
tcf(c_2439,negated_conjecture,
m1_group_2(sK4,sK1),
inference(demodulation,[status(thm)],[c_55]) ).
tcf(c_2440,negated_conjecture,
m1_group_2(sK5,sK0),
inference(demodulation,[status(thm)],[c_54]) ).
tcf(c_2441,negated_conjecture,
m1_group_2(sK6,sK0),
inference(demodulation,[status(thm)],[c_53]) ).
tcf(c_2442,negated_conjecture,
iPr_def_15 = iPr_def_16,
inference(demodulation,[status(thm)],[c_51,c_2409,c_2407,c_2408]) ).
tcf(c_2443,negated_conjecture,
iPr_def_18 = iPr_def_19,
inference(demodulation,[status(thm)],[c_50,c_2412,c_2410,c_2411]) ).
tcf(c_4018,plain,
! [X0: $i] :
( m1_group_2(X0,X0)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_120,c_2427]) ).
tcf(c_4029,plain,
! [X0: $i] :
( m1_group_2(X0,X0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_120,c_2428]) ).
tcf(c_4032,plain,
( m1_group_2(sK0,sK0)
| ~ m1_group_2(sK0,sK1) ),
inference(instantiation,[status(thm)],[c_4029]) ).
tcf(c_4037,plain,
m1_group_2(sK6,sK6),
inference(superposition,[status(thm)],[c_2441,c_4018]) ).
tcf(c_4038,plain,
m1_group_2(sK5,sK5),
inference(superposition,[status(thm)],[c_2440,c_4018]) ).
tcf(c_4039,plain,
! [X0: $i] :
( m1_group_2(sK1,X0)
| ~ m1_group_2(sK1,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_12,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2405,c_2428]) ).
tcf(c_4040,plain,
! [X0: $i] :
( m1_group_2(sK1,X0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_12,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2405,c_2427]) ).
tcf(c_4042,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_12) ),
inference(superposition,[status(thm)],[c_2405,c_2427]) ).
tcf(c_4057,plain,
! [X0: $i] :
( m1_group_2(sK0,X0)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_13,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2406,c_2428]) ).
tcf(c_4058,plain,
! [X0: $i] :
( m1_group_2(sK0,X0)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_13,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2406,c_2427]) ).
tcf(c_4059,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_13) ),
inference(superposition,[status(thm)],[c_2406,c_2428]) ).
tcf(c_4073,plain,
! [X0: $i] :
( m1_group_2(sK4,X0)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_14,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2407,c_2428]) ).
tcf(c_4074,plain,
! [X0: $i] :
( m1_group_2(sK4,X0)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_14,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2407,c_2427]) ).
tcf(c_4075,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_14) ),
inference(superposition,[status(thm)],[c_2407,c_2428]) ).
tcf(c_4076,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_14) ),
inference(superposition,[status(thm)],[c_2407,c_2427]) ).
tcf(c_4081,plain,
! [X0: $i] :
( m1_group_2(X0,sK4)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_14) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4075,c_2439]) ).
tcf(c_4089,plain,
! [X0: $i] :
( m1_group_2(sK4,X0)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_14,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4073,c_2439]) ).
tcf(c_4096,plain,
u1_struct_0(sK6) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_2409,c_2442]) ).
tcf(c_4097,plain,
! [X0: $i] :
( m1_group_2(sK6,X0)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_15,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4096,c_2428]) ).
tcf(c_4098,plain,
! [X0: $i] :
( m1_group_2(sK6,X0)
| ~ m1_group_2(sK6,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_15,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4096,c_2427]) ).
tcf(c_4099,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_15) ),
inference(superposition,[status(thm)],[c_4096,c_2428]) ).
tcf(c_4100,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_15) ),
inference(superposition,[status(thm)],[c_4096,c_2427]) ).
tcf(c_4101,plain,
! [X0: $i] :
( m1_group_2(X0,sK6)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4100,c_2441]) ).
tcf(c_4109,plain,
! [X0: $i] :
( m1_group_2(sK6,X0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_15,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4098,c_2441]) ).
tcf(c_4119,plain,
! [X0: $i] :
( m1_group_2(sK3,X0)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2410,c_2428]) ).
tcf(c_4120,plain,
! [X0: $i] :
( m1_group_2(sK3,X0)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_2410,c_2427]) ).
tcf(c_4121,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_17) ),
inference(superposition,[status(thm)],[c_2410,c_2428]) ).
tcf(c_4122,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_17) ),
inference(superposition,[status(thm)],[c_2410,c_2427]) ).
tcf(c_4127,plain,
! [X0: $i] :
( m1_group_2(X0,sK3)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4121,c_2438]) ).
tcf(c_4135,plain,
! [X0: $i] :
( m1_group_2(sK3,X0)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_17,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4119,c_2438]) ).
tcf(c_4142,plain,
u1_struct_0(sK5) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_2412,c_2443]) ).
tcf(c_4143,plain,
! [X0: $i] :
( m1_group_2(sK5,X0)
| ~ m1_group_2(sK5,sK1)
| ~ m1_group_2(X0,sK1)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4142,c_2428]) ).
tcf(c_4144,plain,
! [X0: $i] :
( m1_group_2(sK5,X0)
| ~ m1_group_2(sK5,sK0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0)) ),
inference(superposition,[status(thm)],[c_4142,c_2427]) ).
tcf(c_4145,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_18) ),
inference(superposition,[status(thm)],[c_4142,c_2428]) ).
tcf(c_4146,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_18) ),
inference(superposition,[status(thm)],[c_4142,c_2427]) ).
tcf(c_4147,plain,
! [X0: $i] :
( m1_group_2(X0,sK5)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(u1_struct_0(X0),iPr_def_18) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4146,c_2440]) ).
tcf(c_4155,plain,
! [X0: $i] :
( m1_group_2(sK5,X0)
| ~ m1_group_2(X0,sK0)
| ~ r1_tarski(iPr_def_18,u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4144,c_2440]) ).
tcf(c_4175,plain,
( m1_group_2(sK5,sK4)
| ~ r1_tarski(iPr_def_18,iPr_def_14)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_4142,c_4081]) ).
tcf(c_4176,plain,
( m1_group_2(sK0,sK4)
| ~ r1_tarski(iPr_def_13,iPr_def_14)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4081]) ).
tcf(c_4177,plain,
( m1_group_2(sK1,sK4)
| ~ r1_tarski(iPr_def_12,iPr_def_14)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2405,c_4081]) ).
tcf(c_4179,plain,
( m1_group_2(sK6,sK4)
| ~ r1_tarski(iPr_def_15,iPr_def_14)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_4096,c_4081]) ).
tcf(c_4180,plain,
( m1_group_2(sK4,sK4)
| ~ r1_tarski(iPr_def_14,iPr_def_14)
| ~ m1_group_2(sK4,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4081]) ).
tcf(c_4181,plain,
m1_group_2(sK4,sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_4180,c_120,c_2439]) ).
tcf(c_4200,plain,
( m1_group_2(sK4,sK5)
| ~ r1_tarski(iPr_def_14,iPr_def_18)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_4142,c_4089]) ).
tcf(c_4201,plain,
( m1_group_2(sK4,sK0)
| ~ r1_tarski(iPr_def_14,iPr_def_13)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4089]) ).
tcf(c_4203,plain,
( m1_group_2(sK4,sK3)
| ~ r1_tarski(iPr_def_14,iPr_def_17)
| ~ m1_group_2(sK3,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4089]) ).
tcf(c_4204,plain,
( m1_group_2(sK4,sK6)
| ~ r1_tarski(iPr_def_14,iPr_def_15)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_4096,c_4089]) ).
tcf(c_4209,plain,
( m1_group_2(sK4,sK3)
| ~ r1_tarski(iPr_def_14,iPr_def_17) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4203,c_2438]) ).
tcf(c_4228,plain,
( m1_group_2(sK5,sK6)
| ~ r1_tarski(iPr_def_18,iPr_def_15)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_4142,c_4101]) ).
tcf(c_4229,plain,
( m1_group_2(sK0,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_15)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2406,c_4101]) ).
tcf(c_4230,plain,
( m1_group_2(sK1,sK6)
| ~ r1_tarski(iPr_def_12,iPr_def_15)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2405,c_4101]) ).
tcf(c_4231,plain,
( m1_group_2(sK3,sK6)
| ~ r1_tarski(iPr_def_17,iPr_def_15)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_2410,c_4101]) ).
tcf(c_4233,plain,
( m1_group_2(sK4,sK6)
| ~ r1_tarski(iPr_def_14,iPr_def_15)
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_2407,c_4101]) ).
tcf(c_4246,plain,
~ r1_tarski(iPr_def_18,iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_4228,c_2422,c_2440]) ).
tcf(c_4253,plain,
( m1_group_2(sK6,sK5)
| ~ r1_tarski(iPr_def_15,iPr_def_18)
| ~ m1_group_2(sK5,sK0) ),
inference(superposition,[status(thm)],[c_4142,c_4109]) ).
tcf(c_4255,plain,
( m1_group_2(sK6,sK1)
| ~ r1_tarski(iPr_def_15,iPr_def_12)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2405,c_4109]) ).
tcf(c_4256,plain,
( m1_group_2(sK6,sK3)
| ~ r1_tarski(iPr_def_15,iPr_def_17)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_2410,c_4109]) ).
tcf(c_4258,plain,
( m1_group_2(sK6,sK4)
| ~ r1_tarski(iPr_def_15,iPr_def_14)
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_2407,c_4109]) ).
tcf(c_4268,plain,
( m1_group_2(sK6,sK5)
| ~ r1_tarski(iPr_def_15,iPr_def_18) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4253,c_2440]) ).
tcf(c_4293,plain,
( m1_group_2(sK5,sK3)
| ~ r1_tarski(iPr_def_18,iPr_def_17)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_4142,c_4127]) ).
tcf(c_4294,plain,
( m1_group_2(sK0,sK3)
| ~ r1_tarski(iPr_def_13,iPr_def_17)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4127]) ).
tcf(c_4295,plain,
( m1_group_2(sK1,sK3)
| ~ r1_tarski(iPr_def_12,iPr_def_17)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2405,c_4127]) ).
tcf(c_4296,plain,
( m1_group_2(sK3,sK3)
| ~ r1_tarski(iPr_def_17,iPr_def_17)
| ~ m1_group_2(sK3,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4127]) ).
tcf(c_4297,plain,
( m1_group_2(sK6,sK3)
| ~ r1_tarski(iPr_def_15,iPr_def_17)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_4096,c_4127]) ).
tcf(c_4302,plain,
m1_group_2(sK3,sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4296,c_120,c_2438]) ).
tcf(c_4318,plain,
( m1_group_2(sK3,sK5)
| ~ r1_tarski(iPr_def_17,iPr_def_18)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_4142,c_4135]) ).
tcf(c_4319,plain,
( m1_group_2(sK3,sK0)
| ~ r1_tarski(iPr_def_17,iPr_def_13)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4135]) ).
tcf(c_4322,plain,
( m1_group_2(sK3,sK6)
| ~ r1_tarski(iPr_def_17,iPr_def_15)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_4096,c_4135]) ).
tcf(c_4340,plain,
( m1_group_2(sK0,sK5)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2406,c_4147]) ).
tcf(c_4341,plain,
( m1_group_2(sK1,sK5)
| ~ r1_tarski(iPr_def_12,iPr_def_18)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2405,c_4147]) ).
tcf(c_4342,plain,
( m1_group_2(sK3,sK5)
| ~ r1_tarski(iPr_def_17,iPr_def_18)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_2410,c_4147]) ).
tcf(c_4344,plain,
( m1_group_2(sK4,sK5)
| ~ r1_tarski(iPr_def_14,iPr_def_18)
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_2407,c_4147]) ).
tcf(c_4365,plain,
( m1_group_2(sK5,sK1)
| ~ r1_tarski(iPr_def_18,iPr_def_12)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2405,c_4155]) ).
tcf(c_4366,plain,
( m1_group_2(sK5,sK3)
| ~ r1_tarski(iPr_def_18,iPr_def_17)
| ~ m1_group_2(sK3,sK0) ),
inference(superposition,[status(thm)],[c_2410,c_4155]) ).
tcf(c_4368,plain,
( m1_group_2(sK5,sK4)
| ~ r1_tarski(iPr_def_18,iPr_def_14)
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_2407,c_4155]) ).
tcf(c_4409,plain,
k1_xboole_0 = sK16,
inference(superposition,[status(thm)],[c_104,c_129]) ).
tcf(c_4410,plain,
! [X0: $i] : sK18(X0) = k1_xboole_0,
inference(superposition,[status(thm)],[c_109,c_129]) ).
tcf(c_4412,plain,
! [X0: $i] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(demodulation,[status(thm)],[c_108,c_4410]) ).
tcf(c_4478,plain,
( m1_group_2(iPr_def_10,sK6)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2403,c_2413]) ).
tcf(c_4479,plain,
( m1_group_2(sK10(sK0,sK1),sK10(sK0,sK1))
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2413,c_4029]) ).
tcf(c_4480,plain,
( m1_group_2(sK10(sK0,sK0),sK10(sK0,sK0))
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2413,c_4018]) ).
tcf(c_4481,plain,
m1_group_2(iPr_def_10,sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4478,c_2441]) ).
tcf(c_4498,plain,
! [X0: $i] : r1_tarski(sK12(k1_zfmisc_1(X0)),X0),
inference(superposition,[status(thm)],[c_92,c_125]) ).
tcf(c_4499,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r1_tarski(sK15(X0),X0) ),
inference(superposition,[status(thm)],[c_102,c_125]) ).
tcf(c_4501,plain,
r1_tarski(sK21(sK20),u1_struct_0(sK20)),
inference(superposition,[status(thm)],[c_1358,c_125]) ).
tcf(c_4502,plain,
! [X0: $i] : r1_tarski(k1_xboole_0,X0),
inference(superposition,[status(thm)],[c_4412,c_125]) ).
tcf(c_4511,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_4512,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_4513,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_4514,plain,
v1_relat_1(k1_xboole_0),
inference(superposition,[status(thm)],[c_4412,c_70]) ).
tcf(c_4573,plain,
( m1_group_2(iPr_def_10,sK0)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2403,c_2414]) ).
tcf(c_4574,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK10(sK0,X0))
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2414,c_4018]) ).
tcf(c_4575,plain,
m1_group_2(iPr_def_10,sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_4573,c_2441]) ).
tcf(c_4590,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r2_hidden(sK12(X0),X0) ),
inference(superposition,[status(thm)],[c_92,c_123]) ).
tcf(c_4591,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_4592,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_4593,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_1358,c_123]) ).
tcf(c_4594,plain,
! [X0: $i] :
( v1_xboole_0(k1_zfmisc_1(X0))
| r2_hidden(k1_xboole_0,k1_zfmisc_1(X0)) ),
inference(superposition,[status(thm)],[c_4412,c_123]) ).
tcf(c_4597,plain,
! [X0: $i] : r2_hidden(k1_xboole_0,k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_4594,c_95]) ).
tcf(c_4598,plain,
r2_hidden(sK21(sK20),k1_zfmisc_1(u1_struct_0(sK20))),
inference(forward_subsumption_resolution,[status(thm)],[c_4593,c_95]) ).
tcf(c_4599,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r2_hidden(sK15(X0),k1_zfmisc_1(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4591,c_95]) ).
tcf(c_4602,plain,
! [X0: $i,X1: $i] :
( r2_hidden(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4592,c_95]) ).
tcf(c_4617,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_200,c_70]) ).
tcf(c_4618,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| r2_hidden(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_200,c_123]) ).
tcf(c_4619,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1_tarski(X0,k2_zfmisc_1(X1,X2))
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_200,c_125]) ).
tcf(c_4624,plain,
! [X0: $i,X1: $i,X2: $i] :
( r2_hidden(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
| ~ m1_relset_1(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4618,c_95]) ).
tcf(c_4629,plain,
m1_group_2(iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_4575,c_4018]) ).
tcf(c_4630,plain,
! [X0: $i] : ~ r2_hidden(k1_zfmisc_1(X0),k1_xboole_0),
inference(superposition,[status(thm)],[c_4597,c_68]) ).
tcf(c_4698,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_4029]) ).
tcf(c_4699,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_4018]) ).
tcf(c_4700,plain,
m1_group_2(sK9(sK0),sK9(sK0)),
inference(forward_subsumption_resolution,[status(thm)],[c_4699,c_2433,c_2431,c_2432]) ).
tcf(c_4701,plain,
m1_group_2(sK9(sK1),sK9(sK1)),
inference(forward_subsumption_resolution,[status(thm)],[c_4698,c_2436,c_2434,c_2435]) ).
tcf(c_4712,plain,
( v3_group_1(sK6)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2441,c_80]) ).
tcf(c_4713,plain,
( v3_group_1(sK5)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2440,c_80]) ).
tcf(c_4714,plain,
( v3_group_1(sK4)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2439,c_80]) ).
tcf(c_4715,plain,
( v3_group_1(sK3)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2438,c_80]) ).
tcf(c_4716,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_4718,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_2413,c_80]) ).
tcf(c_4719,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_2414,c_80]) ).
tcf(c_4725,plain,
( v3_group_1(iPr_def_10)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_4575,c_80]) ).
tcf(c_4727,plain,
v3_group_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_4725,c_2433,c_2431,c_2432]) ).
tcf(c_4732,plain,
v3_group_1(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4715,c_2436,c_2434,c_2435]) ).
tcf(c_4733,plain,
v3_group_1(sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_4714,c_2436,c_2434,c_2435]) ).
tcf(c_4734,plain,
v3_group_1(sK5),
inference(forward_subsumption_resolution,[status(thm)],[c_4713,c_2433,c_2431,c_2432]) ).
tcf(c_4735,plain,
v3_group_1(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4712,c_2433,c_2431,c_2432]) ).
tcf(c_4740,plain,
! [X0: $i] :
( v3_group_1(sK10(sK0,X0))
| ~ m1_group_2(X0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4719,c_2433,c_2431,c_2432]) ).
tcf(c_4760,plain,
( l1_group_1(sK6)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2441,c_81]) ).
tcf(c_4761,plain,
( l1_group_1(sK5)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2440,c_81]) ).
tcf(c_4762,plain,
( l1_group_1(sK4)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2439,c_81]) ).
tcf(c_4763,plain,
( l1_group_1(sK3)
| v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2438,c_81]) ).
tcf(c_4764,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_4766,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_2413,c_81]) ).
tcf(c_4767,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_2414,c_81]) ).
tcf(c_4773,plain,
( l1_group_1(iPr_def_10)
| v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_4575,c_81]) ).
tcf(c_4775,plain,
l1_group_1(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_4773,c_2433,c_2431,c_2432]) ).
tcf(c_4780,plain,
l1_group_1(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4763,c_2436,c_2434,c_2435]) ).
tcf(c_4781,plain,
l1_group_1(sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_4762,c_2436,c_2434,c_2435]) ).
tcf(c_4782,plain,
l1_group_1(sK5),
inference(forward_subsumption_resolution,[status(thm)],[c_4761,c_2433,c_2431,c_2432]) ).
tcf(c_4783,plain,
l1_group_1(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4760,c_2433,c_2431,c_2432]) ).
tcf(c_4788,plain,
! [X0: $i] :
( l1_group_1(sK10(sK0,X0))
| ~ m1_group_2(X0,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4767,c_2433,c_2431,c_2432]) ).
tcf(c_4826,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(sK6) ),
inference(superposition,[status(thm)],[c_2441,c_79]) ).
tcf(c_4827,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(sK5) ),
inference(superposition,[status(thm)],[c_2440,c_79]) ).
tcf(c_4828,plain,
( v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v3_struct_0(sK4) ),
inference(superposition,[status(thm)],[c_2439,c_79]) ).
tcf(c_4829,plain,
( v3_struct_0(sK1)
| ~ l1_group_1(sK1)
| ~ v3_group_1(sK1)
| ~ v3_struct_0(sK3) ),
inference(superposition,[status(thm)],[c_2438,c_79]) ).
tcf(c_4830,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_4831,plain,
( v3_struct_0(sK4)
| ~ l1_group_1(sK4)
| ~ v3_group_1(sK4)
| ~ v3_struct_0(sK3) ),
inference(superposition,[status(thm)],[c_2420,c_79]) ).
tcf(c_4833,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_2414,c_79]) ).
tcf(c_4839,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(iPr_def_10) ),
inference(superposition,[status(thm)],[c_4575,c_79]) ).
tcf(c_4843,plain,
~ v3_struct_0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_4839,c_2433,c_2431,c_2432]) ).
tcf(c_4847,plain,
~ v3_struct_0(sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_4829,c_2436,c_2434,c_2435]) ).
tcf(c_4848,plain,
~ v3_struct_0(sK4),
inference(forward_subsumption_resolution,[status(thm)],[c_4828,c_2436,c_2434,c_2435]) ).
tcf(c_4849,plain,
~ v3_struct_0(sK5),
inference(forward_subsumption_resolution,[status(thm)],[c_4827,c_2433,c_2431,c_2432]) ).
tcf(c_4850,plain,
~ v3_struct_0(sK6),
inference(forward_subsumption_resolution,[status(thm)],[c_4826,c_2433,c_2431,c_2432]) ).
tcf(c_4855,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| ~ v3_struct_0(sK10(sK0,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4833,c_2433,c_2431,c_2432]) ).
tcf(c_4872,plain,
( m1_subset_1(iPr_def_15,k1_zfmisc_1(iPr_def_13))
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,iPr_def_13,iPr_def_12) ),
inference(superposition,[status(thm)],[c_2408,c_77]) ).
tcf(c_4873,plain,
( m1_subset_1(iPr_def_18,k1_zfmisc_1(iPr_def_13))
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,iPr_def_13,iPr_def_12) ),
inference(superposition,[status(thm)],[c_2411,c_77]) ).
tcf(c_4874,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_relat_1(k3_funct_2(k2_zfmisc_1(X1,X2),X3,X0,X4))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X2),X3) ),
inference(superposition,[status(thm)],[c_77,c_70]) ).
tcf(c_4875,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v1_xboole_0(k1_zfmisc_1(X1))
| r2_hidden(k3_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_77,c_123]) ).
tcf(c_4876,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1_tarski(k3_funct_2(X1,X2,X0,X3),X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_77,c_125]) ).
tcf(c_4877,plain,
m1_subset_1(iPr_def_18,k1_zfmisc_1(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_4873,c_2437,c_2430]) ).
tcf(c_4878,plain,
m1_subset_1(iPr_def_15,k1_zfmisc_1(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_4872,c_2437,c_2430]) ).
tcf(c_4885,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r2_hidden(k3_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X1))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4875,c_95]) ).
tcf(c_4901,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k3_funct_2(X0,X1,sK11(X0,X1),X2) = k10_relat_1(sK11(X0,X1),X2) )
| ~ v1_funct_1(sK11(X0,X1)) ),
inference(superposition,[status(thm)],[c_91,c_115]) ).
tcf(c_4902,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k3_funct_2(X0,X1,sK14(X0,X1),X2) = k10_relat_1(sK14(X0,X1),X2) )
| ~ v1_funct_1(sK14(X0,X1)) ),
inference(superposition,[status(thm)],[c_98,c_115]) ).
tcf(c_4903,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k3_funct_2(X0,X1,sK17(X0,X1),X2) = k10_relat_1(sK17(X0,X1),X2) )
| ~ v1_funct_1(sK17(X0,X1)) ),
inference(superposition,[status(thm)],[c_105,c_115]) ).
tcf(c_4904,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( k3_funct_2(X0,X1,sK13(X0,X1),X2) = k10_relat_1(sK13(X0,X1),X2) )
| ~ v1_funct_1(sK13(X0,X1)) ),
inference(superposition,[status(thm)],[c_1093,c_115]) ).
tcf(c_4905,plain,
! [X0: $i] :
( ( k3_funct_2(iPr_def_13,iPr_def_12,sK2,X0) = k10_relat_1(sK2,X0) )
| ~ v1_funct_1(sK2) ),
inference(superposition,[status(thm)],[c_2430,c_115]) ).
tcf(c_4906,plain,
! [X0: $i] : k3_funct_2(iPr_def_13,iPr_def_12,sK2,X0) = k10_relat_1(sK2,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_4905,c_2437]) ).
tcf(c_4909,plain,
! [X0: $i,X1: $i,X2: $i] : k3_funct_2(X0,X1,sK17(X0,X1),X2) = k10_relat_1(sK17(X0,X1),X2),
inference(forward_subsumption_resolution,[status(thm)],[c_4903,c_107]) ).
tcf(c_4910,plain,
! [X0: $i,X1: $i,X2: $i] : k3_funct_2(X0,X1,sK14(X0,X1),X2) = k10_relat_1(sK14(X0,X1),X2),
inference(forward_subsumption_resolution,[status(thm)],[c_4902,c_100]) ).
tcf(c_4913,plain,
k10_relat_1(sK2,iPr_def_14) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2408,c_4906]) ).
tcf(c_4914,plain,
k10_relat_1(sK2,iPr_def_17) = iPr_def_18,
inference(demodulation,[status(thm)],[c_2411,c_4906]) ).
tcf(c_4936,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_18) != u1_group_1(sK5) ) ),
inference(superposition,[status(thm)],[c_4142,c_74]) ).
tcf(c_4937,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_13) != u1_group_1(sK0) ) ),
inference(superposition,[status(thm)],[c_2406,c_74]) ).
tcf(c_4938,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_12) != u1_group_1(sK1) ) ),
inference(superposition,[status(thm)],[c_2405,c_74]) ).
tcf(c_4939,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_17) != u1_group_1(sK3) ) ),
inference(superposition,[status(thm)],[c_2410,c_74]) ).
tcf(c_4940,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_15) != u1_group_1(sK6) ) ),
inference(superposition,[status(thm)],[c_4096,c_74]) ).
tcf(c_4941,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_14) != u1_group_1(sK4) ) ),
inference(superposition,[status(thm)],[c_2407,c_74]) ).
tcf(c_4942,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_14,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_14) != u1_group_1(sK4) ) ),
inference(light_normalisation,[status(thm)],[c_4941,c_2407]) ).
tcf(c_4943,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_14,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_14) != u1_group_1(sK4) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4942,c_4781,c_4733]) ).
tcf(c_4951,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_15,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_15) != u1_group_1(sK6) ) ),
inference(light_normalisation,[status(thm)],[c_4940,c_4096]) ).
tcf(c_4952,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_15,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_15) != u1_group_1(sK6) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4951,c_4783,c_4735]) ).
tcf(c_4960,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_17,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK3) ) ),
inference(light_normalisation,[status(thm)],[c_4939,c_2410]) ).
tcf(c_4961,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_17,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK3) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4960,c_4780,c_4732]) ).
tcf(c_4969,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_12,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_12) != u1_group_1(sK1) ) ),
inference(light_normalisation,[status(thm)],[c_4938,c_2405]) ).
tcf(c_4970,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK1,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(sK1) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4969,c_2436,c_2434,c_2435]) ).
tcf(c_4977,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_13,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_13) != u1_group_1(sK0) ) ),
inference(light_normalisation,[status(thm)],[c_4937,c_2406]) ).
tcf(c_4978,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK0,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(sK0) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4977,c_2433,c_2431,c_2432]) ).
tcf(c_4985,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_18,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK5) ) ),
inference(light_normalisation,[status(thm)],[c_4936,c_4142]) ).
tcf(c_4986,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_18,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK5) ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4985,c_4782,c_4734]) ).
tcf(c_5008,plain,
( v1_xboole_0(k1_zfmisc_1(iPr_def_13))
| r2_hidden(iPr_def_18,k1_zfmisc_1(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_4877,c_123]) ).
tcf(c_5009,plain,
r1_tarski(iPr_def_18,iPr_def_13),
inference(superposition,[status(thm)],[c_4877,c_125]) ).
tcf(c_5010,plain,
r2_hidden(iPr_def_18,k1_zfmisc_1(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_5008,c_95]) ).
tcf(c_5011,plain,
( v1_xboole_0(k1_zfmisc_1(iPr_def_13))
| r2_hidden(iPr_def_15,k1_zfmisc_1(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_4878,c_123]) ).
tcf(c_5012,plain,
r1_tarski(iPr_def_15,iPr_def_13),
inference(superposition,[status(thm)],[c_4878,c_125]) ).
tcf(c_5013,plain,
r2_hidden(iPr_def_15,k1_zfmisc_1(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_5011,c_95]) ).
tcf(c_5032,plain,
! [X0: $i] :
( m1_subset_1(k10_relat_1(sK2,X0),k1_zfmisc_1(iPr_def_13))
| ~ v1_funct_1(sK2)
| ~ m1_relset_1(sK2,iPr_def_13,iPr_def_12) ),
inference(superposition,[status(thm)],[c_4906,c_77]) ).
tcf(c_5033,plain,
! [X0: $i] : m1_subset_1(k10_relat_1(sK2,X0),k1_zfmisc_1(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_5032,c_2437,c_2430]) ).
tcf(c_5035,plain,
! [X0: $i] :
( v1_xboole_0(k1_zfmisc_1(iPr_def_13))
| r2_hidden(k10_relat_1(sK2,X0),k1_zfmisc_1(iPr_def_13)) ),
inference(superposition,[status(thm)],[c_5033,c_123]) ).
tcf(c_5036,plain,
! [X0: $i] : r1_tarski(k10_relat_1(sK2,X0),iPr_def_13),
inference(superposition,[status(thm)],[c_5033,c_125]) ).
tcf(c_5037,plain,
! [X0: $i] : r2_hidden(k10_relat_1(sK2,X0),k1_zfmisc_1(iPr_def_13)),
inference(forward_subsumption_resolution,[status(thm)],[c_5035,c_95]) ).
tcf(c_5048,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k10_relat_1(sK17(X0,X1),X2),k1_zfmisc_1(X0))
| ~ v1_funct_1(sK17(X0,X1))
| ~ m1_relset_1(sK17(X0,X1),X0,X1) ),
inference(superposition,[status(thm)],[c_4909,c_77]) ).
tcf(c_5049,plain,
! [X0: $i,X1: $i,X2: $i] : m1_subset_1(k10_relat_1(sK17(X0,X1),X2),k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_5048,c_107,c_105]) ).
tcf(c_5051,plain,
~ r2_hidden(k1_zfmisc_1(iPr_def_13),iPr_def_18),
inference(superposition,[status(thm)],[c_5010,c_68]) ).
tcf(c_5052,plain,
~ v1_xboole_0(k1_zfmisc_1(iPr_def_13)),
inference(superposition,[status(thm)],[c_5010,c_130]) ).
tcf(c_5054,plain,
~ r2_hidden(k1_zfmisc_1(iPr_def_13),iPr_def_15),
inference(superposition,[status(thm)],[c_5013,c_68]) ).
tcf(c_5081,plain,
! [X0: $i] :
( r1_tarski(k10_relat_1(sK2,X0),iPr_def_15)
| ~ v1_relat_1(sK2)
| ~ r1_tarski(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_4913,c_121]) ).
tcf(c_5082,plain,
! [X0: $i] :
( r1_tarski(iPr_def_15,k10_relat_1(sK2,X0))
| ~ v1_relat_1(sK2)
| ~ r1_tarski(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_4913,c_121]) ).
tcf(c_5093,plain,
! [X0: $i] :
( r1_tarski(k10_relat_1(sK2,X0),iPr_def_18)
| ~ v1_relat_1(sK2)
| ~ r1_tarski(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_4914,c_121]) ).
tcf(c_5094,plain,
! [X0: $i] :
( r1_tarski(iPr_def_18,k10_relat_1(sK2,X0))
| ~ v1_relat_1(sK2)
| ~ r1_tarski(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_4914,c_121]) ).
tcf(c_5124,plain,
( m1_group_2(sK6,sK3)
| ~ r1_tarski(iPr_def_15,iPr_def_17)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4097]) ).
tcf(c_5126,plain,
( m1_group_2(sK6,sK4)
| ~ r1_tarski(iPr_def_15,iPr_def_14)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4097]) ).
tcf(c_5138,plain,
( m1_group_2(sK0,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_15)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4099]) ).
tcf(c_5139,plain,
( m1_group_2(sK1,sK6)
| ~ r1_tarski(iPr_def_12,iPr_def_15)
| ~ m1_group_2(sK1,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2405,c_4099]) ).
tcf(c_5140,plain,
( m1_group_2(sK3,sK6)
| ~ r1_tarski(iPr_def_17,iPr_def_15)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4099]) ).
tcf(c_5142,plain,
( m1_group_2(sK4,sK6)
| ~ r1_tarski(iPr_def_14,iPr_def_15)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4099]) ).
tcf(c_5171,plain,
( m1_group_2(sK5,sK3)
| ~ r1_tarski(iPr_def_18,iPr_def_17)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4143]) ).
tcf(c_5173,plain,
( m1_group_2(sK5,sK4)
| ~ r1_tarski(iPr_def_18,iPr_def_14)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4143]) ).
tcf(c_5176,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_subset_1(k10_relat_1(sK14(X0,X1),X2),k1_zfmisc_1(X0))
| ~ v1_funct_1(sK14(X0,X1))
| ~ m1_relset_1(sK14(X0,X1),X0,X1) ),
inference(superposition,[status(thm)],[c_4910,c_77]) ).
tcf(c_5177,plain,
! [X0: $i,X1: $i,X2: $i] : m1_subset_1(k10_relat_1(sK14(X0,X1),X2),k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_5176,c_100,c_98]) ).
tcf(c_5187,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ r2_hidden(X0,sK12(X0)) ),
inference(superposition,[status(thm)],[c_4590,c_68]) ).
tcf(c_5193,plain,
~ r2_hidden(k1_zfmisc_1(u1_struct_0(sK20)),sK21(sK20)),
inference(superposition,[status(thm)],[c_4598,c_68]) ).
tcf(c_5194,plain,
~ v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK20))),
inference(superposition,[status(thm)],[c_4598,c_130]) ).
tcf(c_5198,plain,
! [X0: $i] : ~ r2_hidden(k1_zfmisc_1(iPr_def_13),k10_relat_1(sK2,X0)),
inference(superposition,[status(thm)],[c_5037,c_68]) ).
tcf(c_5214,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ~ r2_hidden(k1_zfmisc_1(X0),sK15(X0)) ),
inference(superposition,[status(thm)],[c_4599,c_68]) ).
tcf(c_5224,plain,
! [X0: $i,X1: $i] : v1_relat_1(sK11(X0,X1)),
inference(superposition,[status(thm)],[c_91,c_4617]) ).
tcf(c_5227,plain,
! [X0: $i,X1: $i] : v1_relat_1(sK13(X0,X1)),
inference(superposition,[status(thm)],[c_1093,c_4617]) ).
tcf(c_5228,plain,
v1_relat_1(sK2),
inference(superposition,[status(thm)],[c_2430,c_4617]) ).
tcf(c_5240,plain,
( m1_group_2(sK0,sK5)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4145]) ).
tcf(c_5241,plain,
( m1_group_2(sK1,sK5)
| ~ r1_tarski(iPr_def_12,iPr_def_18)
| ~ m1_group_2(sK1,sK1)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_2405,c_4145]) ).
tcf(c_5242,plain,
( m1_group_2(sK3,sK5)
| ~ r1_tarski(iPr_def_17,iPr_def_18)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4145]) ).
tcf(c_5244,plain,
( m1_group_2(sK4,sK5)
| ~ r1_tarski(iPr_def_14,iPr_def_18)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK5,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4145]) ).
tcf(c_5257,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_14) != u1_group_1(sK4) )
| ~ r1_tarski(iPr_def_14,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_4943,c_4848,c_4943]) ).
tcf(c_5258,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK4,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_14,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_14) != u1_group_1(sK4) ) ),
inference(renaming,[status(thm)],[c_5257]) ).
tcf(c_5274,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_15) != u1_group_1(sK6) )
| ~ r1_tarski(iPr_def_15,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_4952,c_4850,c_4952]) ).
tcf(c_5275,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK6,X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ r1_tarski(iPr_def_15,u1_struct_0(X0))
| ( k1_realset1(u1_group_1(X0),iPr_def_15) != u1_group_1(sK6) ) ),
inference(renaming,[status(thm)],[c_5274]) ).
tcf(c_5288,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_17) != u1_group_1(sK3) )
| ~ r1_tarski(iPr_def_17,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_4961,c_4847,c_4961]) ).
tcf(c_5289,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK3,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(sK3) ) ),
inference(renaming,[status(thm)],[c_5288]) ).
tcf(c_5303,plain,
! [X0: $i] :
( ( k1_realset1(u1_group_1(X0),iPr_def_18) != u1_group_1(sK5) )
| ~ r1_tarski(iPr_def_18,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_4986,c_4849,c_4986]) ).
tcf(c_5304,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(sK5,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(sK5) ) ),
inference(renaming,[status(thm)],[c_5303]) ).
tcf(c_5321,plain,
( m1_group_2(iPr_def_11,sK6)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_2417]) ).
tcf(c_5322,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK1)
| ~ v3_struct_0(sK10(sK1,X0)) ),
inference(superposition,[status(thm)],[c_2417,c_79]) ).
tcf(c_5323,plain,
! [X0: $i] :
( v3_struct_0(X0)
| l1_group_1(sK10(sK1,X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2417,c_81]) ).
tcf(c_5324,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_group_1(sK10(sK1,X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2417,c_80]) ).
tcf(c_5325,plain,
( m1_group_2(sK10(sK1,sK1),sK10(sK1,sK1))
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2417,c_4029]) ).
tcf(c_5326,plain,
( m1_group_2(sK10(sK1,sK0),sK10(sK1,sK0))
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2417,c_4018]) ).
tcf(c_5361,plain,
( m1_group_2(iPr_def_11,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_2418]) ).
tcf(c_5362,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_2418,c_79]) ).
tcf(c_5363,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_2418,c_81]) ).
tcf(c_5364,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_2418,c_80]) ).
tcf(c_5365,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK10(sK1,X0))
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_2418,c_4029]) ).
tcf(c_5370,plain,
! [X0: $i] :
( v3_group_1(sK10(sK1,X0))
| ~ m1_group_2(X0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5364,c_2436,c_2434,c_2435]) ).
tcf(c_5373,plain,
! [X0: $i] :
( l1_group_1(sK10(sK1,X0))
| ~ m1_group_2(X0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5363,c_2436,c_2434,c_2435]) ).
tcf(c_5376,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| ~ v3_struct_0(sK10(sK1,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5362,c_2436,c_2434,c_2435]) ).
tcf(c_5393,plain,
( v3_group_1(iPr_def_11)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_5370]) ).
tcf(c_5404,plain,
( m1_group_2(sK4,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2439,c_2425]) ).
tcf(c_5405,plain,
( m1_group_2(sK3,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2438,c_2425]) ).
tcf(c_5406,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_2425]) ).
tcf(c_5407,plain,
( m1_group_2(sK3,sK0)
| ~ m1_group_2(sK4,sK0) ),
inference(superposition,[status(thm)],[c_2420,c_2425]) ).
tcf(c_5408,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_2418,c_2425]) ).
tcf(c_5409,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2417,c_2425]) ).
tcf(c_5411,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_2414,c_2425]) ).
tcf(c_5478,plain,
( l1_group_1(iPr_def_11)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_5373]) ).
tcf(c_5485,plain,
( ~ v3_struct_0(iPr_def_11)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_5376]) ).
tcf(c_5506,plain,
( m1_group_2(sK6,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2441,c_2426]) ).
tcf(c_5507,plain,
( m1_group_2(sK5,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2440,c_2426]) ).
tcf(c_5510,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_2426]) ).
tcf(c_5512,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_2418,c_2426]) ).
tcf(c_5514,plain,
! [X0: $i] :
( m1_group_2(sK10(sK0,X0),sK1)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_2413,c_2426]) ).
tcf(c_5515,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_2414,c_2426]) ).
tcf(c_5520,plain,
( m1_group_2(iPr_def_10,sK1)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_4481,c_2426]) ).
tcf(c_5521,plain,
( m1_group_2(iPr_def_10,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_4575,c_2426]) ).
tcf(c_5582,plain,
( v3_struct_0(sK8)
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK8)))
| r2_hidden(sK21(sK8),k1_zfmisc_1(u1_struct_0(sK8))) ),
inference(superposition,[status(thm)],[c_1334,c_123]) ).
tcf(c_5583,plain,
( v3_struct_0(sK8)
| r1_tarski(sK21(sK8),u1_struct_0(sK8)) ),
inference(superposition,[status(thm)],[c_1334,c_125]) ).
tcf(c_5586,plain,
( v3_struct_0(sK8)
| r2_hidden(sK21(sK8),k1_zfmisc_1(u1_struct_0(sK8))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5582,c_95]) ).
tcf(c_5605,plain,
! [X0: $i,X1: $i] : v1_relat_1(k2_zfmisc_1(X0,X1)),
inference(superposition,[status(thm)],[c_120,c_4513]) ).
tcf(c_5610,plain,
! [X0: $i] :
( r1_tarski(k10_relat_1(sK2,X0),iPr_def_15)
| ~ r1_tarski(X0,iPr_def_14) ),
inference(global_subsumption_just,[status(thm)],[c_5081,c_5081,c_5228]) ).
tcf(c_5617,plain,
( r1_tarski(iPr_def_15,iPr_def_15)
| ~ r1_tarski(iPr_def_14,iPr_def_14) ),
inference(superposition,[status(thm)],[c_4913,c_5610]) ).
tcf(c_5618,plain,
( r1_tarski(iPr_def_18,iPr_def_15)
| ~ r1_tarski(iPr_def_17,iPr_def_14) ),
inference(superposition,[status(thm)],[c_4914,c_5610]) ).
tcf(c_5619,plain,
~ r1_tarski(iPr_def_17,iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_5618,c_4246]) ).
tcf(c_5620,plain,
! [X0: $i] :
( r1_tarski(iPr_def_15,k10_relat_1(sK2,X0))
| ~ r1_tarski(iPr_def_14,X0) ),
inference(global_subsumption_just,[status(thm)],[c_5082,c_5082,c_5228]) ).
tcf(c_5628,plain,
( r1_tarski(iPr_def_15,iPr_def_18)
| ~ r1_tarski(iPr_def_14,iPr_def_17) ),
inference(superposition,[status(thm)],[c_4914,c_5620]) ).
tcf(c_5637,plain,
! [X0: $i] :
( r1_tarski(k10_relat_1(sK2,X0),iPr_def_18)
| ~ r1_tarski(X0,iPr_def_17) ),
inference(global_subsumption_just,[status(thm)],[c_5093,c_5093,c_5228]) ).
tcf(c_5645,plain,
( r1_tarski(iPr_def_18,iPr_def_18)
| ~ r1_tarski(iPr_def_17,iPr_def_17) ),
inference(superposition,[status(thm)],[c_4914,c_5637]) ).
tcf(c_5649,plain,
! [X0: $i] :
( r1_tarski(iPr_def_18,k10_relat_1(sK2,X0))
| ~ r1_tarski(iPr_def_17,X0) ),
inference(global_subsumption_just,[status(thm)],[c_5094,c_5094,c_5228]) ).
tcf(c_5658,plain,
( m1_group_2(sK0,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_15)
| ~ m1_group_2(sK0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_5138,c_4032,c_4229]) ).
tcf(c_5692,plain,
! [X0: $i,X1: $i] :
( ~ r1_tarski(X1,X0)
| ~ r2_hidden(k1_zfmisc_1(X0),X1) ),
inference(superposition,[status(thm)],[c_4602,c_68]) ).
tcf(c_5693,plain,
! [X0: $i,X1: $i] :
( ~ v1_xboole_0(k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(superposition,[status(thm)],[c_4602,c_130]) ).
tcf(c_5698,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : v1_relat_1(k10_relat_1(sK17(k2_zfmisc_1(X0,X1),X2),X3)),
inference(superposition,[status(thm)],[c_5049,c_70]) ).
tcf(c_5699,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_xboole_0(k1_zfmisc_1(X0))
| r2_hidden(k10_relat_1(sK17(X0,X1),X2),k1_zfmisc_1(X0)) ),
inference(superposition,[status(thm)],[c_5049,c_123]) ).
tcf(c_5700,plain,
! [X0: $i,X1: $i,X2: $i] : r1_tarski(k10_relat_1(sK17(X0,X1),X2),X0),
inference(superposition,[status(thm)],[c_5049,c_125]) ).
tcf(c_5701,plain,
! [X0: $i,X1: $i,X2: $i] : r2_hidden(k10_relat_1(sK17(X0,X1),X2),k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_5699,c_95]) ).
tcf(c_5706,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : v1_relat_1(k10_relat_1(sK14(k2_zfmisc_1(X0,X1),X2),X3)),
inference(superposition,[status(thm)],[c_5177,c_70]) ).
tcf(c_5707,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_xboole_0(k1_zfmisc_1(X0))
| r2_hidden(k10_relat_1(sK14(X0,X1),X2),k1_zfmisc_1(X0)) ),
inference(superposition,[status(thm)],[c_5177,c_123]) ).
tcf(c_5708,plain,
! [X0: $i,X1: $i,X2: $i] : r1_tarski(k10_relat_1(sK14(X0,X1),X2),X0),
inference(superposition,[status(thm)],[c_5177,c_125]) ).
tcf(c_5709,plain,
! [X0: $i,X1: $i,X2: $i] : r2_hidden(k10_relat_1(sK14(X0,X1),X2),k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[status(thm)],[c_5707,c_95]) ).
tcf(c_5727,plain,
( v3_struct_0(sK8)
| ~ r2_hidden(k1_zfmisc_1(u1_struct_0(sK8)),sK21(sK8)) ),
inference(superposition,[status(thm)],[c_5586,c_68]) ).
tcf(c_5728,plain,
( v3_struct_0(sK8)
| ~ v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK8))) ),
inference(superposition,[status(thm)],[c_5586,c_130]) ).
tcf(c_5732,plain,
( m1_group_2(sK0,sK5)
| ~ r1_tarski(iPr_def_13,iPr_def_18)
| ~ m1_group_2(sK0,sK1) ),
inference(global_subsumption_just,[status(thm)],[c_5240,c_4032,c_4340]) ).
tcf(c_5757,plain,
( m1_group_2(sK1,sK0)
| ~ r1_tarski(iPr_def_12,iPr_def_13)
| ~ m1_group_2(sK1,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4039]) ).
tcf(c_5759,plain,
( m1_group_2(sK1,sK3)
| ~ r1_tarski(iPr_def_12,iPr_def_17)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4039]) ).
tcf(c_5761,plain,
( m1_group_2(sK1,sK4)
| ~ r1_tarski(iPr_def_12,iPr_def_14)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK1,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4039]) ).
tcf(c_5778,plain,
( m1_group_2(sK1,sK1)
| ~ r1_tarski(iPr_def_12,iPr_def_12)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2405,c_4040]) ).
tcf(c_5779,plain,
( m1_group_2(sK1,sK3)
| ~ r1_tarski(iPr_def_12,iPr_def_17)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2410,c_4040]) ).
tcf(c_5781,plain,
( m1_group_2(sK1,sK4)
| ~ r1_tarski(iPr_def_12,iPr_def_14)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK1,sK0) ),
inference(superposition,[status(thm)],[c_2407,c_4040]) ).
tcf(c_5782,plain,
( m1_group_2(sK1,sK1)
| ~ m1_group_2(sK1,sK0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5778,c_120]) ).
tcf(c_5806,plain,
( m1_group_2(sK0,sK1)
| ~ r1_tarski(iPr_def_13,iPr_def_12)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2406,c_4042]) ).
tcf(c_5824,plain,
( m1_group_2(sK0,sK0)
| ~ r1_tarski(iPr_def_13,iPr_def_13)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2406,c_4057]) ).
tcf(c_5826,plain,
( m1_group_2(sK0,sK3)
| ~ r1_tarski(iPr_def_13,iPr_def_17)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4057]) ).
tcf(c_5828,plain,
( m1_group_2(sK0,sK4)
| ~ r1_tarski(iPr_def_13,iPr_def_14)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4057]) ).
tcf(c_5829,plain,
( m1_group_2(sK0,sK0)
| ~ m1_group_2(sK0,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5824,c_120]) ).
tcf(c_5848,plain,
( m1_group_2(sK0,sK3)
| ~ r1_tarski(iPr_def_13,iPr_def_17)
| ~ m1_group_2(sK3,sK0)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2410,c_4058]) ).
tcf(c_5849,plain,
( m1_group_2(sK0,sK6)
| ~ r1_tarski(iPr_def_13,iPr_def_15)
| ~ m1_group_2(sK6,sK0)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_4096,c_4058]) ).
tcf(c_5850,plain,
( m1_group_2(sK0,sK4)
| ~ r1_tarski(iPr_def_13,iPr_def_14)
| ~ m1_group_2(sK4,sK0)
| ~ m1_group_2(sK0,sK0) ),
inference(superposition,[status(thm)],[c_2407,c_4058]) ).
tcf(c_5871,plain,
( m1_group_2(sK3,sK0)
| ~ r1_tarski(iPr_def_17,iPr_def_13)
| ~ m1_group_2(sK3,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2410,c_4059]) ).
tcf(c_5873,plain,
( m1_group_2(sK4,sK0)
| ~ r1_tarski(iPr_def_14,iPr_def_13)
| ~ m1_group_2(sK4,sK1)
| ~ m1_group_2(sK0,sK1) ),
inference(superposition,[status(thm)],[c_2407,c_4059]) ).
tcf(c_5888,plain,
! [X0: $i,X1: $i,X2: $i] : ~ r2_hidden(k1_zfmisc_1(X0),k10_relat_1(sK17(X0,X1),X2)),
inference(superposition,[status(thm)],[c_5701,c_68]) ).
tcf(c_5892,plain,
! [X0: $i,X1: $i,X2: $i] : ~ r2_hidden(k1_zfmisc_1(X0),k10_relat_1(sK14(X0,X1),X2)),
inference(superposition,[status(thm)],[c_5709,c_68]) ).
tcf(c_5914,plain,
( v3_struct_0(sK5)
| ~ v1_xboole_0(iPr_def_18)
| ~ l1_group_1(sK5) ),
inference(superposition,[status(thm)],[c_4142,c_1314]) ).
tcf(c_5915,plain,
( v3_struct_0(sK0)
| ~ v1_xboole_0(iPr_def_13)
| ~ l1_group_1(sK0) ),
inference(superposition,[status(thm)],[c_2406,c_1314]) ).
tcf(c_5916,plain,
( v3_struct_0(sK1)
| ~ v1_xboole_0(iPr_def_12)
| ~ l1_group_1(sK1) ),
inference(superposition,[status(thm)],[c_2405,c_1314]) ).
tcf(c_5917,plain,
( v3_struct_0(sK3)
| ~ v1_xboole_0(iPr_def_17)
| ~ l1_group_1(sK3) ),
inference(superposition,[status(thm)],[c_2410,c_1314]) ).
tcf(c_5918,plain,
( v3_struct_0(sK6)
| ~ v1_xboole_0(iPr_def_15)
| ~ l1_group_1(sK6) ),
inference(superposition,[status(thm)],[c_4096,c_1314]) ).
tcf(c_5919,plain,
( v3_struct_0(sK4)
| ~ v1_xboole_0(iPr_def_14)
| ~ l1_group_1(sK4) ),
inference(superposition,[status(thm)],[c_2407,c_1314]) ).
tcf(c_5920,plain,
~ v1_xboole_0(iPr_def_14),
inference(forward_subsumption_resolution,[status(thm)],[c_5919,c_4848,c_4781]) ).
tcf(c_5921,plain,
~ v1_xboole_0(iPr_def_15),
inference(forward_subsumption_resolution,[status(thm)],[c_5918,c_4850,c_4783]) ).
tcf(c_5922,plain,
~ v1_xboole_0(iPr_def_17),
inference(forward_subsumption_resolution,[status(thm)],[c_5917,c_4847,c_4780]) ).
tcf(c_5923,plain,
~ v1_xboole_0(iPr_def_12),
inference(forward_subsumption_resolution,[status(thm)],[c_5916,c_2436,c_2434]) ).
tcf(c_5924,plain,
~ v1_xboole_0(iPr_def_13),
inference(forward_subsumption_resolution,[status(thm)],[c_5915,c_2433,c_2431]) ).
tcf(c_5925,plain,
~ v1_xboole_0(iPr_def_18),
inference(forward_subsumption_resolution,[status(thm)],[c_5914,c_4849,c_4782]) ).
tcf(c_5926,plain,
~ v1_xboole_0(sK2),
inference(backward_subsumption_resolution,[status(thm)],[c_2429,c_5923]) ).
tcf(c_5976,plain,
! [X0: $i,X1: $i] :
( ~ r1_tarski(k1_zfmisc_1(X1),X0)
| ~ r1_tarski(k1_zfmisc_1(X0),X1) ),
inference(superposition,[status(thm)],[c_4602,c_5692]) ).
tcf(c_5993,plain,
! [X0: $i] : ~ r1_tarski(k1_zfmisc_1(k1_zfmisc_1(X0)),X0),
inference(superposition,[status(thm)],[c_120,c_5976]) ).
tcf(c_5994,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m1_relset_1(k1_zfmisc_1(X2),X0,X1)
| ~ r1_tarski(k1_zfmisc_1(k2_zfmisc_1(X0,X1)),X2) ),
inference(superposition,[status(thm)],[c_4619,c_5976]) ).
tcf(c_5999,plain,
! [X0: $i,X1: $i] : ~ m1_relset_1(k1_zfmisc_1(k1_zfmisc_1(k2_zfmisc_1(X0,X1))),X0,X1),
inference(superposition,[status(thm)],[c_4619,c_5993]) ).
tcf(c_6056,plain,
( m1_group_2(iPr_def_11,iPr_def_11)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_5365]) ).
tcf(c_6071,plain,
( m1_group_2(iPr_def_11,sK0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(sK6,sK1) ),
inference(superposition,[status(thm)],[c_2404,c_5408]) ).
tcf(c_6072,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_5408,c_2426]) ).
tcf(c_6073,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(sK1,sK0)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(X0,sK1) ),
inference(superposition,[status(thm)],[c_5408,c_2425]) ).
tcf(c_6075,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_5408,c_81]) ).
tcf(c_6076,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_5408,c_80]) ).
tcf(c_6077,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_5408,c_4018]) ).
tcf(c_6092,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_6076,c_2433,c_2431,c_2432]) ).
tcf(c_6096,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_6075,c_2433,c_2431,c_2432]) ).
tcf(c_6113,plain,
( m1_group_2(iPr_def_11,sK0)
| ~ m1_group_2(sK6,sK1)
| ~ m1_group_2(sK6,sK0) ),
inference(superposition,[status(thm)],[c_2404,c_5409]) ).
tcf(c_6114,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK1)
| ~ m1_group_2(sK0,sK1)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_5409,c_2426]) ).
tcf(c_6115,plain,
! [X0: $i] :
( m1_group_2(sK10(sK1,X0),sK0)
| ~ m1_group_2(sK0,sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_5409,c_2425]) ).
tcf(c_6116,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0)
| ~ v3_struct_0(sK10(sK1,X0)) ),
inference(superposition,[status(thm)],[c_5409,c_79]) ).
tcf(c_6117,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| l1_group_1(sK10(sK1,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_5409,c_81]) ).
tcf(c_6118,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v3_group_1(sK10(sK1,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0) ),
inference(superposition,[status(thm)],[c_5409,c_80]) ).
tcf(c_6120,plain,
( m1_group_2(iPr_def_11,sK0)
| ~ m1_group_2(sK6,sK1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6113,c_2441]) ).
tcf(c_6133,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK1)
| ~ m1_group_2(X0,sK0)
| ~ v3_struct_0(sK10(sK1,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6116,c_2433,c_2431,c_2432]) ).
tcf(c_6143,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_6133,c_6120,c_6118,c_6117,c_6116,c_6115,c_6114,c_6113,c_6096,c_6092,c_6077,c_6076,c_6075,c_6073,c_6072,c_6071,c_6056,c_5999,c_5994,c_5993,c_5976,c_5926,c_5925,c_5924,c_5923,c_5922,c_5921,c_5920,c_5919,c_5918,c_5917,c_5916,c_5915,c_5914,c_5892,c_5888,c_5873,c_5871,c_5850,c_5849,c_5848,c_5828,c_5826,c_5824,c_5806,c_5782,c_5781,c_5779,c_5778,c_5761,c_5759,c_5757,c_5732,c_5728,c_5727,c_5709,c_5708,c_5707,c_5706,c_5701,c_5700,c_5699,c_5698,c_5693,c_5692,c_5658,c_5649,c_5645,c_5637,c_5628,c_5620,c_5619,c_5618,c_5617,c_5610,c_5605,c_5583,c_5521,c_5520,c_5515,c_5514,c_5512,c_5510,c_5507,c_5506,c_5485,c_5478,c_5411,c_5409,c_5408,c_5407,c_5406,c_5405,c_5404,c_5393,c_5376,c_5373,c_5370,c_5365,c_5364,c_5363,c_5362,c_5361,c_5326,c_5325,c_5324,c_5323,c_5322,c_5321,c_5304,c_5289,c_5275,c_5258,c_5244,c_5242,c_5241,c_5240,c_5228,c_5227,c_5224,c_5214,c_5198,c_5194,c_5193,c_5187,c_5177,c_5176,c_5173,c_5171,c_5142,c_5140,c_5139,c_5138,c_5126,c_5124,c_5094,c_5093,c_5082,c_5081,c_5054,c_5052,c_5051,c_5049,c_5048,c_5037,c_5036,c_5035,c_5033,c_5032,c_5013,c_5012,c_5011,c_5010,c_5009,c_5008,c_4986,c_4985,c_4978,c_4977,c_4970,c_4969,c_4961,c_4960,c_4952,c_4951,c_4943,c_4942,c_4941,c_4940,c_4939,c_4938,c_4937,c_4936,c_4914,c_4913,c_4906,c_4905,c_4878,c_4877,c_4876,c_4874,c_4873,c_4872,c_4855,c_4850,c_4849,c_4848,c_4847,c_4843,c_4839,c_4833,c_4831,c_4830,c_4829,c_4828,c_4827,c_4826,c_4788,c_4783,c_4782,c_4781,c_4780,c_4775,c_4773,c_4767,c_4766,c_4764,c_4763,c_4762,c_4761,c_4760,c_4740,c_4735,c_4734,c_4733,c_4732,c_4727,c_4725,c_4719,c_4718,c_4716,c_4715,c_4714,c_4713,c_4712,c_4701,c_4700,c_4699,c_4698,c_4630,c_4629,c_4619,c_4617,c_4597,c_4594,c_4575,c_4574,c_4573,c_4514,c_4513,c_4512,c_4502,c_4501,c_4499,c_4481,c_4480,c_4479,c_4478,c_4412,c_4410,c_4409,c_4368,c_4366,c_4365,c_4344,c_4342,c_4341,c_4340,c_4322,c_4319,c_4318,c_4302,c_4297,c_4296,c_4295,c_4294,c_4293,c_4268,c_4258,c_4256,c_4255,c_4253,c_4246,c_4233,c_4231,c_4230,c_4229,c_4228,c_4209,c_4204,c_4203,c_4201,c_4200,c_4181,c_4180,c_4179,c_4177,c_4176,c_4175,c_4155,c_4147,c_4146,c_4145,c_4144,c_4143,c_4142,c_4135,c_4127,c_4122,c_4121,c_4120,c_4119,c_4109,c_4101,c_4100,c_4099,c_4098,c_4097,c_4096,c_4089,c_4081,c_4076,c_4075,c_4074,c_4073,c_4059,c_4058,c_4057,c_4042,c_4040,c_4039,c_4038,c_4037,c_5829,c_4029,c_4018,c_2443,c_2442,c_2430,c_2429,c_2423,c_2421,c_2412,c_2411,c_2410,c_2409,c_2408,c_2407,c_2406,c_2405,c_2404,c_2403,c_4598,c_4593,c_5586,c_5582,c_4602,c_4592,c_4599,c_4591,c_4498,c_4590,c_4885,c_4875,c_4624,c_4618,c_4511,c_2413,c_2414,c_2415,c_2416,c_2417,c_2418,c_2419,c_2420,c_2422,c_2424,c_2425,c_2426,c_2427,c_2428,c_4904,c_4909,c_4903,c_4910,c_4902,c_4901,c_1365,c_1358,c_1351,c_1342,c_1334,c_1326,c_1314,c_1302,c_1290,c_1172,c_1154,c_1093,c_1084,c_361,c_360,c_200,c_183,c_181,c_131,c_130,c_129,c_125,c_124,c_123,c_122,c_121,c_120,c_115,c_112,c_110,c_109,c_108,c_107,c_106,c_105,c_104,c_103,c_102,c_100,c_99,c_98,c_97,c_96,c_95,c_92,c_91,c_89,c_87,c_84,c_81,c_80,c_79,c_77,c_74,c_70,c_68,c_2431,c_2432,c_2433,c_2434,c_2435,c_2436,c_2437,c_2438,c_2439,c_2440,c_2441]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP638+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.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 15:25:38 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/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.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 3.75/1.18 % SZS status Started for theBenchmark.p
% 3.75/1.18 % SZS status Theorem for theBenchmark.p
% 3.75/1.18
% 3.75/1.18 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.75/1.18
% 3.75/1.18 % ------ iProver source info
% 3.75/1.18
% 3.75/1.18 % git: date: 2026-07-19 20:42:38 +0200
% 3.75/1.18 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.75/1.18 % git: non_committed_changes: false
% 3.75/1.18
% 3.75/1.18 % ------ Parsing...
% 3.75/1.18 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.75/1.18
% 3.75/1.18 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e %
% 3.75/1.18
% 3.75/1.18 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.75/1.18
% 3.75/1.18 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.75/1.18 % ------ Proving...
% 3.75/1.18 % ------ Problem Properties
% 3.75/1.18
% 3.75/1.18 %
% 3.75/1.18 % clauses 97
% 3.75/1.18 % conjectures 13
% 3.75/1.18 % EPR 40
% 3.75/1.18 % Horn 84
% 3.75/1.18 % unary 48
% 3.75/1.18 % binary 20
% 3.75/1.18 % lits 197
% 3.75/1.18 % lits eq 26
% 3.75/1.18 % fd_pure 0
% 3.75/1.18 % fd_pseudo 0
% 3.75/1.18 % fd_cond 1
% 3.75/1.18 % fd_pseudo_cond 1
% 3.75/1.18 % AC symbols 0
% 3.75/1.18
% 3.75/1.18 % ------ Schedule dynamic 5 is on
% 3.75/1.18
% 3.75/1.18 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.75/1.18
% 3.75/1.18
% 3.75/1.18 % ------
% 3.75/1.18 % Current options:
% 3.75/1.18 % ------
% 3.75/1.18
% 3.75/1.18
% 3.75/1.18 %
% 3.75/1.18
% 3.75/1.18 % ------ Proving...
% 3.75/1.18 %
% 3.75/1.18
% 3.75/1.18 % SZS status Theorem for theBenchmark.p
% 3.75/1.18
% 3.75/1.18 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.25/1.21
% 4.25/1.21
%------------------------------------------------------------------------------