include('Axioms/SET010^0.ax').
thf(v2_struct_0_type, type, v2_struct_0: $i > $o).
thf(v13_algstr_0_type, type, v13_algstr_0: $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(v3_group_1_type, type, v3_group_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(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k5_numbers_type, type, k5_numbers: $i).
thf(k2_compos_0_type, type, k2_compos_0: $i > $i > $i).
thf(u1_compos_1_type, type, u1_compos_1: $i > $i).
thf(k1_scmring2_type, type, k1_scmring2: $i > $i).
thf(k8_scmring2_type, type, k8_scmring2: $i > $i > $i).
thf(n6_type, type, 6: $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_compos_0_type, type, v1_compos_0: $i > $o).
thf(k4_xtuple_0_type, type, k4_xtuple_0: $i > $i).
thf(k1_xtuple_0_type, type, k1_xtuple_0: $i > $i).
thf(k4_tarski_type, type, k4_tarski: $i > $i > $i).
thf(l1_compos_1_type, type, l1_compos_1: $i > $o).
thf(v2_compos_0_type, type, v2_compos_0: $i > $o).
thf(v3_compos_0_type, type, v3_compos_0: $i > $o).
thf(v5_compos_0_type, type, v5_compos_0: $i > $o).
thf(l1_extpro_1_type, type, l1_extpro_1: $i > $i > $o).
thf(l1_memstr_0_type, type, l1_memstr_0: $i > $i > $o).
thf(v1_extpro_1_type, type, v1_extpro_1: $i > $i > $o).
thf(n2_type, type, 2: $i).
thf(k3_xtuple_0_type, type, k3_xtuple_0: $i > $i > $i > $i).
thf(k12_finseq_1_type, type, k12_finseq_1: $i > $i > $i).
thf(k1_xboole_0_type, type, k1_xboole_0: $i).
thf(redefinition_k2_compos_0, axiom,   (! [A: $i, B: $i] :  ( ( ( ~ ( (v1_xboole_0 @ A) )  &  (v1_compos_0 @ A) )  &  ( (m1_subset_1 @ B)  @ A) )  =>  ( (= @  ( (k2_compos_0 @ A)  @ B) )  @  (k4_xtuple_0 @ B) ) ) ) , file(compos_0, k2_compos_0)).
thf(rd1_xtuple_0, axiom,   (! [A: $i, B: $i] :  ( (= @  (k1_xtuple_0 @  ( (k4_tarski @ A)  @ B) ) )  @ A) ) , file(xtuple_0, rd1_xtuple_0)).
thf(dt_u1_compos_1, axiom,   (! [A: $i] :  ( (l1_compos_1 @ A)  =>  ( (v1_compos_0 @  (u1_compos_1 @ A) )  &  ( (v2_compos_0 @  (u1_compos_1 @ A) )  &  ( (v3_compos_0 @  (u1_compos_1 @ A) )  &  (v5_compos_0 @  (u1_compos_1 @ A) ) ) ) ) ) ) , file(compos_1, u1_compos_1)).
thf(dt_l1_extpro_1, axiom,   (! [A: $i] :  (! [B: $i] :  ( ( (l1_extpro_1 @ B)  @ A)  =>  ( ( (l1_memstr_0 @ B)  @ A)  &  (l1_compos_1 @ B) ) ) ) ) , file(extpro_1, l1_extpro_1)).
thf(dt_k8_scmring2, axiom,   (! [A: $i, B: $i] :  ( ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  ( (v3_group_1 @ A)  &  ( (v4_vectsp_1 @ A)  &  ( (v5_vectsp_1 @ A)  &  (l6_algstr_0 @ A) ) ) ) ) ) ) ) )  &  ( (m1_subset_1 @ B)  @ k5_numbers) )  =>  ( (m1_subset_1 @  ( (k8_scmring2 @ A)  @ B) )  @  (u1_compos_1 @  (k1_scmring2 @ A) ) ) ) ) , file(scmring2, k8_scmring2)).
thf(dt_k1_scmring2, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  ( (v3_group_1 @ A)  &  ( (v4_vectsp_1 @ A)  &  ( (v5_vectsp_1 @ A)  &  (l6_algstr_0 @ A) ) ) ) ) ) ) ) )  =>  ( ( (v1_extpro_1 @  (k1_scmring2 @ A) )  @ 2)  &  ( (l1_extpro_1 @  (k1_scmring2 @ A) )  @ 2) ) ) ) , file(scmring2, k1_scmring2)).
thf(d8_scmring2, axiom,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  ( (v3_group_1 @ A)  &  ( (v4_vectsp_1 @ A)  &  ( (v5_vectsp_1 @ A)  &  (l6_algstr_0 @ A) ) ) ) ) ) ) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @ k5_numbers)  =>  ( (= @  ( (k8_scmring2 @ A)  @ B) )  @  ( ( (k3_xtuple_0 @ 6)  @  ( (k12_finseq_1 @ k5_numbers)  @ B) )  @ k1_xboole_0) ) ) ) ) ) , file(scmring2, d8_scmring2)).
thf(d6_xtuple_0, axiom,   (! [A: $i] :  ( (= @  (k4_xtuple_0 @ A) )  @  (k1_xtuple_0 @  (k1_xtuple_0 @ A) ) ) ) , file(xtuple_0, d6_xtuple_0)).
thf(d4_xtuple_0, axiom,   (! [A: $i] :  (! [B: $i] :  (! [C: $i] :  ( (= @  ( ( (k3_xtuple_0 @ A)  @ B)  @ C) )  @  ( (k4_tarski @  ( (k4_tarski @ A)  @ B) )  @ C) ) ) ) ) , file(xtuple_0, d4_xtuple_0)).
thf(cc2_compos_0, axiom,   (! [A: $i] :  ( (v5_compos_0 @ A)  =>  ~ ( (v1_xboole_0 @ A) ) ) ) , file(compos_0, cc2_compos_0)).
thf(t10_scmring3, conjecture,   (! [A: $i] :  ( ( ~ ( (v2_struct_0 @ A) )  &  ( (v13_algstr_0 @ A)  &  ( (v2_rlvect_1 @ A)  &  ( (v3_rlvect_1 @ A)  &  ( (v4_rlvect_1 @ A)  &  ( (v3_group_1 @ A)  &  ( (v4_vectsp_1 @ A)  &  ( (v5_vectsp_1 @ A)  &  (l6_algstr_0 @ A) ) ) ) ) ) ) ) )  =>  (! [B: $i] :  ( ( (m1_subset_1 @ B)  @ k5_numbers)  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @  (k1_scmring2 @ A) ) )  @  ( (k8_scmring2 @ A)  @ B) ) )  @ 6) ) ) ) ) , file(scmring3, t10_scmring3)).