Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known 0e1c2.. : ∀ x0 x1 : ι → ο . ∀ x2 x3 x4 x5 x6 x7 . (∀ x8 : ι → ο . x8 x2 ⟶ x8 x3 ⟶ x8 x4 ⟶ x8 x5 ⟶ x8 x6 ⟶ x8 x7 ⟶ ∀ x9 . x0 x9 ⟶ x8 x9) ⟶ x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ ∀ x8 x9 x10 : ι → ι . x8 x2 = x3 ⟶ x8 x3 = x2 ⟶ x8 x4 = x5 ⟶ x8 x5 = x4 ⟶ x9 x2 = x4 ⟶ x9 x3 = x5 ⟶ x9 x4 = x2 ⟶ x9 x5 = x3 ⟶ x10 x2 = x5 ⟶ x10 x3 = x4 ⟶ x10 x4 = x3 ⟶ x10 x5 = x2 ⟶ ∀ x11 : ι → ι → ι → ι → ο . (∀ x12 x13 . x0 x12 ⟶ x0 x13 ⟶ not (x11 x12 x13 x12 x13)) ⟶ (∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15 ⟶ x11 x14 x15 x12 x13) ⟶ (∀ x12 x13 . x0 x12 ⟶ x0 x13 ⟶ not (x11 x12 x13 x7 x7)) ⟶ (∀ x12 x13 x14 x15 . x0 x12 ⟶ x1 x13 ⟶ x0 x14 ⟶ x1 x15 ⟶ not (x11 x12 x13 x14 x15) ⟶ not (x11 x12 (x8 x13) x14 (x8 x15))) ⟶ (∀ x12 x13 x14 x15 . x0 x12 ⟶ x1 x13 ⟶ x0 x14 ⟶ x1 x15 ⟶ not (x11 x12 x13 x14 x15) ⟶ not (x11 x12 (x9 x13) x14 (x9 x15))) ⟶ (∀ x12 x13 x14 x15 . x0 x12 ⟶ x1 x13 ⟶ x0 x14 ⟶ x1 x15 ⟶ not (x11 x12 x13 x14 x15) ⟶ not (x11 x12 (x10 x13) x14 (x10 x15))) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x6 x5 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x6 x7 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x7 x5 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x4 x7 x7 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x6 x6 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x7 x6 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x6 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x6 x4 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x7 x2 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x7 x4 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x7 x6 x7 x12)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x2 x2 x12 x7)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x2 x3 x12 x6)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x5 x5 x12 x7)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x2 x12 x6)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x3 x12 x7)) ⟶ (∀ x12 . x0 x12 ⟶ not (x11 x6 x7 x12 x7)) ⟶ not (x11 x2 x2 x2 x3) ⟶ not (x11 x2 x2 x2 x5) ⟶ not (x11 x2 x2 x3 x4) ⟶ not (x11 x2 x2 x3 x5) ⟶ not (x11 x2 x2 x4 x2) ⟶ not (x11 x2 x2 x4 x3) ⟶ not (x11 x2 x2 x5 x2) ⟶ not (x11 x2 x2 x5 x5) ⟶ not (x11 x2 x2 x6 x2) ⟶ not (x11 x2 x2 x6 x3) ⟶ not (x11 x2 x2 x7 x3) ⟶ not (x11 x2 x2 x7 x6) ⟶ not (x11 x2 x3 x4 x2) ⟶ not (x11 x2 x3 x6 x2) ⟶ not (x11 x2 x3 x7 x2) ⟶ not (x11 x2 x4 x2 x6) ⟶ not (x11 x2 x4 x3 x2) ⟶ not (x11 x2 x4 x3 x7) ⟶ not (x11 x2 x4 x4 x7) ⟶ not (x11 x2 x4 x5 x6) ⟶ not (x11 x2 x4 x7 x6) ⟶ not (x11 x2 x5 x2 x7) ⟶ not (x11 x2 x5 x3 x2) ⟶ not (x11 x2 x5 x3 x6) ⟶ not (x11 x2 x5 x4 x6) ⟶ not (x11 x2 x5 x5 x2) ⟶ not (x11 x2 x5 x5 x7) ⟶ not (x11 x2 x5 x7 x6) ⟶ not (x11 x2 x6 x2 x7) ⟶ not (x11 x2 x6 x3 x2) ⟶ not (x11 x2 x6 x3 x5) ⟶ not (x11 x2 x6 x3 x6) ⟶ not (x11 x2 x6 x3 x7) ⟶ not (x11 x2 x6 x4 x3) ⟶ not (x11 x2 x6 x4 x4) ⟶ not (x11 x2 x6 x5 x3) ⟶ not (x11 x2 x6 x5 x4) ⟶ not (x11 x2 x6 x6 x5) ⟶ not (x11 x2 x6 x7 x2) ⟶ not (x11 x2 x6 x7 x3) ⟶ not (x11 x2 x6 x7 x4) ⟶ not (x11 x2 x6 x7 x5) ⟶ not (x11 x2 x7 x3 x3) ⟶ not (x11 x2 x7 x3 x4) ⟶ not (x11 x2 x7 x3 x6) ⟶ not (x11 x2 x7 x3 x7) ⟶ not (x11 x2 x7 x4 x2) ⟶ not (x11 x2 x7 x4 x5) ⟶ not (x11 x2 x7 x5 x2) ⟶ not (x11 x2 x7 x6 x4) ⟶ not (x11 x2 x7 x7 x2) ⟶ not (x11 x2 x7 x7 x3) ⟶ not (x11 x2 x7 x7 x4) ⟶ not (x11 x2 x7 x7 x5) ⟶ not (x11 x3 x2 x3 x3) ⟶ not (x11 x3 x2 x3 x5) ⟶ not (x11 x3 x2 x3 x6) ⟶ not (x11 x3 x2 x4 x3) ⟶ not (x11 x3 x2 x4 x4) ⟶ not (x11 x3 x2 x4 x5) ⟶ not (x11 x3 x2 x4 x7) ⟶ not (x11 x3 x2 x5 x2) ⟶ not (x11 x3 x2 x5 x7) ⟶ not (x11 x3 x2 x6 x2) ⟶ not (x11 x3 x2 x6 x5) ⟶ not (x11 x3 x2 x6 x6) ⟶ not (x11 x3 x2 x7 x2) ⟶ not (x11 x3 x2 x7 x4) ⟶ not (x11 x3 x2 x7 x5) ⟶ not (x11 x3 x2 x7 x6) ⟶ not (x11 x3 x3 x3 x7) ⟶ not (x11 x3 x3 x4 x2) ⟶ not (x11 x3 x3 x4 x6) ⟶ not (x11 x3 x3 x5 x6) ⟶ not (x11 x3 x3 x6 x7) ⟶ not (x11 x3 x3 x7 x6) ⟶ not (x11 x3 x4 x3 x6) ⟶ not (x11 x3 x4 x4 x2) ⟶ not (x11 x3 x4 x4 x7) ⟶ not (x11 x3 x4 x5 x6) ⟶ not (x11 x3 x4 x6 x6) ⟶ not (x11 x3 x4 x7 x2) ⟶ not (x11 x3 x4 x7 x6) ⟶ not (x11 x3 x5 x3 x7) ⟶ not (x11 x3 x5 x4 x2) ⟶ not (x11 x3 x5 x4 x6) ⟶ not (x11 x3 x5 x5 x7) ⟶ not (x11 x3 x5 x6 x2) ⟶ not (x11 x3 x5 x6 x7) ⟶ not (x11 x3 x5 x7 x2) ⟶ not (x11 x3 x5 x7 x6) ⟶ not (x11 x3 x6 x4 x2) ⟶ not (x11 x3 x6 x4 x4) ⟶ not (x11 x3 x6 x4 x6) ⟶ not (x11 x3 x6 x4 x7) ⟶ not (x11 x3 x6 x5 x2) ⟶ not (x11 x3 x6 x5 x3) ⟶ not (x11 x3 x6 x5 x4) ⟶ not (x11 x3 x6 x5 x5) ⟶ not (x11 x3 x6 x6 x3) ⟶ not (x11 x3 x6 x6 x4) ⟶ not (x11 x3 x6 x6 x5) ⟶ not (x11 x3 x6 x6 x6) ⟶ not (x11 x3 x6 x7 x2) ⟶ not (x11 x3 x6 x7 x4) ⟶ not (x11 x3 x7 x4 x3) ⟶ not (x11 x3 x7 x4 x5) ⟶ not (x11 x3 x7 x4 x6) ⟶ not (x11 x3 x7 x4 x7) ⟶ not (x11 x3 x7 x5 x2) ⟶ not (x11 x3 x7 x5 x3) ⟶ not (x11 x3 x7 x5 x4) ⟶ not (x11 x3 x7 x6 x2) ⟶ not (x11 x3 x7 x6 x4) ⟶ not (x11 x3 x7 x6 x5) ⟶ not (x11 x3 x7 x7 x3) ⟶ not (x11 x3 x7 x7 x5) ⟶ not (x11 x4 x2 x4 x4) ⟶ not (x11 x4 x2 x4 x5) ⟶ not (x11 x4 x2 x4 x7) ⟶ not (x11 x4 x2 x5 x2) ⟶ not (x11 x4 x2 x5 x5) ⟶ not (x11 x4 x2 x5 x6) ⟶ not (x11 x4 x2 x6 x2) ⟶ not (x11 x4 x2 x6 x3) ⟶ not (x11 x4 x2 x7 x2) ⟶ not (x11 x4 x2 x7 x3) ⟶ not (x11 x4 x2 x7 x5) ⟶ not (x11 x4 x3 x4 x6) ⟶ not (x11 x4 x3 x5 x7) ⟶ not (x11 x4 x3 x6 x2) ⟶ not (x11 x4 x3 x7 x2) ⟶ not (x11 x4 x4 x4 x7) ⟶ not (x11 x4 x4 x5 x7) ⟶ not (x11 x4 x5 x4 x6) ⟶ not (x11 x4 x5 x5 x2) ⟶ not (x11 x4 x5 x5 x6) ⟶ not (x11 x4 x5 x7 x2) ⟶ not (x11 x4 x6 x6 x4) ⟶ not (x11 x4 x7 x6 x5) ⟶ not (x11 x5 x2 x5 x4) ⟶ not (x11 x5 x2 x5 x5) ⟶ not (x11 x5 x2 x5 x7) ⟶ not (x11 x5 x2 x6 x2) ⟶ not (x11 x5 x2 x6 x3) ⟶ not (x11 x5 x2 x6 x5) ⟶ not (x11 x5 x2 x6 x6) ⟶ not (x11 x5 x2 x7 x4) ⟶ not (x11 x5 x2 x7 x5) ⟶ not (x11 x5 x3 x5 x6) ⟶ not (x11 x5 x3 x6 x2) ⟶ not (x11 x5 x3 x6 x7) ⟶ not (x11 x5 x4 x5 x6) ⟶ not (x11 x5 x4 x6 x6) ⟶ not (x11 x5 x4 x7 x2) ⟶ not (x11 x5 x5 x6 x2) ⟶ not (x11 x5 x5 x7 x2) ⟶ not (x11 x5 x6 x5 x7) ⟶ not (x11 x5 x6 x7 x2) ⟶ not (x11 x5 x6 x7 x5) ⟶ not (x11 x5 x6 x7 x6) ⟶ not (x11 x5 x7 x7 x3) ⟶ not (x11 x5 x7 x7 x4) ⟶ not (x11 x5 x7 x7 x6) ⟶ not (x11 x6 x2 x6 x3) ⟶ not (x11 x6 x2 x7 x4) ⟶ not (x11 x6 x2 x7 x5) ⟶ not (x11 x6 x3 x7 x6) ⟶ not (x11 x6 x4 x6 x6) ⟶ not (x11 x6 x4 x7 x2) ⟶ not (x11 x6 x4 x7 x6) ⟶ not (x11 x6 x5 x6 x7) ⟶ not (x11 x6 x5 x7 x2) ⟶ not (x11 x6 x5 x7 x6) ⟶ not (x11 x6 x6 x6 x7) ⟶ not (x11 x7 x2 x7 x3) ⟶ not (x11 x7 x2 x7 x4) ⟶ ∀ x12 . x0 x12 ⟶ ∀ x13 . x0 x13 ⟶ ∀ x14 . x0 x14 ⟶ ∀ x15 . x0 x15 ⟶ ∀ x16 . x0 x16 ⟶ ∀ x17 . x0 x17 ⟶ ∀ x18 . x0 x18 ⟶ ∀ x19 . x0 x19 ⟶ x11 x12 x13 x14 x15 ⟶ x11 x12 x13 x16 x17 ⟶ x11 x12 x13 x18 x19 ⟶ x11 x14 x15 x16 x17 ⟶ x11 x14 x15 x18 x19 ⟶ x11 x16 x17 x18 x19 ⟶ False
Param u6 : ι
Definition TwoRamseyGraph_4_6_Church6_squared_b := λ x0 x1 x2 x3 : ι → ι → ι → ι → ι → ι → ι . λ x4 x5 . x0 (x1 (x2 (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x4 x5 x4 x4 x5 x5)) (x2 (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x4 x4 x4 x5 x5)) (x2 (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x4 x5 x5 x5)) (x2 (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x4 x5 x5)) (x2 (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x5)) (x2 (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x5))) (x1 (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x4 x4 x4 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x4 x5 x5 x5 x5)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x4 x5 x4 x4 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x5)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x4 x5) (x3 x4 x4 x5 x4 x5 x4) (x3 x4 x5 x5 x4 x5 x4) (x3 x5 x5 x5 x4 x5 x5)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x5)) (x2 (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x4 x4 x5)) (x2 (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x5) (x3 x4 x5 x4 x5 x4 x5))) (x1 (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x4 x4 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5)) (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x4 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x4 x5 x5) (x3 x5 x5 x5 x4 x4 x5)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5) (x3 x4 x5 x5 x5 x4 x5)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x5)) (x2 (x3 x4 x5 x4 x5 x4 x4) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x5)) (x2 (x3 x5 x4 x5 x4 x4 x4) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5))) (x1 (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x5 x4 x4 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x5)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x5 x4 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x5 x4 x4 x5) (x3 x4 x4 x5 x5 x4 x5)) (x2 (x3 x4 x5 x5 x4 x5 x4) (x3 x4 x4 x5 x4 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x4 x5)) (x2 (x3 x5 x4 x4 x5 x4 x5) (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x4 x5)) (x2 (x3 x4 x5 x5 x4 x4 x4) (x3 x4 x5 x5 x4 x4 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x4 x5 x5 x5)) (x2 (x3 x5 x4 x4 x5 x4 x4) (x3 x5 x4 x4 x5 x4 x4) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x5 x4 x5 x5))) (x1 (x2 (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x4 x4 x5 x5 x5 x5)) (x2 (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x4 x4 x5 x5 x5 x5)) (x2 (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x4 x5 x5)) (x2 (x3 x4 x4 x5 x5 x5 x4) (x3 x5 x4 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x5 x5 x4 x4 x5 x5)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x4) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x5 x4 x5 x4 x5 x5) (x3 x4 x4 x4 x4 x4 x5)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x4 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x5 x4 x5 x5 x5) (x3 x4 x4 x4 x4 x4 x5))) (x1 (x2 (x3 x4 x5 x4 x4 x5 x5) (x3 x5 x4 x5 x5 x5 x4) (x3 x5 x5 x4 x5 x5 x5) (x3 x4 x4 x5 x5 x5 x4) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x5 x5 x4 x5 x5)) (x2 (x3 x5 x4 x4 x4 x5 x5) (x3 x4 x5 x5 x5 x4 x5) (x3 x5 x5 x5 x4 x5 x5) (x3 x4 x4 x5 x5 x4 x5) (x3 x4 x4 x5 x5 x4 x4) (x3 x5 x5 x4 x5 x5 x5)) (x2 (x3 x4 x4 x4 x5 x5 x5) (x3 x5 x5 x5 x4 x5 x4) (x3 x4 x5 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x4 x5) (x3 x5 x5 x4 x4 x4 x4) (x3 x5 x4 x5 x5 x5 x5)) (x2 (x3 x4 x4 x5 x4 x5 x5) (x3 x5 x5 x4 x5 x4 x5) (x3 x5 x4 x5 x5 x5 x5) (x3 x5 x5 x4 x4 x5 x4) (x3 x5 x5 x4 x4 x4 x4) (x3 x4 x5 x5 x5 x5 x5)) (x2 (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x4 x4) (x3 x4 x4 x4 x4 x5 x5) (x3 x4 x4 x4 x4 x5 x5) (x3 x5 x5 x5 x5 x4 x4) (x3 x5 x5 x5 x5 x5 x5)) (x2 (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5) (x3 x5 x5 x5 x5 x5 x5)))
Param nth_6_tuple : ι → ι → ι → ι → ι → ι → ι → ι
Definition TwoRamseyGraph_4_6_35_b := λ x0 x1 x2 x3 . x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x2 ∈ u6 ⟶ x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x5 x6 . x5
Param ordsucc^ordsucc : ι → ι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Param u5 : ι
Definition Church6_to_u6 := λ x0 : ι → ι → ι → ι → ι → ι → ι . x0 0 u1 u2 u3 u4 u5
Definition permargs_i_1_0_3_2_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x2 x1 x4 x3
Definition 9defa.. := λ x0 . Church6_to_u6 (permargs_i_1_0_3_2_4_5 (nth_6_tuple x0))
Definition permargs_i_2_3_0_1_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x3 x4 x1 x2
Definition 247c9.. := λ x0 . Church6_to_u6 (permargs_i_2_3_0_1_4_5 (nth_6_tuple x0))
Definition permargs_i_3_2_1_0_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 . x0 x4 x3 x2 x1
Definition 3ffd5.. := λ x0 . Church6_to_u6 (permargs_i_3_2_1_0_4_5 (nth_6_tuple x0))
Known In_0_6^In_0_6 : 0 ∈ u6
Known In_1_6^In_1_6 : u1 ∈ u6
Known In_2_6^In_2_6 : u2 ∈ u6
Known In_3_6^In_3_6 : u3 ∈ u6
Known In_4_6^In_4_6 : u4 ∈ u6
Known In_5_6^In_5_6 : u5 ∈ u6
Known In_0_4^In_0_4 : 0 ∈ 4
Known In_1_4^In_1_4 : 1 ∈ 4
Known In_2_4^In_2_4 : 2 ∈ 4
Known In_3_4^In_3_4 : 3 ∈ 4
Known 26f6c.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u2 u4 u3 x0)
Known 15002.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u2 u4 u5 x0)
Known 7df24.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u2 u5 u3 x0)
Known c146d.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u2 u5 u5 x0)
Known a1470.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u3 u4 u4 x0)
Known 14b47.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u3 u5 u4 x0)
Known f7b63.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 u4 0 x0)
Known a400d.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 u4 u2 x0)
Known 2e8bc.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 u5 0 x0)
Known c08c2.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 u5 u2 x0)
Known 54691.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u5 u4 u5 x0)
Known e902e.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b 0 0 x0 u5)
Known ca8df.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b 0 u1 x0 u4)
Known f12e2.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u3 u3 x0 u5)
Known 9b9cd.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 0 x0 u4)
Known 6e2f9.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 u1 x0 u5)
Known 5d253.. : ∀ x0 . x0 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b u4 u5 x0 u5)
Known a84c4.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u4 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u4 ⟶ not (TwoRamseyGraph_4_6_35_b x0 x1 x2 x3) ⟶ not (TwoRamseyGraph_4_6_35_b x0 (3ffd5.. x1) x2 (3ffd5.. x3))
Known 40ee6.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u4 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u4 ⟶ not (TwoRamseyGraph_4_6_35_b x0 x1 x2 x3) ⟶ not (TwoRamseyGraph_4_6_35_b x0 (247c9.. x1) x2 (247c9.. x3))
Known c4ec3.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u4 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u4 ⟶ not (TwoRamseyGraph_4_6_35_b x0 x1 x2 x3) ⟶ not (TwoRamseyGraph_4_6_35_b x0 (9defa.. x1) x2 (9defa.. x3))
Known 89684.. : nth_6_tuple u3 = λ x1 x2 x3 x4 x5 x6 . x4
Known a0d60.. : nth_6_tuple u2 = λ x1 x2 x3 x4 x5 x6 . x3
Known a7cad.. : nth_6_tuple u1 = λ x1 x2 x3 x4 x5 x6 . x2
Known a1243.. : nth_6_tuple 0 = λ x1 x2 x3 x4 x5 x6 . x1
Known 925f5.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b x0 x1 u5 u5)
Known a3e36.. : ∀ x0 x1 x2 x3 . TwoRamseyGraph_4_6_35_b x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_b x2 x3 x0 x1
Known c0174.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ not (TwoRamseyGraph_4_6_35_b x0 x1 x0 x1)
Known cases_6^cases_6 : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 u1 ⟶ x1 u2 ⟶ x1 u3 ⟶ x1 u4 ⟶ x1 u5 ⟶ x1 x0
Known fed6d.. : nth_6_tuple u5 = λ x1 x2 x3 x4 x5 x6 . x6
Known 33924.. : nth_6_tuple u4 = λ x1 x2 x3 x4 x5 x6 . x5
Known 768c1.. : ((λ x1 x2 . x2) = λ x1 x2 . x1) ⟶ ∀ x0 : ο . x0
Theorem 1f9f5.. : ∀ x0 . x0 ∈ u6 ⟶ ∀ x1 . x1 ∈ u6 ⟶ ∀ x2 . x2 ∈ u6 ⟶ ∀ x3 . x3 ∈ u6 ⟶ ∀ x4 . x4 ∈ u6 ⟶ ∀ x5 . x5 ∈ u6 ⟶ ∀ x6 . x6 ∈ u6 ⟶ ∀ x7 . x7 ∈ u6 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x2 x3 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x4 x5 ⟶ TwoRamseyGraph_4_6_35_b x0 x1 x6 x7 ⟶ TwoRamseyGraph_4_6_35_b x2 x3 x4 x5 ⟶ TwoRamseyGraph_4_6_35_b x2 x3 x6 x7 ⟶ TwoRamseyGraph_4_6_35_b x4 x5 x6 x7 ⟶ False (proof)