Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 5303f.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 x7 x8 : ι → ι → ι → ι . ∀ x9 x10 x11 x12 . ∀ x13 x14 : ι → ι → ι → ι → ι . ∀ x15 : ι → ι . ∀ x16 x17 . ∀ x18 : ι → ο . (∀ x19 x20 . x18 x20 ⟶ (x20 = x19 ⟶ False) ⟶ x18 x19 ⟶ False) ⟶ (∀ x19 x20 . x0 x19 x20 ⟶ x18 x20 ⟶ False) ⟶ (∀ x19 . x18 x19 ⟶ (x19 = x17 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x1 x20 x22 = x1 x19 x21 ⟶ (x22 = x21 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x1 x22 x20 = x1 x21 x19 ⟶ (x22 = x21 ⟶ False) ⟶ False) ⟶ (x18 x2 ⟶ False) ⟶ ((x18 x16 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . x18 (x3 x19 x20) ⟶ False) ⟶ (∀ x19 . x18 (x15 x19) ⟶ False) ⟶ (∀ x19 x20 . x18 (x1 x19 x20) ⟶ False) ⟶ ((x18 x17 ⟶ False) ⟶ False) ⟶ ((x18 x4 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . (x1 x20 x19 = x3 (x3 x20 x19) (x15 x20) ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 . (x6 x19 x20 x21 = x1 (x8 x19 x20 x21) (x7 x19 x20 x21) ⟶ False) ⟶ (x0 (x6 x19 x20 x21) x19 ⟶ False) ⟶ (x19 = x5 x21 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 . (x0 (x7 x19 x20 x21) x20 ⟶ False) ⟶ (x0 (x6 x19 x20 x21) x19 ⟶ False) ⟶ (x19 = x5 x21 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 . (x0 (x8 x19 x20 x21) x21 ⟶ False) ⟶ (x0 (x6 x19 x20 x21) x19 ⟶ False) ⟶ (x19 = x5 x21 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 x23 . x0 (x6 x23 x21 x22) x23 ⟶ x0 x19 x22 ⟶ x0 x20 x21 ⟶ x6 x23 x21 x22 = x1 x19 x20 ⟶ (x23 = x5 x22 x21 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 x23 x24 . x24 = x5 x22 x23 ⟶ x0 x19 x22 ⟶ x0 x21 x23 ⟶ x20 = x1 x19 x21 ⟶ (x0 x20 x24 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x22 = x5 x20 x21 ⟶ x0 x19 x22 ⟶ (x19 = x1 (x13 x19 x22 x21 x20) (x14 x19 x22 x21 x20) ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x22 = x5 x20 x21 ⟶ x0 x19 x22 ⟶ (x0 (x14 x19 x22 x21 x20) x21 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 x21 x22 . x22 = x5 x20 x21 ⟶ x0 x19 x22 ⟶ (x0 (x13 x19 x22 x21 x20) x20 ⟶ False) ⟶ False) ⟶ ((x17 = x4 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . (x3 x20 x19 = x3 x19 x20 ⟶ False) ⟶ False) ⟶ (∀ x19 x20 . x0 x19 x20 ⟶ x0 x20 x19 ⟶ False) ⟶ ((x0 x10 x9 ⟶ False) ⟶ (x0 (x1 x12 x10) (x5 x11 x9) ⟶ False) ⟶ False) ⟶ ((x0 x12 x11 ⟶ False) ⟶ (x0 (x1 x12 x10) (x5 x11 x9) ⟶ False) ⟶ False) ⟶ (x0 (x1 x12 x10) (x5 x11 x9) ⟶ x0 x12 x11 ⟶ x0 x10 x9 ⟶ False) ⟶ False (proof)

Proofgold Address