Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 9ae00.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι . ∀ x6 : ι → ι → ο . ∀ x7 : ι → ι . ∀ x8 : ι → ι → ο . ∀ x9 : ι → ι → ι . ∀ x10 : ι → ο . ∀ x11 : ι → ι . ∀ x12 : ι → ο . ∀ x13 x14 x15 . ∀ x16 : ι → ι . ∀ x17 : ι → ο . ∀ x18 : ι → ι → ο . ∀ x19 x20 x21 x22 x23 x24 . ∀ x25 : ι → ι → ι . ∀ x26 : ι → ι . ∀ x27 . ∀ x28 : ι → ι → ο . ∀ x29 : ι → ι . ∀ x30 : ι → ι → ι . ∀ x31 : ι → ι → ο . ∀ x32 : ι → ι → ι . ∀ x33 : ι → ι → ι → ι . ∀ x34 : ι → ι → ο . ∀ x35 : ι → ι → ι → ι → ι . ∀ x36 . ∀ x37 : ι → ο . (∀ x38 x39 . x37 x39 ⟶ (x39 = x38 ⟶ False) ⟶ x37 x38 ⟶ False) ⟶ (∀ x38 x39 . x0 x38 x39 ⟶ x37 x39 ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x38 = x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x0 x38 x39 ⟶ x2 x39 (x1 x40) ⟶ x37 x40 ⟶ False) ⟶ (∀ x38 x39 x40 . x0 x39 x40 ⟶ x2 x40 (x1 x38) ⟶ (x2 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x3 x36 x38 = x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 x42 . x2 x41 (x1 x42) ⟶ x2 x39 (x1 x38) ⟶ x2 x40 (x1 (x32 x42 x38)) ⟶ x34 x39 (x35 x42 x38 x40 x41) ⟶ (x34 x41 (x35 x38 x42 (x33 x42 x38 x40) x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 x42 . x2 x41 (x1 x42) ⟶ x2 x39 (x1 x38) ⟶ x2 x40 (x1 (x32 x42 x38)) ⟶ x34 x41 (x35 x38 x42 (x33 x42 x38 x40) x39) ⟶ (x34 x39 (x35 x42 x38 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x31 x39 x38 ⟶ (x2 x39 (x1 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x2 x39 (x1 x38) ⟶ (x31 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x3 x38 x36 = x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x2 x38 x39 ⟶ (x37 x39 ⟶ False) ⟶ (x0 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x39 (x1 x40) ⟶ x2 x38 (x1 x40) ⟶ x31 x39 x38 ⟶ (x34 x39 (x30 x40 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x39 (x1 x40) ⟶ x2 x38 (x1 x40) ⟶ x34 x39 (x30 x40 x38) ⟶ (x31 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x39 (x1 x40) ⟶ x2 x38 (x1 x40) ⟶ x31 x39 (x30 x40 x38) ⟶ (x34 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x39 (x1 x40) ⟶ x2 x38 (x1 x40) ⟶ x34 x39 x38 ⟶ (x31 x39 (x30 x40 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x0 x39 x38 ⟶ (x2 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x34 x38 x39 ⟶ (x34 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x31 x38 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x2 x41 (x1 (x32 x40 x39)) ⟶ (x35 x40 x39 x41 x38 = x4 x41 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x38 (x1 (x32 x40 x39)) ⟶ (x33 x40 x39 x38 = x29 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x6 (x5 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x2 (x5 x38) (x1 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x6 (x7 x38) x38 ⟶ False) ⟶ (∀ x38 . (x2 (x7 x38) (x1 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x8 (x9 x38 x39) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x28 (x9 x39 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x10 (x9 x38 x39) ⟶ False) ⟶ False) ⟶ (x37 x27 ⟶ False) ⟶ (∀ x38 . (x37 (x11 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x2 (x11 x38) (x1 x38) ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ ((x10 x13 ⟶ False) ⟶ False) ⟶ ((x37 x14 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ x37 (x26 x38) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x2 (x26 x38) (x1 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x8 (x25 x38 x39) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x28 (x25 x39 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x10 (x25 x38 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x37 (x25 x38 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x2 (x25 x38 x39) (x1 (x32 x39 x38)) ⟶ False) ⟶ False) ⟶ ((x10 x15 ⟶ False) ⟶ False) ⟶ (x37 x15 ⟶ False) ⟶ (∀ x38 x39 . x2 x38 (x1 x39) ⟶ (x30 x39 (x30 x39 x38) = x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x38 (x1 (x32 x40 x39)) ⟶ (x33 x40 x39 (x33 x40 x39 x38) = x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x10 x38 ⟶ (x29 (x29 x38) = x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x10 x40 ⟶ x8 x40 x38 ⟶ x10 x39 ⟶ (x8 (x3 x40 x39) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x10 (x32 x38 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x10 x40 ⟶ x28 x40 x38 ⟶ x10 x39 ⟶ (x28 (x3 x40 x39) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x10 x39 ⟶ (x10 (x3 x39 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x39 ⟶ (x37 (x4 x39 x38) ⟶ False) ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 (x1 x38) ⟶ False) ⟶ (∀ x38 x39 . x10 x39 ⟶ x37 x38 ⟶ (x37 (x4 x39 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x10 (x29 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x37 (x29 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x37 x39 ⟶ False) ⟶ (x37 x38 ⟶ False) ⟶ x37 (x32 x39 x38) ⟶ False) ⟶ (∀ x38 . (x2 (x16 x38) x38 ⟶ False) ⟶ False) ⟶ ((x37 x24 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x2 x41 (x1 (x32 x40 x39)) ⟶ (x2 (x35 x40 x39 x41 x38) (x1 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x2 x39 (x1 x38) ⟶ (x2 (x30 x38 x39) (x1 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x40 (x1 (x32 x38 x39)) ⟶ (x2 (x33 x38 x39 x40) (x1 (x32 x39 x38)) ⟶ False) ⟶ False) ⟶ (∀ x38 . x10 x38 ⟶ (x10 (x29 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x2 x39 (x1 x38) ⟶ (x30 x38 x39 = x3 x38 x39 ⟶ False) ⟶ False) ⟶ ((x36 = x24 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x38 ⟶ x8 x38 x39 ⟶ (x8 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x38 ⟶ x8 x38 x39 ⟶ (x10 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x38 ⟶ x8 x38 x39 ⟶ (x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x38 ⟶ x28 x38 x39 ⟶ (x28 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x38 ⟶ x28 x38 x39 ⟶ (x10 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x10 x38 ⟶ x28 x38 x39 ⟶ (x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x10 x40 ⟶ x8 x40 x38 ⟶ x2 x39 (x1 x40) ⟶ (x8 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x10 x40 ⟶ x28 x40 x38 ⟶ x2 x39 (x1 x40) ⟶ (x28 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x2 x38 (x1 x39) ⟶ x6 x38 x39 ⟶ False) ⟶ (∀ x38 x39 x40 . x37 x40 ⟶ x2 x38 (x1 (x32 x39 x40)) ⟶ (x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x10 x38 ⟶ (x12 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x10 x38 ⟶ (x10 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x37 x39 ⟶ False) ⟶ x2 x38 (x1 x39) ⟶ x37 x38 ⟶ (x6 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x37 x40 ⟶ x2 x38 (x1 (x32 x40 x39)) ⟶ (x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x10 x38 ⟶ (x17 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ x10 x38 ⟶ (x10 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x37 x39 ⟶ False) ⟶ x2 x38 (x1 x39) ⟶ (x6 x38 x39 ⟶ False) ⟶ x37 x38 ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x40 (x1 (x32 x38 x39)) ⟶ (x8 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x40 (x1 (x32 x39 x38)) ⟶ (x28 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x10 x39 ⟶ x2 x38 (x1 x39) ⟶ (x10 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . (x37 x40 ⟶ False) ⟶ x37 x38 ⟶ x2 x39 (x1 (x32 x40 x38)) ⟶ x18 x39 x40 ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ x2 x38 (x1 x39) ⟶ (x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x2 x40 (x1 (x32 x38 x39)) ⟶ (x10 x40 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x10 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x37 x40 ⟶ x2 x38 (x1 (x32 x40 x39)) ⟶ (x18 x38 x40 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x0 x38 x39 ⟶ x0 x39 x38 ⟶ False) ⟶ ((x31 (x35 x20 x21 (x33 x21 x20 x22) x19) x23 ⟶ False) ⟶ (x31 (x35 x21 x20 x22 (x30 x21 x23)) (x30 x20 x19) ⟶ False) ⟶ False) ⟶ (x31 (x35 x21 x20 x22 (x30 x21 x23)) (x30 x20 x19) ⟶ x31 (x35 x20 x21 (x33 x21 x20 x22) x19) x23 ⟶ False) ⟶ ((x2 x22 (x1 (x32 x21 x20)) ⟶ False) ⟶ False) ⟶ ((x2 x19 (x1 x20) ⟶ False) ⟶ False) ⟶ ((x2 x23 (x1 x21) ⟶ False) ⟶ False) ⟶ False (proof)

Proofgold Address