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

Proofgold Address