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(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(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(k3_finseq_1_type, type, k3_finseq_1: $i > $i).
thf(k1_matrix_1_type, type, k1_matrix_1: $i > $i).
thf(k1_matrix_4_type, type, k1_matrix_4: $i > $i > $i > $i).
thf(k3_matrix_3_type, type, k3_matrix_3: $i > $i > $i > $i).
thf(k2_matrix_3_type, type, k2_matrix_3: $i > $i > $i).
thf(m1_finseq_1_type, type, m1_finseq_1: $i > $i > $o).
thf(v7_ordinal1_type, type, v7_ordinal1: $i > $o).
thf(k4_tarski_type, type, k4_tarski: $i > $i > $i).
thf(k2_matrix_1_type, type, k2_matrix_1: $i > $i).
thf(k3_matrix_1_type, type, k3_matrix_1: $i > $i > $i > $i > $i).
thf(k4_algstr_0_type, type, k4_algstr_0: $i > $i > $i).
thf(t31_matrix_4, 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) ) ) )  =>  ( ( ( (= @  (k3_finseq_1 @ B) )  @  (k3_finseq_1 @ C) )  &  ( ( (= @  (k3_finseq_1 @ C) )  @  (k3_finseq_1 @ D) )  &  ( ( (= @  (k1_matrix_1 @ B) )  @  (k1_matrix_1 @ C) )  &  ( (= @  (k1_matrix_1 @ C) )  @  (k1_matrix_1 @ D) ) ) ) )  =>  ( (= @  ( ( (k1_matrix_4 @ A)  @ B)  @  ( ( (k3_matrix_3 @ A)  @ C)  @ D) ) )  @  ( ( (k1_matrix_4 @ A)  @  ( ( (k1_matrix_4 @ A)  @ B)  @ C) )  @ D) ) ) ) ) ) ) ) ) ) ) , file(matrix_4, t31_matrix_4)).
thf(t1_matrix_4, 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) ) ) )  =>  ( (= @  ( (k2_matrix_3 @ A)  @  ( (k2_matrix_3 @ A)  @ B) ) )  @ B) ) ) ) ) , file(matrix_4, t1_matrix_4)).
thf(redefinition_m2_finseq_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (m2_finseq_1 @ B)  @ A)  <=>  ( (m1_finseq_1 @ B)  @ A) ) ) ) , file(finseq_1, m2_finseq_1)).
thf(dt_k2_matrix_3, axiom,   (! [A: $i, B: $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) ) ) ) ) ) ) ) ) ) ) )  &  ( (v1_matrix_1 @ B)  &  ( (m1_finseq_1 @ B)  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) ) )  =>  ( (v1_matrix_1 @  ( (k2_matrix_3 @ A)  @ B) )  &  ( (m2_finseq_1 @  ( (k2_matrix_3 @ A)  @ B) )  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) ) ) ) , file(matrix_3, k2_matrix_3)).
thf(dt_k1_matrix_4, axiom,   (! [A: $i, B: $i, C: $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) ) ) ) ) ) ) ) ) ) ) )  &  ( ( (v1_matrix_1 @ B)  &  ( (m1_finseq_1 @ B)  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) )  &  ( (v1_matrix_1 @ C)  &  ( (m1_finseq_1 @ C)  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) ) ) )  =>  ( (v1_matrix_1 @  ( ( (k1_matrix_4 @ A)  @ B)  @ C) )  &  ( (m2_finseq_1 @  ( ( (k1_matrix_4 @ A)  @ B)  @ C) )  @  (k3_finseq_2 @  (u1_struct_0 @ A) ) ) ) ) ) , file(matrix_4, k1_matrix_4)).
thf(d2_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) ) ) )  =>  ( ( (= @ C)  @  ( (k2_matrix_3 @ A)  @ B) )  <=>  ( ( (= @  (k3_finseq_1 @ C) )  @  (k3_finseq_1 @ B) )  &  ( ( (= @  (k1_matrix_1 @ C) )  @  (k1_matrix_1 @ B) )  &  (! [D: $i] :  ( (v7_ordinal1 @ D)  =>  (! [E: $i] :  ( (v7_ordinal1 @ E)  =>  ( ( (r2_hidden @  ( (k4_tarski @ D)  @ E) )  @  (k2_matrix_1 @ B) )  =>  ( (= @  ( ( ( (k3_matrix_1 @  (u1_struct_0 @ A) )  @ C)  @ D)  @ E) )  @  ( (k4_algstr_0 @ A)  @  ( ( ( (k3_matrix_1 @  (u1_struct_0 @ A) )  @ B)  @ D)  @ E) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(matrix_3, d2_matrix_3)).
thf(d1_matrix_4, 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) ) ) )  =>  ( (= @  ( ( (k1_matrix_4 @ A)  @ B)  @ C) )  @  ( ( (k3_matrix_3 @ A)  @ B)  @  ( (k2_matrix_3 @ A)  @ C) ) ) ) ) ) ) ) ) , file(matrix_4, d1_matrix_4)).
thf(t32_matrix_4, 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] :  ( ( (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) ) ) )  =>  ( ( ( (= @  (k3_finseq_1 @ B) )  @  (k3_finseq_1 @ C) )  &  ( ( (= @  (k3_finseq_1 @ C) )  @  (k3_finseq_1 @ D) )  &  ( ( (= @  (k1_matrix_1 @ B) )  @  (k1_matrix_1 @ C) )  &  ( (= @  (k1_matrix_1 @ C) )  @  (k1_matrix_1 @ D) ) ) ) )  =>  ( (= @  ( ( (k1_matrix_4 @ A)  @ B)  @  ( ( (k1_matrix_4 @ A)  @ C)  @ D) ) )  @  ( ( (k3_matrix_3 @ A)  @  ( ( (k1_matrix_4 @ A)  @ B)  @ C) )  @ D) ) ) ) ) ) ) ) ) ) ) , file(matrix_4, t32_matrix_4)).