include('Axioms/SET010^0.ax').
thf(v1_ami_2_type, type, v1_ami_2: $i > $o).
thf(m1_subset_1_type, type, m1_subset_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(r3_scmfsa7b_type, type, r3_scmfsa7b: $i > $i > $o).
thf(k6_scmfsa_2_type, type, k6_scmfsa_2: $i > $i > $i).
thf(m1_scmfsa_2_type, type, m1_scmfsa_2: $i > $o).
thf(k2_compos_0_type, type, k2_compos_0: $i > $i > $i).
thf(u1_compos_1_type, type, u1_compos_1: $i > $i).
thf(k16_scmfsa_2_type, type, k16_scmfsa_2: $i > $i > $i).
thf(n11_type, type, 11: $i).
thf(k14_scmfsa_2_type, type, k14_scmfsa_2: $i > $i > $i > $i).
thf(n9_type, type, 9: $i).
thf(k10_scmfsa_2_type, type, k10_scmfsa_2: $i > $i > $i).
thf(n5_type, type, 5: $i).
thf(k9_scmfsa_2_type, type, k9_scmfsa_2: $i > $i > $i).
thf(n4_type, type, 4: $i).
thf(k8_scmfsa_2_type, type, k8_scmfsa_2: $i > $i > $i).
thf(n3_type, type, 3: $i).
thf(k7_scmfsa_2_type, type, k7_scmfsa_2: $i > $i > $i).
thf(n2_type, type, 2: $i).
thf(n1_type, type, 1: $i).
thf(t28_scmfsa_2, axiom,   (! [A: $i] :  ( (m1_scmfsa_2 @ A)  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( (k16_scmfsa_2 @ B)  @ A) ) )  @ 11) ) ) ) ) , file(scmfsa_2, t28_scmfsa_2)).
thf(t26_scmfsa_2, axiom,   (! [A: $i] :  ( (m1_scmfsa_2 @ A)  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [C: $i] :  ( ( (v1_ami_2 @ C)  &  ( (m1_subset_1 @ C)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( ( (k14_scmfsa_2 @ B)  @ C)  @ A) ) )  @ 9) ) ) ) ) ) ) , file(scmfsa_2, t26_scmfsa_2)).
thf(t22_scmfsa_2, axiom,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( (k10_scmfsa_2 @ A)  @ B) ) )  @ 5) ) ) ) ) , file(scmfsa_2, t22_scmfsa_2)).
thf(t21_scmfsa_2, axiom,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( (k9_scmfsa_2 @ A)  @ B) ) )  @ 4) ) ) ) ) , file(scmfsa_2, t21_scmfsa_2)).
thf(t20_scmfsa_2, axiom,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( (k8_scmfsa_2 @ A)  @ B) ) )  @ 3) ) ) ) ) , file(scmfsa_2, t20_scmfsa_2)).
thf(t1_sf_mastr, axiom,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [C: $i] :  ( ( (v1_ami_2 @ C)  &  ( (m1_subset_1 @ C)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [D: $i] :  ( ( (v1_ami_2 @ D)  &  ( (m1_subset_1 @ D)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( ( (= @  ( (k6_scmfsa_2 @ A)  @ B) )  @  ( (k6_scmfsa_2 @ C)  @ D) )  =>  ( ( (= @ A)  @ C)  &  ( (= @ B)  @ D) ) ) ) ) ) ) ) ) ) ) , file(sf_mastr, t1_sf_mastr)).
thf(t19_scmfsa_2, axiom,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( (k7_scmfsa_2 @ A)  @ B) ) )  @ 2) ) ) ) ) , file(scmfsa_2, t19_scmfsa_2)).
thf(t18_scmfsa_2, axiom,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( (= @  ( (k2_compos_0 @  (u1_compos_1 @ k1_scmfsa_2) )  @  ( (k6_scmfsa_2 @ A)  @ B) ) )  @ 1) ) ) ) ) , file(scmfsa_2, t18_scmfsa_2)).
thf(dt_k6_scmfsa_2, axiom,   (! [A: $i, B: $i] :  ( ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  &  ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) ) )  =>  ( (m1_subset_1 @  ( (k6_scmfsa_2 @ A)  @ B) )  @  (u1_compos_1 @ k1_scmfsa_2) ) ) ) , file(scmfsa_2, k6_scmfsa_2)).
thf(d3_scmfsa7b, axiom,   (! [A: $i] :  ( ( (m1_subset_1 @ A)  @  (u1_compos_1 @ k1_scmfsa_2) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ( ( (r3_scmfsa7b @ A)  @ B)  <=>  ~ ( (! [C: $i] :  ( ( (v1_ami_2 @ C)  &  ( (m1_subset_1 @ C)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [D: $i] :  ( (m1_scmfsa_2 @ D)  =>  ( ~ ( ( (= @  ( (k6_scmfsa_2 @ B)  @ C) )  @ A) )  &  ( ~ ( ( (= @  ( (k7_scmfsa_2 @ B)  @ C) )  @ A) )  &  ( ~ ( ( (= @  ( (k8_scmfsa_2 @ B)  @ C) )  @ A) )  &  ( ~ ( ( (= @  ( (k9_scmfsa_2 @ B)  @ C) )  @ A) )  &  ( ~ ( ( (= @  ( (k10_scmfsa_2 @ B)  @ C) )  @ A) )  &  ( ~ ( ( (= @  ( (k10_scmfsa_2 @ C)  @ B) )  @ A) )  &  ( ~ ( ( (= @  ( ( (k14_scmfsa_2 @ B)  @ C)  @ D) )  @ A) )  &  ~ ( ( (= @  ( (k16_scmfsa_2 @ B)  @ D) )  @ A) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(scmfsa7b, d3_scmfsa7b)).
thf(t6_scmfsa7b, conjecture,   (! [A: $i] :  ( ( (v1_ami_2 @ A)  &  ( (m1_subset_1 @ A)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [B: $i] :  ( ( (v1_ami_2 @ B)  &  ( (m1_subset_1 @ B)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  (! [C: $i] :  ( ( (v1_ami_2 @ C)  &  ( (m1_subset_1 @ C)  @  (u1_struct_0 @ k1_scmfsa_2) ) )  =>  ~ ( ( ~ ( ( (= @ A)  @ B) )  &  ( (r3_scmfsa7b @  ( (k6_scmfsa_2 @ B)  @ C) )  @ A) ) ) ) ) ) ) ) ) , file(scmfsa7b, t6_scmfsa7b)).