include('Axioms/SET010^0.ax').
thf(m2_finseq_2_type, type, m2_finseq_2: $i > $i > $i > $o).
thf(k1_numbers_type, type, k1_numbers: $i).
thf(k1_euclid_type, type, k1_euclid: $i > $i).
thf(n3_type, type, 3: $i).
thf(v1_funct_1_type, type, v1_funct_1: $i > $o).
thf(m1_subset_1_type, type, m1_subset_1: $i > $i > $o).
thf(k1_zfmisc_1_type, type, k1_zfmisc_1: $i > $i).
thf(k2_zfmisc_1_type, type, k2_zfmisc_1: $i > $i > $i).
thf(r5_pdiff_5_type, type, r5_pdiff_5: $i > $i > $o).
thf(r3_pdiff_1_type, type, r3_pdiff_1: $i > $i > $i > $i > $o).
thf(n2_type, type, 2: $i).
thf(k1_pdiff_3_type, type, k1_pdiff_3: $i > $i > $i > $i).
thf(k11_finseq_1_type, type, k11_finseq_1: $i > $i > $i > $i).
thf(m1_rcomp_1_type, type, m1_rcomp_1: $i > $i > $o).
thf(r1_tarski_type, type, r1_tarski: $i > $i > $o).
thf(k1_relset_1_type, type, k1_relset_1: $i > $i > $i).
thf(k1_pdiff_2_type, type, k1_pdiff_2: $i > $i > $i > $i > $i).
thf(v3_fdiff_1_type, type, v3_fdiff_1: $i > $o).
thf(v2_fdiff_1_type, type, v2_fdiff_1: $i > $o).
thf(k9_real_1_type, type, k9_real_1: $i > $i > $i).
thf(k1_seq_1_type, type, k1_seq_1: $i > $i > $i).
thf(k7_real_1_type, type, k7_real_1: $i > $i > $i).
thf(v2_xxreal_0_type, type, v2_xxreal_0: $i > $o).
thf(m2_subset_1_type, type, m2_subset_1: $i > $i > $i > $o).
thf(k5_numbers_type, type, k5_numbers: $i).
thf(v1_xboole_0_type, type, v1_xboole_0: $i > $o).
thf(v1_funct_2_type, type, v1_funct_2: $i > $i > $i > $o).
thf(t14_pdiff_4, axiom,   (! [A: $i] :  ( ( (v1_funct_1 @ A)  &  ( (m1_subset_1 @ A)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (k1_euclid @ 3) )  @ k1_numbers) ) ) )  =>  (! [B: $i] :  ( ( ( (m2_finseq_2 @ B)  @ k1_numbers)  @  (k1_euclid @ 3) )  =>  ( ( ( ( (r3_pdiff_1 @ 3)  @ 2)  @ A)  @ B)  <=>  (? [C: $i] :  ( ( (m1_subset_1 @ C)  @ k1_numbers)  &  (? [D: $i] :  ( ( (m1_subset_1 @ D)  @ k1_numbers)  &  (? [E: $i] :  ( ( (m1_subset_1 @ E)  @ k1_numbers)  &  ( ( (= @ B)  @  ( ( (k11_finseq_1 @ C)  @ D)  @ E) )  &  (? [F: $i] :  ( ( (m1_rcomp_1 @ F)  @ D)  &  ( ( (r1_tarski @ F)  @  ( (k1_relset_1 @ k1_numbers)  @  ( ( ( (k1_pdiff_2 @ 3)  @ 2)  @ A)  @ B) ) )  &  (? [G: $i] :  ( ( (v1_funct_1 @ G)  &  ( (v3_fdiff_1 @ G)  &  ( (m1_subset_1 @ G)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ k1_numbers)  @ k1_numbers) ) ) ) )  &  (? [H: $i] :  ( ( (v1_funct_1 @ H)  &  ( (v2_fdiff_1 @ H)  &  ( (m1_subset_1 @ H)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ k1_numbers)  @ k1_numbers) ) ) ) )  &  (! [I: $i] :  ( ( (m1_subset_1 @ I)  @ k1_numbers)  =>  ( ( (r2_hidden @ I)  @ F)  =>  ( (= @  ( (k9_real_1 @  ( (k1_seq_1 @  ( ( ( (k1_pdiff_2 @ 3)  @ 2)  @ A)  @ B) )  @ I) )  @  ( (k1_seq_1 @  ( ( ( (k1_pdiff_2 @ 3)  @ 2)  @ A)  @ B) )  @ D) ) )  @  ( (k7_real_1 @  ( (k1_seq_1 @ G)  @  ( (k9_real_1 @ I)  @ D) ) )  @  ( (k1_seq_1 @ H)  @  ( (k9_real_1 @ I)  @ D) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(pdiff_4, t14_pdiff_4)).
thf(spc3_numerals, axiom,   ( ( (v2_xxreal_0 @ 3)  &  ( ( (m2_subset_1 @ 3)  @ k1_numbers)  @ k5_numbers) )  &  ( ( (m1_subset_1 @ 3)  @ k5_numbers)  &  ( (m1_subset_1 @ 3)  @ k1_numbers) ) ) , file(numerals, spc3_numerals)).
thf(spc3_boole, axiom,   ~ ( (v1_xboole_0 @ 3) ) , file(boole, spc3_boole)).
thf(spc2_numerals, axiom,   ( ( (v2_xxreal_0 @ 2)  &  ( ( (m2_subset_1 @ 2)  @ k1_numbers)  @ k5_numbers) )  &  ( ( (m1_subset_1 @ 2)  @ k5_numbers)  &  ( (m1_subset_1 @ 2)  @ k1_numbers) ) ) , file(numerals, spc2_numerals)).
thf(dt_k1_pdiff_3, axiom,   (! [A: $i, B: $i, C: $i] :  ( ( ( (m1_subset_1 @ A)  @ k5_numbers)  &  ( ( ~ ( (v1_xboole_0 @ B) )  &  ( (m1_subset_1 @ B)  @ k5_numbers) )  &  ( (v1_funct_1 @ C)  &  ( (m1_subset_1 @ C)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (k1_euclid @ B) )  @ k1_numbers) ) ) ) ) )  =>  ( (v1_funct_1 @  ( ( (k1_pdiff_3 @ A)  @ B)  @ C) )  &  ( ( ( (v1_funct_2 @  ( ( (k1_pdiff_3 @ A)  @ B)  @ C) )  @  (k1_euclid @ B) )  @ k1_numbers)  &  ( (m1_subset_1 @  ( ( (k1_pdiff_3 @ A)  @ B)  @ C) )  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (k1_euclid @ B) )  @ k1_numbers) ) ) ) ) ) ) , file(pdiff_3, k1_pdiff_3)).
thf(d5_pdiff_5, axiom,   (! [A: $i] :  ( ( (v1_funct_1 @ A)  &  ( (m1_subset_1 @ A)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (k1_euclid @ 3) )  @ k1_numbers) ) ) )  =>  (! [B: $i] :  ( ( ( (m2_finseq_2 @ B)  @ k1_numbers)  @  (k1_euclid @ 3) )  =>  ( ( (r5_pdiff_5 @ A)  @ B)  <=>  (? [C: $i] :  ( ( (m1_subset_1 @ C)  @ k1_numbers)  &  (? [D: $i] :  ( ( (m1_subset_1 @ D)  @ k1_numbers)  &  (? [E: $i] :  ( ( (m1_subset_1 @ E)  @ k1_numbers)  &  ( ( (= @ B)  @  ( ( (k11_finseq_1 @ C)  @ D)  @ E) )  &  (? [F: $i] :  ( ( (m1_rcomp_1 @ F)  @ D)  &  ( ( (r1_tarski @ F)  @  ( (k1_relset_1 @ k1_numbers)  @  ( ( ( (k1_pdiff_2 @ 3)  @ 2)  @  ( ( (k1_pdiff_3 @ 2)  @ 3)  @ A) )  @ B) ) )  &  (? [G: $i] :  ( ( (v1_funct_1 @ G)  &  ( (v3_fdiff_1 @ G)  &  ( (m1_subset_1 @ G)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ k1_numbers)  @ k1_numbers) ) ) ) )  &  (? [H: $i] :  ( ( (v1_funct_1 @ H)  &  ( (v2_fdiff_1 @ H)  &  ( (m1_subset_1 @ H)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @ k1_numbers)  @ k1_numbers) ) ) ) )  &  (! [I: $i] :  ( ( (m1_subset_1 @ I)  @ k1_numbers)  =>  ( ( (r2_hidden @ I)  @ F)  =>  ( (= @  ( (k9_real_1 @  ( (k1_seq_1 @  ( ( ( (k1_pdiff_2 @ 3)  @ 2)  @  ( ( (k1_pdiff_3 @ 2)  @ 3)  @ A) )  @ B) )  @ I) )  @  ( (k1_seq_1 @  ( ( ( (k1_pdiff_2 @ 3)  @ 2)  @  ( ( (k1_pdiff_3 @ 2)  @ 3)  @ A) )  @ B) )  @ D) ) )  @  ( (k7_real_1 @  ( (k1_seq_1 @ G)  @  ( (k9_real_1 @ I)  @ D) ) )  @  ( (k1_seq_1 @ H)  @  ( (k9_real_1 @ I)  @ D) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) , file(pdiff_5, d5_pdiff_5)).
thf(t23_pdiff_5, conjecture,   (! [A: $i] :  ( ( ( (m2_finseq_2 @ A)  @ k1_numbers)  @  (k1_euclid @ 3) )  =>  (! [B: $i] :  ( ( (v1_funct_1 @ B)  &  ( (m1_subset_1 @ B)  @  (k1_zfmisc_1 @  ( (k2_zfmisc_1 @  (k1_euclid @ 3) )  @ k1_numbers) ) ) )  =>  ( ( (r5_pdiff_5 @ B)  @ A)  <=>  ( ( ( (r3_pdiff_1 @ 3)  @ 2)  @  ( ( (k1_pdiff_3 @ 2)  @ 3)  @ B) )  @ A) ) ) ) ) ) , file(pdiff_5, t23_pdiff_5)).