%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP646+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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:35:01 PM UTC 2026
% Result : Theorem 94.65s 15.08s
% Output : CNFRefutation 94.65s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f348ERROR: Could not build tree for root c_83793ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
& ~ v1_xboole_0(X1) )
=> ( r2_hidden(k5_group_2(X0),X1)
=> r1_group_2(X0,k2_latsubgr(X0,X1),k5_group_2(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t25_latsubgr) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
& ~ v1_xboole_0(X1) )
=> ( r2_hidden(k5_group_2(X0),X1)
=> r1_group_2(X0,k2_latsubgr(X0,X1),k5_group_2(X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X1,X0)
& r1_tarski(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f11,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_1(X1) )
=> ( X1 = k1_latsubgr(X0)
<=> ! [X2] :
( ( m1_group_2(X2,X0)
& v1_group_1(X2) )
=> k1_funct_1(X1,X2) = u1_struct_0(X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_latsubgr) ).
fof(f12,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
& ~ v1_xboole_0(X1) )
=> ! [X2] :
( ( m1_group_2(X2,X0)
& v1_group_1(X2) )
=> ( X2 = k2_latsubgr(X0,X1)
<=> u1_struct_0(X2) = k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_latsubgr) ).
fof(f13,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] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m1_group_2(X1,X0)
& v1_group_1(X1) )
=> ( X1 = k5_group_2(X0)
<=> u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_group_2) ).
fof(f19,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_1(k1_latsubgr(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_latsubgr) ).
fof(f25,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,X0,X1)
& v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_funct_2) ).
fof(f27,axiom,
! [X0,X1] :
( ( m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
& ~ v1_xboole_0(X1)
& l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( m1_group_2(k2_latsubgr(X0,X1),X0)
& v1_group_1(k2_latsubgr(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_latsubgr) ).
fof(f30,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ( m1_group_2(k5_group_2(X0),X0)
& v1_group_1(k5_group_2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_group_2) ).
fof(f37,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(f51,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ~ v1_xboole_0(k1_group_3(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_group_3) ).
fof(f53,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f54,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f67,axiom,
! [X0,X1,X2,X3] :
( ( m1_relset_1(X2,X0,X1)
& v1_funct_2(X2,X0,X1)
& v1_funct_1(X2) )
=> k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_funct_2) ).
fof(f69,axiom,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
=> k6_setfam_1(X0,X1) = k1_setfam_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_setfam_1) ).
fof(f72,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(f74,axiom,
! [X0,X1,X2] :
( ( m1_group_2(X2,X0)
& v1_group_1(X2)
& m1_group_2(X1,X0)
& v1_group_1(X1)
& l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> r1_group_2(X0,X1,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_group_2) ).
fof(f75,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f78,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(f79,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(f80,axiom,
! [X0,X1,X2,X3] :
( ( m2_relset_1(X3,X0,X1)
& v1_funct_2(X3,X0,X1)
& v1_funct_1(X3) )
=> ( X1 != k1_xboole_0
=> ! [X4] :
( ? [X5] :
( X4 = k1_funct_1(X3,X5)
& r2_hidden(X5,X2)
& r2_hidden(X5,X0) )
=> r2_hidden(X4,k9_relat_1(X3,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t43_funct_2) ).
fof(f81,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> r1_tarski(k1_setfam_1(X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_setfam_1) ).
fof(f82,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(f83,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(f85,axiom,
! [X0] :
( ( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_group_2(X1,X0)
=> m1_group_2(k5_group_2(X0),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t77_group_2) ).
fof(f88,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f75]) ).
fof(f93,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
& ~ v1_xboole_0(X1)
& r2_hidden(k5_group_2(X0),X1)
& ~ r1_group_2(X0,k2_latsubgr(X0,X1),k5_group_2(X0)) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f94,plain,
? [X0] :
( l1_group_1(X0)
& v4_group_1(X0)
& v3_group_1(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
& ~ v1_xboole_0(X1)
& r2_hidden(k5_group_2(X0),X1)
& ~ r1_group_2(X0,k2_latsubgr(X0,X1),k5_group_2(X0)) ) ),
inference(flattening,[],[f93]) ).
fof(f106,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ( X1 = k1_latsubgr(X0)
<=> ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| k1_funct_1(X1,X2) = u1_struct_0(X2) ) ) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f107,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ( X1 = k1_latsubgr(X0)
<=> ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| k1_funct_1(X1,X2) = u1_struct_0(X2) ) ) ) ),
inference(flattening,[],[f106]) ).
fof(f108,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ( X2 = k2_latsubgr(X0,X1)
<=> u1_struct_0(X2) = k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) ) ) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f109,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ( X2 = k2_latsubgr(X0,X1)
<=> u1_struct_0(X2) = k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) ) ) ) ),
inference(flattening,[],[f108]) ).
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)) ) ) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f111,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,[],[f110]) ).
fof(f112,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ( X1 = k5_group_2(X0)
<=> u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) ) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f113,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ( X1 = k5_group_2(X0)
<=> u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) ) ) ),
inference(flattening,[],[f112]) ).
fof(f118,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_1(k1_latsubgr(X0)) ) ),
inference(ennf_transformation,[],[f19]) ).
fof(f119,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
& v1_funct_1(k1_latsubgr(X0)) ) ),
inference(flattening,[],[f118]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f25]) ).
fof(f121,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(flattening,[],[f120]) ).
fof(f124,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( m1_group_2(k2_latsubgr(X0,X1),X0)
& v1_group_1(k2_latsubgr(X0,X1)) ) ),
inference(ennf_transformation,[],[f27]) ).
fof(f125,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( m1_group_2(k2_latsubgr(X0,X1),X0)
& v1_group_1(k2_latsubgr(X0,X1)) ) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( m1_group_2(k5_group_2(X0),X0)
& v1_group_1(k5_group_2(X0)) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f127,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ( m1_group_2(k5_group_2(X0),X0)
& v1_group_1(k5_group_2(X0)) ) ),
inference(flattening,[],[f126]) ).
fof(f134,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,[],[f37]) ).
fof(f135,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,[],[f134]) ).
fof(f144,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k1_group_3(X0)) ),
inference(ennf_transformation,[],[f51]) ).
fof(f145,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k1_group_3(X0)) ),
inference(flattening,[],[f144]) ).
fof(f157,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f67]) ).
fof(f158,plain,
! [X0,X1,X2,X3] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(flattening,[],[f157]) ).
fof(f161,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| k6_setfam_1(X0,X1) = k1_setfam_1(X1) ),
inference(ennf_transformation,[],[f69]) ).
fof(f168,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| r1_group_2(X0,X1,X1) ),
inference(ennf_transformation,[],[f74]) ).
fof(f169,plain,
! [X0,X1,X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| r1_group_2(X0,X1,X1) ),
inference(flattening,[],[f168]) ).
fof(f173,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f78]) ).
fof(f174,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(flattening,[],[f173]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ m2_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| k1_xboole_0 = X1
| ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X5) != X4
| ~ r2_hidden(X5,X2)
| ~ r2_hidden(X5,X0) )
| r2_hidden(X4,k9_relat_1(X3,X2)) ) ),
inference(ennf_transformation,[],[f80]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ~ m2_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| k1_xboole_0 = X1
| ! [X4] :
( ! [X5] :
( k1_funct_1(X3,X5) != X4
| ~ r2_hidden(X5,X2)
| ~ r2_hidden(X5,X0) )
| r2_hidden(X4,k9_relat_1(X3,X2)) ) ),
inference(flattening,[],[f175]) ).
fof(f177,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| r1_tarski(k1_setfam_1(X1),X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f178,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(ennf_transformation,[],[f82]) ).
fof(f179,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(flattening,[],[f178]) ).
fof(f180,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f83]) ).
fof(f182,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| m1_group_2(k5_group_2(X0),X1) ) ),
inference(ennf_transformation,[],[f85]) ).
fof(f183,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| m1_group_2(k5_group_2(X0),X1) ) ),
inference(flattening,[],[f182]) ).
fof(f186,plain,
( l1_group_1(sK0)
& v4_group_1(sK0)
& v3_group_1(sK0)
& ~ v3_struct_0(sK0)
& m1_subset_1(sK1,k1_zfmisc_1(k1_group_3(sK0)))
& ~ v1_xboole_0(sK1)
& r2_hidden(k5_group_2(sK0),sK1)
& ~ r1_group_2(sK0,k2_latsubgr(sK0,sK1),k5_group_2(sK0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f94]) ).
fof(f187,plain,
! [X0,X1] :
( ( X0 != X1
| ( r1_tarski(X1,X0)
& r1_tarski(X0,X1) ) )
& ( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f188,plain,
! [X0,X1] :
( ( X0 != X1
| ( r1_tarski(X1,X0)
& r1_tarski(X0,X1) ) )
& ( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ) ),
inference(flattening,[],[f187]) ).
fof(f193,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ( ( k1_latsubgr(X0) != X1
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| k1_funct_1(X1,X2) = u1_struct_0(X2) ) )
& ( ? [X2] :
( m1_group_2(X2,X0)
& v1_group_1(X2)
& k1_funct_1(X1,X2) != u1_struct_0(X2) )
| X1 = k1_latsubgr(X0) ) ) ) ),
inference(nnf_transformation,[],[f107]) ).
fof(f194,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ( ( k1_latsubgr(X0) != X1
| ! [X3] :
( ~ m1_group_2(X3,X0)
| ~ v1_group_1(X3)
| k1_funct_1(X1,X3) = u1_struct_0(X3) ) )
& ( ? [X2] :
( m1_group_2(X2,X0)
& v1_group_1(X2)
& k1_funct_1(X1,X2) != u1_struct_0(X2) )
| X1 = k1_latsubgr(X0) ) ) ) ),
inference(rectify,[],[f193]) ).
fof(f195,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| ( ( k1_latsubgr(X0) != X1
| ! [X3] :
( ~ m1_group_2(X3,X0)
| ~ v1_group_1(X3)
| k1_funct_1(X1,X3) = u1_struct_0(X3) ) )
& ( ( m1_group_2(sK3(X0,X1),X0)
& v1_group_1(sK3(X0,X1))
& k1_funct_1(X1,sK3(X0,X1)) != u1_struct_0(sK3(X0,X1)) )
| X1 = k1_latsubgr(X0) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f194]) ).
fof(f196,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ! [X2] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ( ( k2_latsubgr(X0,X1) != X2
| u1_struct_0(X2) = k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) )
& ( u1_struct_0(X2) != k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1))
| X2 = k2_latsubgr(X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f109]) ).
fof(f197,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,[],[f111]) ).
fof(f198,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,[],[f197]) ).
fof(f199,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ( ( k5_group_2(X0) != X1
| u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) )
& ( u1_struct_0(X1) != k6_domain_1(u1_struct_0(X0),k2_group_1(X0))
| X1 = k5_group_2(X0) ) ) ) ),
inference(nnf_transformation,[],[f113]) ).
fof(f216,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,[],[f72]) ).
fof(f218,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,[],[f79]) ).
fof(f219,plain,
l1_group_1(sK0),
inference(cnf_transformation,[],[f186]) ).
fof(f220,plain,
v4_group_1(sK0),
inference(cnf_transformation,[],[f186]) ).
fof(f221,plain,
v3_group_1(sK0),
inference(cnf_transformation,[],[f186]) ).
fof(f222,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f186]) ).
fof(f223,plain,
m1_subset_1(sK1,k1_zfmisc_1(k1_group_3(sK0))),
inference(cnf_transformation,[],[f186]) ).
fof(f224,plain,
~ v1_xboole_0(sK1),
inference(cnf_transformation,[],[f186]) ).
fof(f225,plain,
r2_hidden(k5_group_2(sK0),sK1),
inference(cnf_transformation,[],[f186]) ).
fof(f226,plain,
~ r1_group_2(sK0,k2_latsubgr(sK0,sK1),k5_group_2(sK0)),
inference(cnf_transformation,[],[f186]) ).
fof(f240,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f188]) ).
fof(f247,plain,
! [X3,X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(X1)
| k1_latsubgr(X0) != X1
| ~ m1_group_2(X3,X0)
| ~ v1_group_1(X3)
| k1_funct_1(X1,X3) = u1_struct_0(X3) ),
inference(cnf_transformation,[],[f195]) ).
fof(f251,plain,
! [X2,X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| k2_latsubgr(X0,X1) != X2
| u1_struct_0(X2) = k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) ),
inference(cnf_transformation,[],[f196]) ).
fof(f254,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,[],[f198]) ).
fof(f256,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| k5_group_2(X0) != X1
| u1_struct_0(X1) = k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) ),
inference(cnf_transformation,[],[f199]) ).
fof(f257,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| u1_struct_0(X1) != k6_domain_1(u1_struct_0(X0),k2_group_1(X0))
| k5_group_2(X0) = X1 ),
inference(cnf_transformation,[],[f199]) ).
fof(f261,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f119]) ).
fof(f262,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f119]) ).
fof(f263,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_funct_1(k1_latsubgr(X0)) ),
inference(cnf_transformation,[],[f119]) ).
fof(f264,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| m1_subset_1(k2_funct_2(X0,X1,X2,X3),k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f121]) ).
fof(f266,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(k2_latsubgr(X0,X1),X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f267,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_group_1(k2_latsubgr(X0,X1)) ),
inference(cnf_transformation,[],[f125]) ).
fof(f268,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| m1_group_2(k5_group_2(X0),X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f269,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| v1_group_1(k5_group_2(X0)) ),
inference(cnf_transformation,[],[f127]) ).
fof(f274,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,[],[f135]) ).
fof(f275,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,[],[f135]) ).
fof(f276,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,[],[f135]) ).
fof(f289,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k1_group_3(X0)) ),
inference(cnf_transformation,[],[f145]) ).
fof(f291,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f53]) ).
fof(f292,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f54]) ).
fof(f313,plain,
! [X2,X3,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| ~ v1_funct_2(X2,X0,X1)
| ~ v1_funct_1(X2)
| k2_funct_2(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f158]) ).
fof(f315,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(k1_zfmisc_1(X0)))
| k6_setfam_1(X0,X1) = k1_setfam_1(X1) ),
inference(cnf_transformation,[],[f161]) ).
fof(f319,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f216]) ).
fof(f323,plain,
! [X2,X0,X1] :
( ~ m1_group_2(X2,X0)
| ~ v1_group_1(X2)
| ~ m1_group_2(X1,X0)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| r1_group_2(X0,X1,X1) ),
inference(cnf_transformation,[],[f169]) ).
fof(f324,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f88]) ).
fof(f327,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f174]) ).
fof(f328,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f218]) ).
fof(f329,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X1)
| m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f218]) ).
fof(f330,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ m2_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| k1_xboole_0 = X1
| k1_funct_1(X3,X5) != X4
| ~ r2_hidden(X5,X2)
| ~ r2_hidden(X5,X0)
| r2_hidden(X4,k9_relat_1(X3,X2)) ),
inference(cnf_transformation,[],[f176]) ).
fof(f331,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| r1_tarski(k1_setfam_1(X1),X0) ),
inference(cnf_transformation,[],[f177]) ).
fof(f332,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X2) ),
inference(cnf_transformation,[],[f179]) ).
fof(f333,plain,
! [X2,X0,X1] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f335,plain,
! [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(k5_group_2(X0),X1) ),
inference(cnf_transformation,[],[f183]) ).
fof(f343,plain,
! [X3,X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_1(k1_latsubgr(X0))
| ~ m1_group_2(X3,X0)
| ~ v1_group_1(X3)
| u1_struct_0(X3) = k1_funct_1(k1_latsubgr(X0),X3) ),
inference(equality_resolution,[],[f247]) ).
fof(f344,plain,
! [X0,X1] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| v1_xboole_0(X1)
| ~ m1_group_2(k2_latsubgr(X0,X1),X0)
| ~ v1_group_1(k2_latsubgr(X0,X1))
| k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) = u1_struct_0(k2_latsubgr(X0,X1)) ),
inference(equality_resolution,[],[f251]) ).
fof(f345,plain,
! [X0] :
( ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| v3_struct_0(X0)
| ~ m1_group_2(k5_group_2(X0),X0)
| ~ v1_group_1(k5_group_2(X0))
| k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) = u1_struct_0(k5_group_2(X0)) ),
inference(equality_resolution,[],[f256]) ).
fof(f347,plain,
! [X2,X3,X0,X1,X5] :
( ~ m2_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| k1_xboole_0 = X1
| ~ r2_hidden(X5,X2)
| ~ r2_hidden(X5,X0)
| r2_hidden(k1_funct_1(X3,X5),k9_relat_1(X3,X2)) ),
inference(equality_resolution,[],[f330]) ).
tcf(c_49,negated_conjecture,
~ r1_group_2(sK0,k2_latsubgr(sK0,sK1),k5_group_2(sK0)),
inference(cnf_transformation,[],[f226]) ).
tcf(c_50,negated_conjecture,
r2_hidden(k5_group_2(sK0),sK1),
inference(cnf_transformation,[],[f225]) ).
tcf(c_51,negated_conjecture,
~ v1_xboole_0(sK1),
inference(cnf_transformation,[],[f224]) ).
tcf(c_52,negated_conjecture,
m1_subset_1(sK1,k1_zfmisc_1(k1_group_3(sK0))),
inference(cnf_transformation,[],[f223]) ).
tcf(c_53,negated_conjecture,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f222]) ).
tcf(c_54,negated_conjecture,
v3_group_1(sK0),
inference(cnf_transformation,[],[f221]) ).
tcf(c_55,negated_conjecture,
v4_group_1(sK0),
inference(cnf_transformation,[],[f220]) ).
tcf(c_56,negated_conjecture,
l1_group_1(sK0),
inference(cnf_transformation,[],[f219]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| ( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1) )
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_funct_1(k1_latsubgr(X0))
| ~ m1_group_2(X1,X0)
| ~ m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf_transformation,[],[f343]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v1_xboole_0(X1)
| ( k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) = u1_struct_0(k2_latsubgr(X0,X1)) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(k2_latsubgr(X0,X1))
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| ~ m1_group_2(k2_latsubgr(X0,X1),X0) ),
inference(cnf_transformation,[],[f344]) ).
tcf(c_79,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,[],[f254]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| ( k5_group_2(X0) = X1 )
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) != u1_struct_0(X1) ) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_82,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) = u1_struct_0(k5_group_2(X0)) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_group_1(k5_group_2(X0))
| ~ m1_group_2(k5_group_2(X0),X0) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_86,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_1(k1_latsubgr(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_87,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_88,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f261]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k2_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X2))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v1_xboole_0(X0)
| v1_group_1(k2_latsubgr(X1,X0))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(X1))) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v1_xboole_0(X0)
| m1_group_2(k2_latsubgr(X1,X0),X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(X1))) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_93,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_group_1(k5_group_2(X0))
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_94,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(k5_group_2(X0),X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_99,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,[],[f276]) ).
tcf(c_100,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,[],[f275]) ).
tcf(c_101,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,[],[f274]) ).
tcf(c_114,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_xboole_0(k1_group_3(X0)) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_116,plain,
! [X0: $i] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f291]) ).
tcf(c_117,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f292]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i] :
( ( k6_setfam_1(X1,X0) = k1_setfam_1(X0) )
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_zfmisc_1(X1))) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r1_group_2(X1,X0,X0)
| ~ v1_group_1(X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f348]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| r1_group_2(X1,X0,X0)
| ~ v1_group_1(X2)
| ~ v1_group_1(X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_149,plain,
! [X0: $i] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f324]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f328]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r2_hidden(k1_funct_1(X0,X3),k9_relat_1(X0,X4))
| ( X2 = k1_xboole_0 )
| ~ v1_funct_1(X0)
| ~ r2_hidden(X3,X4)
| ~ r2_hidden(X3,X1)
| ~ m2_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f347]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] :
( r1_tarski(k1_setfam_1(X1),X0)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_157,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,[],[f332]) ).
tcf(c_158,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,[],[f333]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| m1_group_2(k5_group_2(X1),X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_206,plain,
( v3_struct_0(sK0)
| v1_group_1(k5_group_2(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_207,plain,
( v3_struct_0(sK0)
| v1_funct_1(k1_latsubgr(sK0))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_209,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_xboole_0(k1_group_3(sK0)) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_210,plain,
( v3_struct_0(sK0)
| m1_group_2(k5_group_2(sK0),sK0)
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_214,plain,
( v3_struct_0(sK0)
| m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_215,plain,
( v3_struct_0(sK0)
| v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_235,plain,
( v3_struct_0(sK0)
| ( k6_domain_1(u1_struct_0(sK0),k2_group_1(sK0)) = u1_struct_0(k5_group_2(sK0)) )
| ~ l1_group_1(sK0)
| ~ v4_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(k5_group_2(sK0))
| ~ m1_group_2(k5_group_2(sK0),sK0) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_248,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_79,c_101,c_100,c_99,c_79]) ).
tcf(c_249,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_248]) ).
tcf(c_250,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r1_group_2(X1,X0,X0)
| ~ m1_group_2(X0,X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_148,c_146]) ).
tcf(c_251,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| r1_group_2(X1,X0,X0)
| ~ v1_group_1(X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_250]) ).
tcf(c_254,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) = u1_struct_0(k5_group_2(X0)) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_82,c_93,c_94,c_82]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| ( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1) )
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_75,c_86,c_88,c_87,c_75]) ).
tcf(c_258,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| ( k1_funct_1(k1_latsubgr(X1),X0) = u1_struct_0(X0) )
| ~ v1_group_1(X0)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X0,X1) ),
inference(renaming,[status(thm)],[c_257]) ).
tcf(c_262,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(prop_impl_just,[status(thm)],[c_145]) ).
tcf(c_266,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_153]) ).
tcf(c_497,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k2_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X2))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(bin_hyper_res,[status(thm)],[c_89,c_262]) ).
tcf(c_499,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ~ v1_funct_2(X0,X1,X2) ),
inference(bin_hyper_res,[status(thm)],[c_138,c_262]) ).
tcf(c_501,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_157,c_266]) ).
tcf(c_502,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_158,c_266]) ).
tcf(c_1049,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v1_xboole_0(X1)
| ( k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) = u1_struct_0(k2_latsubgr(X0,X1)) )
| ~ l1_group_1(X0)
| ~ v4_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| ~ m1_group_2(k2_latsubgr(X0,X1),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_77,c_91]) ).
tcf(c_1107,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v1_xboole_0(X0)
| ( k6_setfam_1(u1_struct_0(X1),k2_funct_2(k1_group_3(X1),k1_zfmisc_1(u1_struct_0(X1)),k1_latsubgr(X1),X0)) = u1_struct_0(k2_latsubgr(X1,X0)) )
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(X1))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1049,c_92]) ).
tcf(c_2639,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ( k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) = u1_struct_0(k5_group_2(X0)) )
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_254]) ).
tcf(c_2640,plain,
( v3_struct_0(sK0)
| ( k6_domain_1(u1_struct_0(sK0),k2_group_1(sK0)) = u1_struct_0(k5_group_2(sK0)) )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_2639]) ).
tcf(c_2641,plain,
k6_domain_1(u1_struct_0(sK0),k2_group_1(sK0)) = u1_struct_0(k5_group_2(sK0)),
inference(global_subsumption_just,[status(thm)],[c_2640,c_56,c_55,c_54,c_53,c_206,c_210,c_235]) ).
tcf(c_2692,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ v1_xboole_0(k1_group_3(X0))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_114]) ).
tcf(c_2693,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_xboole_0(k1_group_3(sK0)) ),
inference(unflattening,[status(thm)],[c_2692]) ).
tcf(c_2694,plain,
~ v1_xboole_0(k1_group_3(sK0)),
inference(global_subsumption_just,[status(thm)],[c_2693,c_56,c_55,c_54,c_53,c_209]) ).
tcf(c_2699,plain,
! [X0: $i] :
( v3_struct_0(X0)
| m1_group_2(k5_group_2(X0),X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_94]) ).
tcf(c_2700,plain,
( v3_struct_0(sK0)
| m1_group_2(k5_group_2(sK0),sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_2699]) ).
tcf(c_2701,plain,
m1_group_2(k5_group_2(sK0),sK0),
inference(global_subsumption_just,[status(thm)],[c_2700,c_56,c_55,c_54,c_53,c_210]) ).
tcf(c_2706,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_group_1(k5_group_2(X0))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_93]) ).
tcf(c_2707,plain,
( v3_struct_0(sK0)
| v1_group_1(k5_group_2(sK0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_2706]) ).
tcf(c_2708,plain,
v1_group_1(k5_group_2(sK0)),
inference(global_subsumption_just,[status(thm)],[c_2707,c_56,c_55,c_54,c_53,c_206]) ).
tcf(c_2720,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_87]) ).
tcf(c_2721,plain,
( v3_struct_0(sK0)
| v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(unflattening,[status(thm)],[c_2720]) ).
tcf(c_2722,plain,
v1_funct_2(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))),
inference(global_subsumption_just,[status(thm)],[c_2721,c_56,c_55,c_54,c_53,c_215]) ).
tcf(c_2734,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| ( k5_group_2(X0) = X1 )
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 )
| ( k6_domain_1(u1_struct_0(X0),k2_group_1(X0)) != u1_struct_0(X1) ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_81]) ).
tcf(c_2735,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| ( k5_group_2(sK0) = X0 )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0)
| ( k6_domain_1(u1_struct_0(sK0),k2_group_1(sK0)) != u1_struct_0(X0) ) ),
inference(unflattening,[status(thm)],[c_2734]) ).
tcf(c_2737,plain,
! [X0: $i] :
( ( k6_domain_1(u1_struct_0(sK0),k2_group_1(sK0)) != u1_struct_0(X0) )
| ~ m1_group_2(X0,sK0)
| ~ v1_group_1(X0)
| ( k5_group_2(sK0) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_2735,c_56,c_54,c_53,c_2735]) ).
tcf(c_2738,plain,
! [X0: $i] :
( ( k5_group_2(sK0) = X0 )
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0)
| ( k6_domain_1(u1_struct_0(sK0),k2_group_1(sK0)) != u1_struct_0(X0) ) ),
inference(renaming,[status(thm)],[c_2737]) ).
tcf(c_2846,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v1_xboole_0(X1)
| ( k6_setfam_1(u1_struct_0(X0),k2_funct_2(k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_latsubgr(X0),X1)) = u1_struct_0(k2_latsubgr(X0,X1)) )
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_1107]) ).
tcf(c_2847,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v1_xboole_0(X0)
| ( k6_setfam_1(u1_struct_0(sK0),k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0)) = u1_struct_0(k2_latsubgr(sK0,X0)) )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(unflattening,[status(thm)],[c_2846]) ).
tcf(c_2849,plain,
! [X0: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0)))
| ( k6_setfam_1(u1_struct_0(sK0),k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0)) = u1_struct_0(k2_latsubgr(sK0,X0)) )
| v1_xboole_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_2847,c_56,c_54,c_53,c_2847]) ).
tcf(c_2850,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ( k6_setfam_1(u1_struct_0(sK0),k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0)) = u1_struct_0(k2_latsubgr(sK0,X0)) )
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(renaming,[status(thm)],[c_2849]) ).
tcf(c_2861,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| ( k1_funct_1(k1_latsubgr(X0),X1) = u1_struct_0(X1) )
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_258]) ).
tcf(c_2862,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| ( k1_funct_1(k1_latsubgr(sK0),X0) = u1_struct_0(X0) )
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_2861]) ).
tcf(c_2864,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| ~ v1_group_1(X0)
| ( k1_funct_1(k1_latsubgr(sK0),X0) = u1_struct_0(X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_2862,c_56,c_54,c_53,c_2862]) ).
tcf(c_2865,plain,
! [X0: $i] :
( ( k1_funct_1(k1_latsubgr(sK0),X0) = u1_struct_0(X0) )
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_2864]) ).
tcf(c_2876,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| m1_group_2(k5_group_2(X0),X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_160]) ).
tcf(c_2877,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| m1_group_2(k5_group_2(sK0),X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_2876]) ).
tcf(c_2878,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| m1_group_2(k5_group_2(sK0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_2877,c_56,c_54,c_53,c_2877]) ).
tcf(c_2879,plain,
! [X0: $i] :
( m1_group_2(k5_group_2(sK0),X0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_2878]) ).
tcf(c_2886,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| r1_group_2(X0,X1,X1)
| ~ v1_group_1(X1)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_group_2(X1,X0)
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_251]) ).
tcf(c_2887,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| r1_group_2(sK0,X0,X0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(unflattening,[status(thm)],[c_2886]) ).
tcf(c_2889,plain,
! [X0: $i] :
( ~ m1_group_2(X0,sK0)
| ~ v1_group_1(X0)
| r1_group_2(sK0,X0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2887,c_56,c_54,c_53,c_2887]) ).
tcf(c_2890,plain,
! [X0: $i] :
( r1_group_2(sK0,X0,X0)
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0) ),
inference(renaming,[status(thm)],[c_2889]) ).
tcf(c_2901,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v1_xboole_0(X1)
| m1_group_2(k2_latsubgr(X0,X1),X0)
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_92]) ).
tcf(c_2902,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v1_xboole_0(X0)
| m1_group_2(k2_latsubgr(sK0,X0),sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(unflattening,[status(thm)],[c_2901]) ).
tcf(c_2904,plain,
! [X0: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0)))
| m1_group_2(k2_latsubgr(sK0,X0),sK0)
| v1_xboole_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_2902,c_56,c_54,c_53,c_2902]) ).
tcf(c_2905,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| m1_group_2(k2_latsubgr(sK0,X0),sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(renaming,[status(thm)],[c_2904]) ).
tcf(c_2916,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v1_xboole_0(X1)
| v1_group_1(k2_latsubgr(X0,X1))
| ~ l1_group_1(X0)
| ~ v3_group_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(k1_group_3(X0)))
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_55,c_91]) ).
tcf(c_2917,plain,
! [X0: $i] :
( v3_struct_0(sK0)
| v1_xboole_0(X0)
| v1_group_1(k2_latsubgr(sK0,X0))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(unflattening,[status(thm)],[c_2916]) ).
tcf(c_2919,plain,
! [X0: $i] :
( ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0)))
| v1_group_1(k2_latsubgr(sK0,X0))
| v1_xboole_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_2917,c_56,c_54,c_53,c_2917]) ).
tcf(c_2920,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| v1_group_1(k2_latsubgr(sK0,X0))
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(renaming,[status(thm)],[c_2919]) ).
tcf(c_3319,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ( k1_latsubgr(sK0) != X0 )
| ( k1_group_3(sK0) != X1 )
| ( k1_zfmisc_1(u1_struct_0(sK0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_499,c_2722]) ).
tcf(c_3320,plain,
! [X0: $i] :
( ( k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0) = k9_relat_1(k1_latsubgr(sK0),X0) )
| ~ v1_funct_1(k1_latsubgr(sK0))
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(unflattening,[status(thm)],[c_3319]) ).
tcf(c_3340,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k2_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X2))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ( k1_latsubgr(sK0) != X0 )
| ( k1_group_3(sK0) != X1 )
| ( k1_zfmisc_1(u1_struct_0(sK0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_497,c_2722]) ).
tcf(c_3341,plain,
! [X0: $i] :
( m1_subset_1(k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0))))
| ~ v1_funct_1(k1_latsubgr(sK0))
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(unflattening,[status(thm)],[c_3340]) ).
tcf(c_3359,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r2_hidden(k1_funct_1(X0,X3),k9_relat_1(X0,X4))
| ( X2 = k1_xboole_0 )
| ~ v1_funct_1(X0)
| ~ r2_hidden(X3,X4)
| ~ r2_hidden(X3,X1)
| ~ m2_relset_1(X0,X1,X2)
| ( k1_latsubgr(sK0) != X0 )
| ( k1_group_3(sK0) != X1 )
| ( k1_zfmisc_1(u1_struct_0(sK0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_155,c_2722]) ).
tcf(c_3360,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ( k1_zfmisc_1(u1_struct_0(sK0)) = k1_xboole_0 )
| ~ v1_funct_1(k1_latsubgr(sK0))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,k1_group_3(sK0))
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(unflattening,[status(thm)],[c_3359]) ).
tcf(c_3361,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ( k1_zfmisc_1(u1_struct_0(sK0)) = k1_xboole_0 )
| ~ r2_hidden(X0,k1_group_3(sK0))
| ~ r2_hidden(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_3360,c_56,c_55,c_54,c_53,c_207,c_214,c_3360]) ).
tcf(c_3362,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ( k1_zfmisc_1(u1_struct_0(sK0)) = k1_xboole_0 )
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,k1_group_3(sK0)) ),
inference(renaming,[status(thm)],[c_3361]) ).
tcf(c_5574,plain,
! [X0: $i] :
( m1_group_2(k5_group_2(sK0),X0)
| ~ m1_group_2(X0,sK0) ),
inference(prop_impl_just,[status(thm)],[c_2879]) ).
tcf(c_6660,plain,
! [X0: $i] :
( ( k5_group_2(sK0) = X0 )
| ~ v1_group_1(X0)
| ~ m1_group_2(X0,sK0)
| ( u1_struct_0(k5_group_2(sK0)) != u1_struct_0(X0) ) ),
inference(light_normalisation,[status(thm)],[c_2738,c_2641]) ).
tcf(c_7291,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k2_funct_2(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ( k1_latsubgr(sK0) != X0 )
| ( k1_group_3(sK0) != X1 )
| ( k1_zfmisc_1(u1_struct_0(sK0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_499,c_2722]) ).
tcf(c_7292,plain,
! [X0: $i] :
( ( k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0) = k9_relat_1(k1_latsubgr(sK0),X0) )
| ~ v1_funct_1(k1_latsubgr(sK0))
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(unflattening,[status(thm)],[c_7291]) ).
tcf(c_7293,plain,
! [X0: $i] : k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0) = k9_relat_1(k1_latsubgr(sK0),X0),
inference(global_subsumption_just,[status(thm)],[c_7292,c_56,c_55,c_54,c_53,c_207,c_214,c_3320]) ).
tcf(c_7308,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k2_funct_2(X1,X2,X0,X3),k1_zfmisc_1(X2))
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,X1,X2)
| ( k1_latsubgr(sK0) != X0 )
| ( k1_group_3(sK0) != X1 )
| ( k1_zfmisc_1(u1_struct_0(sK0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_497,c_2722]) ).
tcf(c_7309,plain,
! [X0: $i] :
( m1_subset_1(k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0))))
| ~ v1_funct_1(k1_latsubgr(sK0))
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(unflattening,[status(thm)],[c_7308]) ).
tcf(c_7310,plain,
! [X0: $i] : m1_subset_1(k2_funct_2(k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0)),k1_latsubgr(sK0),X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0)))),
inference(global_subsumption_just,[status(thm)],[c_7309,c_56,c_55,c_54,c_53,c_207,c_214,c_3341]) ).
tcf(c_7322,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r2_hidden(k1_funct_1(X0,X3),k9_relat_1(X0,X4))
| ( X2 = k1_xboole_0 )
| ~ v1_funct_1(X0)
| ~ r2_hidden(X3,X4)
| ~ r2_hidden(X3,X1)
| ~ m2_relset_1(X0,X1,X2)
| ( k1_latsubgr(sK0) != X0 )
| ( k1_group_3(sK0) != X1 )
| ( k1_zfmisc_1(u1_struct_0(sK0)) != X2 ) ),
inference(resolution_lifted,[status(thm)],[c_155,c_2722]) ).
tcf(c_7323,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ( k1_zfmisc_1(u1_struct_0(sK0)) = k1_xboole_0 )
| ~ v1_funct_1(k1_latsubgr(sK0))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,k1_group_3(sK0))
| ~ m2_relset_1(k1_latsubgr(sK0),k1_group_3(sK0),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(unflattening,[status(thm)],[c_7322]) ).
tcf(c_7324,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ( k1_zfmisc_1(u1_struct_0(sK0)) = k1_xboole_0 )
| ~ r2_hidden(X0,k1_group_3(sK0))
| ~ r2_hidden(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_7323,c_3362]) ).
tcf(c_7325,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ( k1_zfmisc_1(u1_struct_0(sK0)) = k1_xboole_0 )
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,k1_group_3(sK0)) ),
inference(renaming,[status(thm)],[c_7324]) ).
tcf(c_8779,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X0)
| ~ v1_xboole_0(X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_11445,plain,
( v1_xboole_0(sK1)
| m1_group_2(k2_latsubgr(sK0,sK1),sK0)
| ~ m1_subset_1(sK1,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(instantiation,[status(thm)],[c_2905]) ).
tcf(c_11450,plain,
( r1_group_2(sK0,k5_group_2(sK0),k5_group_2(sK0))
| ~ v1_group_1(k5_group_2(sK0))
| ~ m1_group_2(k5_group_2(sK0),sK0) ),
inference(instantiation,[status(thm)],[c_2890]) ).
tcf(c_11523,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(k1_zfmisc_1(X0))
| ~ v1_xboole_0(X1)
| ( k1_zfmisc_1(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_8779]) ).
tcf(c_11690,plain,
! [X0: $i] :
( ~ v1_xboole_0(X0)
| ~ r1_tarski(sK1,X0)
| ~ r2_hidden(k5_group_2(sK0),sK1) ),
inference(instantiation,[status(thm)],[c_502]) ).
tcf(c_12295,plain,
( v3_struct_0(sK0)
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0)
| ~ v3_struct_0(k2_latsubgr(sK0,sK1))
| ~ m1_group_2(k2_latsubgr(sK0,sK1),sK0) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_12301,plain,
( m1_group_2(k5_group_2(sK0),k2_latsubgr(sK0,sK1))
| ~ m1_group_2(k2_latsubgr(sK0,sK1),sK0) ),
inference(instantiation,[status(thm)],[c_5574]) ).
tcf(c_12633,plain,
( v1_xboole_0(sK1)
| m1_group_2(k2_latsubgr(sK0,sK1),sK0) ),
inference(superposition,[status(thm)],[c_52,c_2905]) ).
tcf(c_12635,plain,
m1_group_2(k2_latsubgr(sK0,sK1),sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_12633,c_51]) ).
tcf(c_13287,plain,
( v3_struct_0(sK0)
| v3_group_1(k2_latsubgr(sK0,sK1))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_12635,c_100]) ).
tcf(c_13293,plain,
v3_group_1(k2_latsubgr(sK0,sK1)),
inference(forward_subsumption_resolution,[status(thm)],[c_13287,c_53,c_56,c_54]) ).
tcf(c_13632,plain,
( v3_struct_0(sK0)
| l1_group_1(k2_latsubgr(sK0,sK1))
| ~ l1_group_1(sK0)
| ~ v3_group_1(sK0) ),
inference(superposition,[status(thm)],[c_12635,c_101]) ).
tcf(c_13638,plain,
l1_group_1(k2_latsubgr(sK0,sK1)),
inference(forward_subsumption_resolution,[status(thm)],[c_13632,c_53,c_56,c_54]) ).
tcf(c_13756,plain,
! [X0: $i] :
( v1_xboole_0(k1_zfmisc_1(X0))
| ~ v1_xboole_0(k1_xboole_0)
| ( k1_zfmisc_1(X0) != k1_xboole_0 ) ),
inference(instantiation,[status(thm)],[c_11523]) ).
tcf(c_14166,plain,
! [X0: $i] : ~ v1_xboole_0(k1_zfmisc_1(u1_struct_0(X0))),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_14167,plain,
~ v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0))),
inference(instantiation,[status(thm)],[c_14166]) ).
tcf(c_17472,plain,
( v3_struct_0(k2_latsubgr(sK0,sK1))
| r1_tarski(u1_struct_0(k5_group_2(sK0)),u1_struct_0(k2_latsubgr(sK0,sK1)))
| ~ l1_group_1(k2_latsubgr(sK0,sK1))
| ~ v3_group_1(k2_latsubgr(sK0,sK1))
| ~ m1_group_2(k5_group_2(sK0),k2_latsubgr(sK0,sK1)) ),
inference(instantiation,[status(thm)],[c_249]) ).
tcf(c_24132,plain,
! [X0: $i] :
( m1_subset_1(k5_group_2(sK0),X0)
| ~ r1_tarski(sK1,X0) ),
inference(superposition,[status(thm)],[c_50,c_501]) ).
tcf(c_24335,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r2_hidden(k5_group_2(sK0),X0)
| ~ r1_tarski(sK1,X0) ),
inference(superposition,[status(thm)],[c_24132,c_152]) ).
tcf(c_24352,plain,
! [X0: $i] :
( ~ r1_tarski(sK1,X0)
| r2_hidden(k5_group_2(sK0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_24335,c_50,c_11690,c_24335]) ).
tcf(c_24353,plain,
! [X0: $i] :
( r2_hidden(k5_group_2(sK0),X0)
| ~ r1_tarski(sK1,X0) ),
inference(renaming,[status(thm)],[c_24352]) ).
tcf(c_25588,plain,
( v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_xboole_0(k1_xboole_0)
| ( k1_zfmisc_1(u1_struct_0(sK0)) != k1_xboole_0 ) ),
inference(instantiation,[status(thm)],[c_13756]) ).
tcf(c_56771,plain,
( v1_xboole_0(sK1)
| v1_group_1(k2_latsubgr(sK0,sK1)) ),
inference(superposition,[status(thm)],[c_52,c_2920]) ).
tcf(c_56773,plain,
v1_group_1(k2_latsubgr(sK0,sK1)),
inference(forward_subsumption_resolution,[status(thm)],[c_56771,c_51]) ).
tcf(c_56778,plain,
( v1_xboole_0(sK1)
| m1_group_2(k2_latsubgr(sK0,sK1),sK0) ),
inference(superposition,[status(thm)],[c_52,c_2905]) ).
tcf(c_56781,plain,
m1_group_2(k2_latsubgr(sK0,sK1),sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_56778,c_51]) ).
tcf(c_56792,plain,
( ( k1_funct_1(k1_latsubgr(sK0),k5_group_2(sK0)) = u1_struct_0(k5_group_2(sK0)) )
| ~ v1_group_1(k5_group_2(sK0)) ),
inference(superposition,[status(thm)],[c_2701,c_2865]) ).
tcf(c_56794,plain,
k1_funct_1(k1_latsubgr(sK0),k5_group_2(sK0)) = u1_struct_0(k5_group_2(sK0)),
inference(forward_subsumption_resolution,[status(thm)],[c_56792,c_2708]) ).
tcf(c_56834,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| ( k6_setfam_1(u1_struct_0(sK0),k9_relat_1(k1_latsubgr(sK0),X0)) = u1_struct_0(k2_latsubgr(sK0,X0)) )
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_group_3(sK0))) ),
inference(light_normalisation,[status(thm)],[c_2850,c_7293]) ).
tcf(c_56841,plain,
( v1_xboole_0(sK1)
| ( k6_setfam_1(u1_struct_0(sK0),k9_relat_1(k1_latsubgr(sK0),sK1)) = u1_struct_0(k2_latsubgr(sK0,sK1)) ) ),
inference(superposition,[status(thm)],[c_52,c_56834]) ).
tcf(c_56845,plain,
k6_setfam_1(u1_struct_0(sK0),k9_relat_1(k1_latsubgr(sK0),sK1)) = u1_struct_0(k2_latsubgr(sK0,sK1)),
inference(forward_subsumption_resolution,[status(thm)],[c_56841,c_51]) ).
tcf(c_56921,plain,
! [X0: $i] : m1_subset_1(k9_relat_1(k1_latsubgr(sK0),X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0)))),
inference(light_normalisation,[status(thm)],[c_7310,c_7293]) ).
tcf(c_56935,plain,
r1_tarski(sK1,k1_group_3(sK0)),
inference(superposition,[status(thm)],[c_52,c_154]) ).
tcf(c_57043,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ~ r2_hidden(X0,k1_group_3(sK0))
| ~ r2_hidden(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_7325,c_117,c_3362,c_14167,c_25588]) ).
tcf(c_57044,plain,
! [X0: $i,X1: $i] :
( r2_hidden(k1_funct_1(k1_latsubgr(sK0),X0),k9_relat_1(k1_latsubgr(sK0),X1))
| ~ r2_hidden(X0,X1)
| ~ r2_hidden(X0,k1_group_3(sK0)) ),
inference(renaming,[status(thm)],[c_57043]) ).
tcf(c_57048,plain,
! [X0: $i] :
( r2_hidden(u1_struct_0(k5_group_2(sK0)),k9_relat_1(k1_latsubgr(sK0),X0))
| ~ r2_hidden(k5_group_2(sK0),X0)
| ~ r2_hidden(k5_group_2(sK0),k1_group_3(sK0)) ),
inference(superposition,[status(thm)],[c_56794,c_57044]) ).
tcf(c_57318,plain,
! [X0: $i] : k6_setfam_1(u1_struct_0(sK0),k9_relat_1(k1_latsubgr(sK0),X0)) = k1_setfam_1(k9_relat_1(k1_latsubgr(sK0),X0)),
inference(superposition,[status(thm)],[c_56921,c_140]) ).
tcf(c_58951,plain,
! [X0: $i] :
( m1_subset_1(k5_group_2(sK0),X0)
| ~ r1_tarski(sK1,X0) ),
inference(superposition,[status(thm)],[c_50,c_501]) ).
tcf(c_58987,plain,
! [X0: $i] :
( v1_xboole_0(X0)
| r2_hidden(k5_group_2(sK0),X0)
| ~ r1_tarski(sK1,X0) ),
inference(superposition,[status(thm)],[c_58951,c_152]) ).
tcf(c_59004,plain,
! [X0: $i] :
( ~ r1_tarski(sK1,X0)
| r2_hidden(k5_group_2(sK0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_58987,c_24353]) ).
tcf(c_59005,plain,
! [X0: $i] :
( r2_hidden(k5_group_2(sK0),X0)
| ~ r1_tarski(sK1,X0) ),
inference(renaming,[status(thm)],[c_59004]) ).
tcf(c_59009,plain,
! [X0: $i,X1: $i] :
( m1_subset_1(k5_group_2(sK0),X1)
| ~ r1_tarski(sK1,X0)
| ~ r1_tarski(X0,X1) ),
inference(superposition,[status(thm)],[c_59005,c_501]) ).
tcf(c_60934,plain,
( m1_subset_1(k5_group_2(sK0),k1_group_3(sK0))
| ~ r1_tarski(sK1,sK1) ),
inference(superposition,[status(thm)],[c_56935,c_59009]) ).
tcf(c_60975,plain,
m1_subset_1(k5_group_2(sK0),k1_group_3(sK0)),
inference(forward_subsumption_resolution,[status(thm)],[c_60934,c_149]) ).
tcf(c_60988,plain,
( v1_xboole_0(k1_group_3(sK0))
| r2_hidden(k5_group_2(sK0),k1_group_3(sK0)) ),
inference(superposition,[status(thm)],[c_60975,c_152]) ).
tcf(c_60990,plain,
r2_hidden(k5_group_2(sK0),k1_group_3(sK0)),
inference(forward_subsumption_resolution,[status(thm)],[c_60988,c_2694]) ).
tcf(c_60992,plain,
! [X0: $i] :
( r2_hidden(u1_struct_0(k5_group_2(sK0)),k9_relat_1(k1_latsubgr(sK0),X0))
| ~ r2_hidden(k5_group_2(sK0),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_57048,c_60990]) ).
tcf(c_65263,plain,
k1_setfam_1(k9_relat_1(k1_latsubgr(sK0),sK1)) = u1_struct_0(k2_latsubgr(sK0,sK1)),
inference(demodulation,[status(thm)],[c_56845,c_57318]) ).
tcf(c_65279,plain,
! [X0: $i] :
( r1_tarski(u1_struct_0(k2_latsubgr(sK0,sK1)),X0)
| ~ r2_hidden(X0,k9_relat_1(k1_latsubgr(sK0),sK1)) ),
inference(superposition,[status(thm)],[c_65263,c_156]) ).
tcf(c_83003,plain,
( r1_tarski(u1_struct_0(k2_latsubgr(sK0,sK1)),u1_struct_0(k5_group_2(sK0)))
| ~ r2_hidden(k5_group_2(sK0),sK1) ),
inference(superposition,[status(thm)],[c_60992,c_65279]) ).
tcf(c_83004,plain,
r1_tarski(u1_struct_0(k2_latsubgr(sK0,sK1)),u1_struct_0(k5_group_2(sK0))),
inference(forward_subsumption_resolution,[status(thm)],[c_83003,c_50]) ).
tcf(c_83225,plain,
( ( u1_struct_0(k2_latsubgr(sK0,sK1)) = u1_struct_0(k5_group_2(sK0)) )
| ~ r1_tarski(u1_struct_0(k5_group_2(sK0)),u1_struct_0(k2_latsubgr(sK0,sK1))) ),
inference(superposition,[status(thm)],[c_83004,c_63]) ).
tcf(c_83332,plain,
u1_struct_0(k2_latsubgr(sK0,sK1)) = u1_struct_0(k5_group_2(sK0)),
inference(global_subsumption_just,[status(thm)],[c_83225,c_56,c_54,c_53,c_51,c_52,c_11445,c_12295,c_12301,c_13293,c_13638,c_17472,c_83225]) ).
tcf(c_83378,plain,
( ( k2_latsubgr(sK0,sK1) = k5_group_2(sK0) )
| ~ v1_group_1(k2_latsubgr(sK0,sK1))
| ~ m1_group_2(k2_latsubgr(sK0,sK1),sK0) ),
inference(superposition,[status(thm)],[c_83332,c_6660]) ).
tcf(c_83383,plain,
k2_latsubgr(sK0,sK1) = k5_group_2(sK0),
inference(forward_subsumption_resolution,[status(thm)],[c_83378,c_56773,c_56781]) ).
tcf(c_83792,plain,
~ r1_group_2(sK0,k5_group_2(sK0),k5_group_2(sK0)),
inference(demodulation,[status(thm)],[c_49,c_83383]) ).
tcf(c_83793,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_83792,c_11450,c_210,c_206,c_53,c_54,c_55,c_56]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP646+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.15/0.39 % Computer : n010.cluster.edu
% 0.15/0.39 % Model : x86_64 x86_64
% 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.39 % Memory : 8046.5625MB
% 0.15/0.39 % OS : Linux 6.8.0-71-generic
% 0.15/0.39 % CPULimit : 300
% 0.15/0.39 % WCLimit : 300
% 0.15/0.39 % DateTime : Wed Sep 23 15:26:28 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/0.44 Running first-order theorem proving
% 0.17/0.44 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.17/0.46
% 0.17/0.46 % ======== iProver multi-core TPTP/SMT =========
% 0.17/0.46
% 0.17/0.46 % Detected problem language: tptp
% 0.17/0.48 % Proving...
% 94.65/15.08 % SZS status Started for theBenchmark.p
% 94.65/15.08 % SZS status Theorem for theBenchmark.p
% 94.65/15.08
% 94.65/15.08 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 94.65/15.08
% 94.65/15.08 % ------ iProver source info
% 94.65/15.08
% 94.65/15.08 % git: date: 2026-07-19 20:42:38 +0200
% 94.65/15.08 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 94.65/15.08 % git: non_committed_changes: false
% 94.65/15.08
% 94.65/15.08 % ------ Parsing...
% 94.65/15.08 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 94.65/15.08
% 94.65/15.08 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe_e sup_sim: 1 sf_s rm: 4 0s sf_e pe_s pe:1:0s pe:2:0s pe_e %
% 94.65/15.08
% 94.65/15.08 % ------ Preprocessing... gs_s sp: 8 0s gs_e snvd_s sp: 0 0s snvd_e %
% 94.65/15.08
% 94.65/15.08 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 94.65/15.08 % ------ Proving...
% 94.65/15.08 % ------ Problem Properties
% 94.65/15.08
% 94.65/15.08 %
% 94.65/15.08 % clauses 137
% 94.65/15.08 % conjectures 7
% 94.65/15.08 % EPR 26
% 94.65/15.08 % Horn 102
% 94.65/15.08 % unary 37
% 94.65/15.08 % binary 30
% 94.65/15.08 % lits 353
% 94.65/15.08 % lits eq 87
% 94.65/15.08 % fd_pure 0
% 94.65/15.08 % fd_pseudo 0
% 94.65/15.08 % fd_cond 8
% 94.65/15.08 % fd_pseudo_cond 8
% 94.65/15.08 % AC symbols 0
% 94.65/15.08
% 94.65/15.08 % ------ Input Options Time Limit: Unbounded
% 94.65/15.08
% 94.65/15.08
% 94.65/15.08 % ------
% 94.65/15.08 % Current options:
% 94.65/15.08 % ------
% 94.65/15.08
% 94.65/15.08
% 94.65/15.08 %
% 94.65/15.08
% 94.65/15.08 % ------ Proving...
% 94.65/15.08 %
% 94.65/15.08
% 94.65/15.08 % SZS status Theorem for theBenchmark.p
% 94.65/15.08
% 94.65/15.08 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 94.65/15.10
% 94.65/15.10
%------------------------------------------------------------------------------