include('Axioms/SET010^0.ax').
thf(v1_relat_1_type, type, v1_relat_1: $i > $o).
thf(v4_relat_1_type, type, v4_relat_1: $i > $i > $o).
thf(u1_struct_0_type, type, u1_struct_0: $i > $i).
thf(k1_scmfsa_2_type, type, k1_scmfsa_2: $i).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(v5_funct_1_type, type, v5_funct_1: $i > $i > $o).
thf(k2_memstr_0_type, type, k2_memstr_0: $i > $i > $i).
thf(n3_type, type, 3: $i).
thf(v1_partfun1_type, type, v1_partfun1: $i > $i > $o).
thf(k5_numbers_type, type, k5_numbers: $i).
thf(v5_relat_1_type, type, v5_relat_1: $i > $i > $o).
thf(u1_compos_1_type, type, u1_compos_1: $i > $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_finset_1_type, type, v1_finset_1: $i > $o).
thf(v1_afinsq_1_type, type, v1_afinsq_1: $i > $o).
thf(r5_scmfsa7b_type, type, r5_scmfsa7b: $i > $i > $i > $o).
thf(r6_scmfsa7b_type, type, r6_scmfsa7b: $i > $i > $i > $o).
thf(r1_scmfsa8a_type, type, r1_scmfsa8a: $i > $i > $i > $o).
thf(k2_scmfsa6a_type, type, k2_scmfsa6a: $i > $i).
thf(k2_scmfsa8a_type, type, k2_scmfsa8a: $i > $i > $i > $i).
thf(k2_nat_1_type, type, k2_nat_1: $i > $i > $i).
thf(k8_extpro_1_type, type, k8_extpro_1: $i > $i > $i > $i > $i).
thf(k1_funct_4_type, type, k1_funct_4: $i > $i > $i).
thf(k8_memstr_0_type, type, k8_memstr_0: $i > $i > $i > $i).
thf(n1_type, type, 1: $i).
thf(l28_scmfsa8a, axiom,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( ( (v4_relat_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) )  &  ( (v1_funct_1 @ A)  &  ( ( (v5_funct_1 @ A)  @  ( (k2_memstr_0 @ 3)  @ k1_scmfsa_2) )  &  ( (v1_partfun1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) ) ) ) )  =>  (! [B: $i] :  ( ( (v1_relat_1 @ B)  &  ( ( (v4_relat_1 @ B)  @ k5_numbers)  &  ( ( (v5_relat_1 @ B)  @  (u1_compos_1 @ k1_scmfsa_2) )  &  ( (v1_funct_1 @ B)  &  ( (v1_partfun1 @ B)  @ k5_numbers) ) ) ) )  =>  (! [C: $i] :  ( ( ~ ( (v1_xboole_0 @ C) )  &  ( (v1_relat_1 @ C)  &  ( ( (v4_relat_1 @ C)  @ k5_numbers)  &  ( ( (v5_relat_1 @ C)  @  (u1_compos_1 @ k1_scmfsa_2) )  &  ( (v1_funct_1 @ C)  &  ( (v1_finset_1 @ C)  &  (v1_afinsq_1 @ C) ) ) ) ) ) )  =>  ( ( ( ( (r5_scmfsa7b @ C)  @ A)  @ B)  &  ( ( (r6_scmfsa7b @ C)  @ A)  @ B) )  =>  ( ( ( (r1_scmfsa8a @ A)  @ B)  @  (k2_scmfsa6a @ C) )  &  ( (= @  ( ( (k2_scmfsa8a @ A)  @ B)  @  (k2_scmfsa6a @ C) ) )  @  ( (k2_nat_1 @  ( ( ( (k8_extpro_1 @ 3)  @ k1_scmfsa_2)  @  ( (k1_funct_4 @ B)  @ C) )  @  ( ( (k8_memstr_0 @ 3)  @ k1_scmfsa_2)  @ A) ) )  @ 1) ) ) ) ) ) ) ) ) ) , file(scmfsa8a, l28_scmfsa8a)).
thf(t23_scmfsa8a, conjecture,   (! [A: $i] :  ( ( (v1_relat_1 @ A)  &  ( ( (v4_relat_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) )  &  ( (v1_funct_1 @ A)  &  ( ( (v5_funct_1 @ A)  @  ( (k2_memstr_0 @ 3)  @ k1_scmfsa_2) )  &  ( (v1_partfun1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) ) ) ) )  =>  (! [B: $i] :  ( ( (v1_relat_1 @ B)  &  ( ( (v4_relat_1 @ B)  @ k5_numbers)  &  ( ( (v5_relat_1 @ B)  @  (u1_compos_1 @ k1_scmfsa_2) )  &  ( (v1_funct_1 @ B)  &  ( (v1_partfun1 @ B)  @ k5_numbers) ) ) ) )  =>  (! [C: $i] :  ( ( ~ ( (v1_xboole_0 @ C) )  &  ( (v1_relat_1 @ C)  &  ( ( (v4_relat_1 @ C)  @ k5_numbers)  &  ( ( (v5_relat_1 @ C)  @  (u1_compos_1 @ k1_scmfsa_2) )  &  ( (v1_funct_1 @ C)  &  ( (v1_finset_1 @ C)  &  (v1_afinsq_1 @ C) ) ) ) ) ) )  =>  ( ( ( ( (r5_scmfsa7b @ C)  @ A)  @ B)  &  ( ( (r6_scmfsa7b @ C)  @ A)  @ B) )  =>  ( ( (r1_scmfsa8a @ A)  @ B)  @  (k2_scmfsa6a @ C) ) ) ) ) ) ) ) ) , file(scmfsa8a, t23_scmfsa8a)).