include('Axioms/SET010^0.ax').
thf(v2_struct_0_type, type, v2_struct_0: $i > $o).
thf(v6_struct_0_type, type, v6_struct_0: $i > $o).
thf(v13_algstr_0_type, type, v13_algstr_0: $i > $o).
thf(v33_algstr_0_type, type, v33_algstr_0: $i > $o).
thf(v3_group_1_type, type, v3_group_1: $i > $o).
thf(v5_group_1_type, type, v5_group_1: $i > $o).
thf(v2_rlvect_1_type, type, v2_rlvect_1: $i > $o).
thf(v3_rlvect_1_type, type, v3_rlvect_1: $i > $o).
thf(v4_rlvect_1_type, type, v4_rlvect_1: $i > $o).
thf(v4_vectsp_1_type, type, v4_vectsp_1: $i > $o).
thf(v5_vectsp_1_type, type, v5_vectsp_1: $i > $o).
thf(l6_algstr_0_type, type, l6_algstr_0: $i > $o).
thf(v7_ordinal1_type, type, v7_ordinal1: $i > $o).
thf(m1_matrix_1_type, type, m1_matrix_1: $i > $i > $i > $i > $o).
thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(r2_matrix_6_type, type, r2_matrix_6: $i > $i > $i > $i > $o).
thf(k4_matrix_6_type, type, k4_matrix_6: $i > $i > $i > $i > $i).
thf(v1_matrix_1_type, type, v1_matrix_1: $i > $o).
thf(m2_finseq_1_type, type, m2_finseq_1: $i > $i > $o).
thf(k3_finseq_2_type, type, k3_finseq_2: $i > $i).
thf(k1_matrix_1_type, type, k1_matrix_1: $i > $i).
thf(k3_finseq_1_type, type, k3_finseq_1: $i > $i).
thf(k4_matrix_3_type, type, k4_matrix_3: $i > $i > $i > $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(k2_matrix_1_type, type, k2_matrix_1: $i > $i).
thf(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(k2_finseq_1_type, type, k2_finseq_1: $i > $i).
thf(k12_matrix_1_type, type, k12_matrix_1: $i > $i > $i).
thf(l1_struct_0_type, type, l1_struct_0: $i > $o).
thf(l2_algstr_0_type, type, l2_algstr_0: $i > $o).
thf(l5_algstr_0_type, type, l5_algstr_0: $i > $o).
thf(l2_struct_0_type, type, l2_struct_0: $i > $o).
thf(l1_algstr_0_type, type, l1_algstr_0: $i > $o).
thf(t33_matrix_3, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( ~ ( (v6_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v33_algstr_0 @ A)  &  ( (v3_group_1 @ A)  &  ( (v5_group_1 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  ( (v4_vectsp_1 @ A)  &  ( (v5_vectsp_1 @ A)  &  (l6_algstr_0 @ A) ) ) ) ) ) ) ) ) ) ) )  =>  (! [B: $i] :  ( ( (v1_matrix_1 @ B)  &  ( (m2_finseq_1 @ B)  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) )  =>  (! [C: $i] :  ( ( (v1_matrix_1 @ C)  &  ( (m2_finseq_1 @ C)  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) )  =>  (! [D: $i] :  ( ( (v1_matrix_1 @ D)  &  ( (m2_finseq_1 @ D)  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) )  =>  ( ( ( (= @  (k1_matrix_1 @ B) )  @  (k3_finseq_1 @ C) )  &  ( (= @  (k1_matrix_1 @ C) )  @  (k3_finseq_1 @ D) ) )  =>  ( (= @  ( ( (k4_matrix_3 @ A)  @  ( ( (k4_matrix_3 @ A)  @ B)  @ C) )  @ D) )  @  ( ( (k4_matrix_3 @ A)  @ B)  @  ( ( (k4_matrix_3 @ A)  @ C)  @ D) ) ) ) ) ) ) ) ) ) ) ) , file(matrix_3, t33_matrix_3)).
thf(t24_matrix_1, axiom,   (! [A: $i] :  ( (v7_ordinal1 @ A)  =>  (! [B: $i] :  ( ~ ( (v1_xboole_0 @ B) )  =>  (! [C: $i] :  ( ( ( ( (m1_matrix_1 @ C)  @ B)  @ A)  @ A)  =>  ( ( (= @  (k3_finseq_1 @ C) )  @ A)  &  ( ( (= @  (k1_matrix_1 @ C) )  @ A)  &  ( (= @  (k2_matrix_1 @ C) )  @  ( (k2_zfmisc_1 @  (k2_finseq_1 @ A) )  @  (k2_finseq_1 @ A) ) ) ) ) ) ) ) ) ) ) , file(matrix_1, t24_matrix_1)).
thf(t19_matrix_3, axiom,   (! [A: $i] :  ( (v7_ordinal1 @ A)  =>  (! [B: $i] :  ( ( ~ ( (v2_struct_0 @ B) )  &  ( ~ ( (v6_struct_0 @ B) )  &  ( (v13_algstr_0 @ B)  &  ( (v33_algstr_0 @ B)  &  ( (v3_group_1 @ B)  &  ( (v5_group_1 @ B)  &  ( (v2_rlvect_1 @ B)  &  ( (v3_rlvect_1 @ B)  &  ( (v4_rlvect_1 @ B)  &  ( (v4_vectsp_1 @ B)  &  ( (v5_vectsp_1 @ B)  &  (l6_algstr_0 @ B) ) ) ) ) ) ) ) ) ) ) )  =>  (! [C: $i] :  ( ( ( ( (m1_matrix_1 @ C)  @  (u1_struct_0 @ B) )  @ A)  @ A)  =>  ( (= @  ( ( (k4_matrix_3 @ B)  @ C)  @  ( (k12_matrix_1 @ B)  @ A) ) )  @ C) ) ) ) ) ) ) , file(matrix_3, t19_matrix_3)).
thf(redefinition_k4_matrix_6, axiom,   (! [A: $i, B: $i, C: $i, D: $i] :  ( ( (v7_ordinal1 @ A)  &  ( ( ~ ( (v2_struct_0 @ B) )  &  ( ~ ( (v6_struct_0 @ B) )  &  ( (v13_algstr_0 @ B)  &  ( (v33_algstr_0 @ B)  &  ( (v3_group_1 @ B)  &  ( (v5_group_1 @ B)  &  ( (v2_rlvect_1 @ B)  &  ( (v3_rlvect_1 @ B)  &  ( (v4_rlvect_1 @ B)  &  ( (v4_vectsp_1 @ B)  &  ( (v5_vectsp_1 @ B)  &  (l6_algstr_0 @ B) ) ) ) ) ) ) ) ) ) ) )  &  ( ( ( ( (m1_matrix_1 @ C)  @  (u1_struct_0 @ B) )  @ A)  @ A)  &  ( ( ( (m1_matrix_1 @ D)  @  (u1_struct_0 @ B) )  @ A)  @ A) ) ) )  =>  ( (= @  ( ( ( (k4_matrix_6 @ A)  @ B)  @ C)  @ D) )  @  ( ( (k4_matrix_3 @ B)  @ C)  @ D) ) ) ) , file(matrix_6, k4_matrix_6)).
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(dt_m1_matrix_1, axiom,   (! [A: $i, B: $i, C: $i] :  ( ( ~ ( (v1_xboole_0 @ A) )  &  ( (v7_ordinal1 @ B)  &  (v7_ordinal1 @ C) ) )  =>  (! [D: $i] :  ( ( ( ( (m1_matrix_1 @ D)  @ A)  @ B)  @ C)  =>  ( (v1_matrix_1 @ D)  &  ( (m2_finseq_1 @ D)  @  (k3_finseq_2 @ A) ) ) ) ) ) ) , file(matrix_1, m1_matrix_1)).
thf(dt_l6_algstr_0, axiom,   (! [A: $i] :  ( (l6_algstr_0 @ A)  =>  ( (l2_algstr_0 @ A)  &  (l5_algstr_0 @ A) ) ) ) , file(algstr_0, l6_algstr_0)).
thf(dt_l2_algstr_0, axiom,   (! [A: $i] :  ( (l2_algstr_0 @ A)  =>  ( (l2_struct_0 @ A)  &  (l1_algstr_0 @ A) ) ) ) , file(algstr_0, l2_algstr_0)).
thf(dt_l1_algstr_0, axiom,   (! [A: $i] :  ( (l1_algstr_0 @ A)  =>  (l1_struct_0 @ A) ) ) , file(algstr_0, l1_algstr_0)).
thf(dt_k4_matrix_6, axiom,   (! [A: $i, B: $i, C: $i, D: $i] :  ( ( (v7_ordinal1 @ A)  &  ( ( ~ ( (v2_struct_0 @ B) )  &  ( ~ ( (v6_struct_0 @ B) )  &  ( (v13_algstr_0 @ B)  &  ( (v33_algstr_0 @ B)  &  ( (v3_group_1 @ B)  &  ( (v5_group_1 @ B)  &  ( (v2_rlvect_1 @ B)  &  ( (v3_rlvect_1 @ B)  &  ( (v4_rlvect_1 @ B)  &  ( (v4_vectsp_1 @ B)  &  ( (v5_vectsp_1 @ B)  &  (l6_algstr_0 @ B) ) ) ) ) ) ) ) ) ) ) )  &  ( ( ( ( (m1_matrix_1 @ C)  @  (u1_struct_0 @ B) )  @ A)  @ A)  &  ( ( ( (m1_matrix_1 @ D)  @  (u1_struct_0 @ B) )  @ A)  @ A) ) ) )  =>  ( ( ( (m1_matrix_1 @  ( ( ( (k4_matrix_6 @ A)  @ B)  @ C)  @ D) )  @  (u1_struct_0 @ B) )  @ A)  @ A) ) ) , file(matrix_6, k4_matrix_6)).
thf(dt_k12_matrix_1, axiom,   (! [A: $i, B: $i] :  ( ( ( ~ ( (v2_struct_0 @ A) )  &  (l6_algstr_0 @ A) )  &  (v7_ordinal1 @ B) )  =>  ( ( ( (m1_matrix_1 @  ( (k12_matrix_1 @ A)  @ B) )  @  (u1_struct_0 @ A) )  @ B)  @ B) ) ) , file(matrix_1, k12_matrix_1)).
thf(d2_matrix_6, axiom,   (! [A: $i] :  ( (v7_ordinal1 @ A)  =>  (! [B: $i] :  ( ( ~ ( (v2_struct_0 @ B) )  &  ( ~ ( (v6_struct_0 @ B) )  &  ( (v13_algstr_0 @ B)  &  ( (v33_algstr_0 @ B)  &  ( (v3_group_1 @ B)  &  ( (v5_group_1 @ B)  &  ( (v2_rlvect_1 @ B)  &  ( (v3_rlvect_1 @ B)  &  ( (v4_rlvect_1 @ B)  &  ( (v4_vectsp_1 @ B)  &  ( (v5_vectsp_1 @ B)  &  (l6_algstr_0 @ B) ) ) ) ) ) ) ) ) ) ) )  =>  (! [C: $i] :  ( ( ( ( (m1_matrix_1 @ C)  @  (u1_struct_0 @ B) )  @ A)  @ A)  =>  (! [D: $i] :  ( ( ( ( (m1_matrix_1 @ D)  @  (u1_struct_0 @ B) )  @ A)  @ A)  =>  ( ( ( ( (r2_matrix_6 @ A)  @ B)  @ C)  @ D)  <=>  ( ( (= @  ( ( (k4_matrix_3 @ B)  @ C)  @ D) )  @  ( ( (k4_matrix_3 @ B)  @ D)  @ C) )  &  ( (= @  ( ( (k4_matrix_3 @ B)  @ C)  @ D) )  @  ( (k12_matrix_1 @ B)  @ A) ) ) ) ) ) ) ) ) ) ) ) , file(matrix_6, d2_matrix_6)).
thf(t14_matrix_6, conjecture,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( ~ ( (v6_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v33_algstr_0 @ A)  &  ( (v3_group_1 @ A)  &  ( (v5_group_1 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  ( (v4_vectsp_1 @ A)  &  ( (v5_vectsp_1 @ A)  &  (l6_algstr_0 @ A) ) ) ) ) ) ) ) ) ) ) )  =>  (! [B: $i] :  ( (v7_ordinal1 @ B)  =>  (! [C: $i] :  ( ( ( ( (m1_matrix_1 @ C)  @  (u1_struct_0 @ A) )  @ B)  @ B)  =>  (! [D: $i] :  ( ( ( ( (m1_matrix_1 @ D)  @  (u1_struct_0 @ A) )  @ B)  @ B)  =>  (! [E: $i] :  ( ( ( ( (m1_matrix_1 @ E)  @  (u1_struct_0 @ A) )  @ B)  @ B)  =>  (! [F: $i] :  ( ( ( ( (m1_matrix_1 @ F)  @  (u1_struct_0 @ A) )  @ B)  @ B)  =>  ( ( ( ( ( (r2_matrix_6 @ B)  @ A)  @ E)  @ C)  &  ( ( ( (r2_matrix_6 @ B)  @ A)  @ F)  @ D) )  =>  ( ( ( (r2_matrix_6 @ B)  @ A)  @  ( ( ( (k4_matrix_6 @ B)  @ A)  @ E)  @ F) )  @  ( ( ( (k4_matrix_6 @ B)  @ A)  @ D)  @ C) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(matrix_6, t14_matrix_6)).