include('Axioms/SET010^0.ax').
thf(v2_struct_0_type, type, v2_struct_0: $i > $o).
thf(l1_graph_1_type, type, l1_graph_1: $i > $o).
thf(v7_graph_1_type, type, v7_graph_1: $i > $i > $o).
thf(k1_xboole_0_type, type, k1_xboole_0: $i).
thf(v1_graph_4_type, type, v1_graph_4: $i > $i > $o).
thf(m2_graph_1_type, type, m2_graph_1: $i > $i > $o).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(m2_finseq_1_type, type, m2_finseq_1: $i > $i > $o).
thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(r1_graph_2_type, type, r1_graph_2: $i > $i > $i > $o).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k1_zfmisc_1_type, type, k1_zfmisc_1: $i > $i).
thf(v3_graph_2_type, type, v3_graph_2: $i > $i > $o).
thf(k15_finseq_1_type, type, k15_finseq_1: $i > $i).
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(n1_type, type, 1: $i).
thf(k3_finseq_1_type, type, k3_finseq_1: $i > $i).
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(v1_finseq_1_type, type, v1_finseq_1: $i > $o).
thf(v2_funct_1_type, type, v2_funct_1: $i > $o).
thf(v2_finseq_1_type, type, v2_finseq_1: $i > $o).
thf(m1_graph_1_type, type, m1_graph_1: $i > $i > $o).
thf(v4_relat_1_type, type, v4_relat_1: $i > $i > $o).
thf(k5_numbers_type, type, k5_numbers: $i).
thf(v5_relat_1_type, type, v5_relat_1: $i > $i > $o).
thf(u4_struct_0_type, type, u4_struct_0: $i > $i).
thf(v1_finset_1_type, type, v1_finset_1: $i > $o).
thf(t6_boole, axiom,   (! [A: $i] :  ( (v1_xboole_0 @ A)  =>  ( (= @ A)  @ k1_xboole_0) ) ) , file(boole, t6_boole)).
thf(t49_graph_2, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( (m2_finseq_1 @ B)  @  (u1_struct_0 @ A) )  =>  (! [C: $i] :  ( ( (m2_graph_1 @ C)  @ A)  =>  ~ ( ( ( ( (r1_graph_2 @ A)  @ B)  @ C)  &  (! [D: $i] :  ( ( (m1_subset_1 @ D)  @  (k1_zfmisc_1 @ C) )  =>  (! [E: $i] :  ( ( (m1_subset_1 @ E)  @  (k1_zfmisc_1 @ B) )  =>  (! [F: $i] :  ( ( ( (v3_graph_2 @ F)  @ A)  &  ( (m2_graph_1 @ F)  @ A) )  =>  (! [G: $i] :  ( ( (m2_finseq_1 @ G)  @  (u1_struct_0 @ A) )  =>  ~ ( ( ( (= @  (k15_finseq_1 @ D) )  @ F)  &  ( ( (= @  (k15_finseq_1 @ E) )  @ G)  &  ( ( ( (r1_graph_2 @ A)  @ G)  @ F)  &  ( ( (= @  ( (k1_funct_1 @ B)  @ 1) )  @  ( (k1_funct_1 @ G)  @ 1) )  &  ( (= @  ( (k1_funct_1 @ B)  @  (k3_finseq_1 @ B) ) )  @  ( (k1_funct_1 @ G)  @  (k3_finseq_1 @ G) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(graph_2, t49_graph_2)).
thf(t24_graph_4, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( (v1_relat_1 @ B)  &  ( (v1_funct_1 @ B)  &  (v1_finseq_1 @ B) ) )  =>  ( ( ( ( (v7_graph_1 @ B)  @ A)  &  ( ( (v1_graph_4 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) ) )  =>  ( ( (v7_graph_1 @ B)  @ A)  &  ( ( (v3_graph_2 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) ) ) )  &  ( ( ( ( (v7_graph_1 @ B)  @ A)  &  ( ( (v3_graph_2 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) ) )  =>  ( ( (v7_graph_1 @ B)  @ A)  &  ( ( (v1_graph_4 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) ) ) )  &  ( ( ( (v7_graph_1 @ B)  @ A)  &  ( ( (v3_graph_2 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) ) )  =>  ( (v2_funct_1 @ B)  &  ( ( (v7_graph_1 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) ) ) ) ) ) ) ) ) ) , file(graph_4, t24_graph_4)).
thf(t14_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  ( (m2_graph_1 @ k1_xboole_0)  @ A) ) ) , file(graph_1, t14_graph_1)).
thf(t116_finseq_3, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v2_finseq_1 @ A) ) )  =>  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v1_finseq_1 @ A) ) )  =>  ( (= @  (k15_finseq_1 @ A) )  @ A) ) ) ) , file(finseq_3, t116_finseq_3)).
thf(redefinition_m2_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( (m2_graph_1 @ B)  @ A)  <=>  ( (m1_graph_1 @ B)  @ A) ) ) ) ) , file(graph_1, m2_graph_1)).
thf(rc5_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (? [B: $i] :  ( ( (m1_graph_1 @ B)  @ A)  &  ( (v1_relat_1 @ B)  &  ( ( (v4_relat_1 @ B)  @ k5_numbers)  &  ( ( (v5_relat_1 @ B)  @  (u4_struct_0 @ A) )  &  ( (v1_funct_1 @ B)  &  ( (v1_xboole_0 @ B)  &  ( (v1_finset_1 @ B)  &  ( (v1_finseq_1 @ B)  &  (v2_finseq_1 @ B) ) ) ) ) ) ) ) ) ) ) ) , file(graph_1, rc5_graph_1)).
thf(l15_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  ( (m1_graph_1 @ k1_xboole_0)  @ A) ) ) , file(graph_1, l15_graph_1)).
thf(fc1_xboole_0, axiom,   (v1_xboole_0 @ k1_xboole_0) , file(xboole_0, fc1_xboole_0)).
thf(dt_m1_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( (m1_graph_1 @ B)  @ A)  =>  ( (v1_relat_1 @ B)  &  ( (v1_funct_1 @ B)  &  (v1_finseq_1 @ B) ) ) ) ) ) ) , file(graph_1, m1_graph_1)).
thf(d1_msscyc_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( (v1_relat_1 @ B)  &  ( (v1_funct_1 @ B)  &  (v1_finseq_1 @ B) ) )  =>  ( ( (m1_graph_1 @ B)  @ A)  <=>  ( ( (m2_finseq_1 @ B)  @  (u4_struct_0 @ A) )  &  (? [C: $i] :  ( ( (m2_finseq_1 @ C)  @  (u1_struct_0 @ A) )  &  ( ( (r1_graph_2 @ A)  @ C)  @ B) ) ) ) ) ) ) ) ) , file(msscyc_1, d1_msscyc_1)).
thf(cc6_finseq_1, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v1_finseq_1 @ A) ) )  =>  ( (v1_relat_1 @ A)  &  ( (v1_funct_1 @ A)  &  (v2_finseq_1 @ A) ) ) ) ) , file(finseq_1, cc6_finseq_1)).
thf(cc1_subset_1, axiom,   (! [A: $i] :  ( (v1_xboole_0 @ A)  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @ A) )  =>  (v1_xboole_0 @ B) ) ) ) ) , file(subset_1, cc1_subset_1)).
thf(cc1_graph_1, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( (m1_graph_1 @ B)  @ A)  =>  ( (v1_xboole_0 @ B)  =>  ( (v7_graph_1 @ B)  @ A) ) ) ) ) ) , file(graph_1, cc1_graph_1)).
thf(t13_graph_5, conjecture,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  ( ( (v7_graph_1 @ k1_xboole_0)  @ A)  &  ( ( (v1_graph_4 @ k1_xboole_0)  @ A)  &  ( (m2_graph_1 @ k1_xboole_0)  @ A) ) ) ) ) , file(graph_5, t13_graph_5)).