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(l1_graph_1_type, type, l1_graph_1: $i > $o).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v7_graph_1_type, type, v7_graph_1: $i > $i > $o).
thf(m1_graph_1_type, type, m1_graph_1: $i > $i > $o).
thf(k3_finseq_1_type, type, k3_finseq_1: $i > $i).
thf(k7_graph_2_type, type, k7_graph_2: $i > $i > $i).
thf(k2_nat_1_type, type, k2_nat_1: $i > $i > $i).
thf(n1_type, type, 1: $i).
thf(m2_graph_1_type, type, m2_graph_1: $i > $i > $o).
thf(k1_xboole_0_type, type, k1_xboole_0: $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(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(m2_subset_1_type, type, m2_subset_1: $i > $i > $i > $o).
thf(k1_numbers_type, type, k1_numbers: $i).
thf(k5_numbers_type, type, k5_numbers: $i).
thf(r1_xxreal_0_type, type, r1_xxreal_0: $i > $i > $o).
thf(r2_graph_1_type, type, r2_graph_1: $i > $i > $i > $i > $o).
thf(k7_partfun1_type, type, k7_partfun1: $i > $i > $i > $i).
thf(k1_funct_1_type, type, k1_funct_1: $i > $i > $i).
thf(u1_graph_1_type, type, u1_graph_1: $i > $i).
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(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(dt_k7_graph_2, axiom,   (! [A: $i, B: $i] :  ( ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  &  ( ( (v7_graph_1 @ B)  @ A)  &  ( (m1_graph_1 @ B)  @ A) ) )  =>  ( (m2_finseq_1 @  ( (k7_graph_2 @ A)  @ B) )  @  (u1_struct_0 @ A) ) ) ) , file(graph_2, k7_graph_2)).
thf(d6_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] :  ( ( (v1_relat_1 @ C)  &  ( (v1_funct_1 @ C)  &  (v1_finseq_1 @ C) ) )  =>  ( ( ( (r1_graph_2 @ A)  @ B)  @ C)  <=>  ( ( (= @  (k3_finseq_1 @ B) )  @  ( (k2_nat_1 @  (k3_finseq_1 @ C) )  @ 1) )  &  (! [D: $i] :  ( ( ( (m2_subset_1 @ D)  @ k1_numbers)  @ k5_numbers)  =>  ( ( ( (r1_xxreal_0 @ 1)  @ D)  &  ( (r1_xxreal_0 @ D)  @  (k3_finseq_1 @ C) ) )  =>  ( ( ( (r2_graph_1 @ A)  @  ( ( (k7_partfun1 @  (u1_struct_0 @ A) )  @ B)  @ D) )  @  ( ( (k7_partfun1 @  (u1_struct_0 @ A) )  @ B)  @  ( (k2_nat_1 @ D)  @ 1) ) )  @  ( (k1_funct_1 @ C)  @ D) ) ) ) ) ) ) ) ) ) ) ) ) , file(graph_2, d6_graph_2)).
thf(d10_graph_2, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  (l1_graph_1 @ A) )  =>  (! [B: $i] :  ( ( ( (v7_graph_1 @ B)  @ A)  &  ( (m2_graph_1 @ B)  @ A) )  =>  ( ~ ( ( (= @ B)  @ k1_xboole_0) )  =>  (! [C: $i] :  ( ( (m2_finseq_1 @ C)  @  (u1_struct_0 @ A) )  =>  ( ( (= @ C)  @  ( (k7_graph_2 @ A)  @ B) )  <=>  ( ( ( (r1_graph_2 @ A)  @ C)  @ B)  &  ( (= @  ( (k1_funct_1 @ C)  @ 1) )  @  ( (k1_funct_1 @  (u1_graph_1 @ A) )  @  ( (k1_funct_1 @ B)  @ 1) ) ) ) ) ) ) ) ) ) ) ) , file(graph_2, d10_graph_2)).
thf(t10_msscyc_1, conjecture,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( ~ ( (v11_struct_0 @ A) )  &  (l1_graph_1 @ A) ) )  =>  (! [B: $i] :  ( ( ~ ( (v1_xboole_0 @ B) )  &  ( ( (v7_graph_1 @ B)  @ A)  &  ( (m1_graph_1 @ B)  @ A) ) )  =>  ( (= @  (k3_finseq_1 @  ( (k7_graph_2 @ A)  @ B) ) )  @  ( (k2_nat_1 @  (k3_finseq_1 @ B) )  @ 1) ) ) ) ) ) , file(msscyc_1, t10_msscyc_1)).