Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x4 x5 x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_8ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x5 ⟶ ChurchNum_8ary_proj_p x6 ⟶ ChurchNum_8ary_proj_p x7 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x1 x5 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x2 x6 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x4 x3 x7 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x2 x6 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x5 x3 x7 = λ x9 x10 . x9) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x6 x3 x7 = λ x9 x10 . x9) ⟶ ChurchNums_3x8_neq x0 x4 x1 x5 ⟶ ChurchNums_3x8_neq x0 x4 x2 x6 ⟶ ChurchNums_3x8_neq x0 x4 x3 x7 ⟶ ChurchNums_3x8_neq x1 x5 x2 x6 ⟶ ChurchNums_3x8_neq x1 x5 x3 x7 ⟶ ChurchNums_3x8_neq x2 x6 x3 x7 ⟶ False

as obj
-

as prop
aa35a..

theory
HotG

stx
e4dd4..

address
TMcpr..