%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : LAT378+1 : TPTP v9.2.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.9WHDHhBSPp true
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 2 04:41:46 PM UTC 2025
% Result : Theorem 47.14s 7.39s
% Output : Refutation 47.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 18
% Syntax : Number of formulae : 378 ( 116 unt; 0 typ; 0 def)
% Number of atoms : 2052 ( 74 equ; 63 cnn)
% Maximal formula atoms : 25 ( 5 avg)
% Number of connectives : 8327 ( 500 ~; 562 |; 494 &;6284 @)
% ( 20 <=>; 267 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 9 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 34 ( 29 usr; 11 con; 0-5 aty)
% ( 199 !!; 1 ??; 0 @@+; 0 @@-)
% Number of variables : 659 ( 201 ^; 457 !; 1 ?; 659 :)
% Comments :
%------------------------------------------------------------------------------
thf(m2_relset_1_type,type,
m2_relset_1: $i > $i > $i > $o ).
thf(m1_subset_1_type,type,
m1_subset_1: $i > $i > $o ).
thf(v3_struct_0_type,type,
v3_struct_0: $i > $o ).
thf('#sk19_type',type,
'#sk19': $i > $i > $i > $i ).
thf(v1_funct_1_type,type,
v1_funct_1: $i > $o ).
thf(r4_waybel_0_type,type,
r4_waybel_0: $i > $i > $i > $i > $o ).
thf(u1_struct_0_type,type,
u1_struct_0: $i > $i ).
thf(k4_pre_topc_type,type,
k4_pre_topc: $i > $i > $i > $i > $i ).
thf(l1_struct_0_type,type,
l1_struct_0: $i > $o ).
thf('#sk5_type',type,
'#sk5': $i ).
thf('#sk14_type',type,
'#sk14': $i ).
thf(v1_funct_2_type,type,
v1_funct_2: $i > $i > $i > $o ).
thf(l1_orders_2_type,type,
l1_orders_2: $i > $o ).
thf(v4_waybel34_type,type,
v4_waybel34: $i > $i > $i > $o ).
thf('#sk1_type',type,
'#sk1': $i ).
thf(v1_xboole_0_type,type,
v1_xboole_0: $i > $o ).
thf(k5_relat_1_type,type,
k5_relat_1: $i > $i > $i ).
thf('#sk2_type',type,
'#sk2': $i ).
thf(r1_tarski_type,type,
r1_tarski: $i > $i > $o ).
thf(k1_xboole_0_type,type,
k1_xboole_0: $i ).
thf(v1_finset_1_type,type,
v1_finset_1: $i > $o ).
thf(k1_zfmisc_1_type,type,
k1_zfmisc_1: $i > $i ).
thf(k7_funct_2_type,type,
k7_funct_2: $i > $i > $i > $i > $i > $i ).
thf(v1_relat_1_type,type,
v1_relat_1: $i > $o ).
thf(k9_relat_1_type,type,
k9_relat_1: $i > $i > $i ).
thf(k2_zfmisc_1_type,type,
k2_zfmisc_1: $i > $i > $i ).
thf(m1_relset_1_type,type,
m1_relset_1: $i > $i > $i > $o ).
thf('#sk4_type',type,
'#sk4': $i ).
thf('#sk3_type',type,
'#sk3': $i ).
thf(redefinition_m2_relset_1,axiom,
! [A: $i,B: $i,C: $i] :
( ( m2_relset_1 @ C @ A @ B )
<=> ( m1_relset_1 @ C @ A @ B ) ) ).
thf(zip_derived_cl58,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( m2_relset_1 @ Y2 @ Y0 @ Y1 )
<=> ( m1_relset_1 @ Y2 @ Y0 @ Y1 ) ) ) ) ),
inference(cnf,[status(esa)],[redefinition_m2_relset_1]) ).
thf(zip_derived_cl327,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( m2_relset_1 @ Y1 @ X2 @ Y0 )
<=> ( m1_relset_1 @ Y1 @ X2 @ Y0 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl58]) ).
thf(zip_derived_cl328,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( ( m2_relset_1 @ Y0 @ X2 @ X4 )
<=> ( m1_relset_1 @ Y0 @ X2 @ X4 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl327]) ).
thf(zip_derived_cl329,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
<=> ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl328]) ).
thf(zip_derived_cl330,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(t63_waybel34,conjecture,
! [A: $i] :
( ( ( l1_orders_2 @ A )
& ~ ( v3_struct_0 @ A ) )
=> ! [B: $i] :
( ( ( l1_orders_2 @ B )
& ~ ( v3_struct_0 @ B ) )
=> ! [C: $i] :
( ( ( l1_orders_2 @ C )
& ~ ( v3_struct_0 @ C ) )
=> ! [D: $i] :
( ( ( m2_relset_1 @ D @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_2 @ D @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_1 @ D ) )
=> ! [E: $i] :
( ( ( m2_relset_1 @ E @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) )
& ( v1_funct_2 @ E @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) )
& ( v1_funct_1 @ E ) )
=> ( ( ( v4_waybel34 @ E @ B @ C )
& ( v4_waybel34 @ D @ A @ B ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) @ D @ E ) @ A @ C ) ) ) ) ) ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [A: $i] :
( ( ( l1_orders_2 @ A )
& ~ ( v3_struct_0 @ A ) )
=> ! [B: $i] :
( ( ( l1_orders_2 @ B )
& ~ ( v3_struct_0 @ B ) )
=> ! [C: $i] :
( ( ( l1_orders_2 @ C )
& ~ ( v3_struct_0 @ C ) )
=> ! [D: $i] :
( ( ( m2_relset_1 @ D @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_2 @ D @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_1 @ D ) )
=> ! [E: $i] :
( ( ( m2_relset_1 @ E @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) )
& ( v1_funct_2 @ E @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) )
& ( v1_funct_1 @ E ) )
=> ( ( ( v4_waybel34 @ E @ B @ C )
& ( v4_waybel34 @ D @ A @ B ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) @ D @ E ) @ A @ C ) ) ) ) ) ) ),
inference('cnf.neg',[status(esa)],[t63_waybel34]) ).
thf(zip_derived_cl0,plain,
~ ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( l1_orders_2 @ Y2 )
& ( (~) @ ( v3_struct_0 @ Y2 ) ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( !!
@ ^ [Y4: $i] :
( ( ( m2_relset_1 @ Y4 @ ( u1_struct_0 @ Y1 ) @ ( u1_struct_0 @ Y2 ) )
& ( v1_funct_2 @ Y4 @ ( u1_struct_0 @ Y1 ) @ ( u1_struct_0 @ Y2 ) )
& ( v1_funct_1 @ Y4 ) )
=> ( ( ( v4_waybel34 @ Y4 @ Y1 @ Y2 )
& ( v4_waybel34 @ Y3 @ Y0 @ Y1 ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ ( u1_struct_0 @ Y2 ) @ Y3 @ Y4 ) @ Y0 @ Y2 ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl69,plain,
~ ( ( ( l1_orders_2 @ '#sk1' )
& ( (~) @ ( v3_struct_0 @ '#sk1' ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( ( ( v4_waybel34 @ Y3 @ Y0 @ Y1 )
& ( v4_waybel34 @ Y2 @ '#sk1' @ Y0 ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ Y2 @ Y3 ) @ '#sk1' @ Y1 ) ) ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl0]) ).
thf(zip_derived_cl71,plain,
~ ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( ( ( v4_waybel34 @ Y3 @ Y0 @ Y1 )
& ( v4_waybel34 @ Y2 @ '#sk1' @ Y0 ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ Y2 @ Y3 ) @ '#sk1' @ Y1 ) ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl69]) ).
thf(zip_derived_cl74,plain,
~ ( ( ( l1_orders_2 @ '#sk2' )
& ( (~) @ ( v3_struct_0 @ '#sk2' ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_1 @ Y1 ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( ( ( v4_waybel34 @ Y2 @ '#sk2' @ Y0 )
& ( v4_waybel34 @ Y1 @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ Y0 ) @ Y1 @ Y2 ) @ '#sk1' @ Y0 ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl71]) ).
thf(zip_derived_cl76,plain,
~ ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_1 @ Y1 ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( ( ( v4_waybel34 @ Y2 @ '#sk2' @ Y0 )
& ( v4_waybel34 @ Y1 @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ Y0 ) @ Y1 @ Y2 ) @ '#sk1' @ Y0 ) ) ) ) ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl74]) ).
thf(zip_derived_cl79,plain,
~ ( ( ( l1_orders_2 @ '#sk3' )
& ( (~) @ ( v3_struct_0 @ '#sk3' ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_1 @ Y0 ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( ( v4_waybel34 @ Y1 @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ Y0 @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ Y0 @ Y1 ) @ '#sk1' @ '#sk3' ) ) ) ) ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl76]) ).
thf(zip_derived_cl81,plain,
~ ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_funct_1 @ Y0 ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( ( v4_waybel34 @ Y1 @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ Y0 @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ Y0 @ Y1 ) @ '#sk1' @ '#sk3' ) ) ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl79]) ).
thf(zip_derived_cl84,plain,
~ ( ( ( 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' ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( ( v4_waybel34 @ Y0 @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ Y0 ) @ '#sk1' @ '#sk3' ) ) ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl81]) ).
thf(zip_derived_cl85,plain,
( ( 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' ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl84]) ).
thf(zip_derived_cl87,plain,
m2_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl331,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl330_001,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl86,plain,
~ ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( ( v4_waybel34 @ Y0 @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ Y0 ) @ '#sk1' @ '#sk3' ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl84]) ).
thf(zip_derived_cl90,plain,
~ ( ( ( m2_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_1 @ '#sk5' ) )
=> ( ( ( v4_waybel34 @ '#sk5' @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl86]) ).
thf(zip_derived_cl91,plain,
( ( m2_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
& ( v1_funct_1 @ '#sk5' ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl90]) ).
thf(zip_derived_cl93,plain,
m2_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl332,plain,
m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl93]) ).
thf(redefinition_k7_funct_2,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( m1_relset_1 @ E @ B @ C )
& ( v1_funct_2 @ E @ B @ C )
& ( v1_funct_1 @ E )
& ( m1_relset_1 @ D @ A @ B )
& ( v1_funct_2 @ D @ A @ B )
& ( v1_funct_1 @ D )
& ~ ( v1_xboole_0 @ B ) )
=> ( ( k7_funct_2 @ A @ B @ C @ D @ E )
= ( k5_relat_1 @ D @ E ) ) ) ).
thf(zip_derived_cl57,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( !!
@ ^ [Y3: $i] :
( !!
@ ^ [Y4: $i] :
( ( ( m1_relset_1 @ Y4 @ Y1 @ Y2 )
& ( v1_funct_2 @ Y4 @ Y1 @ Y2 )
& ( v1_funct_1 @ Y4 )
& ( m1_relset_1 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_2 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_1 @ Y3 )
& ( (~) @ ( v1_xboole_0 @ Y1 ) ) )
=> ( ( k7_funct_2 @ Y0 @ Y1 @ Y2 @ Y3 @ Y4 )
= ( k5_relat_1 @ Y3 @ Y4 ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[redefinition_k7_funct_2]) ).
thf(zip_derived_cl762,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( !!
@ ^ [Y3: $i] :
( ( ( m1_relset_1 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_2 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_1 @ Y3 )
& ( m1_relset_1 @ Y2 @ X2 @ Y0 )
& ( v1_funct_2 @ Y2 @ X2 @ Y0 )
& ( v1_funct_1 @ Y2 )
& ( (~) @ ( v1_xboole_0 @ Y0 ) ) )
=> ( ( k7_funct_2 @ X2 @ Y0 @ Y1 @ Y2 @ Y3 )
= ( k5_relat_1 @ Y2 @ Y3 ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl57]) ).
thf(zip_derived_cl763,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( ( m1_relset_1 @ Y2 @ X4 @ Y0 )
& ( v1_funct_2 @ Y2 @ X4 @ Y0 )
& ( v1_funct_1 @ Y2 )
& ( m1_relset_1 @ Y1 @ X2 @ X4 )
& ( v1_funct_2 @ Y1 @ X2 @ X4 )
& ( v1_funct_1 @ Y1 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( k7_funct_2 @ X2 @ X4 @ Y0 @ Y1 @ Y2 )
= ( k5_relat_1 @ Y1 @ Y2 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl762]) ).
thf(zip_derived_cl764,plain,
! [X2: $i,X4: $i,X6: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( ( m1_relset_1 @ Y1 @ X4 @ X6 )
& ( v1_funct_2 @ Y1 @ X4 @ X6 )
& ( v1_funct_1 @ Y1 )
& ( m1_relset_1 @ Y0 @ X2 @ X4 )
& ( v1_funct_2 @ Y0 @ X2 @ X4 )
& ( v1_funct_1 @ Y0 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( k7_funct_2 @ X2 @ X4 @ X6 @ Y0 @ Y1 )
= ( k5_relat_1 @ Y0 @ Y1 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl763]) ).
thf(zip_derived_cl765,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( !!
@ ^ [Y0: $i] :
( ( ( m1_relset_1 @ Y0 @ X4 @ X6 )
& ( v1_funct_2 @ Y0 @ X4 @ X6 )
& ( v1_funct_1 @ Y0 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ Y0 )
= ( k5_relat_1 @ X8 @ Y0 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl764]) ).
thf(zip_derived_cl766,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( ( m1_relset_1 @ X10 @ X4 @ X6 )
& ( v1_funct_2 @ X10 @ X4 @ X6 )
& ( v1_funct_1 @ X10 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 )
= ( k5_relat_1 @ X8 @ X10 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl765]) ).
thf(zip_derived_cl767,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( ( m1_relset_1 @ X10 @ X4 @ X6 )
& ( v1_funct_2 @ X10 @ X4 @ X6 )
& ( v1_funct_1 @ X10 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
| ( ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 )
= ( k5_relat_1 @ X8 @ X10 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl766]) ).
thf(zip_derived_cl768,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( ( m1_relset_1 @ X10 @ X4 @ X6 )
& ( v1_funct_2 @ X10 @ X4 @ X6 )
& ( v1_funct_1 @ X10 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
| ( ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 )
= ( k5_relat_1 @ X8 @ X10 ) ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl767]) ).
thf(zip_derived_cl769,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( m1_relset_1 @ X10 @ X4 @ X6 )
| ~ ( v1_funct_2 @ X10 @ X4 @ X6 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( m1_relset_1 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_2 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_1 @ X8 )
| ( v1_xboole_0 @ X4 )
| ( ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 )
= ( k5_relat_1 @ X8 @ X10 ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl768]) ).
thf(zip_derived_cl771,plain,
! [X0: $i,X1: $i] :
( ~ ( v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ '#sk5' )
| ~ ( m1_relset_1 @ X1 @ X0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ X1 @ X0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X1 )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ X0 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ X1 @ '#sk5' )
= ( k5_relat_1 @ X1 @ '#sk5' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl332,zip_derived_cl769]) ).
thf(zip_derived_cl94,plain,
v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl95,plain,
v1_funct_1 @ '#sk5',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl774,plain,
! [X0: $i,X1: $i] :
( ~ ( m1_relset_1 @ X1 @ X0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ X1 @ X0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X1 )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ X0 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ X1 @ '#sk5' )
= ( k5_relat_1 @ X1 @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl771,zip_derived_cl94,zip_derived_cl95]) ).
thf(zip_derived_cl2681,plain,
( ~ ( v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk4' )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl331,zip_derived_cl774]) ).
thf(zip_derived_cl88,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl89,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl2684,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl331_002,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(redefinition_k4_pre_topc,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( m1_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_1 @ C )
& ( l1_struct_0 @ B )
& ( l1_struct_0 @ A ) )
=> ( ( k4_pre_topc @ A @ B @ C @ D )
= ( k9_relat_1 @ C @ D ) ) ) ).
thf(zip_derived_cl56,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( !!
@ ^ [Y3: $i] :
( ( ( m1_relset_1 @ Y2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y2 )
& ( l1_struct_0 @ Y1 )
& ( l1_struct_0 @ Y0 ) )
=> ( ( k4_pre_topc @ Y0 @ Y1 @ Y2 @ Y3 )
= ( k9_relat_1 @ Y2 @ Y3 ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[redefinition_k4_pre_topc]) ).
thf(zip_derived_cl720,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( ( m1_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y1 )
& ( l1_struct_0 @ Y0 )
& ( l1_struct_0 @ X2 ) )
=> ( ( k4_pre_topc @ X2 @ Y0 @ Y1 @ Y2 )
= ( k9_relat_1 @ Y1 @ Y2 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl56]) ).
thf(zip_derived_cl721,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( ( m1_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( ( k4_pre_topc @ X2 @ X4 @ Y0 @ Y1 )
= ( k9_relat_1 @ Y0 @ Y1 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl720]) ).
thf(zip_derived_cl722,plain,
! [X2: $i,X4: $i,X6: $i] :
( !!
@ ^ [Y0: $i] :
( ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( ( k4_pre_topc @ X2 @ X4 @ X6 @ Y0 )
= ( k9_relat_1 @ X6 @ Y0 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl721]) ).
thf(zip_derived_cl723,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 )
= ( k9_relat_1 @ X6 @ X8 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl722]) ).
thf(zip_derived_cl724,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
| ( ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 )
= ( k9_relat_1 @ X6 @ X8 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl723]) ).
thf(zip_derived_cl725,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
| ( ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 )
= ( k9_relat_1 @ X6 @ X8 ) ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl724]) ).
thf(zip_derived_cl726,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_struct_0 @ X4 )
| ~ ( l1_struct_0 @ X2 )
| ( ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 )
= ( k9_relat_1 @ X6 @ X8 ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl725]) ).
thf(zip_derived_cl727,plain,
! [X0: $i] :
( ~ ( v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( l1_struct_0 @ '#sk2' )
| ~ ( l1_struct_0 @ '#sk1' )
| ( ( k4_pre_topc @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
= ( k9_relat_1 @ '#sk4' @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl331,zip_derived_cl726]) ).
thf(zip_derived_cl88_003,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl89_004,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(dt_l1_orders_2,axiom,
! [A: $i] :
( ( l1_orders_2 @ A )
=> ( l1_struct_0 @ A ) ) ).
thf(zip_derived_cl30,plain,
( !!
@ ^ [Y0: $i] :
( ( l1_orders_2 @ Y0 )
=> ( l1_struct_0 @ Y0 ) ) ),
inference(cnf,[status(esa)],[dt_l1_orders_2]) ).
thf(zip_derived_cl124,plain,
! [X2: $i] :
( ( l1_orders_2 @ X2 )
=> ( l1_struct_0 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl30]) ).
thf(zip_derived_cl125,plain,
! [X2: $i] :
( ~ ( l1_orders_2 @ X2 )
| ( l1_struct_0 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl124]) ).
thf(zip_derived_cl75,plain,
( ( l1_orders_2 @ '#sk2' )
& ( (~) @ ( v3_struct_0 @ '#sk2' ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl74]) ).
thf(zip_derived_cl77,plain,
l1_orders_2 @ '#sk2',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl127,plain,
l1_struct_0 @ '#sk2',
inference('s_sup+',[status(thm)],[zip_derived_cl125,zip_derived_cl77]) ).
thf(zip_derived_cl125_005,plain,
! [X2: $i] :
( ~ ( l1_orders_2 @ X2 )
| ( l1_struct_0 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl124]) ).
thf(zip_derived_cl70,plain,
( ( l1_orders_2 @ '#sk1' )
& ( (~) @ ( v3_struct_0 @ '#sk1' ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl69]) ).
thf(zip_derived_cl72,plain,
l1_orders_2 @ '#sk1',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl126,plain,
l1_struct_0 @ '#sk1',
inference('s_sup+',[status(thm)],[zip_derived_cl125,zip_derived_cl72]) ).
thf(zip_derived_cl730,plain,
! [X0: $i] :
( ( k4_pre_topc @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
= ( k9_relat_1 @ '#sk4' @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl727,zip_derived_cl88,zip_derived_cl89,zip_derived_cl127,zip_derived_cl126]) ).
thf(dt_k4_pre_topc,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( m1_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_1 @ C )
& ( l1_struct_0 @ B )
& ( l1_struct_0 @ A ) )
=> ( m1_subset_1 @ ( k4_pre_topc @ A @ B @ C @ D ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ B ) ) ) ) ).
thf(zip_derived_cl26,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( !!
@ ^ [Y3: $i] :
( ( ( m1_relset_1 @ Y2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y2 )
& ( l1_struct_0 @ Y1 )
& ( l1_struct_0 @ Y0 ) )
=> ( m1_subset_1 @ ( k4_pre_topc @ Y0 @ Y1 @ Y2 @ Y3 ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ Y1 ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[dt_k4_pre_topc]) ).
thf(zip_derived_cl529,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( ( m1_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y1 )
& ( l1_struct_0 @ Y0 )
& ( l1_struct_0 @ X2 ) )
=> ( m1_subset_1 @ ( k4_pre_topc @ X2 @ Y0 @ Y1 @ Y2 ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ Y0 ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl26]) ).
thf(zip_derived_cl530,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( ( m1_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( m1_subset_1 @ ( k4_pre_topc @ X2 @ X4 @ Y0 @ Y1 ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X4 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl529]) ).
thf(zip_derived_cl531,plain,
! [X2: $i,X4: $i,X6: $i] :
( !!
@ ^ [Y0: $i] :
( ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( m1_subset_1 @ ( k4_pre_topc @ X2 @ X4 @ X6 @ Y0 ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X4 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl530]) ).
thf(zip_derived_cl532,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( m1_subset_1 @ ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X4 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl531]) ).
thf(t3_subset,axiom,
! [A: $i,B: $i] :
( ( m1_subset_1 @ A @ ( k1_zfmisc_1 @ B ) )
<=> ( r1_tarski @ A @ B ) ) ).
thf(zip_derived_cl62,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ Y1 ) )
<=> ( r1_tarski @ Y0 @ Y1 ) ) ) ),
inference(cnf,[status(esa)],[t3_subset]) ).
thf(zip_derived_cl261,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ Y0 ) )
<=> ( r1_tarski @ X2 @ Y0 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl62]) ).
thf(zip_derived_cl262,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
<=> ( r1_tarski @ X2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl261]) ).
thf(zip_derived_cl263,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl533,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
=> ( r1_tarski @ ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl532,zip_derived_cl263]) ).
thf(zip_derived_cl534,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 )
& ( l1_struct_0 @ X4 )
& ( l1_struct_0 @ X2 ) )
| ( r1_tarski @ ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl533]) ).
thf(zip_derived_cl535,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_struct_0 @ X4 )
| ~ ( l1_struct_0 @ X2 )
| ( r1_tarski @ ( k4_pre_topc @ X2 @ X4 @ X6 @ X8 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl534]) ).
thf(zip_derived_cl1024,plain,
! [X0: $i] :
( ~ ( m1_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' )
| ~ ( l1_struct_0 @ '#sk2' )
| ~ ( l1_struct_0 @ '#sk1' )
| ( r1_tarski @ ( k9_relat_1 @ '#sk4' @ X0 ) @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl730,zip_derived_cl535]) ).
thf(zip_derived_cl331_006,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl88_007,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl89_008,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl127_009,plain,
l1_struct_0 @ '#sk2',
inference('s_sup+',[status(thm)],[zip_derived_cl125,zip_derived_cl77]) ).
thf(zip_derived_cl126_010,plain,
l1_struct_0 @ '#sk1',
inference('s_sup+',[status(thm)],[zip_derived_cl125,zip_derived_cl72]) ).
thf(zip_derived_cl1026,plain,
! [X0: $i] : ( r1_tarski @ ( k9_relat_1 @ '#sk4' @ X0 ) @ ( u1_struct_0 @ '#sk2' ) ),
inference(demod,[status(thm)],[zip_derived_cl1024,zip_derived_cl331,zip_derived_cl88,zip_derived_cl89,zip_derived_cl127,zip_derived_cl126]) ).
thf(zip_derived_cl332_011,plain,
m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl93]) ).
thf(d15_waybel34,axiom,
! [A: $i] :
( ( ( l1_orders_2 @ A )
& ~ ( v3_struct_0 @ A ) )
=> ! [B: $i] :
( ( ( l1_orders_2 @ B )
& ~ ( v3_struct_0 @ B ) )
=> ! [C: $i] :
( ( ( m2_relset_1 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_2 @ C @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_1 @ C ) )
=> ( ( v4_waybel34 @ C @ A @ B )
<=> ! [D: $i] :
( ( ( m1_subset_1 @ D @ ( k1_zfmisc_1 @ ( u1_struct_0 @ A ) ) )
& ( v1_finset_1 @ D ) )
=> ( r4_waybel_0 @ A @ B @ C @ D ) ) ) ) ) ) ).
thf(zip_derived_cl22,plain,
( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( ( v4_waybel34 @ Y2 @ Y0 @ Y1 )
<=> ( !!
@ ^ [Y3: $i] :
( ( ( m1_subset_1 @ Y3 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ Y0 ) ) )
& ( v1_finset_1 @ Y3 ) )
=> ( r4_waybel_0 @ Y0 @ Y1 @ Y2 @ Y3 ) ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[d15_waybel34]) ).
thf(zip_derived_cl472,plain,
! [X2: $i] :
( ( ( l1_orders_2 @ X2 )
& ( (~) @ ( v3_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( v4_waybel34 @ Y1 @ X2 @ Y0 )
<=> ( !!
@ ^ [Y2: $i] :
( ( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y2 ) )
=> ( r4_waybel_0 @ X2 @ Y0 @ Y1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl22]) ).
thf(zip_derived_cl473,plain,
! [X2: $i] :
( ~ ( ( l1_orders_2 @ X2 )
& ( (~) @ ( v3_struct_0 @ X2 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( v4_waybel34 @ Y1 @ X2 @ Y0 )
<=> ( !!
@ ^ [Y2: $i] :
( ( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y2 ) )
=> ( r4_waybel_0 @ X2 @ Y0 @ Y1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl472]) ).
thf(zip_derived_cl474,plain,
! [X2: $i] :
( ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( v4_waybel34 @ Y1 @ X2 @ Y0 )
<=> ( !!
@ ^ [Y2: $i] :
( ( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y2 ) )
=> ( r4_waybel_0 @ X2 @ Y0 @ Y1 @ Y2 ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl473]) ).
thf(zip_derived_cl475,plain,
! [X2: $i,X4: $i] :
( ( ( ( l1_orders_2 @ X4 )
& ( (~) @ ( v3_struct_0 @ X4 ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( v4_waybel34 @ Y0 @ X2 @ X4 )
<=> ( !!
@ ^ [Y1: $i] :
( ( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y1 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ Y0 @ Y1 ) ) ) ) ) ) )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl474]) ).
thf(zip_derived_cl476,plain,
! [X2: $i,X4: $i] :
( ~ ( ( l1_orders_2 @ X4 )
& ( (~) @ ( v3_struct_0 @ X4 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( v4_waybel34 @ Y0 @ X2 @ X4 )
<=> ( !!
@ ^ [Y1: $i] :
( ( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y1 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ Y0 @ Y1 ) ) ) ) ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl475]) ).
thf(zip_derived_cl477,plain,
! [X2: $i,X4: $i] :
( ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( v4_waybel34 @ Y0 @ X2 @ X4 )
<=> ( !!
@ ^ [Y1: $i] :
( ( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y1 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl476]) ).
thf(zip_derived_cl478,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( ( ( m2_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 ) )
=> ( ( v4_waybel34 @ X6 @ X2 @ X4 )
<=> ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl477]) ).
thf(zip_derived_cl330_012,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl479,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 ) )
=> ( ( v4_waybel34 @ X6 @ X2 @ X4 )
<=> ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl478,zip_derived_cl330]) ).
thf(zip_derived_cl480,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 ) )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
<=> ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl479]) ).
thf(zip_derived_cl481,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X6 ) )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl480]) ).
thf(zip_derived_cl482,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl481]) ).
thf(zip_derived_cl484,plain,
( ~ ( v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ '#sk5' )
| ~ ( l1_orders_2 @ '#sk2' )
| ( v3_struct_0 @ '#sk2' )
| ( v3_struct_0 @ '#sk3' )
| ~ ( l1_orders_2 @ '#sk3' )
| ( ( v4_waybel34 @ '#sk5' @ '#sk2' @ '#sk3' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk2' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ Y0 ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl332,zip_derived_cl482]) ).
thf(zip_derived_cl94_013,plain,
v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl95_014,plain,
v1_funct_1 @ '#sk5',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl77_015,plain,
l1_orders_2 @ '#sk2',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl78,plain,
~ ( v3_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl80,plain,
( ( l1_orders_2 @ '#sk3' )
& ( (~) @ ( v3_struct_0 @ '#sk3' ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl79]) ).
thf(zip_derived_cl83,plain,
~ ( v3_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl82,plain,
l1_orders_2 @ '#sk3',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl92,plain,
~ ( ( ( v4_waybel34 @ '#sk5' @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2' ) )
=> ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl90]) ).
thf(zip_derived_cl96,plain,
( ( v4_waybel34 @ '#sk5' @ '#sk2' @ '#sk3' )
& ( v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2' ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl92]) ).
thf(zip_derived_cl98,plain,
v4_waybel34 @ '#sk5' @ '#sk2' @ '#sk3',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl96]) ).
thf(zip_derived_cl489,plain,
( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk2' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ Y0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl484,zip_derived_cl94,zip_derived_cl95,zip_derived_cl77,zip_derived_cl78,zip_derived_cl83,zip_derived_cl82,zip_derived_cl98]) ).
thf(zip_derived_cl555,plain,
! [X2: $i] :
( ( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk2' ) ) )
& ( v1_finset_1 @ X2 ) )
=> ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl489]) ).
thf(zip_derived_cl263_016,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl556,plain,
! [X2: $i] :
( ( ( r1_tarski @ X2 @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_finset_1 @ X2 ) )
=> ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl555,zip_derived_cl263]) ).
thf(zip_derived_cl557,plain,
! [X2: $i] :
( ~ ( ( r1_tarski @ X2 @ ( u1_struct_0 @ '#sk2' ) )
& ( v1_finset_1 @ X2 ) )
| ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl556]) ).
thf(zip_derived_cl558,plain,
! [X2: $i] :
( ~ ( r1_tarski @ X2 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_finset_1 @ X2 )
| ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ X2 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl557]) ).
thf(zip_derived_cl1134,plain,
! [X0: $i] :
( ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ X0 ) )
| ( r4_waybel_0 @ '#sk2' @ '#sk3' @ '#sk5' @ ( k9_relat_1 @ '#sk4' @ X0 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1026,zip_derived_cl558]) ).
thf(zip_derived_cl730_017,plain,
! [X0: $i] :
( ( k4_pre_topc @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
= ( k9_relat_1 @ '#sk4' @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl727,zip_derived_cl88,zip_derived_cl89,zip_derived_cl127,zip_derived_cl126]) ).
thf(t62_waybel34,axiom,
! [A: $i] :
( ( ( l1_orders_2 @ A )
& ~ ( v3_struct_0 @ A ) )
=> ! [B: $i] :
( ( ( l1_orders_2 @ B )
& ~ ( v3_struct_0 @ B ) )
=> ! [C: $i] :
( ( ( l1_orders_2 @ C )
& ~ ( v3_struct_0 @ C ) )
=> ! [D: $i] :
( ( m1_subset_1 @ D @ ( k1_zfmisc_1 @ ( u1_struct_0 @ A ) ) )
=> ! [E: $i] :
( ( ( m2_relset_1 @ E @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_2 @ E @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) )
& ( v1_funct_1 @ E ) )
=> ! [F: $i] :
( ( ( m2_relset_1 @ F @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) )
& ( v1_funct_2 @ F @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) )
& ( v1_funct_1 @ F ) )
=> ( ( ( r4_waybel_0 @ B @ C @ F @ ( k4_pre_topc @ A @ B @ E @ D ) )
& ( r4_waybel_0 @ A @ B @ E @ D ) )
=> ( r4_waybel_0 @ A @ C @ ( k7_funct_2 @ ( u1_struct_0 @ A ) @ ( u1_struct_0 @ B ) @ ( u1_struct_0 @ C ) @ E @ F ) @ D ) ) ) ) ) ) ) ) ).
thf(zip_derived_cl65,plain,
( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( l1_orders_2 @ Y2 )
& ( (~) @ ( v3_struct_0 @ Y2 ) ) )
=> ( !!
@ ^ [Y3: $i] :
( ( m1_subset_1 @ Y3 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y4: $i] :
( ( ( m2_relset_1 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y4 ) )
=> ( !!
@ ^ [Y5: $i] :
( ( ( m2_relset_1 @ Y5 @ ( u1_struct_0 @ Y1 ) @ ( u1_struct_0 @ Y2 ) )
& ( v1_funct_2 @ Y5 @ ( u1_struct_0 @ Y1 ) @ ( u1_struct_0 @ Y2 ) )
& ( v1_funct_1 @ Y5 ) )
=> ( ( ( r4_waybel_0 @ Y1 @ Y2 @ Y5 @ ( k4_pre_topc @ Y0 @ Y1 @ Y4 @ Y3 ) )
& ( r4_waybel_0 @ Y0 @ Y1 @ Y4 @ Y3 ) )
=> ( r4_waybel_0 @ Y0 @ Y2 @ ( k7_funct_2 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ ( u1_struct_0 @ Y2 ) @ Y4 @ Y5 ) @ Y3 ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[t62_waybel34]) ).
thf(zip_derived_cl813,plain,
! [X2: $i] :
( ( ( l1_orders_2 @ X2 )
& ( (~) @ ( v3_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( !!
@ ^ [Y4: $i] :
( ( ( m2_relset_1 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y4 ) )
=> ( ( ( r4_waybel_0 @ Y0 @ Y1 @ Y4 @ ( k4_pre_topc @ X2 @ Y0 @ Y3 @ Y2 ) )
& ( r4_waybel_0 @ X2 @ Y0 @ Y3 @ Y2 ) )
=> ( r4_waybel_0 @ X2 @ Y1 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ Y3 @ Y4 ) @ Y2 ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl65]) ).
thf(zip_derived_cl814,plain,
! [X2: $i] :
( ~ ( ( l1_orders_2 @ X2 )
& ( (~) @ ( v3_struct_0 @ X2 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( !!
@ ^ [Y4: $i] :
( ( ( m2_relset_1 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y4 ) )
=> ( ( ( r4_waybel_0 @ Y0 @ Y1 @ Y4 @ ( k4_pre_topc @ X2 @ Y0 @ Y3 @ Y2 ) )
& ( r4_waybel_0 @ X2 @ Y0 @ Y3 @ Y2 ) )
=> ( r4_waybel_0 @ X2 @ Y1 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ Y3 @ Y4 ) @ Y2 ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl813]) ).
thf(zip_derived_cl815,plain,
! [X2: $i] :
( ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( l1_orders_2 @ Y1 )
& ( (~) @ ( v3_struct_0 @ Y1 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( !!
@ ^ [Y4: $i] :
( ( ( m2_relset_1 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_2 @ Y4 @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) )
& ( v1_funct_1 @ Y4 ) )
=> ( ( ( r4_waybel_0 @ Y0 @ Y1 @ Y4 @ ( k4_pre_topc @ X2 @ Y0 @ Y3 @ Y2 ) )
& ( r4_waybel_0 @ X2 @ Y0 @ Y3 @ Y2 ) )
=> ( r4_waybel_0 @ X2 @ Y1 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ Y0 ) @ ( u1_struct_0 @ Y1 ) @ Y3 @ Y4 ) @ Y2 ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl814]) ).
thf(zip_derived_cl816,plain,
! [X2: $i,X4: $i] :
( ( ( ( l1_orders_2 @ X4 )
& ( (~) @ ( v3_struct_0 @ X4 ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( ( ( r4_waybel_0 @ X4 @ Y0 @ Y3 @ ( k4_pre_topc @ X2 @ X4 @ Y2 @ Y1 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y2 @ Y1 ) )
=> ( r4_waybel_0 @ X2 @ Y0 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) @ Y2 @ Y3 ) @ Y1 ) ) ) ) ) ) ) ) ) ) )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl815]) ).
thf(zip_derived_cl817,plain,
! [X2: $i,X4: $i] :
( ~ ( ( l1_orders_2 @ X4 )
& ( (~) @ ( v3_struct_0 @ X4 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( ( ( r4_waybel_0 @ X4 @ Y0 @ Y3 @ ( k4_pre_topc @ X2 @ X4 @ Y2 @ Y1 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y2 @ Y1 ) )
=> ( r4_waybel_0 @ X2 @ Y0 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) @ Y2 @ Y3 ) @ Y1 ) ) ) ) ) ) ) ) ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl816]) ).
thf(zip_derived_cl818,plain,
! [X2: $i,X4: $i] :
( ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( ( l1_orders_2 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( !!
@ ^ [Y3: $i] :
( ( ( m2_relset_1 @ Y3 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_2 @ Y3 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) )
& ( v1_funct_1 @ Y3 ) )
=> ( ( ( r4_waybel_0 @ X4 @ Y0 @ Y3 @ ( k4_pre_topc @ X2 @ X4 @ Y2 @ Y1 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y2 @ Y1 ) )
=> ( r4_waybel_0 @ X2 @ Y0 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ Y0 ) @ Y2 @ Y3 ) @ Y1 ) ) ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl817]) ).
thf(zip_derived_cl819,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( ( ( l1_orders_2 @ X6 )
& ( (~) @ ( v3_struct_0 @ X6 ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y2 @ ( k4_pre_topc @ X2 @ X4 @ Y1 @ Y0 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ Y1 @ Y2 ) @ Y0 ) ) ) ) ) ) ) ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl818]) ).
thf(zip_derived_cl820,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( ( l1_orders_2 @ X6 )
& ( (~) @ ( v3_struct_0 @ X6 ) ) )
| ( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y2 @ ( k4_pre_topc @ X2 @ X4 @ Y1 @ Y0 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ Y1 @ Y2 ) @ Y0 ) ) ) ) ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl819]) ).
thf(zip_derived_cl821,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( !!
@ ^ [Y2: $i] :
( ( ( m2_relset_1 @ Y2 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y2 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y2 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y2 @ ( k4_pre_topc @ X2 @ X4 @ Y1 @ Y0 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ Y1 @ Y2 ) @ Y0 ) ) ) ) ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl820]) ).
thf(zip_derived_cl822,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( ( m1_subset_1 @ X8 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y1 @ ( k4_pre_topc @ X2 @ X4 @ Y0 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y0 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ Y0 @ Y1 ) @ X8 ) ) ) ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl821]) ).
thf(zip_derived_cl263_018,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl823,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ( ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y1 @ ( k4_pre_topc @ X2 @ X4 @ Y0 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y0 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ Y0 @ Y1 ) @ X8 ) ) ) ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 ) ),
inference(demod,[status(thm)],[zip_derived_cl822,zip_derived_cl263]) ).
thf(zip_derived_cl824,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( !!
@ ^ [Y1: $i] :
( ( ( m2_relset_1 @ Y1 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y1 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y1 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y1 @ ( k4_pre_topc @ X2 @ X4 @ Y0 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ Y0 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ Y0 @ Y1 ) @ X8 ) ) ) ) ) )
| ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl823]) ).
thf(zip_derived_cl825,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( ( ( m2_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X10 ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y0 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ Y0 ) @ X8 ) ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl824]) ).
thf(zip_derived_cl330_019,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl826,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( ( ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X10 ) )
=> ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y0 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ Y0 ) @ X8 ) ) ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl825,zip_derived_cl330]) ).
thf(zip_derived_cl827,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
& ( v1_funct_1 @ X10 ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y0 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ Y0 ) @ X8 ) ) ) )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl826]) ).
thf(zip_derived_cl828,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X10 )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ( !!
@ ^ [Y0: $i] :
( ( ( m2_relset_1 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ Y0 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ Y0 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ Y0 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ Y0 ) @ X8 ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl827]) ).
thf(zip_derived_cl829,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ( ( ( m2_relset_1 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ X12 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ X12 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ X12 ) @ X8 ) ) )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl828]) ).
thf(zip_derived_cl330_020,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl830,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ( ( ( m1_relset_1 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ X12 ) )
=> ( ( ( r4_waybel_0 @ X4 @ X6 @ X12 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ X12 ) @ X8 ) ) )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl829,zip_derived_cl330]) ).
thf(zip_derived_cl831,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( ( m1_relset_1 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_2 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
& ( v1_funct_1 @ X12 ) )
| ( ( ( r4_waybel_0 @ X4 @ X6 @ X12 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ X12 ) @ X8 ) )
| ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X10 )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl830]) ).
thf(zip_derived_cl832,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( m1_relset_1 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
| ~ ( v1_funct_2 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
| ~ ( v1_funct_1 @ X12 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ( ( ( r4_waybel_0 @ X4 @ X6 @ X12 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
=> ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ X12 ) @ X8 ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl831]) ).
thf(zip_derived_cl833,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( ( r4_waybel_0 @ X4 @ X6 @ X12 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
& ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 ) )
| ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ X12 ) @ X8 )
| ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X10 )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X6 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ~ ( v1_funct_1 @ X12 )
| ~ ( v1_funct_2 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
| ~ ( m1_relset_1 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl832]) ).
thf(zip_derived_cl834,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i,X12: $i] :
( ~ ( r4_waybel_0 @ X4 @ X6 @ X12 @ ( k4_pre_topc @ X2 @ X4 @ X10 @ X8 ) )
| ~ ( r4_waybel_0 @ X2 @ X4 @ X10 @ X8 )
| ~ ( m1_relset_1 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
| ~ ( v1_funct_2 @ X12 @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) )
| ~ ( v1_funct_1 @ X12 )
| ~ ( r1_tarski @ X8 @ ( u1_struct_0 @ X2 ) )
| ~ ( l1_orders_2 @ X6 )
| ( v3_struct_0 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( m1_relset_1 @ X10 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ( r4_waybel_0 @ X2 @ X6 @ ( k7_funct_2 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) @ ( u1_struct_0 @ X6 ) @ X10 @ X12 ) @ X8 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl833]) ).
thf(zip_derived_cl1025,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( r4_waybel_0 @ '#sk2' @ X2 @ X1 @ ( k9_relat_1 @ '#sk4' @ X0 ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
| ~ ( m1_relset_1 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ X2 ) )
| ~ ( v1_funct_2 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ X2 ) )
| ~ ( v1_funct_1 @ X1 )
| ~ ( r1_tarski @ X0 @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ '#sk1' )
| ( v3_struct_0 @ '#sk1' )
| ( v3_struct_0 @ '#sk2' )
| ~ ( l1_orders_2 @ '#sk2' )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ( r4_waybel_0 @ '#sk1' @ X2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ X2 ) @ '#sk4' @ X1 ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl730,zip_derived_cl834]) ).
thf(zip_derived_cl72_021,plain,
l1_orders_2 @ '#sk1',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl73,plain,
~ ( v3_struct_0 @ '#sk1' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl78_022,plain,
~ ( v3_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl77_023,plain,
l1_orders_2 @ '#sk2',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl89_024,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl88_025,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl331_026,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl1027,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( r4_waybel_0 @ '#sk2' @ X2 @ X1 @ ( k9_relat_1 @ '#sk4' @ X0 ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
| ~ ( m1_relset_1 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ X2 ) )
| ~ ( v1_funct_2 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ X2 ) )
| ~ ( v1_funct_1 @ X1 )
| ~ ( r1_tarski @ X0 @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( r4_waybel_0 @ '#sk1' @ X2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ X2 ) @ '#sk4' @ X1 ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl1025,zip_derived_cl72,zip_derived_cl73,zip_derived_cl78,zip_derived_cl77,zip_derived_cl89,zip_derived_cl88,zip_derived_cl331]) ).
thf(zip_derived_cl2952,plain,
! [X0: $i] :
( ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ X0 ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
| ~ ( m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ '#sk5' )
| ~ ( r1_tarski @ X0 @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( l1_orders_2 @ '#sk3' )
| ( v3_struct_0 @ '#sk3' )
| ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1134,zip_derived_cl1027]) ).
thf(zip_derived_cl332_027,plain,
m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl93]) ).
thf(zip_derived_cl94_028,plain,
v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl95_029,plain,
v1_funct_1 @ '#sk5',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl82_030,plain,
l1_orders_2 @ '#sk3',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl83_031,plain,
~ ( v3_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl2953,plain,
! [X0: $i] :
( ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ X0 ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X0 )
| ~ ( r1_tarski @ X0 @ ( u1_struct_0 @ '#sk1' ) )
| ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl2952,zip_derived_cl332,zip_derived_cl94,zip_derived_cl95,zip_derived_cl82,zip_derived_cl83]) ).
thf(zip_derived_cl94_032,plain,
v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl88_033,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(dt_k7_funct_2,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( m1_relset_1 @ E @ B @ C )
& ( v1_funct_2 @ E @ B @ C )
& ( v1_funct_1 @ E )
& ( m1_relset_1 @ D @ A @ B )
& ( v1_funct_2 @ D @ A @ B )
& ( v1_funct_1 @ D )
& ~ ( v1_xboole_0 @ B ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ A @ B @ C @ D @ E ) @ A @ C )
& ( v1_funct_2 @ ( k7_funct_2 @ A @ B @ C @ D @ E ) @ A @ C )
& ( v1_funct_1 @ ( k7_funct_2 @ A @ B @ C @ D @ E ) ) ) ) ).
thf(zip_derived_cl28,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( !!
@ ^ [Y3: $i] :
( !!
@ ^ [Y4: $i] :
( ( ( m1_relset_1 @ Y4 @ Y1 @ Y2 )
& ( v1_funct_2 @ Y4 @ Y1 @ Y2 )
& ( v1_funct_1 @ Y4 )
& ( m1_relset_1 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_2 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_1 @ Y3 )
& ( (~) @ ( v1_xboole_0 @ Y1 ) ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ Y0 @ Y1 @ Y2 @ Y3 @ Y4 ) @ Y0 @ Y2 )
& ( v1_funct_2 @ ( k7_funct_2 @ Y0 @ Y1 @ Y2 @ Y3 @ Y4 ) @ Y0 @ Y2 )
& ( v1_funct_1 @ ( k7_funct_2 @ Y0 @ Y1 @ Y2 @ Y3 @ Y4 ) ) ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[dt_k7_funct_2]) ).
thf(zip_derived_cl567,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( !!
@ ^ [Y3: $i] :
( ( ( m1_relset_1 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_2 @ Y3 @ Y0 @ Y1 )
& ( v1_funct_1 @ Y3 )
& ( m1_relset_1 @ Y2 @ X2 @ Y0 )
& ( v1_funct_2 @ Y2 @ X2 @ Y0 )
& ( v1_funct_1 @ Y2 )
& ( (~) @ ( v1_xboole_0 @ Y0 ) ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ X2 @ Y0 @ Y1 @ Y2 @ Y3 ) @ X2 @ Y1 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ Y0 @ Y1 @ Y2 @ Y3 ) @ X2 @ Y1 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ Y0 @ Y1 @ Y2 @ Y3 ) ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl28]) ).
thf(zip_derived_cl568,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( ( m1_relset_1 @ Y2 @ X4 @ Y0 )
& ( v1_funct_2 @ Y2 @ X4 @ Y0 )
& ( v1_funct_1 @ Y2 )
& ( m1_relset_1 @ Y1 @ X2 @ X4 )
& ( v1_funct_2 @ Y1 @ X2 @ X4 )
& ( v1_funct_1 @ Y1 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ Y0 @ Y1 @ Y2 ) @ X2 @ Y0 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ Y0 @ Y1 @ Y2 ) @ X2 @ Y0 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ Y0 @ Y1 @ Y2 ) ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl567]) ).
thf(zip_derived_cl569,plain,
! [X2: $i,X4: $i,X6: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( ( m1_relset_1 @ Y1 @ X4 @ X6 )
& ( v1_funct_2 @ Y1 @ X4 @ X6 )
& ( v1_funct_1 @ Y1 )
& ( m1_relset_1 @ Y0 @ X2 @ X4 )
& ( v1_funct_2 @ Y0 @ X2 @ X4 )
& ( v1_funct_1 @ Y0 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ Y0 @ Y1 ) @ X2 @ X6 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ Y0 @ Y1 ) @ X2 @ X6 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ Y0 @ Y1 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl568]) ).
thf(zip_derived_cl570,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i] :
( !!
@ ^ [Y0: $i] :
( ( ( m1_relset_1 @ Y0 @ X4 @ X6 )
& ( v1_funct_2 @ Y0 @ X4 @ X6 )
& ( v1_funct_1 @ Y0 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ Y0 ) @ X2 @ X6 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ Y0 ) @ X2 @ X6 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ Y0 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl569]) ).
thf(zip_derived_cl571,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( ( m1_relset_1 @ X10 @ X4 @ X6 )
& ( v1_funct_2 @ X10 @ X4 @ X6 )
& ( v1_funct_1 @ X10 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( m2_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl570]) ).
thf(zip_derived_cl330_034,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl572,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( ( m1_relset_1 @ X10 @ X4 @ X6 )
& ( v1_funct_2 @ X10 @ X4 @ X6 )
& ( v1_funct_1 @ X10 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
=> ( ( m1_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl571,zip_derived_cl330]) ).
thf(zip_derived_cl573,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( ( m1_relset_1 @ X10 @ X4 @ X6 )
& ( v1_funct_2 @ X10 @ X4 @ X6 )
& ( v1_funct_1 @ X10 )
& ( m1_relset_1 @ X8 @ X2 @ X4 )
& ( v1_funct_2 @ X8 @ X2 @ X4 )
& ( v1_funct_1 @ X8 )
& ( (~) @ ( v1_xboole_0 @ X4 ) ) )
| ( ( m1_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl572]) ).
thf(zip_derived_cl574,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ~ ( m1_relset_1 @ X10 @ X4 @ X6 )
| ~ ( v1_funct_2 @ X10 @ X4 @ X6 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( m1_relset_1 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_2 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_1 @ X8 )
| ( v1_xboole_0 @ X4 )
| ( ( m1_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
& ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl573]) ).
thf(zip_derived_cl575,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( m1_relset_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
| ( v1_xboole_0 @ X4 )
| ~ ( v1_funct_1 @ X8 )
| ~ ( v1_funct_2 @ X8 @ X2 @ X4 )
| ~ ( m1_relset_1 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ X4 @ X6 )
| ~ ( m1_relset_1 @ X10 @ X4 @ X6 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl574]) ).
thf(zip_derived_cl578,plain,
! [X0: $i,X1: $i] :
( ( m1_relset_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ X0 @ '#sk4' @ X1 ) @ ( u1_struct_0 @ '#sk1' ) @ X0 )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X1 )
| ~ ( v1_funct_2 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 )
| ~ ( m1_relset_1 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl575]) ).
thf(zip_derived_cl89_035,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl331_036,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl580,plain,
! [X0: $i,X1: $i] :
( ( m1_relset_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ X0 @ '#sk4' @ X1 ) @ ( u1_struct_0 @ '#sk1' ) @ X0 )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X1 )
| ~ ( v1_funct_2 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 )
| ~ ( m1_relset_1 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl578,zip_derived_cl89,zip_derived_cl331]) ).
thf(zip_derived_cl584,plain,
( ( m1_relset_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk5' )
| ~ ( m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl580]) ).
thf(zip_derived_cl95_037,plain,
v1_funct_1 @ '#sk5',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl332_038,plain,
m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl93]) ).
thf(zip_derived_cl585,plain,
( ( m1_relset_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl584,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl482_039,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl481]) ).
thf(zip_derived_cl2360,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ~ ( l1_orders_2 @ '#sk1' )
| ( v3_struct_0 @ '#sk1' )
| ( v3_struct_0 @ '#sk3' )
| ~ ( l1_orders_2 @ '#sk3' )
| ( ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ Y0 ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl585,zip_derived_cl482]) ).
thf(zip_derived_cl72_040,plain,
l1_orders_2 @ '#sk1',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl73_041,plain,
~ ( v3_struct_0 @ '#sk1' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl83_042,plain,
~ ( v3_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl82_043,plain,
l1_orders_2 @ '#sk3',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl97,plain,
~ ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl92]) ).
thf(zip_derived_cl2363,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ~ ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ Y0 ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2360,zip_derived_cl72,zip_derived_cl73,zip_derived_cl83,zip_derived_cl82,zip_derived_cl97]) ).
thf(zip_derived_cl94_044,plain,
v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl88_045,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl577,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( v1_funct_1 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) )
| ( v1_xboole_0 @ X4 )
| ~ ( v1_funct_1 @ X8 )
| ~ ( v1_funct_2 @ X8 @ X2 @ X4 )
| ~ ( m1_relset_1 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ X4 @ X6 )
| ~ ( m1_relset_1 @ X10 @ X4 @ X6 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl574]) ).
thf(zip_derived_cl601,plain,
! [X0: $i,X1: $i] :
( ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ X1 @ '#sk4' @ X0 ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X0 )
| ~ ( v1_funct_2 @ X0 @ ( u1_struct_0 @ '#sk2' ) @ X1 )
| ~ ( m1_relset_1 @ X0 @ ( u1_struct_0 @ '#sk2' ) @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl577]) ).
thf(zip_derived_cl89_046,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl331_047,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl603,plain,
! [X0: $i,X1: $i] :
( ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ X1 @ '#sk4' @ X0 ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X0 )
| ~ ( v1_funct_2 @ X0 @ ( u1_struct_0 @ '#sk2' ) @ X1 )
| ~ ( m1_relset_1 @ X0 @ ( u1_struct_0 @ '#sk2' ) @ X1 ) ),
inference(demod,[status(thm)],[zip_derived_cl601,zip_derived_cl89,zip_derived_cl331]) ).
thf(zip_derived_cl2420,plain,
( ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk5' )
| ~ ( m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl603]) ).
thf(zip_derived_cl95_048,plain,
v1_funct_1 @ '#sk5',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl332_049,plain,
m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl93]) ).
thf(zip_derived_cl2421,plain,
( ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2420,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl5066,plain,
( ~ ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ Y0 ) ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl2363,zip_derived_cl2421]) ).
thf(zip_derived_cl5067,plain,
( ~ ( ( ( m1_subset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl5066]) ).
thf(zip_derived_cl263_050,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl5068,plain,
( ~ ( ( ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
& ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl5067,zip_derived_cl263]) ).
thf(zip_derived_cl5070,plain,
( ~ ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl5068]) ).
thf(zip_derived_cl6048,plain,
( ~ ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2953,zip_derived_cl5070]) ).
thf(zip_derived_cl585_051,plain,
( ( m1_relset_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl584,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl482_052,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl481]) ).
thf(zip_derived_cl486,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( v4_waybel34 @ X6 @ X2 @ X4 )
| ~ ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ~ ( v1_funct_1 @ X6 )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(eq_elim,[status(thm)],[zip_derived_cl482]) ).
thf(zip_derived_cl1842,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( ( ( m1_subset_1 @ ( '#sk19' @ X2 @ X4 @ X6 ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ ( '#sk19' @ X2 @ X4 @ X6 ) ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ ( '#sk19' @ X2 @ X4 @ X6 ) ) )
| ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( v4_waybel34 @ X6 @ X2 @ X4 ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl486]) ).
thf(zip_derived_cl263_053,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl1843,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( ( ( r1_tarski @ ( '#sk19' @ X2 @ X4 @ X6 ) @ ( u1_struct_0 @ X2 ) )
& ( v1_finset_1 @ ( '#sk19' @ X2 @ X4 @ X6 ) ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ ( '#sk19' @ X2 @ X4 @ X6 ) ) )
| ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( v4_waybel34 @ X6 @ X2 @ X4 ) ),
inference(demod,[status(thm)],[zip_derived_cl1842,zip_derived_cl263]) ).
thf(zip_derived_cl1844,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( ( r1_tarski @ ( '#sk19' @ X2 @ X4 @ X6 ) @ ( u1_struct_0 @ X2 ) )
& ( v1_finset_1 @ ( '#sk19' @ X2 @ X4 @ X6 ) ) )
| ( v4_waybel34 @ X6 @ X2 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( v3_struct_0 @ X4 )
| ( v3_struct_0 @ X2 )
| ~ ( l1_orders_2 @ X2 )
| ~ ( v1_funct_1 @ X6 )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl1843]) ).
thf(zip_derived_cl1846,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( r1_tarski @ ( '#sk19' @ X2 @ X4 @ X6 ) @ ( u1_struct_0 @ X2 ) )
| ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( v4_waybel34 @ X6 @ X2 @ X4 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl1844]) ).
thf(zip_derived_cl4303,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ~ ( l1_orders_2 @ '#sk1' )
| ( v3_struct_0 @ '#sk1' )
| ( v3_struct_0 @ '#sk3' )
| ~ ( l1_orders_2 @ '#sk3' )
| ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl585,zip_derived_cl1846]) ).
thf(zip_derived_cl72_054,plain,
l1_orders_2 @ '#sk1',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl73_055,plain,
~ ( v3_struct_0 @ '#sk1' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl83_056,plain,
~ ( v3_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl82_057,plain,
l1_orders_2 @ '#sk3',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl97_058,plain,
~ ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl92]) ).
thf(zip_derived_cl4309,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl4303,zip_derived_cl72,zip_derived_cl73,zip_derived_cl83,zip_derived_cl82,zip_derived_cl97]) ).
thf(zip_derived_cl94_059,plain,
v1_funct_2 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl88_060,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl576,plain,
! [X2: $i,X4: $i,X6: $i,X8: $i,X10: $i] :
( ( v1_funct_2 @ ( k7_funct_2 @ X2 @ X4 @ X6 @ X8 @ X10 ) @ X2 @ X6 )
| ( v1_xboole_0 @ X4 )
| ~ ( v1_funct_1 @ X8 )
| ~ ( v1_funct_2 @ X8 @ X2 @ X4 )
| ~ ( m1_relset_1 @ X8 @ X2 @ X4 )
| ~ ( v1_funct_1 @ X10 )
| ~ ( v1_funct_2 @ X10 @ X4 @ X6 )
| ~ ( m1_relset_1 @ X10 @ X4 @ X6 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl574]) ).
thf(zip_derived_cl605,plain,
! [X0: $i,X1: $i] :
( ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ X0 @ '#sk4' @ X1 ) @ ( u1_struct_0 @ '#sk1' ) @ X0 )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X1 )
| ~ ( v1_funct_2 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 )
| ~ ( m1_relset_1 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl88,zip_derived_cl576]) ).
thf(zip_derived_cl89_061,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl331_062,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl607,plain,
! [X0: $i,X1: $i] :
( ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ X0 @ '#sk4' @ X1 ) @ ( u1_struct_0 @ '#sk1' ) @ X0 )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ X1 )
| ~ ( v1_funct_2 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 )
| ~ ( m1_relset_1 @ X1 @ ( u1_struct_0 @ '#sk2' ) @ X0 ) ),
inference(demod,[status(thm)],[zip_derived_cl605,zip_derived_cl89,zip_derived_cl331]) ).
thf(zip_derived_cl2476,plain,
( ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk5' )
| ~ ( m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl94,zip_derived_cl607]) ).
thf(zip_derived_cl95_063,plain,
v1_funct_1 @ '#sk5',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl91]) ).
thf(zip_derived_cl332_064,plain,
m1_relset_1 @ '#sk5' @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl93]) ).
thf(zip_derived_cl2477,plain,
( ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2476,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl7104,plain,
( ~ ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl4309,zip_derived_cl2477]) ).
thf(zip_derived_cl2421_065,plain,
( ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2420,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl7105,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl7104,zip_derived_cl2421]) ).
thf(zip_derived_cl10799,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl6048,zip_derived_cl7105]) ).
thf(zip_derived_cl2477_066,plain,
( ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2476,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl10800,plain,
( ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl10799,zip_derived_cl2477]) ).
thf(zip_derived_cl1026_067,plain,
! [X0: $i] : ( r1_tarski @ ( k9_relat_1 @ '#sk4' @ X0 ) @ ( u1_struct_0 @ '#sk2' ) ),
inference(demod,[status(thm)],[zip_derived_cl1024,zip_derived_cl331,zip_derived_cl88,zip_derived_cl89,zip_derived_cl127,zip_derived_cl126]) ).
thf(cc2_finset_1,axiom,
! [A: $i] :
( ( v1_finset_1 @ A )
=> ! [B: $i] :
( ( m1_subset_1 @ B @ ( k1_zfmisc_1 @ A ) )
=> ( v1_finset_1 @ B ) ) ) ).
thf(zip_derived_cl17,plain,
( !!
@ ^ [Y0: $i] :
( ( v1_finset_1 @ Y0 )
=> ( !!
@ ^ [Y1: $i] :
( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ Y0 ) )
=> ( v1_finset_1 @ Y1 ) ) ) ) ),
inference(cnf,[status(esa)],[cc2_finset_1]) ).
thf(zip_derived_cl381,plain,
! [X2: $i] :
( ( v1_finset_1 @ X2 )
=> ( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ X2 ) )
=> ( v1_finset_1 @ Y0 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl17]) ).
thf(zip_derived_cl382,plain,
! [X2: $i] :
( ~ ( v1_finset_1 @ X2 )
| ( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ X2 ) )
=> ( v1_finset_1 @ Y0 ) ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl381]) ).
thf(zip_derived_cl383,plain,
! [X2: $i,X4: $i] :
( ( ( m1_subset_1 @ X4 @ ( k1_zfmisc_1 @ X2 ) )
=> ( v1_finset_1 @ X4 ) )
| ~ ( v1_finset_1 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl382]) ).
thf(zip_derived_cl263_068,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl384,plain,
! [X2: $i,X4: $i] :
( ( ( r1_tarski @ X4 @ X2 )
=> ( v1_finset_1 @ X4 ) )
| ~ ( v1_finset_1 @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl383,zip_derived_cl263]) ).
thf(zip_derived_cl385,plain,
! [X2: $i,X4: $i] :
( ~ ( r1_tarski @ X4 @ X2 )
| ( v1_finset_1 @ X4 )
| ~ ( v1_finset_1 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl384]) ).
thf(zip_derived_cl1117,plain,
! [X0: $i] :
( ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ X0 ) )
| ~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl1026,zip_derived_cl385]) ).
thf(zip_derived_cl10802,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl10800,zip_derived_cl1117]) ).
thf(zip_derived_cl10814,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2684,zip_derived_cl10802]) ).
thf(zip_derived_cl10815,plain,
( ~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl10814]) ).
thf(zip_derived_cl2684_069,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl7105_070,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl7104,zip_derived_cl2421]) ).
thf(zip_derived_cl7142,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2684,zip_derived_cl7105]) ).
thf(zip_derived_cl7143,plain,
( ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl7142]) ).
thf(zip_derived_cl331_071,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl482_072,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl481]) ).
thf(zip_derived_cl483,plain,
( ~ ( v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( l1_orders_2 @ '#sk1' )
| ( v3_struct_0 @ '#sk1' )
| ( v3_struct_0 @ '#sk2' )
| ~ ( l1_orders_2 @ '#sk2' )
| ( ( v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ Y0 ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl331,zip_derived_cl482]) ).
thf(zip_derived_cl88_073,plain,
v1_funct_2 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl89_074,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl72_075,plain,
l1_orders_2 @ '#sk1',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl73_076,plain,
~ ( v3_struct_0 @ '#sk1' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl78_077,plain,
~ ( v3_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl77_078,plain,
l1_orders_2 @ '#sk2',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl99,plain,
v4_waybel34 @ '#sk4' @ '#sk1' @ '#sk2',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl96]) ).
thf(zip_derived_cl488,plain,
( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ Y0 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl483,zip_derived_cl88,zip_derived_cl89,zip_derived_cl72,zip_derived_cl73,zip_derived_cl78,zip_derived_cl77,zip_derived_cl99]) ).
thf(zip_derived_cl521,plain,
! [X2: $i] :
( ( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ X2 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl488]) ).
thf(zip_derived_cl263_079,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl522,plain,
! [X2: $i] :
( ( ( r1_tarski @ X2 @ ( u1_struct_0 @ '#sk1' ) )
& ( v1_finset_1 @ X2 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X2 ) ),
inference(demod,[status(thm)],[zip_derived_cl521,zip_derived_cl263]) ).
thf(zip_derived_cl523,plain,
! [X2: $i] :
( ~ ( ( r1_tarski @ X2 @ ( u1_struct_0 @ '#sk1' ) )
& ( v1_finset_1 @ X2 ) )
| ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl522]) ).
thf(zip_derived_cl524,plain,
! [X2: $i] :
( ~ ( r1_tarski @ X2 @ ( u1_struct_0 @ '#sk1' ) )
| ~ ( v1_finset_1 @ X2 )
| ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ X2 ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl523]) ).
thf(zip_derived_cl7179,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl7143,zip_derived_cl524]) ).
thf(zip_derived_cl2684_080,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl585_081,plain,
( ( m1_relset_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl584,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl2996,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( m1_relset_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2684,zip_derived_cl585]) ).
thf(zip_derived_cl2998,plain,
( ( m1_relset_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl2996]) ).
thf(zip_derived_cl482_082,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( m1_relset_1 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_2 @ X6 @ ( u1_struct_0 @ X2 ) @ ( u1_struct_0 @ X4 ) )
| ~ ( v1_funct_1 @ X6 )
| ~ ( l1_orders_2 @ X2 )
| ( v3_struct_0 @ X2 )
| ( v3_struct_0 @ X4 )
| ~ ( l1_orders_2 @ X4 )
| ( ( v4_waybel34 @ X6 @ X2 @ X4 )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ X2 ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ X2 @ X4 @ X6 @ Y0 ) ) ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl481]) ).
thf(zip_derived_cl3024,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) )
| ~ ( l1_orders_2 @ '#sk1' )
| ( v3_struct_0 @ '#sk1' )
| ( v3_struct_0 @ '#sk3' )
| ~ ( l1_orders_2 @ '#sk3' )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ Y0 ) ) ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2998,zip_derived_cl482]) ).
thf(zip_derived_cl72_083,plain,
l1_orders_2 @ '#sk1',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl73_084,plain,
~ ( v3_struct_0 @ '#sk1' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl70]) ).
thf(zip_derived_cl83_085,plain,
~ ( v3_struct_0 @ '#sk3' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl82_086,plain,
l1_orders_2 @ '#sk3',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl80]) ).
thf(zip_derived_cl3027,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_funct_2 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ~ ( v1_funct_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ Y0 ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl3024,zip_derived_cl72,zip_derived_cl73,zip_derived_cl83,zip_derived_cl82]) ).
thf(zip_derived_cl2684_087,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl2477_088,plain,
( ( v1_funct_2 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2476,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl5121,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v1_funct_2 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2684,zip_derived_cl2477]) ).
thf(zip_derived_cl5122,plain,
( ( v1_funct_2 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk3' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl5121]) ).
thf(zip_derived_cl6238,plain,
( ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ Y0 ) ) ) )
| ~ ( v1_funct_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl3027,zip_derived_cl5122]) ).
thf(zip_derived_cl2684_089,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl2421_090,plain,
( ( v1_funct_1 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2420,zip_derived_cl95,zip_derived_cl332]) ).
thf(zip_derived_cl2997,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v1_funct_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl2684,zip_derived_cl2421]) ).
thf(zip_derived_cl2999,plain,
( ( v1_funct_1 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl2997]) ).
thf(zip_derived_cl6239,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( !!
@ ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ Y0 ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl6238,zip_derived_cl2999]) ).
thf(zip_derived_cl6241,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( ^ [Y0: $i] :
( ( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ Y0 ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ Y0 ) )
@ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ) ),
inference(quantifier_rw,[status(thm)],[zip_derived_cl6239]) ).
thf(zip_derived_cl6242,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( ( ( m1_subset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) @ ( k1_zfmisc_1 @ ( u1_struct_0 @ '#sk1' ) ) )
& ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ) ) ),
inference(rw,[status(thm)],[zip_derived_cl6241]) ).
thf(zip_derived_cl263_091,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl6243,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( ( ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
& ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ) ) ),
inference(demod,[status(thm)],[zip_derived_cl6242,zip_derived_cl263]) ).
thf(zip_derived_cl6250,plain,
( ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' )
= ( ( ( r1_tarski @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) @ ( u1_struct_0 @ '#sk1' ) )
& $false )
=> ( r4_waybel_0 @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ) ) ),
inference(bool_hoist,[status(thm)],[zip_derived_cl6243]) ).
thf(zip_derived_cl6251,plain,
( ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ) ),
inference('simplify boolean subterms',[status(thm)],[zip_derived_cl6250]) ).
thf(zip_derived_cl2684_092,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl97_093,plain,
~ ( v4_waybel34 @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl92]) ).
thf(zip_derived_cl2995,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v4_waybel34 @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) @ '#sk1' @ '#sk3' ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2684,zip_derived_cl97]) ).
thf(zip_derived_cl6256,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl6251,zip_derived_cl2995]) ).
thf(zip_derived_cl9440,plain,
( ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl7179,zip_derived_cl6256]) ).
thf(zip_derived_cl10816,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl10815,zip_derived_cl9440]) ).
thf(fc1_struct_0,axiom,
! [A: $i] :
( ( ( l1_struct_0 @ A )
& ~ ( v3_struct_0 @ A ) )
=> ~ ( v1_xboole_0 @ ( u1_struct_0 @ A ) ) ) ).
thf(zip_derived_cl44,plain,
( !!
@ ^ [Y0: $i] :
( ( ( l1_struct_0 @ Y0 )
& ( (~) @ ( v3_struct_0 @ Y0 ) ) )
=> ( (~) @ ( v1_xboole_0 @ ( u1_struct_0 @ Y0 ) ) ) ) ),
inference(cnf,[status(esa)],[fc1_struct_0]) ).
thf(zip_derived_cl371,plain,
! [X2: $i] :
( ( ( l1_struct_0 @ X2 )
& ( (~) @ ( v3_struct_0 @ X2 ) ) )
=> ( (~) @ ( v1_xboole_0 @ ( u1_struct_0 @ X2 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl44]) ).
thf(zip_derived_cl372,plain,
! [X2: $i] :
( ~ ( ( l1_struct_0 @ X2 )
& ( (~) @ ( v3_struct_0 @ X2 ) ) )
| ~ ( v1_xboole_0 @ ( u1_struct_0 @ X2 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl371]) ).
thf(zip_derived_cl373,plain,
! [X2: $i] :
( ~ ( l1_struct_0 @ X2 )
| ( v3_struct_0 @ X2 )
| ~ ( v1_xboole_0 @ ( u1_struct_0 @ X2 ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl372]) ).
thf(zip_derived_cl10841,plain,
( ~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( l1_struct_0 @ '#sk2' )
| ( v3_struct_0 @ '#sk2' ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl10816,zip_derived_cl373]) ).
thf(zip_derived_cl127_094,plain,
l1_struct_0 @ '#sk2',
inference('s_sup+',[status(thm)],[zip_derived_cl125,zip_derived_cl77]) ).
thf(zip_derived_cl78_095,plain,
~ ( v3_struct_0 @ '#sk2' ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl75]) ).
thf(zip_derived_cl10887,plain,
~ ( v1_finset_1 @ ( u1_struct_0 @ '#sk2' ) ),
inference(demod,[status(thm)],[zip_derived_cl10841,zip_derived_cl127,zip_derived_cl78]) ).
thf(fc13_finset_1,axiom,
! [A: $i,B: $i] :
( ( ( v1_finset_1 @ B )
& ( v1_funct_1 @ A )
& ( v1_relat_1 @ A ) )
=> ( v1_finset_1 @ ( k9_relat_1 @ A @ B ) ) ) ).
thf(zip_derived_cl41,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( ( v1_finset_1 @ Y1 )
& ( v1_funct_1 @ Y0 )
& ( v1_relat_1 @ Y0 ) )
=> ( v1_finset_1 @ ( k9_relat_1 @ Y0 @ Y1 ) ) ) ) ),
inference(cnf,[status(esa)],[fc13_finset_1]) ).
thf(zip_derived_cl461,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( ( ( v1_finset_1 @ Y0 )
& ( v1_funct_1 @ X2 )
& ( v1_relat_1 @ X2 ) )
=> ( v1_finset_1 @ ( k9_relat_1 @ X2 @ Y0 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl41]) ).
thf(zip_derived_cl462,plain,
! [X2: $i,X4: $i] :
( ( ( v1_finset_1 @ X4 )
& ( v1_funct_1 @ X2 )
& ( v1_relat_1 @ X2 ) )
=> ( v1_finset_1 @ ( k9_relat_1 @ X2 @ X4 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl461]) ).
thf(zip_derived_cl463,plain,
! [X2: $i,X4: $i] :
( ~ ( ( v1_finset_1 @ X4 )
& ( v1_funct_1 @ X2 )
& ( v1_relat_1 @ X2 ) )
| ( v1_finset_1 @ ( k9_relat_1 @ X2 @ X4 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl462]) ).
thf(zip_derived_cl464,plain,
! [X2: $i,X4: $i] :
( ~ ( v1_finset_1 @ X4 )
| ~ ( v1_funct_1 @ X2 )
| ~ ( v1_relat_1 @ X2 )
| ( v1_finset_1 @ ( k9_relat_1 @ X2 @ X4 ) ) ),
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl463]) ).
thf(zip_derived_cl2684_096,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' )
= ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl2681,zip_derived_cl88,zip_derived_cl89]) ).
thf(zip_derived_cl10800_097,plain,
( ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k7_funct_2 @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ) @ ( u1_struct_0 @ '#sk3' ) @ '#sk4' @ '#sk5' ) ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl10799,zip_derived_cl2477]) ).
thf(zip_derived_cl10808,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl2684,zip_derived_cl10800]) ).
thf(zip_derived_cl10811,plain,
( ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) )
| ~ ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(simplify,[status(thm)],[zip_derived_cl10808]) ).
thf(zip_derived_cl9440_098,plain,
( ( r4_waybel_0 @ '#sk1' @ '#sk2' @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(clc,[status(thm)],[zip_derived_cl7179,zip_derived_cl6256]) ).
thf(zip_derived_cl11910,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ~ ( v1_finset_1 @ ( k9_relat_1 @ '#sk4' @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl10811,zip_derived_cl9440]) ).
thf(zip_derived_cl11913,plain,
( ~ ( v1_relat_1 @ '#sk4' )
| ~ ( v1_funct_1 @ '#sk4' )
| ~ ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl464,zip_derived_cl11910]) ).
thf(dt_m2_relset_1,axiom,
! [A: $i,B: $i,C: $i] :
( ( m2_relset_1 @ C @ A @ B )
=> ( m1_subset_1 @ C @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ A @ B ) ) ) ) ).
thf(zip_derived_cl34,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( m2_relset_1 @ Y2 @ Y0 @ Y1 )
=> ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ Y0 @ Y1 ) ) ) ) ) ) ),
inference(cnf,[status(esa)],[dt_m2_relset_1]) ).
thf(zip_derived_cl441,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( m2_relset_1 @ Y1 @ X2 @ Y0 )
=> ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ X2 @ Y0 ) ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl34]) ).
thf(zip_derived_cl442,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( ( m2_relset_1 @ Y0 @ X2 @ X4 )
=> ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ X2 @ X4 ) ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl441]) ).
thf(zip_derived_cl443,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
=> ( m1_subset_1 @ X6 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ X2 @ X4 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl442]) ).
thf(zip_derived_cl330_099,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m2_relset_1 @ X6 @ X2 @ X4 )
= ( m1_relset_1 @ X6 @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl329]) ).
thf(zip_derived_cl263_100,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl444,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m1_relset_1 @ X6 @ X2 @ X4 )
=> ( r1_tarski @ X6 @ ( k2_zfmisc_1 @ X2 @ X4 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl443,zip_derived_cl330,zip_derived_cl263]) ).
thf(zip_derived_cl445,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( m1_relset_1 @ X6 @ X2 @ X4 )
| ( r1_tarski @ X6 @ ( k2_zfmisc_1 @ X2 @ X4 ) ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl444]) ).
thf(cc1_relset_1,axiom,
! [A: $i,B: $i,C: $i] :
( ( m1_subset_1 @ C @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ A @ B ) ) )
=> ( v1_relat_1 @ C ) ) ).
thf(zip_derived_cl15,plain,
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( !!
@ ^ [Y2: $i] :
( ( m1_subset_1 @ Y2 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ Y0 @ Y1 ) ) )
=> ( v1_relat_1 @ Y2 ) ) ) ) ),
inference(cnf,[status(esa)],[cc1_relset_1]) ).
thf(zip_derived_cl361,plain,
! [X2: $i] :
( !!
@ ^ [Y0: $i] :
( !!
@ ^ [Y1: $i] :
( ( m1_subset_1 @ Y1 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ X2 @ Y0 ) ) )
=> ( v1_relat_1 @ Y1 ) ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl15]) ).
thf(zip_derived_cl362,plain,
! [X2: $i,X4: $i] :
( !!
@ ^ [Y0: $i] :
( ( m1_subset_1 @ Y0 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ X2 @ X4 ) ) )
=> ( v1_relat_1 @ Y0 ) ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl361]) ).
thf(zip_derived_cl363,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( m1_subset_1 @ X6 @ ( k1_zfmisc_1 @ ( k2_zfmisc_1 @ X2 @ X4 ) ) )
=> ( v1_relat_1 @ X6 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl362]) ).
thf(zip_derived_cl263_101,plain,
! [X2: $i,X4: $i] :
( ( m1_subset_1 @ X2 @ ( k1_zfmisc_1 @ X4 ) )
= ( r1_tarski @ X2 @ X4 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl262]) ).
thf(zip_derived_cl364,plain,
! [X2: $i,X4: $i,X6: $i] :
( ( r1_tarski @ X6 @ ( k2_zfmisc_1 @ X2 @ X4 ) )
=> ( v1_relat_1 @ X6 ) ),
inference(demod,[status(thm)],[zip_derived_cl363,zip_derived_cl263]) ).
thf(zip_derived_cl365,plain,
! [X2: $i,X4: $i,X6: $i] :
( ~ ( r1_tarski @ X6 @ ( k2_zfmisc_1 @ X2 @ X4 ) )
| ( v1_relat_1 @ X6 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl364]) ).
thf(zip_derived_cl460,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( m1_relset_1 @ X2 @ X1 @ X0 )
| ( v1_relat_1 @ X2 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl445,zip_derived_cl365]) ).
thf(zip_derived_cl331_102,plain,
m1_relset_1 @ '#sk4' @ ( u1_struct_0 @ '#sk1' ) @ ( u1_struct_0 @ '#sk2' ),
inference('s_sup+',[status(thm)],[zip_derived_cl330,zip_derived_cl87]) ).
thf(zip_derived_cl1808,plain,
v1_relat_1 @ '#sk4',
inference('s_sup+',[status(thm)],[zip_derived_cl460,zip_derived_cl331]) ).
thf(zip_derived_cl89_103,plain,
v1_funct_1 @ '#sk4',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl85]) ).
thf(zip_derived_cl11916,plain,
( ~ ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) )
| ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) ) ),
inference(demod,[status(thm)],[zip_derived_cl11913,zip_derived_cl1808,zip_derived_cl89]) ).
thf(zip_derived_cl6256_104,plain,
( ( v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ) )
| ( v1_finset_1 @ ( '#sk19' @ '#sk1' @ '#sk3' @ ( k5_relat_1 @ '#sk4' @ '#sk5' ) ) ) ),
inference(clc,[status(thm)],[zip_derived_cl6251,zip_derived_cl2995]) ).
thf(zip_derived_cl11919,plain,
v1_xboole_0 @ ( u1_struct_0 @ '#sk2' ),
inference(clc,[status(thm)],[zip_derived_cl11916,zip_derived_cl6256]) ).
thf(t6_boole,axiom,
! [A: $i] :
( ( v1_xboole_0 @ A )
=> ( A = k1_xboole_0 ) ) ).
thf(zip_derived_cl66,plain,
( !!
@ ^ [Y0: $i] :
( ( v1_xboole_0 @ Y0 )
=> ( Y0 = k1_xboole_0 ) ) ),
inference(cnf,[status(esa)],[t6_boole]) ).
thf(zip_derived_cl218,plain,
! [X2: $i] :
( ( v1_xboole_0 @ X2 )
=> ( X2 = k1_xboole_0 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl66]) ).
thf(zip_derived_cl219,plain,
! [X2: $i] :
( ~ ( v1_xboole_0 @ X2 )
| ( X2 = k1_xboole_0 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl218]) ).
thf(zip_derived_cl220,plain,
! [X2: $i] :
( ~ ( v1_xboole_0 @ X2 )
| ( X2 = k1_xboole_0 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl219]) ).
thf(zip_derived_cl11983,plain,
( ( u1_struct_0 @ '#sk2' )
= k1_xboole_0 ),
inference('s_sup-',[status(thm)],[zip_derived_cl11919,zip_derived_cl220]) ).
thf(rc2_funct_1,axiom,
? [A: $i] :
( ( v1_relat_1 @ A )
& ( v1_xboole_0 @ A )
& ( v1_funct_1 @ A ) ) ).
thf(zip_derived_cl50,plain,
( ??
@ ^ [Y0: $i] :
( ( v1_relat_1 @ Y0 )
& ( v1_xboole_0 @ Y0 )
& ( v1_funct_1 @ Y0 ) ) ),
inference(cnf,[status(esa)],[rc2_funct_1]) ).
thf(zip_derived_cl230,plain,
( ( v1_relat_1 @ '#sk14' )
& ( v1_xboole_0 @ '#sk14' )
& ( v1_funct_1 @ '#sk14' ) ),
inference(lazy_cnf_exists,[status(thm)],[zip_derived_cl50]) ).
thf(zip_derived_cl232,plain,
v1_xboole_0 @ '#sk14',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl230]) ).
thf(zip_derived_cl232_105,plain,
v1_xboole_0 @ '#sk14',
inference(lazy_cnf_and,[status(thm)],[zip_derived_cl230]) ).
thf(zip_derived_cl220_106,plain,
! [X2: $i] :
( ~ ( v1_xboole_0 @ X2 )
| ( X2 = k1_xboole_0 ) ),
inference('simplify nested equalities',[status(thm)],[zip_derived_cl219]) ).
thf(zip_derived_cl235,plain,
'#sk14' = k1_xboole_0,
inference('s_sup-',[status(thm)],[zip_derived_cl232,zip_derived_cl220]) ).
thf(zip_derived_cl241,plain,
v1_xboole_0 @ k1_xboole_0,
inference(demod,[status(thm)],[zip_derived_cl232,zip_derived_cl235]) ).
thf(cc1_finset_1,axiom,
! [A: $i] :
( ( v1_xboole_0 @ A )
=> ( v1_finset_1 @ A ) ) ).
thf(zip_derived_cl12,plain,
( !!
@ ^ [Y0: $i] :
( ( v1_xboole_0 @ Y0 )
=> ( v1_finset_1 @ Y0 ) ) ),
inference(cnf,[status(esa)],[cc1_finset_1]) ).
thf(zip_derived_cl116,plain,
! [X2: $i] :
( ( v1_xboole_0 @ X2 )
=> ( v1_finset_1 @ X2 ) ),
inference(lazy_cnf_forall,[status(thm)],[zip_derived_cl12]) ).
thf(zip_derived_cl117,plain,
! [X2: $i] :
( ~ ( v1_xboole_0 @ X2 )
| ( v1_finset_1 @ X2 ) ),
inference(lazy_cnf_imply,[status(thm)],[zip_derived_cl116]) ).
thf(zip_derived_cl304,plain,
v1_finset_1 @ k1_xboole_0,
inference('s_sup-',[status(thm)],[zip_derived_cl241,zip_derived_cl117]) ).
thf(zip_derived_cl12437,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl10887,zip_derived_cl11983,zip_derived_cl304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT378+1 : TPTP v9.2.0. Released v3.4.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.9WHDHhBSPp true
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 1 14:37:23 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % Running portfolio for 300 s
% 0.12/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 % Number of cores: 8
% 0.12/0.35 % Python version: Python 3.6.8
% 0.12/0.35 % Running in FO mode
% 0.42/0.61 % Total configuration time : 435
% 0.42/0.61 % Estimated wc time : 1092
% 0.42/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.50/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.50/0.72 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.50/0.72 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.50/0.73 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.50/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.50/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.50/0.73 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.53/0.90 % /export/starexec/sandbox/solver/bin/fo/fo1_lcnf.sh running for 50s
% 47.14/7.39 % Solved by fo/fo1_lcnf.sh.
% 47.14/7.39 % done 6920 iterations in 6.385s
% 47.14/7.39 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 47.14/7.39 % SZS output start Refutation
% See solution above
% 47.14/7.40
% 47.14/7.40
% 47.14/7.40 % Terminating...
% 47.14/7.40 % /export/starexec/sandbox/solver/bin/fo/fo17_bce.sh running for 50s
% 47.70/7.51 % Runner terminated.
% 47.70/7.52 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------