Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 5581c.. : ∀ 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 x40 x41 . (x36 x41 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x41 x35 ⟶ x26 x37 (x28 (x27 x41 x35)) ⟶ x25 x40 ⟶ x34 x40 x41 x35 ⟶ x26 x40 (x28 (x27 x41 x35)) ⟶ x26 x38 (x28 (x29 x41)) ⟶ x33 x39 x41 ⟶ x30 x41 x37 x40 ⟶ (x30 x41 (x32 x41 x37 x38 x39) (x31 x41 x40 x38 x39) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x36 x38 ⟶ (x38 = x37 ⟶ False) ⟶ x36 x37 ⟶ False) ⟶ (∀ x37 x38 . x24 x37 x38 ⟶ x36 x38 ⟶ False) ⟶ (∀ x37 . x36 x37 ⟶ (x37 = x0 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 . x24 x37 x38 ⟶ x26 x38 (x28 x39) ⟶ x36 x39 ⟶ False) ⟶ (∀ x37 x38 x39 . x24 x38 x39 ⟶ x26 x39 (x28 x37) ⟶ (x26 x38 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x23 x38 x37 ⟶ (x26 x38 (x28 x37) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x26 x38 (x28 x37) ⟶ (x23 x38 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x26 x37 x38 ⟶ (x36 x38 ⟶ False) ⟶ (x24 x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x24 x38 x37 ⟶ (x26 x38 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x25 x39 ⟶ x34 x39 x40 x35 ⟶ x26 x39 (x28 (x27 x40 x35)) ⟶ x25 x38 ⟶ x34 x38 x40 x35 ⟶ x26 x38 (x28 (x27 x40 x35)) ⟶ x30 x40 x37 x39 ⟶ x30 x40 x39 x38 ⟶ (x30 x40 x37 x38 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x25 x39 ⟶ x34 x39 x40 x35 ⟶ x26 x39 (x28 (x27 x40 x35)) ⟶ x25 x38 ⟶ x34 x38 x40 x35 ⟶ x26 x38 (x28 (x27 x40 x35)) ⟶ x30 x40 x37 x39 ⟶ x30 x40 x39 x37 ⟶ (x1 x40 x35 x37 x39 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x26 x37 (x28 (x22 x40)) ⟶ x25 x39 ⟶ x34 x39 x40 x35 ⟶ x26 x39 (x28 (x27 x40 x35)) ⟶ x33 x38 x40 ⟶ (x30 x40 x39 (x31 x40 x39 x37 x38) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x26 x37 (x28 (x22 x40)) ⟶ x25 x39 ⟶ x34 x39 x40 x35 ⟶ x26 x39 (x28 (x27 x40 x35)) ⟶ x33 x38 x40 ⟶ (x30 x40 (x32 x40 x39 x37 x38) x39 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . x25 x40 ⟶ x34 x40 x37 x38 ⟶ x26 x40 (x28 (x27 x37 x38)) ⟶ x25 x39 ⟶ x34 x39 x37 x38 ⟶ x26 x39 (x28 (x27 x37 x38)) ⟶ x1 x37 x38 x40 x39 ⟶ (x1 x37 x38 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . x25 x40 ⟶ x34 x40 x37 x38 ⟶ x26 x40 (x28 (x27 x37 x38)) ⟶ x25 x39 ⟶ x34 x39 x37 x38 ⟶ x26 x39 (x28 (x27 x37 x38)) ⟶ (x1 x37 x38 x40 x40 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x23 x37 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 . (x36 x39 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x39 x35 ⟶ x26 x37 (x28 (x27 x39 x35)) ⟶ x25 x38 ⟶ x34 x38 x39 x35 ⟶ x26 x38 (x28 (x27 x39 x35)) ⟶ (x30 x39 x37 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . x25 x40 ⟶ x34 x40 x37 x38 ⟶ x26 x40 (x28 (x27 x37 x38)) ⟶ x25 x39 ⟶ x34 x39 x37 x38 ⟶ x26 x39 (x28 (x27 x37 x38)) ⟶ x40 = x39 ⟶ (x1 x37 x38 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . x25 x40 ⟶ x34 x40 x37 x38 ⟶ x26 x40 (x28 (x27 x37 x38)) ⟶ x25 x39 ⟶ x34 x39 x37 x38 ⟶ x26 x39 (x28 (x27 x37 x38)) ⟶ x1 x37 x38 x40 x39 ⟶ (x40 = x39 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x21 x37 = x28 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x29 x37 = x22 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x36 x37 ⟶ False) ⟶ (x19 (x20 x37) ⟶ False) ⟶ False) ⟶ (∀ x37 . (x36 x37 ⟶ False) ⟶ x36 (x20 x37) ⟶ False) ⟶ (∀ x37 . (x36 x37 ⟶ False) ⟶ (x33 (x20 x37) x37 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x2 (x3 x37) x37 ⟶ False) ⟶ False) ⟶ (∀ x37 . x36 (x3 x37) ⟶ False) ⟶ (∀ x37 . (x26 (x3 x37) (x28 (x28 (x21 x37))) ⟶ False) ⟶ False) ⟶ (x36 x18 ⟶ False) ⟶ (∀ x37 . (x36 x37 ⟶ False) ⟶ (x19 (x4 x37) ⟶ False) ⟶ False) ⟶ (∀ x37 . (x36 x37 ⟶ False) ⟶ x36 (x4 x37) ⟶ False) ⟶ (∀ x37 . (x36 x37 ⟶ False) ⟶ (x33 (x4 x37) x37 ⟶ False) ⟶ False) ⟶ ((x36 x17 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x2 (x5 x37) x37 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x26 (x5 x37) (x28 (x28 (x21 x37))) ⟶ False) ⟶ False) ⟶ (x36 x35 ⟶ False) ⟶ ((x36 x0 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x26 (x6 x37) x37 ⟶ False) ⟶ False) ⟶ (∀ x37 . (x33 (x16 x37) x37 ⟶ False) ⟶ False) ⟶ ((x36 x7 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x33 x38 x37 ⟶ (x26 x38 (x28 (x28 x37)) ⟶ False) ⟶ False) ⟶ (∀ x37 . (x26 (x21 x37) (x28 (x28 x37)) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x26 x39 (x28 (x29 x40)) ⟶ x33 x38 x40 ⟶ (x26 (x31 x40 x37 x39 x38) (x28 (x27 x40 x35)) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x26 x39 (x28 (x29 x40)) ⟶ x33 x38 x40 ⟶ (x34 (x31 x40 x37 x39 x38) x40 x35 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x26 x39 (x28 (x29 x40)) ⟶ x33 x38 x40 ⟶ (x25 (x31 x40 x37 x39 x38) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x26 x39 (x28 (x29 x40)) ⟶ x33 x38 x40 ⟶ (x26 (x32 x40 x37 x39 x38) (x28 (x27 x40 x35)) ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x26 x39 (x28 (x29 x40)) ⟶ x33 x38 x40 ⟶ (x34 (x32 x40 x37 x39 x38) x40 x35 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 x39 x40 . (x36 x40 ⟶ False) ⟶ x25 x37 ⟶ x34 x37 x40 x35 ⟶ x26 x37 (x28 (x27 x40 x35)) ⟶ x26 x39 (x28 (x29 x40)) ⟶ x33 x38 x40 ⟶ (x25 (x32 x40 x37 x39 x38) ⟶ False) ⟶ False) ⟶ (∀ x37 . (x26 (x29 x37) (x28 (x28 (x21 x37))) ⟶ False) ⟶ False) ⟶ (∀ x37 . (x2 (x29 x37) x37 ⟶ False) ⟶ False) ⟶ ((x0 = x7 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x26 x38 (x28 (x27 x37 x35)) ⟶ x25 x38 ⟶ x34 x38 x37 x35 ⟶ (x8 x38 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x26 x38 (x28 (x27 x37 x35)) ⟶ x25 x38 ⟶ x34 x38 x37 x35 ⟶ (x34 x38 x37 x35 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x26 x38 (x28 (x27 x37 x35)) ⟶ x25 x38 ⟶ x34 x38 x37 x35 ⟶ (x25 x38 ⟶ False) ⟶ False) ⟶ (∀ x37 . x26 x37 x35 ⟶ (x15 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . x33 x38 x37 ⟶ (x19 x38 ⟶ False) ⟶ False) ⟶ (∀ x37 . x36 x37 ⟶ (x14 x37 ⟶ False) ⟶ False) ⟶ (∀ x37 x38 . (x36 x38 ⟶ False) ⟶ x33 x37 x38 ⟶ x36 x37 ⟶ False) ⟶ (∀ x37 x38 . x24 x37 x38 ⟶ x24 x38 x37 ⟶ False) ⟶ (x30 x9 (x32 x9 (x32 x9 x13 x11 x10) x11 x12) (x31 x9 (x31 x9 x13 x11 x12) x11 x10) ⟶ False) ⟶ ((x33 x12 x9 ⟶ False) ⟶ False) ⟶ ((x33 x10 x9 ⟶ False) ⟶ False) ⟶ ((x26 x11 (x28 (x29 x9)) ⟶ False) ⟶ False) ⟶ ((x26 x13 (x28 (x27 x9 x35)) ⟶ False) ⟶ False) ⟶ ((x34 x13 x9 x35 ⟶ False) ⟶ False) ⟶ ((x25 x13 ⟶ False) ⟶ False) ⟶ (x36 x9 ⟶ False) ⟶ False (proof)

Proofgold Asset