% Mizar problem: e3_35_1,orders_3,770,63 
include('Axioms/SET010^0.ax').
thf(f1_s1_orders_3_type,type,( f1_s1_orders_3: $i )).
thf(f2_s1_orders_3_type,type,( f2_s1_orders_3: $i > $i > $i )).
thf(k1_multop_1_type,type,( k1_multop_1: $i > $i > $i > $i > $i )).
thf(k2_zfmisc_1_type,type,( k2_zfmisc_1: $i > $i > $i )).
thf(k3_zfmisc_1_type,type,( k3_zfmisc_1: $i > $i > $i > $i )).
thf(k6_altcat_1_type,type,( k6_altcat_1: $i > $i > $i )).
thf(m1_subset_1_type,type,( m1_subset_1: $i > $i > $o )).
thf(v1_funcop_1_type,type,( v1_funcop_1: $i > $o )).
thf(v1_funct_1_type,type,( v1_funct_1: $i > $o )).
thf(v1_partfun1_type,type,( v1_partfun1: $i > $i > $o )).
thf(v1_relat_1_type,type,( v1_relat_1: $i > $o )).
thf(v1_xboole_0_type,type,( v1_xboole_0: $i > $o )).
thf(v1_zfmisc_1_type,type,( v1_zfmisc_1: $i > $o )).
thf(v2_funct_1_type,type,( v2_funct_1: $i > $o )).
thf(v3_funct_1_type,type,( v3_funct_1: $i > $o )).
thf(v4_funct_1_type,type,( v4_funct_1: $i > $o )).
thf(v4_relat_1_type,type,( v4_relat_1: $i > $i > $o )).
thf(v7_altcat_1_type,type,( v7_altcat_1: $i > $o )).
thf(cc6_funct_1,axiom,( ! [A: $i] : ( ( ( v1_zfmisc_1 @ A ) & ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) ) => ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) & ( v3_funct_1 @ A ) ) ) ),file(funct_1,cc6_funct_1)).
thf(cc5_funct_1,axiom,( ! [A: $i] : ( ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) & ~ ( v3_funct_1 @ A ) ) => ( ~ ( v1_zfmisc_1 @ A ) & ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) ) ) ),file(funct_1,cc5_funct_1)).
thf(rc2_funct_1,axiom,( ? [A: $i] : ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) & ( v2_funct_1 @ A ) ) ),file(funct_1,rc2_funct_1)).
thf(rc5_funct_1,axiom,( ? [A: $i] : ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) & ~ ( v3_funct_1 @ A ) ) ),file(funct_1,rc5_funct_1)).
thf(dt_k2_zfmisc_1,axiom,( $true ),file(zfmisc_1,k2_zfmisc_1)).
thf(cc1_funct_1,axiom,( ! [A: $i] : ( ( v1_xboole_0 @ A ) => ( v1_funct_1 @ A ) ) ),file(funct_1,cc1_funct_1)).
thf(cc2_funct_1,axiom,( ! [A: $i] : ( ( ( v1_xboole_0 @ A ) & ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) ) => ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) & ( v2_funct_1 @ A ) ) ) ),file(funct_1,cc2_funct_1)).
thf(cc4_funct_1,axiom,( ! [A: $i] : ( ( ( v1_xboole_0 @ A ) & ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) ) => ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) & ( v3_funct_1 @ A ) ) ) ),file(funct_1,cc4_funct_1)).
thf(cc7_funct_1,axiom,( ! [A: $i] : ( ( v1_xboole_0 @ A ) => ( v4_funct_1 @ A ) ) ),file(funct_1,cc7_funct_1)).
thf(cc8_funct_1,axiom,( ! [A: $i] : ( ( v4_funct_1 @ A ) => ! [B: $i] : ( ( m1_subset_1 @ B @ A ) => ( ( v1_relat_1 @ B ) & ( v1_funct_1 @ B ) ) ) ) ),file(funct_1,cc8_funct_1)).
thf(fc10_subset_1,axiom,( ! [A: $i] : ! [B: $i] : ( ( ~ ( v1_xboole_0 @ A ) & ~ ( v1_xboole_0 @ B ) ) => ~ ( v1_xboole_0 @ ( k2_zfmisc_1 @ A @ B ) ) ) ),file(subset_1,fc10_subset_1)).
thf(fc11_subset_1,axiom,( ! [A: $i] : ! [B: $i] : ! [C: $i] : ( ( ~ ( v1_xboole_0 @ A ) & ~ ( v1_xboole_0 @ B ) & ~ ( v1_xboole_0 @ C ) ) => ~ ( v1_xboole_0 @ ( k3_zfmisc_1 @ A @ B @ C ) ) ) ),file(subset_1,fc11_subset_1)).
thf(rc1_xboole_0,axiom,( ? [A: $i] : ( v1_xboole_0 @ A ) ),file(xboole_0,rc1_xboole_0)).
thf(rc2_xboole_0,axiom,( ? [A: $i] : ~ ( v1_xboole_0 @ A ) ),file(xboole_0,rc2_xboole_0)).
thf(rc7_funct_1,axiom,( ? [A: $i] : ( ~ ( v1_xboole_0 @ A ) & ( v4_funct_1 @ A ) ) ),file(funct_1,rc7_funct_1)).
thf(dt_k1_multop_1,axiom,( $true ),file(multop_1,k1_multop_1)).
thf(dt_k3_zfmisc_1,axiom,( $true ),file(zfmisc_1,k3_zfmisc_1)).
thf(dt_k6_altcat_1,axiom,( ! [A: $i] : ! [B: $i] : ( ( ( v4_funct_1 @ A ) & ( v4_funct_1 @ B ) ) => ( ( v1_relat_1 @ ( k6_altcat_1 @ A @ B ) ) & ( v4_relat_1 @ ( k6_altcat_1 @ A @ B ) @ ( k2_zfmisc_1 @ B @ A ) ) & ( v1_funct_1 @ ( k6_altcat_1 @ A @ B ) ) & ( v1_partfun1 @ ( k6_altcat_1 @ A @ B ) @ ( k2_zfmisc_1 @ B @ A ) ) & ( v1_funcop_1 @ ( k6_altcat_1 @ A @ B ) ) & ( v7_altcat_1 @ ( k6_altcat_1 @ A @ B ) ) ) ) ),file(altcat_1,k6_altcat_1)).
thf(dt_m1_subset_1,axiom,( $true ),file(subset_1,m1_subset_1)).
thf(dt_f1_s1_orders_3,axiom,( ~ ( v1_xboole_0 @ f1_s1_orders_3 ) ),file(orders_3,f1_s1_orders_3)).
thf(dt_f2_s1_orders_3,axiom,( ! [A: $i] : ! [B: $i] : ( v4_funct_1 @ ( f2_s1_orders_3 @ A @ B ) ) ),file(orders_3,f2_s1_orders_3)).
thf(rc1_funct_1,axiom,( ? [A: $i] : ( ( v1_relat_1 @ A ) & ( v1_funct_1 @ A ) ) ),file(funct_1,rc1_funct_1)).
thf(s4_altcat_1,axiom,( ! [A: $i > $i > $i > $i] : ! [B: $i] : ! [C: $i] : ! [D: $i] : ? [E: $i] : ( ( v1_relat_1 @ E ) & ( v4_relat_1 @ E @ ( k3_zfmisc_1 @ D @ C @ B ) ) & ( v1_funct_1 @ E ) & ( v1_partfun1 @ E @ ( k3_zfmisc_1 @ D @ C @ B ) ) & ! [F: $i] : ( ( m1_subset_1 @ F @ D ) => ! [G: $i] : ( ( m1_subset_1 @ G @ C ) => ! [H: $i] : ( ( m1_subset_1 @ H @ B ) => ( = @ ( k1_multop_1 @ E @ F @ G @ H ) @ ( A @ F @ G @ H ) ) ) ) ) ) ),file(altcat_1,s4_altcat_1)).
thf(e3_35_1__orders_3,conjecture,( ? [A: $i] : ( ( v1_relat_1 @ A ) & ( v4_relat_1 @ A @ ( k3_zfmisc_1 @ f1_s1_orders_3 @ f1_s1_orders_3 @ f1_s1_orders_3 ) ) & ( v1_funct_1 @ A ) & ( v1_partfun1 @ A @ ( k3_zfmisc_1 @ f1_s1_orders_3 @ f1_s1_orders_3 @ f1_s1_orders_3 ) ) & ! [B: $i] : ( ( m1_subset_1 @ B @ f1_s1_orders_3 ) => ! [C: $i] : ( ( m1_subset_1 @ C @ f1_s1_orders_3 ) => ! [D: $i] : ( ( m1_subset_1 @ D @ f1_s1_orders_3 ) => ( = @ ( k1_multop_1 @ A @ B @ C @ D ) @ ( k6_altcat_1 @ ( f2_s1_orders_3 @ B @ C ) @ ( f2_s1_orders_3 @ C @ D ) ) ) ) ) ) ) ),file(orders_3,e3_35_1__orders_3)).
