Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem f6b5f.. : ∀ 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 x42 x43 : ι → ο . ∀ x44 . ∀ x45 : ι → ο . ∀ x46 . ∀ x47 : ι → ο . ∀ x48 : ι → ι . ∀ x49 . ∀ x50 x51 : ι → ο . ∀ x52 x53 . ∀ x54 : ι → ι → ι . ∀ x55 . ∀ x56 : ι → ο . (∀ x57 x58 . x56 x58 ⟶ (x58 = x57 ⟶ False) ⟶ x56 x57 ⟶ False) ⟶ (∀ x57 x58 . x0 x57 x58 ⟶ x56 x58 ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x57 = x55 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x57 x58 ⟶ x2 x58 (x1 x59) ⟶ x56 x59 ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x58 x59 ⟶ x2 x59 (x1 x57) ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x3 x58 x57 ⟶ (x2 x58 (x1 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 (x1 x57) ⟶ (x3 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x9 x62 ⟶ x5 x62 ⟶ x8 x62 ⟶ x2 x61 (x6 x62) ⟶ x2 x57 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x2 x58 (x6 x62) ⟶ x2 x59 (x6 x62) ⟶ x7 x62 x61 x57 x60 ⟶ x7 x62 x61 x57 x58 ⟶ x7 x62 x61 x57 x59 ⟶ (x61 = x57 ⟶ False) ⟶ (x7 x62 x60 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x58 x59 ⟶ x0 x57 x59 ⟶ x0 x57 (x54 x59 x58) ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x57 ⟶ (x0 (x54 x57 x58) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x57 x58 ⟶ (x56 x58 ⟶ False) ⟶ (x0 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x57 ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ ((x2 x55 x53 ⟶ False) ⟶ False) ⟶ ((x2 x11 x10 ⟶ False) ⟶ False) ⟶ ((x2 x11 x52 ⟶ False) ⟶ False) ⟶ ((x12 x11 x10 x52 ⟶ False) ⟶ False) ⟶ ((x51 x11 ⟶ False) ⟶ False) ⟶ (x56 x11 ⟶ False) ⟶ (∀ x57 . (x3 x57 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x56 x59 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x59) ⟶ x2 x58 x57 ⟶ (x12 x58 x59 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x56 x59 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x59) ⟶ x12 x58 x59 x57 ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ ((x52 = x53 ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ (x56 x49 ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x47 x57 ⟶ x56 (x48 x57) ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x47 x57 ⟶ (x2 (x48 x57) (x1 (x6 x57)) ⟶ False) ⟶ False) ⟶ ((x50 x46 ⟶ False) ⟶ False) ⟶ (x56 x13 ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ ((x14 x44 ⟶ False) ⟶ False) ⟶ ((x43 x44 ⟶ False) ⟶ False) ⟶ (x56 x44 ⟶ False) ⟶ (∀ x57 . (x42 x57 ⟶ False) ⟶ x47 x57 ⟶ x41 (x40 x57) ⟶ False) ⟶ (∀ x57 . (x42 x57 ⟶ False) ⟶ x47 x57 ⟶ (x2 (x40 x57) (x1 (x6 x57)) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x47 x57 ⟶ (x41 (x39 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x47 x57 ⟶ x56 (x39 x57) ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x47 x57 ⟶ (x2 (x39 x57) (x1 (x6 x57)) ⟶ False) ⟶ False) ⟶ ((x56 x15 ⟶ False) ⟶ False) ⟶ ((x45 x38 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 x61 . (x4 x61 ⟶ False) ⟶ x9 x61 ⟶ x5 x61 ⟶ x8 x61 ⟶ x2 x60 (x6 x61) ⟶ x2 x57 (x6 x61) ⟶ x2 x59 (x6 x61) ⟶ x58 = x59 ⟶ x7 x61 x60 x57 x59 ⟶ (x0 x58 (x16 x61 x60 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . (x4 x60 ⟶ False) ⟶ x9 x60 ⟶ x5 x60 ⟶ x8 x60 ⟶ x2 x59 (x6 x60) ⟶ x2 x57 (x6 x60) ⟶ x0 x58 (x16 x60 x59 x57) ⟶ (x7 x60 x59 x57 (x37 x57 x59 x60 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . (x4 x60 ⟶ False) ⟶ x9 x60 ⟶ x5 x60 ⟶ x8 x60 ⟶ x2 x59 (x6 x60) ⟶ x2 x57 (x6 x60) ⟶ x0 x58 (x16 x60 x59 x57) ⟶ (x58 = x37 x57 x59 x60 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . (x4 x60 ⟶ False) ⟶ x9 x60 ⟶ x5 x60 ⟶ x8 x60 ⟶ x2 x59 (x6 x60) ⟶ x2 x57 (x6 x60) ⟶ x0 x58 (x16 x60 x59 x57) ⟶ (x2 (x37 x57 x59 x60 x58) (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x17 x57 ⟶ False) ⟶ x47 x57 ⟶ x18 (x6 x57) ⟶ False) ⟶ (∀ x57 . x17 x57 ⟶ x47 x57 ⟶ (x18 (x6 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . x42 x57 ⟶ x47 x57 ⟶ (x41 (x6 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x42 x57 ⟶ False) ⟶ x47 x57 ⟶ x41 (x6 x57) ⟶ False) ⟶ ((x45 x53 ⟶ False) ⟶ False) ⟶ (x56 x53 ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x47 x57 ⟶ x56 (x6 x57) ⟶ False) ⟶ ((x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x57 . x4 x57 ⟶ x47 x57 ⟶ (x56 (x6 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x58) ⟶ (x12 (x36 x57 x58) x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x4 x57 ⟶ False) ⟶ x9 x57 ⟶ x5 x57 ⟶ x21 x57 ⟶ x8 x57 ⟶ (x20 (x19 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x2 (x35 x57) x57 ⟶ False) ⟶ False) ⟶ ((x47 x22 ⟶ False) ⟶ False) ⟶ ((x8 x34 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x56 x59 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x59) ⟶ x12 x58 x59 x57 ⟶ (x2 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x57 . x8 x57 ⟶ (x47 x57 ⟶ False) ⟶ False) ⟶ ((x2 x52 (x1 x10) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 x60 . (x4 x60 ⟶ False) ⟶ x9 x60 ⟶ x5 x60 ⟶ x21 x60 ⟶ x8 x60 ⟶ x2 x57 (x6 x60) ⟶ x2 x59 (x6 x60) ⟶ (x57 = x59 ⟶ False) ⟶ x58 = x33 x60 x57 x59 ⟶ (x20 x58 x60 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x4 x58 ⟶ False) ⟶ x9 x58 ⟶ x5 x58 ⟶ x21 x58 ⟶ x8 x58 ⟶ x20 x57 x58 ⟶ (x57 = x33 x58 (x23 x57 x58) (x24 x57 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x4 x58 ⟶ False) ⟶ x9 x58 ⟶ x5 x58 ⟶ x21 x58 ⟶ x8 x58 ⟶ x20 x57 x58 ⟶ x23 x57 x58 = x24 x57 x58 ⟶ False) ⟶ (∀ x57 x58 . (x4 x58 ⟶ False) ⟶ x9 x58 ⟶ x5 x58 ⟶ x21 x58 ⟶ x8 x58 ⟶ x20 x57 x58 ⟶ (x2 (x24 x57 x58) (x6 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x4 x58 ⟶ False) ⟶ x9 x58 ⟶ x5 x58 ⟶ x21 x58 ⟶ x8 x58 ⟶ x20 x57 x58 ⟶ (x2 (x23 x57 x58) (x6 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x4 x59 ⟶ False) ⟶ x9 x59 ⟶ x5 x59 ⟶ x8 x59 ⟶ x2 x58 (x6 x59) ⟶ x2 x57 (x6 x59) ⟶ (x33 x59 x58 x57 = x16 x59 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x32 x57 x55 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x25 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x4 x57 ⟶ (x32 x57 x55 ⟶ False) ⟶ False) ⟶ (∀ x57 . x2 x57 x53 ⟶ (x50 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ (x17 x57 ⟶ False) ⟶ x42 x57 ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x50 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x42 x57 ⟶ (x17 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x50 x57 ⟶ (x45 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ (x17 x57 ⟶ False) ⟶ x17 x57 ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ (x17 x57 ⟶ False) ⟶ x4 x57 ⟶ False) ⟶ (∀ x57 x58 . x45 x58 ⟶ x2 x57 x58 ⟶ (x45 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x4 x57 ⟶ (x17 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x4 x57 ⟶ (x4 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x26 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x45 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ (x42 x57 ⟶ False) ⟶ x4 x57 ⟶ False) ⟶ (∀ x57 . x43 x57 ⟶ x14 x57 ⟶ (x45 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x4 x57 ⟶ (x42 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x45 x57 ⟶ (x14 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x45 x57 ⟶ (x43 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ (x42 x57 ⟶ False) ⟶ x4 x57 ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x32 x57 x11 ⟶ (x42 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ x32 x57 x11 ⟶ x4 x57 ⟶ False) ⟶ (∀ x57 . x47 x57 ⟶ (x4 x57 ⟶ False) ⟶ x42 x57 ⟶ (x32 x57 x11 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x25 x58 ⟶ x2 x57 (x1 x58) ⟶ (x25 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 x57 x58 ⟶ x0 x58 x57 ⟶ False) ⟶ (x7 x31 x28 x29 x30 ⟶ False) ⟶ ((x0 x30 x27 ⟶ False) ⟶ False) ⟶ ((x0 x29 x27 ⟶ False) ⟶ False) ⟶ ((x0 x28 x27 ⟶ False) ⟶ False) ⟶ ((x20 x27 x31 ⟶ False) ⟶ False) ⟶ ((x2 x30 (x6 x31) ⟶ False) ⟶ False) ⟶ ((x2 x29 (x6 x31) ⟶ False) ⟶ False) ⟶ ((x2 x28 (x6 x31) ⟶ False) ⟶ False) ⟶ ((x8 x31 ⟶ False) ⟶ False) ⟶ ((x21 x31 ⟶ False) ⟶ False) ⟶ ((x5 x31 ⟶ False) ⟶ False) ⟶ ((x9 x31 ⟶ False) ⟶ False) ⟶ (x4 x31 ⟶ False) ⟶ False (proof)

Proofgold Asset