%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT378+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 : n014.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:59:44 PM UTC 2026
% Result : Theorem 8.17s 1.63s
% Output : CNFRefutation 8.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 199 ( 47 unt; 0 def)
% Number of atoms : 1101 ( 37 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 1582 ( 680 ~; 756 |; 110 &)
% ( 4 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-5 aty)
% Number of variables : 374 ( 0 sgn 362 !; 12 ?; 164 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( l1_orders_2(X2)
& ~ v3_struct_0(X2) )
=> ! [X3] :
( ( m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X3) )
=> ! [X4] :
( ( m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_1(X4) )
=> ( ( v4_waybel34(X4,X1,X2)
& v4_waybel34(X3,X0,X1) )
=> v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t63_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( l1_orders_2(X2)
& ~ v3_struct_0(X2) )
=> ! [X3] :
( ( m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X3) )
=> ! [X4] :
( ( m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_1(X4) )
=> ( ( v4_waybel34(X4,X1,X2)
& v4_waybel34(X3,X0,X1) )
=> v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f17,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(f24,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(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) )
=> ( v4_waybel34(X2,X0,X1)
<=> ! [X3] :
( ( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v1_finset_1(X3) )
=> r4_waybel_0(X0,X1,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d15_waybel34) ).
fof(f28,axiom,
! [X0,X1,X2,X3] :
( ( m1_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)
& l1_struct_0(X1)
& l1_struct_0(X0) )
=> m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_pre_topc) ).
fof(f30,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_relset_1(X4,X1,X2)
& v1_funct_2(X4,X1,X2)
& v1_funct_1(X4)
& m1_relset_1(X3,X0,X1)
& v1_funct_2(X3,X0,X1)
& v1_funct_1(X3)
& ~ v1_xboole_0(X1) )
=> ( m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_funct_2) ).
fof(f32,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f36,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(f43,axiom,
! [X0,X1] :
( ( v1_finset_1(X1)
& v1_funct_1(X0)
& v1_relat_1(X0) )
=> v1_finset_1(k9_relat_1(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc13_finset_1) ).
fof(f46,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(f58,axiom,
! [X0,X1,X2,X3] :
( ( m1_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)
& l1_struct_0(X1)
& l1_struct_0(X0) )
=> k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_pre_topc) ).
fof(f59,axiom,
! [X0,X1,X2,X3,X4] :
( ( m1_relset_1(X4,X1,X2)
& v1_funct_2(X4,X1,X2)
& v1_funct_1(X4)
& m1_relset_1(X3,X0,X1)
& v1_funct_2(X3,X0,X1)
& v1_funct_1(X3)
& ~ v1_xboole_0(X1) )
=> k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k7_funct_2) ).
fof(f60,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(f67,axiom,
! [X0] :
( ( l1_orders_2(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( l1_orders_2(X1)
& ~ v3_struct_0(X1) )
=> ! [X2] :
( ( l1_orders_2(X2)
& ~ v3_struct_0(X2) )
=> ! [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
=> ! [X4] :
( ( m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X4) )
=> ! [X5] :
( ( m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_1(X5) )
=> ( ( r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
& r4_waybel_0(X0,X1,X4,X3) )
=> r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_waybel34) ).
fof(f90,plain,
? [X0] :
( l1_orders_2(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_orders_2(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( l1_orders_2(X2)
& ~ v3_struct_0(X2)
& ? [X3] :
( m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X3)
& ? [X4] :
( m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_1(X4)
& v4_waybel34(X4,X1,X2)
& v4_waybel34(X3,X0,X1)
& ~ v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2) ) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f91,plain,
? [X0] :
( l1_orders_2(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( l1_orders_2(X1)
& ~ v3_struct_0(X1)
& ? [X2] :
( l1_orders_2(X2)
& ~ v3_struct_0(X2)
& ? [X3] :
( m2_relset_1(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_2(X3,u1_struct_0(X0),u1_struct_0(X1))
& v1_funct_1(X3)
& ? [X4] :
( m2_relset_1(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_2(X4,u1_struct_0(X1),u1_struct_0(X2))
& v1_funct_1(X4)
& v4_waybel34(X4,X1,X2)
& v4_waybel34(X3,X0,X1)
& ~ v4_waybel34(k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X3,X4),X0,X2) ) ) ) ) ),
inference(flattening,[],[f90]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f109,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(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)
| ( v4_waybel34(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_finset_1(X3)
| r4_waybel_0(X0,X1,X2,X3) ) ) ) ) ),
inference(ennf_transformation,[],[f24]) ).
fof(f110,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(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)
| ( v4_waybel34(X2,X0,X1)
<=> ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_finset_1(X3)
| r4_waybel_0(X0,X1,X2,X3) ) ) ) ) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
! [X0,X1,X2,X3] :
( ~ m1_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)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(ennf_transformation,[],[f28]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( ~ m1_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)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(flattening,[],[f111]) ).
fof(f115,plain,
! [X0,X1,X2,X3,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| ( m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4)) ) ),
inference(ennf_transformation,[],[f30]) ).
fof(f116,plain,
! [X0,X1,X2,X3,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| ( m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2)
& v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4)) ) ),
inference(flattening,[],[f115]) ).
fof(f117,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f118,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,[],[f36]) ).
fof(f119,plain,
! [X0,X1] :
( ~ v1_finset_1(X1)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| v1_finset_1(k9_relat_1(X0,X1)) ),
inference(ennf_transformation,[],[f43]) ).
fof(f120,plain,
! [X0,X1] :
( ~ v1_finset_1(X1)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| v1_finset_1(k9_relat_1(X0,X1)) ),
inference(flattening,[],[f119]) ).
fof(f125,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f46]) ).
fof(f126,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(flattening,[],[f125]) ).
fof(f133,plain,
! [X0,X1,X2,X3] :
( ~ m1_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)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(ennf_transformation,[],[f58]) ).
fof(f134,plain,
! [X0,X1,X2,X3] :
( ~ m1_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)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(flattening,[],[f133]) ).
fof(f135,plain,
! [X0,X1,X2,X3,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
inference(ennf_transformation,[],[f59]) ).
fof(f136,plain,
! [X0,X1,X2,X3,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
inference(flattening,[],[f135]) ).
fof(f144,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ l1_orders_2(X2)
| v3_struct_0(X2)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ! [X4] :
( ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ! [X5] :
( ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X5)
| ~ r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
| ~ r4_waybel_0(X0,X1,X4,X3)
| r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3) ) ) ) ) ) ),
inference(ennf_transformation,[],[f67]) ).
fof(f145,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ! [X2] :
( ~ l1_orders_2(X2)
| v3_struct_0(X2)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ! [X4] :
( ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ! [X5] :
( ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X5)
| ~ r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
| ~ r4_waybel_0(X0,X1,X4,X3)
| r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3) ) ) ) ) ) ),
inference(flattening,[],[f144]) ).
fof(f149,plain,
( l1_orders_2(sK0)
& ~ v3_struct_0(sK0)
& l1_orders_2(sK1)
& ~ v3_struct_0(sK1)
& l1_orders_2(sK2)
& ~ v3_struct_0(sK2)
& m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
& v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
& v1_funct_1(sK3)
& m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
& v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
& v1_funct_1(sK4)
& v4_waybel34(sK4,sK1,sK2)
& v4_waybel34(sK3,sK0,sK1)
& ~ v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),sK0,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4)],[f91]) ).
fof(f150,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(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)
| ( ( ~ v4_waybel34(X2,X0,X1)
| ! [X3] :
( ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_finset_1(X3)
| r4_waybel_0(X0,X1,X2,X3) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v1_finset_1(X3)
& ~ r4_waybel_0(X0,X1,X2,X3) )
| v4_waybel34(X2,X0,X1) ) ) ) ) ),
inference(nnf_transformation,[],[f110]) ).
fof(f151,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(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)
| ( ( ~ v4_waybel34(X2,X0,X1)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_finset_1(X4)
| r4_waybel_0(X0,X1,X2,X4) ) )
& ( ? [X3] :
( m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
& v1_finset_1(X3)
& ~ r4_waybel_0(X0,X1,X2,X3) )
| v4_waybel34(X2,X0,X1) ) ) ) ) ),
inference(rectify,[],[f150]) ).
fof(f152,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ l1_orders_2(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)
| ( ( ~ v4_waybel34(X2,X0,X1)
| ! [X4] :
( ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_finset_1(X4)
| r4_waybel_0(X0,X1,X2,X4) ) )
& ( ( m1_subset_1(sK5(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
& v1_finset_1(sK5(X0,X1,X2))
& ~ r4_waybel_0(X0,X1,X2,sK5(X0,X1,X2)) )
| v4_waybel34(X2,X0,X1) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X3,sK5(X0,X1,X2))],[f151]) ).
fof(f167,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,[],[f60]) ).
fof(f168,plain,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f149]) ).
fof(f169,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f149]) ).
fof(f170,plain,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f149]) ).
fof(f171,plain,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f149]) ).
fof(f172,plain,
l1_orders_2(sK2),
inference(cnf_transformation,[],[f149]) ).
fof(f173,plain,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f149]) ).
fof(f174,plain,
m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f149]) ).
fof(f175,plain,
v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f149]) ).
fof(f176,plain,
v1_funct_1(sK3),
inference(cnf_transformation,[],[f149]) ).
fof(f177,plain,
m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(cnf_transformation,[],[f149]) ).
fof(f178,plain,
v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(cnf_transformation,[],[f149]) ).
fof(f179,plain,
v1_funct_1(sK4),
inference(cnf_transformation,[],[f149]) ).
fof(f180,plain,
v4_waybel34(sK4,sK1,sK2),
inference(cnf_transformation,[],[f149]) ).
fof(f181,plain,
v4_waybel34(sK3,sK0,sK1),
inference(cnf_transformation,[],[f149]) ).
fof(f182,plain,
~ v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),sK0,sK2),
inference(cnf_transformation,[],[f149]) ).
fof(f202,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(k2_zfmisc_1(X0,X1)))
| v1_relat_1(X2) ),
inference(cnf_transformation,[],[f101]) ).
fof(f214,plain,
! [X2,X0,X1,X4] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ 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)
| ~ v4_waybel34(X2,X0,X1)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X0)))
| ~ v1_finset_1(X4)
| r4_waybel_0(X0,X1,X2,X4) ),
inference(cnf_transformation,[],[f152]) ).
fof(f215,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ 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)
| m1_subset_1(sK5(X0,X1,X2),k1_zfmisc_1(u1_struct_0(X0)))
| v4_waybel34(X2,X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f216,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ 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)
| v1_finset_1(sK5(X0,X1,X2))
| v4_waybel34(X2,X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f217,plain,
! [X2,X0,X1] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ 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)
| ~ r4_waybel_0(X0,X1,X2,sK5(X0,X1,X2))
| v4_waybel34(X2,X0,X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f218,plain,
! [X2,X3,X0,X1] :
( ~ m1_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)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| m1_subset_1(k4_pre_topc(X0,X1,X2,X3),k1_zfmisc_1(u1_struct_0(X1))) ),
inference(cnf_transformation,[],[f112]) ).
fof(f220,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| m2_relset_1(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f221,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| v1_funct_2(k7_funct_2(X0,X1,X2,X3,X4),X0,X2) ),
inference(cnf_transformation,[],[f116]) ).
fof(f222,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| v1_funct_1(k7_funct_2(X0,X1,X2,X3,X4)) ),
inference(cnf_transformation,[],[f116]) ).
fof(f223,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f224,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,[],[f118]) ).
fof(f230,plain,
! [X0,X1] :
( ~ v1_finset_1(X1)
| ~ v1_funct_1(X0)
| ~ v1_relat_1(X0)
| v1_finset_1(k9_relat_1(X0,X1)) ),
inference(cnf_transformation,[],[f120]) ).
fof(f234,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f126]) ).
fof(f267,plain,
! [X2,X3,X0,X1] :
( ~ m1_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)
| ~ l1_struct_0(X1)
| ~ l1_struct_0(X0)
| k4_pre_topc(X0,X1,X2,X3) = k9_relat_1(X2,X3) ),
inference(cnf_transformation,[],[f134]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_relset_1(X4,X1,X2)
| ~ v1_funct_2(X4,X1,X2)
| ~ v1_funct_1(X4)
| ~ m1_relset_1(X3,X0,X1)
| ~ v1_funct_2(X3,X0,X1)
| ~ v1_funct_1(X3)
| v1_xboole_0(X1)
| k7_funct_2(X0,X1,X2,X3,X4) = k5_relat_1(X3,X4) ),
inference(cnf_transformation,[],[f136]) ).
fof(f269,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f270,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,X0,X1)
| m2_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f277,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X2)
| v3_struct_0(X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_relset_1(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X5,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_1(X5)
| ~ r4_waybel_0(X1,X2,X5,k4_pre_topc(X0,X1,X4,X3))
| ~ r4_waybel_0(X0,X1,X4,X3)
| r4_waybel_0(X0,X2,k7_funct_2(u1_struct_0(X0),u1_struct_0(X1),u1_struct_0(X2),X4,X5),X3) ),
inference(cnf_transformation,[],[f145]) ).
tcf(c_49,negated_conjecture,
~ v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),sK0,sK2),
inference(cnf_transformation,[],[f182]) ).
tcf(c_50,negated_conjecture,
v4_waybel34(sK3,sK0,sK1),
inference(cnf_transformation,[],[f181]) ).
tcf(c_51,negated_conjecture,
v4_waybel34(sK4,sK1,sK2),
inference(cnf_transformation,[],[f180]) ).
tcf(c_52,negated_conjecture,
v1_funct_1(sK4),
inference(cnf_transformation,[],[f179]) ).
tcf(c_53,negated_conjecture,
v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(cnf_transformation,[],[f178]) ).
tcf(c_54,negated_conjecture,
m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(cnf_transformation,[],[f177]) ).
tcf(c_55,negated_conjecture,
v1_funct_1(sK3),
inference(cnf_transformation,[],[f176]) ).
tcf(c_56,negated_conjecture,
v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f175]) ).
tcf(c_57,negated_conjecture,
m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(cnf_transformation,[],[f174]) ).
tcf(c_58,negated_conjecture,
~ v3_struct_0(sK2),
inference(cnf_transformation,[],[f173]) ).
tcf(c_59,negated_conjecture,
l1_orders_2(sK2),
inference(cnf_transformation,[],[f172]) ).
tcf(c_60,negated_conjecture,
~ v3_struct_0(sK1),
inference(cnf_transformation,[],[f171]) ).
tcf(c_61,negated_conjecture,
l1_orders_2(sK1),
inference(cnf_transformation,[],[f170]) ).
tcf(c_62,negated_conjecture,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f169]) ).
tcf(c_63,negated_conjecture,
l1_orders_2(sK0),
inference(cnf_transformation,[],[f168]) ).
tcf(c_83,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,[],[f202]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| v4_waybel34(X2,X0,X1)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(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))
| ~ r4_waybel_0(X0,X1,X2,sK5(X0,X1,X2)) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v4_waybel34(X0,X1,X2)
| v1_finset_1(sK5(X1,X2,X0))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v4_waybel34(X0,X1,X2)
| m1_subset_1(sK5(X1,X2,X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| r4_waybel_0(X1,X2,X0,X3)
| ~ v1_finset_1(X3)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v4_waybel34(X0,X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m1_subset_1(k4_pre_topc(X1,X2,X0,X3),k1_zfmisc_1(u1_struct_0(X2)))
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(X1)
| v1_funct_1(k7_funct_2(X4,X1,X2,X3,X0))
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X3,X4,X1)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X3,X4,X1)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(X1)
| v1_funct_2(k7_funct_2(X4,X1,X2,X3,X0),X4,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X3,X4,X1)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X3,X4,X1)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(X1)
| m2_relset_1(k7_funct_2(X4,X1,X2,X3,X0),X4,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X3,X4,X1)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X3,X4,X1)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_102,plain,
! [X0: $i] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_103,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,[],[f224]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i] :
( v1_finset_1(k9_relat_1(X0,X1))
| ~ v1_relat_1(X0)
| ~ v1_finset_1(X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_113,plain,
! [X0: $i] :
( v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( k4_pre_topc(X1,X2,X0,X3) = k9_relat_1(X0,X3) )
| ~ l1_struct_0(X2)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2)) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( v1_xboole_0(X1)
| ( k7_funct_2(X4,X1,X2,X3,X0) = k5_relat_1(X3,X0) )
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X3,X4,X1)
| ~ m1_relset_1(X0,X1,X2)
| ~ v1_funct_2(X3,X4,X1)
| ~ v1_funct_2(X0,X1,X2) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i,X2: $i] :
( m2_relset_1(X0,X1,X2)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( v3_struct_0(X3)
| v3_struct_0(X1)
| v3_struct_0(X0)
| r4_waybel_0(X3,X1,k7_funct_2(u1_struct_0(X3),u1_struct_0(X0),u1_struct_0(X1),X4,X2),X5)
| ~ l1_orders_2(X3)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X3)))
| ~ r4_waybel_0(X3,X0,X4,X5)
| ~ m2_relset_1(X4,u1_struct_0(X3),u1_struct_0(X0))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X4,u1_struct_0(X3),u1_struct_0(X0))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ r4_waybel_0(X0,X1,X2,k4_pre_topc(X3,X0,X4,X5)) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_164,plain,
( l1_struct_0(sK1)
| ~ l1_orders_2(sK1) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_191,plain,
( v3_struct_0(sK1)
| ~ l1_struct_0(sK1)
| ~ v1_xboole_0(u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m1_relset_1(X0,X1,X2)
| m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(prop_impl_just,[status(thm)],[c_148,c_103]) ).
tcf(c_277,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(renaming,[status(thm)],[c_276]) ).
tcf(c_1192,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| m1_subset_1(sK5(X1,X2,X0),k1_zfmisc_1(u1_struct_0(X1)))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ( X2 != sK2 )
| ( X1 != sK0 )
| ( k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_95]) ).
tcf(c_1193,plain,
( v3_struct_0(sK2)
| v3_struct_0(sK0)
| m1_subset_1(sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l1_orders_2(sK2)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(unflattening,[status(thm)],[c_1192]) ).
tcf(c_1194,plain,
( m1_subset_1(sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_1193,c_63,c_59,c_62,c_58,c_1193]) ).
tcf(c_1208,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X2)
| v3_struct_0(X1)
| v1_finset_1(sK5(X1,X2,X0))
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ m2_relset_1(X0,u1_struct_0(X1),u1_struct_0(X2))
| ~ v1_funct_2(X0,u1_struct_0(X1),u1_struct_0(X2))
| ( X2 != sK2 )
| ( X1 != sK0 )
| ( k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_94]) ).
tcf(c_1209,plain,
( v3_struct_0(sK2)
| v3_struct_0(sK0)
| v1_finset_1(sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)))
| ~ l1_orders_2(sK2)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(unflattening,[status(thm)],[c_1208]) ).
tcf(c_1210,plain,
( v1_finset_1(sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(global_subsumption_just,[status(thm)],[c_1209,c_63,c_59,c_62,c_58,c_1209]) ).
tcf(c_1224,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r4_waybel_0(X0,X1,X2,X3)
| ~ v1_finset_1(X3)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ( X2 != sK3 )
| ( X1 != sK1 )
| ( X0 != sK0 ) ),
inference(resolution_lifted,[status(thm)],[c_50,c_96]) ).
tcf(c_1225,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| v3_struct_0(sK0)
| r4_waybel_0(sK0,sK1,sK3,X0)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(sK3)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(unflattening,[status(thm)],[c_1224]) ).
tcf(c_1227,plain,
! [X0: $i] :
( r4_waybel_0(sK0,sK1,sK3,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_finset_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_1225,c_63,c_61,c_55,c_62,c_60,c_57,c_56,c_1225]) ).
tcf(c_1228,plain,
! [X0: $i] :
( r4_waybel_0(sK0,sK1,sK3,X0)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(renaming,[status(thm)],[c_1227]) ).
tcf(c_1239,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v3_struct_0(X1)
| v3_struct_0(X0)
| r4_waybel_0(X0,X1,X2,X3)
| ~ v1_finset_1(X3)
| ~ l1_orders_2(X1)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ( X2 != sK4 )
| ( X1 != sK2 )
| ( X0 != sK1 ) ),
inference(resolution_lifted,[status(thm)],[c_51,c_96]) ).
tcf(c_1240,plain,
! [X0: $i] :
( v3_struct_0(sK2)
| v3_struct_0(sK1)
| r4_waybel_0(sK1,sK2,sK4,X0)
| ~ l1_orders_2(sK2)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK4)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(unflattening,[status(thm)],[c_1239]) ).
tcf(c_1242,plain,
! [X0: $i] :
( r4_waybel_0(sK1,sK2,sK4,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_finset_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_1240,c_61,c_59,c_52,c_60,c_58,c_54,c_53,c_1240]) ).
tcf(c_1243,plain,
! [X0: $i] :
( r4_waybel_0(sK1,sK2,sK4,X0)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(renaming,[status(thm)],[c_1242]) ).
tcf(c_1348,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ m1_relset_1(X0,X1,X2)
| m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
inference(prop_impl_just,[status(thm)],[c_277]) ).
tcf(c_1349,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(renaming,[status(thm)],[c_1348]) ).
tcf(c_3875,plain,
( m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_3876,plain,
( m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_3955,plain,
l1_struct_0(sK0),
inference(superposition,[status(thm)],[c_63,c_102]) ).
tcf(c_4047,plain,
m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(superposition,[status(thm)],[c_57,c_149]) ).
tcf(c_4186,plain,
! [X0: $i,X1: $i,X2: $i] :
( v1_relat_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_1349,c_83]) ).
tcf(c_4203,plain,
v1_relat_1(sK3),
inference(superposition,[status(thm)],[c_4047,c_4186]) ).
tcf(c_4329,plain,
! [X0: $i] :
( ( k4_pre_topc(sK0,sK1,sK3,X0) = k9_relat_1(sK3,X0) )
| ~ l1_struct_0(sK1)
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_146]) ).
tcf(c_4336,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(u1_struct_0(sK1))
| m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),X1,sK3,X0),u1_struct_0(sK0),X1)
| ~ v1_funct_1(sK3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(sK1),X1)
| ~ v1_funct_2(X0,u1_struct_0(sK1),X1)
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_4337,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),X1,sK3,X0),u1_struct_0(sK0),X1)
| ~ v1_funct_1(sK3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(sK1),X1)
| ~ v1_funct_2(X0,u1_struct_0(sK1),X1)
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_4338,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),X1,sK3,X0))
| ~ v1_funct_1(sK3)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,u1_struct_0(sK1),X1)
| ~ v1_funct_2(X0,u1_struct_0(sK1),X1)
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_4620,plain,
m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(superposition,[status(thm)],[c_54,c_149]) ).
tcf(c_4621,plain,
m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(superposition,[status(thm)],[c_57,c_149]) ).
tcf(c_4701,plain,
! [X0: $i] :
( ( k4_pre_topc(sK0,sK1,sK3,X0) = k9_relat_1(sK3,X0) )
| ~ l1_struct_0(sK1)
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK3)
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4621,c_146]) ).
tcf(c_4732,plain,
! [X0: $i] : k4_pre_topc(sK0,sK1,sK3,X0) = k9_relat_1(sK3,X0),
inference(global_subsumption_just,[status(thm)],[c_4701,c_61,c_55,c_164,c_57,c_56,c_3876,c_3955,c_4329]) ).
tcf(c_4735,plain,
! [X0: $i] :
( m1_subset_1(k9_relat_1(sK3,X0),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_struct_0(sK1)
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4732,c_97]) ).
tcf(c_4802,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(u1_struct_0(sK1))
| ( k7_funct_2(X1,u1_struct_0(sK1),u1_struct_0(sK2),X0,sK4) = k5_relat_1(X0,sK4) )
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(superposition,[status(thm)],[c_4620,c_147]) ).
tcf(c_4843,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| v3_struct_0(sK0)
| r4_waybel_0(sK0,sK1,sK3,X0)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(sK3)
| ~ v1_finset_1(X0)
| ~ v4_waybel34(sK3,sK0,sK1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_56,c_96]) ).
tcf(c_5021,plain,
! [X0: $i] :
( r4_waybel_0(sK0,sK1,sK3,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_finset_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_4843,c_63,c_61,c_55,c_62,c_60,c_57,c_56,c_1225]) ).
tcf(c_5022,plain,
! [X0: $i] :
( r4_waybel_0(sK0,sK1,sK3,X0)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(renaming,[status(thm)],[c_5021]) ).
tcf(c_5023,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(X1)
| v4_waybel34(X0,sK0,X1)
| r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X1,X0))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(sK5(sK0,X1,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1)) ),
inference(superposition,[status(thm)],[c_95,c_5022]) ).
tcf(c_5108,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(sK1)
| v3_struct_0(sK0)
| v3_struct_0(X0)
| r4_waybel_0(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),X2)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(sK3)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ r4_waybel_0(sK0,sK1,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,X2)) ),
inference(superposition,[status(thm)],[c_4732,c_156]) ).
tcf(c_5555,plain,
! [X0: $i,X1: $i] :
( ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK1))
| ( k7_funct_2(X1,u1_struct_0(sK1),u1_struct_0(sK2),X0,sK4) = k5_relat_1(X0,sK4) ) ),
inference(global_subsumption_just,[status(thm)],[c_4802,c_61,c_52,c_60,c_164,c_53,c_191,c_4802]) ).
tcf(c_5556,plain,
! [X0: $i,X1: $i] :
( ( k7_funct_2(X1,u1_struct_0(sK1),u1_struct_0(sK2),X0,sK4) = k5_relat_1(X0,sK4) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK1)) ),
inference(renaming,[status(thm)],[c_5555]) ).
tcf(c_5559,plain,
( ( k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4) = k5_relat_1(sK3,sK4) )
| ~ v1_funct_1(sK3)
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_4621,c_5556]) ).
tcf(c_5593,plain,
k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4) = k5_relat_1(sK3,sK4),
inference(global_subsumption_just,[status(thm)],[c_5559,c_55,c_56,c_5559]) ).
tcf(c_5595,plain,
~ v4_waybel34(k5_relat_1(sK3,sK4),sK0,sK2),
inference(superposition,[status(thm)],[c_5593,c_49]) ).
tcf(c_5596,plain,
( v1_xboole_0(u1_struct_0(sK1))
| m2_relset_1(k5_relat_1(sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_5593,c_101]) ).
tcf(c_5597,plain,
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_2(k5_relat_1(sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_5593,c_100]) ).
tcf(c_5598,plain,
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_1(k5_relat_1(sK3,sK4))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_5593,c_99]) ).
tcf(c_5749,plain,
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_4338]) ).
tcf(c_5757,plain,
( v1_xboole_0(u1_struct_0(sK1))
| m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_4336]) ).
tcf(c_5761,plain,
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[c_4337]) ).
tcf(c_5803,plain,
! [X0: $i,X1: $i] :
( ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(sK5(sK0,X1,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X1,X0))
| v4_waybel34(X0,sK0,X1)
| v3_struct_0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_5023,c_63,c_62,c_5023]) ).
tcf(c_5804,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v4_waybel34(X0,sK0,X1)
| r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X1,X0))
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(sK5(sK0,X1,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1)) ),
inference(renaming,[status(thm)],[c_5803]) ).
tcf(c_5957,plain,
m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2)),
inference(superposition,[status(thm)],[c_54,c_149]) ).
tcf(c_5958,plain,
m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)),
inference(superposition,[status(thm)],[c_57,c_149]) ).
tcf(c_6032,plain,
! [X0: $i] :
( ( k4_pre_topc(sK0,sK1,sK3,X0) = k9_relat_1(sK3,X0) )
| ~ l1_struct_0(sK1)
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK3)
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_5958,c_146]) ).
tcf(c_6048,plain,
! [X0: $i] : k4_pre_topc(sK0,sK1,sK3,X0) = k9_relat_1(sK3,X0),
inference(global_subsumption_just,[status(thm)],[c_6032,c_61,c_55,c_164,c_57,c_56,c_3876,c_3955,c_4329]) ).
tcf(c_6050,plain,
! [X0: $i] :
( m1_subset_1(k9_relat_1(sK3,X0),k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l1_struct_0(sK1)
| ~ l1_struct_0(sK0)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_6048,c_97]) ).
tcf(c_6062,plain,
! [X0: $i] : m1_subset_1(k9_relat_1(sK3,X0),k1_zfmisc_1(u1_struct_0(sK1))),
inference(global_subsumption_just,[status(thm)],[c_6050,c_61,c_55,c_164,c_57,c_56,c_3876,c_3955,c_4735]) ).
tcf(c_6079,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(u1_struct_0(sK1))
| ( k7_funct_2(X1,u1_struct_0(sK1),u1_struct_0(sK2),X0,sK4) = k5_relat_1(X0,sK4) )
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(superposition,[status(thm)],[c_5957,c_147]) ).
tcf(c_6082,plain,
! [X0: $i] :
( v3_struct_0(sK2)
| v3_struct_0(sK1)
| r4_waybel_0(sK1,sK2,sK4,X0)
| ~ l1_orders_2(sK2)
| ~ l1_orders_2(sK1)
| ~ v1_funct_1(sK4)
| ~ v1_finset_1(X0)
| ~ v4_waybel34(sK4,sK1,sK2)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2)) ),
inference(superposition,[status(thm)],[c_53,c_96]) ).
tcf(c_6083,plain,
! [X0: $i] :
( v3_struct_0(sK1)
| v3_struct_0(sK0)
| r4_waybel_0(sK0,sK1,sK3,X0)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(sK3)
| ~ v1_finset_1(X0)
| ~ v4_waybel34(sK3,sK0,sK1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_56,c_96]) ).
tcf(c_6091,plain,
! [X0: $i] :
( r4_waybel_0(sK1,sK2,sK4,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ v1_finset_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6082,c_1243]) ).
tcf(c_6092,plain,
! [X0: $i] :
( r4_waybel_0(sK1,sK2,sK4,X0)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(renaming,[status(thm)],[c_6091]) ).
tcf(c_6100,plain,
! [X0: $i] :
( r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,X0))
| ~ v1_finset_1(k9_relat_1(sK3,X0)) ),
inference(superposition,[status(thm)],[c_6062,c_6092]) ).
tcf(c_6101,plain,
! [X0: $i] :
( r4_waybel_0(sK0,sK1,sK3,X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ v1_finset_1(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6083,c_1228]) ).
tcf(c_6102,plain,
! [X0: $i] :
( r4_waybel_0(sK0,sK1,sK3,X0)
| ~ v1_finset_1(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(renaming,[status(thm)],[c_6101]) ).
tcf(c_6103,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(X1)
| v4_waybel34(X0,sK0,X1)
| r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X1,X0))
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(sK5(sK0,X1,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1)) ),
inference(superposition,[status(thm)],[c_95,c_6102]) ).
tcf(c_6113,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(sK1)
| v3_struct_0(sK0)
| v3_struct_0(X0)
| r4_waybel_0(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),X2)
| ~ l1_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(sK3)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ r4_waybel_0(sK0,sK1,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,X2)) ),
inference(superposition,[status(thm)],[c_6048,c_156]) ).
tcf(c_6215,plain,
! [X0: $i,X1: $i] :
( ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK1))
| ( k7_funct_2(X1,u1_struct_0(sK1),u1_struct_0(sK2),X0,sK4) = k5_relat_1(X0,sK4) ) ),
inference(global_subsumption_just,[status(thm)],[c_6079,c_5556]) ).
tcf(c_6216,plain,
! [X0: $i,X1: $i] :
( ( k7_funct_2(X1,u1_struct_0(sK1),u1_struct_0(sK2),X0,sK4) = k5_relat_1(X0,sK4) )
| ~ v1_funct_1(X0)
| ~ m1_relset_1(X0,X1,u1_struct_0(sK1))
| ~ v1_funct_2(X0,X1,u1_struct_0(sK1)) ),
inference(renaming,[status(thm)],[c_6215]) ).
tcf(c_6218,plain,
( ( k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4) = k5_relat_1(sK3,sK4) )
| ~ v1_funct_1(sK3)
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_5958,c_6216]) ).
tcf(c_6222,plain,
k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4) = k5_relat_1(sK3,sK4),
inference(global_subsumption_just,[status(thm)],[c_6218,c_55,c_56,c_5559]) ).
tcf(c_6227,plain,
( v1_xboole_0(u1_struct_0(sK1))
| v1_funct_2(k5_relat_1(sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ m1_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ m1_relset_1(sK3,u1_struct_0(sK0),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK3,u1_struct_0(sK0),u1_struct_0(sK1)) ),
inference(superposition,[status(thm)],[c_6222,c_100]) ).
tcf(c_6259,plain,
! [X0: $i,X1: $i] :
( ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(sK5(sK0,X1,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1))
| r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X1,X0))
| v4_waybel34(X0,sK0,X1)
| v3_struct_0(X1) ),
inference(global_subsumption_just,[status(thm)],[c_6103,c_5804]) ).
tcf(c_6260,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X1)
| v4_waybel34(X0,sK0,X1)
| r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X1,X0))
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X0)
| ~ v1_finset_1(sK5(sK0,X1,X0))
| ~ m2_relset_1(X0,u1_struct_0(sK0),u1_struct_0(X1))
| ~ v1_funct_2(X0,u1_struct_0(sK0),u1_struct_0(X1)) ),
inference(renaming,[status(thm)],[c_6259]) ).
tcf(c_6290,plain,
v1_funct_2(k5_relat_1(sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)),
inference(global_subsumption_just,[status(thm)],[c_6227,c_61,c_55,c_52,c_60,c_164,c_57,c_56,c_54,c_53,c_191,c_3875,c_3876,c_5597]) ).
tcf(c_6293,plain,
( v3_struct_0(sK2)
| v3_struct_0(sK0)
| v4_waybel34(k5_relat_1(sK3,sK4),sK0,sK2)
| v1_finset_1(sK5(sK0,sK2,k5_relat_1(sK3,sK4)))
| ~ l1_orders_2(sK2)
| ~ l1_orders_2(sK0)
| ~ v1_funct_1(k5_relat_1(sK3,sK4))
| ~ m2_relset_1(k5_relat_1(sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(superposition,[status(thm)],[c_6290,c_94]) ).
tcf(c_6307,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r4_waybel_0(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),X2)
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,X2))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r4_waybel_0(sK0,sK1,sK3,X2)
| ~ v1_funct_1(X1)
| ~ l1_orders_2(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6113,c_63,c_61,c_55,c_62,c_60,c_57,c_56,c_5108]) ).
tcf(c_6308,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| r4_waybel_0(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),X2)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ r4_waybel_0(sK0,sK1,sK3,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,X2)) ),
inference(renaming,[status(thm)],[c_6307]) ).
tcf(c_6311,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(sK0)
| v3_struct_0(X0)
| v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),sK0,X0)
| ~ l1_orders_2(sK0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),u1_struct_0(sK0),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),u1_struct_0(sK0),u1_struct_0(X0))
| ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)))
| ~ m1_subset_1(sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)))) ),
inference(superposition,[status(thm)],[c_6308,c_93]) ).
tcf(c_7229,plain,
! [X0: $i,X1: $i] :
( ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),u1_struct_0(sK0),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),u1_struct_0(sK0),u1_struct_0(X0))
| ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)))
| ~ m1_subset_1(sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1))))
| v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),sK0,X0)
| v3_struct_0(X0) ),
inference(global_subsumption_just,[status(thm)],[c_6311,c_63,c_62,c_6311]) ).
tcf(c_7230,plain,
! [X0: $i,X1: $i] :
( v3_struct_0(X0)
| v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),sK0,X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ m2_relset_1(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_2(X1,u1_struct_0(sK1),u1_struct_0(X0))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),u1_struct_0(sK0),u1_struct_0(X0))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1),u1_struct_0(sK0),u1_struct_0(X0))
| ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)))
| ~ m1_subset_1(sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ r4_waybel_0(sK1,X0,X1,k9_relat_1(sK3,sK5(sK0,X0,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(X0),sK3,X1)))) ),
inference(renaming,[status(thm)],[c_7229]) ).
tcf(c_7238,plain,
( v3_struct_0(sK2)
| v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),sK0,sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(sK4)
| ~ m2_relset_1(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_2(sK4,u1_struct_0(sK1),u1_struct_0(sK2))
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4))))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)))
| ~ m1_subset_1(sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(superposition,[status(thm)],[c_6222,c_7230]) ).
tcf(c_7263,plain,
( ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)))
| ~ r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4)))) ),
inference(global_subsumption_just,[status(thm)],[c_7238,c_61,c_59,c_55,c_52,c_60,c_58,c_164,c_57,c_56,c_54,c_53,c_191,c_49,c_1194,c_3875,c_3876,c_5749,c_5757,c_5761,c_7238]) ).
tcf(c_7264,plain,
( ~ r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4))))
| ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))) ),
inference(renaming,[status(thm)],[c_7263]) ).
tcf(c_7265,plain,
( v3_struct_0(sK2)
| v4_waybel34(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),sK0,sK2)
| ~ l1_orders_2(sK2)
| ~ v1_funct_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4))
| ~ r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4))))
| ~ v1_finset_1(sK5(sK0,sK2,k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4)))
| ~ m2_relset_1(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2))
| ~ v1_funct_2(k7_funct_2(u1_struct_0(sK0),u1_struct_0(sK1),u1_struct_0(sK2),sK3,sK4),u1_struct_0(sK0),u1_struct_0(sK2)) ),
inference(superposition,[status(thm)],[c_6260,c_7264]) ).
tcf(c_7266,plain,
( ~ r4_waybel_0(sK0,sK1,sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4)))
| ~ r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4)))) ),
inference(superposition,[status(thm)],[c_6222,c_7264]) ).
tcf(c_7267,plain,
~ r4_waybel_0(sK1,sK2,sK4,k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4)))),
inference(global_subsumption_just,[status(thm)],[c_7266,c_61,c_59,c_55,c_52,c_60,c_58,c_164,c_57,c_56,c_54,c_53,c_191,c_49,c_1210,c_3875,c_3876,c_5749,c_5757,c_5761,c_7265]) ).
tcf(c_7270,plain,
~ v1_finset_1(k9_relat_1(sK3,sK5(sK0,sK2,k5_relat_1(sK3,sK4)))),
inference(superposition,[status(thm)],[c_6100,c_7267]) ).
tcf(c_7271,plain,
( ~ v1_relat_1(sK3)
| ~ v1_funct_1(sK3)
| ~ v1_finset_1(sK5(sK0,sK2,k5_relat_1(sK3,sK4))) ),
inference(superposition,[status(thm)],[c_109,c_7270]) ).
tcf(c_7273,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_7271,c_6293,c_5596,c_5598,c_5595,c_4203,c_3876,c_3875,c_191,c_53,c_54,c_56,c_57,c_164,c_58,c_60,c_62,c_52,c_55,c_59,c_61,c_63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT378+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 21:28:48 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 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.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 8.17/1.63 % SZS status Started for theBenchmark.p
% 8.17/1.63 % SZS status Theorem for theBenchmark.p
% 8.17/1.63
% 8.17/1.63 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.17/1.63
% 8.17/1.63 % ------ iProver source info
% 8.17/1.63
% 8.17/1.63 % git: date: 2026-07-19 20:42:38 +0200
% 8.17/1.63 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.17/1.63 % git: non_committed_changes: false
% 8.17/1.63
% 8.17/1.63 % ------ Parsing...
% 8.17/1.63 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.17/1.63
% 8.17/1.63 % ------ Preprocessing... sup_sim: 0 sf_s rm: 40 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 6 0s sf_e pe_s pe_e %
% 8.17/1.63
% 8.17/1.63 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.17/1.63
% 8.17/1.63 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 8.17/1.63 % ------ Proving...
% 8.17/1.63 % ------ Problem Properties
% 8.17/1.63
% 8.17/1.63 %
% 8.17/1.63 % clauses 75
% 8.17/1.63 % conjectures 15
% 8.17/1.63 % EPR 36
% 8.17/1.63 % Horn 59
% 8.17/1.63 % unary 34
% 8.17/1.63 % binary 17
% 8.17/1.63 % lits 213
% 8.17/1.63 % lits eq 4
% 8.17/1.63 % fd_pure 0
% 8.17/1.63 % fd_pseudo 0
% 8.17/1.63 % fd_cond 1
% 8.17/1.63 % fd_pseudo_cond 1
% 8.17/1.63 % AC symbols 0
% 8.17/1.63
% 8.17/1.63 % ------ Input Options Time Limit: Unbounded
% 8.17/1.63
% 8.17/1.63
% 8.17/1.63 % ------
% 8.17/1.63 % Current options:
% 8.17/1.63 % ------
% 8.17/1.63
% 8.17/1.63
% 8.17/1.63 %
% 8.17/1.63
% 8.17/1.63 % ------ Proving...
% 8.17/1.63 %
% 8.17/1.63
% 8.17/1.63 % SZS status Theorem for theBenchmark.p
% 8.17/1.63
% 8.17/1.63 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.17/1.64
% 8.17/1.64
%------------------------------------------------------------------------------