include('Axioms/SET010^0.ax').
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k5_numbers_type, type, k5_numbers: $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_numbers_type, type, k1_numbers: $i).
thf(k3_finseq_1_type, type, k3_finseq_1: $i > $i).
thf(k1_matrix_1_type, type, k1_matrix_1: $i > $i).
thf(k3_matrixr1_type, type, k3_matrixr1: $i > $i > $i).
thf(k4_matrixr1_type, type, k4_matrixr1: $i > $i).
thf(k8_matrixr1_type, type, k8_matrixr1: $i > $i > $i).
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(u1_struct_0_type, type, u1_struct_0: $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(k1_matrix_3_type, type, k1_matrix_3: $i > $i > $i > $i).
thf(m1_finseq_1_type, type, m1_finseq_1: $i > $i > $o).
thf(k4_ordinal1_type, type, k4_ordinal1: $i).
thf(k2_vectsp_1_type, type, k2_vectsp_1: $i).
thf(v36_algstr_0_type, type, v36_algstr_0: $i > $o).
thf(v3_vectsp_1_type, type, v3_vectsp_1: $i > $o).
thf(v6_vectsp_1_type, type, v6_vectsp_1: $i > $o).
thf(v6_membered_type, type, v6_membered: $i > $o).
thf(k2_matrixr1_type, type, k2_matrixr1: $i > $i).
thf(k1_matrixr1_type, type, k1_matrixr1: $i > $i).
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(t2_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) ) ) )  =>  ( (= @  ( ( (k3_matrix_3 @ A)  @ B)  @  ( (k2_matrix_3 @ A)  @ B) ) )  @  ( ( (k1_matrix_3 @ A)  @  (k3_finseq_1 @ B) )  @  (k1_matrix_1 @ B) ) ) ) ) ) ) , file(matrix_4, t2_matrix_4)).
thf(t2_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) ) ) )  =>  ( ( ( (= @  (k3_finseq_1 @ B) )  @  (k3_finseq_1 @ C) )  &  ( (= @  (k1_matrix_1 @ B) )  @  (k1_matrix_1 @ C) ) )  =>  ( (= @  ( ( (k3_matrix_3 @ A)  @ B)  @ C) )  @  ( ( (k3_matrix_3 @ A)  @ C)  @ B) ) ) ) ) ) ) ) ) , file(matrix_3, t2_matrix_3)).
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(redefinition_k5_numbers, axiom,   ( (= @ k5_numbers)  @ k4_ordinal1) , file(numbers, k5_numbers)).
thf(fc8_vectsp_1, axiom,   ( ~ ( (v6_struct_0 @ k2_vectsp_1) )  &  ( (v13_algstr_0 @ k2_vectsp_1)  &  ( (v33_algstr_0 @ k2_vectsp_1)  &  ( (v36_algstr_0 @ k2_vectsp_1)  &  ( (v2_rlvect_1 @ k2_vectsp_1)  &  ( (v3_rlvect_1 @ k2_vectsp_1)  &  ( (v4_rlvect_1 @ k2_vectsp_1)  &  ( (v3_group_1 @ k2_vectsp_1)  &  ( (v5_group_1 @ k2_vectsp_1)  &  ( (v3_vectsp_1 @ k2_vectsp_1)  &  ( (v5_vectsp_1 @ k2_vectsp_1)  &  (v6_vectsp_1 @ k2_vectsp_1) ) ) ) ) ) ) ) ) ) ) ) , file(vectsp_1, fc8_vectsp_1)).
thf(fc6_vectsp_1, axiom,   ( (v36_algstr_0 @ k2_vectsp_1)  &  (v4_vectsp_1 @ k2_vectsp_1) ) , file(vectsp_1, fc6_vectsp_1)).
thf(fc6_membered, axiom,   (v6_membered @ k4_ordinal1) , file(membered, fc6_membered)).
thf(fc4_vectsp_1, axiom,   ( ~ ( (v2_struct_0 @ k2_vectsp_1) )  &  (v36_algstr_0 @ k2_vectsp_1) ) , file(vectsp_1, fc4_vectsp_1)).
thf(dt_k2_vectsp_1, axiom,   ( (v36_algstr_0 @ k2_vectsp_1)  &  (l6_algstr_0 @ k2_vectsp_1) ) , file(vectsp_1, k2_vectsp_1)).
thf(dt_k2_matrixr1, axiom,   (! [A: $i] :  ( ( (v1_matrix_1 @ A)  &  ( (m1_finseq_1 @ A)  @  (k3_finseq_2 @  (u1_struct_0 @ k2_vectsp_1) ) ) )  =>  ( (v1_matrix_1 @  (k2_matrixr1 @ A) )  &  ( (m2_finseq_1 @  (k2_matrixr1 @ A) )  @  (k3_finseq_2 @ k1_numbers) ) ) ) ) , file(matrixr1, k2_matrixr1)).
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_matrixr1, axiom,   (! [A: $i] :  ( ( (v1_matrix_1 @ A)  &  ( (m1_finseq_1 @ A)  @  (k3_finseq_2 @ k1_numbers) ) )  =>  ( (v1_matrix_1 @  (k1_matrixr1 @ A) )  &  ( (m2_finseq_1 @  (k1_matrixr1 @ A) )  @  (k3_finseq_2 @  (u1_struct_0 @ k2_vectsp_1) ) ) ) ) ) , file(matrixr1, k1_matrixr1)).
thf(d8_matrixr1, axiom,   (! [A: $i] :  ( (v7_ordinal1 @ A)  =>  (! [B: $i] :  ( (v7_ordinal1 @ B)  =>  ( (= @  ( (k8_matrixr1 @ A)  @ B) )  @  (k2_matrixr1 @  ( ( (k1_matrix_3 @ k2_vectsp_1)  @ A)  @ B) ) ) ) ) ) ) , file(matrixr1, d8_matrixr1)).
thf(d4_matrixr1, axiom,   (! [A: $i] :  ( ( (v1_matrix_1 @ A)  &  ( (m2_finseq_1 @ A)  @  (k3_finseq_2 @ k1_numbers) ) )  =>  ( (= @  (k4_matrixr1 @ A) )  @  (k2_matrixr1 @  ( (k2_matrix_3 @ k2_vectsp_1)  @  (k1_matrixr1 @ A) ) ) ) ) ) , file(matrixr1, d4_matrixr1)).
thf(d3_matrixr1, axiom,   (! [A: $i] :  ( ( (v1_matrix_1 @ A)  &  ( (m2_finseq_1 @ A)  @  (k3_finseq_2 @ k1_numbers) ) )  =>  (! [B: $i] :  ( ( (v1_matrix_1 @ B)  &  ( (m2_finseq_1 @ B)  @  (k3_finseq_2 @ k1_numbers) ) )  =>  ( (= @  ( (k3_matrixr1 @ A)  @ B) )  @  (k2_matrixr1 @  ( ( (k3_matrix_3 @ k2_vectsp_1)  @  (k1_matrixr1 @ A) )  @  (k1_matrixr1 @ B) ) ) ) ) ) ) ) , file(matrixr1, d3_matrixr1)).
thf(d2_matrixr1, axiom,   (! [A: $i] :  ( ( (v1_matrix_1 @ A)  &  ( (m2_finseq_1 @ A)  @  (k3_finseq_2 @  (u1_struct_0 @ k2_vectsp_1) ) ) )  =>  ( (= @  (k2_matrixr1 @ A) )  @ A) ) ) , file(matrixr1, d2_matrixr1)).
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_matrixr1, axiom,   (! [A: $i] :  ( ( (v1_matrix_1 @ A)  &  ( (m2_finseq_1 @ A)  @  (k3_finseq_2 @ k1_numbers) ) )  =>  ( (= @  (k1_matrixr1 @ A) )  @ A) ) ) , file(matrixr1, d1_matrixr1)).
thf(cc17_membered, axiom,   (! [A: $i] :  ( (v6_membered @ A)  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @ A)  =>  (v7_ordinal1 @ B) ) ) ) ) , file(membered, cc17_membered)).
thf(t31_matrixr2, conjecture,   (! [A: $i] :  ( ( (m1_subset_1 @ A)  @ k5_numbers)  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @ k5_numbers)  =>  (! [C: $i] :  ( ( (v1_matrix_1 @ C)  &  ( (m2_finseq_1 @ C)  @  (k3_finseq_2 @ k1_numbers) ) )  =>  ( ( ( (= @  (k3_finseq_1 @ C) )  @ A)  &  ( (= @  (k1_matrix_1 @ C) )  @ B) )  =>  ( (= @  ( (k3_matrixr1 @  (k4_matrixr1 @ C) )  @ C) )  @  ( (k8_matrixr1 @ A)  @ B) ) ) ) ) ) ) ) ) , file(matrixr2, t31_matrixr2)).