| ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ ((λ x4 x5 . x0 x5 x5 x5 x5 x5 x5 x5 x5 x5 x4 x4 x4 x4 x4 x4 x4 x4) = λ x4 x5 . x4) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x0 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x1 ⟶ ∀ x3 : ο . x3) ⟶ ((λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x0 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4) ⟶ (TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4) ⟶ False |
|