include('Axioms/SET010^0.ax').
thf(v2_struct_0_type, type, v2_struct_0: $i > $o).
thf(v11_struct_0_type, type, v11_struct_0: $i > $o).
thf(v2_cat_1_type, type, v2_cat_1: $i > $o).
thf(v3_cat_1_type, type, v3_cat_1: $i > $o).
thf(v4_cat_1_type, type, v4_cat_1: $i > $o).
thf(v5_cat_1_type, type, v5_cat_1: $i > $o).
thf(v6_cat_1_type, type, v6_cat_1: $i > $o).
thf(l1_cat_1_type, type, l1_cat_1: $i > $o).
thf(m3_index_1_type, type, m3_index_1: $i > $i > $i > $i > $i > $o).
thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(u4_struct_0_type, type, u4_struct_0: $i > $i).
thf(u1_graph_1_type, type, u1_graph_1: $i > $i).
thf(u2_graph_1_type, type, u2_graph_1: $i > $i).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(m2_cat_1_type, type, m2_cat_1: $i > $i > $i > $o).
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(k2_xtuple_0_type, type, k2_xtuple_0: $i > $i).
thf(k2_index_1_type, type, k2_index_1: $i > $i > $i > $i).
thf(k1_xtuple_0_type, type, k1_xtuple_0: $i > $i).
thf(k3_graph_1_type, type, k3_graph_1: $i > $i > $i).
thf(k4_graph_1_type, type, k4_graph_1: $i > $i > $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(v1_funct_2_type, type, v1_funct_2: $i > $i > $i > $o).
thf(k1_zfmisc_1_type, type, k1_zfmisc_1: $i > $i).
thf(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(k3_funct_2_type, type, k3_funct_2: $i > $i > $i > $i > $i).
thf(l1_struct_0_type, type, l1_struct_0: $i > $o).
thf(l5_struct_0_type, type, l5_struct_0: $i > $o).
thf(l1_graph_1_type, type, l1_graph_1: $i > $o).
thf(t4_index_1, axiom,   (! [A: $i] :  ( ~ ( (v1_xboole_0 @ A) )  =>  (! [B: $i] :  ( ~ ( (v1_xboole_0 @ B) )  =>  (! [C: $i] :  ( ( (v1_funct_1 @ C)  &  ( ( ( (v1_funct_2 @ C)  @ B)  @ A)  &  ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ B)  @ A) ) ) ) )  =>  (! [D: $i] :  ( ( (v1_funct_1 @ D)  &  ( ( ( (v1_funct_2 @ D)  @ B)  @ A)  &  ( (m1_subset_1 @ D)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ B)  @ A) ) ) ) )  =>  (! [E: $i] :  ( ( ( ( ( (m3_index_1 @ E)  @ A)  @ B)  @ C)  @ D)  =>  (! [F: $i] :  ( ( (m1_subset_1 @ F)  @ B)  =>  ( ( (m2_cat_1 @  ( (k1_funct_1 @  (k2_xtuple_0 @ E) )  @ F) )  @  ( ( (k2_index_1 @ A)  @  (k1_xtuple_0 @ E) )  @  ( ( ( (k3_funct_2 @ B)  @ A)  @ C)  @ F) ) )  @  ( ( (k2_index_1 @ A)  @  (k1_xtuple_0 @ E) )  @  ( ( ( (k3_funct_2 @ B)  @ A)  @ D)  @ F) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(index_1, t4_index_1)).
thf(fc2_struct_0, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_struct_0 @ A) )  =>  ~ ( (v1_xboole_0 @  (u1_struct_0 @ A) ) ) ) ) , file(struct_0, fc2_struct_0)).
thf(fc14_struct_0, axiom,   (! [A: $i] :  ( ( ~ ( (v11_struct_0 @ A) )  &  (l5_struct_0 @ A) )  =>  ~ ( (v1_xboole_0 @  (u4_struct_0 @ A) ) ) ) ) , file(struct_0, fc14_struct_0)).
thf(dt_u2_graph_1, axiom,   (! [A: $i] :  ( (l1_graph_1 @ A)  =>  ( (v1_funct_1 @  (u2_graph_1 @ A) )  &  ( ( ( (v1_funct_2 @  (u2_graph_1 @ A) )  @  (u4_struct_0 @ A) )  @  (u1_struct_0 @ A) )  &  ( (m1_subset_1 @  (u2_graph_1 @ A) )  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (u4_struct_0 @ A) )  @  (u1_struct_0 @ A) ) ) ) ) ) ) ) , file(graph_1, u2_graph_1)).
thf(dt_u1_graph_1, axiom,   (! [A: $i] :  ( (l1_graph_1 @ A)  =>  ( (v1_funct_1 @  (u1_graph_1 @ A) )  &  ( ( ( (v1_funct_2 @  (u1_graph_1 @ A) )  @  (u4_struct_0 @ A) )  @  (u1_struct_0 @ A) )  &  ( (m1_subset_1 @  (u1_graph_1 @ A) )  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (u4_struct_0 @ A) )  @  (u1_struct_0 @ A) ) ) ) ) ) ) ) , file(graph_1, u1_graph_1)).
thf(dt_l5_struct_0, axiom,   (! [A: $i] :  ( (l5_struct_0 @ A)  =>  (l1_struct_0 @ A) ) ) , file(struct_0, l5_struct_0)).
thf(dt_l1_graph_1, axiom,   (! [A: $i] :  ( (l1_graph_1 @ A)  =>  (l5_struct_0 @ A) ) ) , file(graph_1, l1_graph_1)).
thf(dt_l1_cat_1, axiom,   (! [A: $i] :  ( (l1_cat_1 @ A)  =>  (l1_graph_1 @ A) ) ) , file(cat_1, l1_cat_1)).
thf(d4_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( ~ ( (v11_struct_0 @ A) )  &  (l1_graph_1 @ A) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (u4_struct_0 @ A) )  =>  ( (= @  ( (k4_graph_1 @ A)  @ B) )  @  ( ( ( (k3_funct_2 @  (u4_struct_0 @ A) )  @  (u1_struct_0 @ A) )  @  (u2_graph_1 @ A) )  @ B) ) ) ) ) ) , file(graph_1, d4_graph_1)).
thf(d3_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( ~ ( (v11_struct_0 @ A) )  &  (l1_graph_1 @ A) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (u4_struct_0 @ A) )  =>  ( (= @  ( (k3_graph_1 @ A)  @ B) )  @  ( ( ( (k3_funct_2 @  (u4_struct_0 @ A) )  @  (u1_struct_0 @ A) )  @  (u1_graph_1 @ A) )  @ B) ) ) ) ) ) , file(graph_1, d3_graph_1)).
thf(t5_index_1, conjecture,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( ~ ( (v11_struct_0 @ A) )  &  ( (v2_cat_1 @ A)  &  ( (v3_cat_1 @ A)  &  ( (v4_cat_1 @ A)  &  ( (v5_cat_1 @ A)  &  ( (v6_cat_1 @ A)  &  (l1_cat_1 @ A) ) ) ) ) ) ) )  =>  (! [B: $i] :  ( ( ( ( ( (m3_index_1 @ B)  @  (u1_struct_0 @ A) )  @  (u4_struct_0 @ A) )  @  (u1_graph_1 @ A) )  @  (u2_graph_1 @ A) )  =>  (! [C: $i] :  ( ( (m1_subset_1 @ C)  @  (u4_struct_0 @ A) )  =>  ( ( (m2_cat_1 @  ( (k1_funct_1 @  (k2_xtuple_0 @ B) )  @ C) )  @  ( ( (k2_index_1 @  (u1_struct_0 @ A) )  @  (k1_xtuple_0 @ B) )  @  ( (k3_graph_1 @ A)  @ C) ) )  @  ( ( (k2_index_1 @  (u1_struct_0 @ A) )  @  (k1_xtuple_0 @ B) )  @  ( (k4_graph_1 @ A)  @ C) ) ) ) ) ) ) ) ) , file(index_1, t5_index_1)).