Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 32e32.. : ∀ 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 . ∀ x59 : ι → ο . ∀ x60 x61 . ∀ x62 : ι → ο . ∀ x63 x64 x65 x66 . ∀ x67 x68 x69 x70 : ι → ο . ∀ x71 . ∀ x72 : ι → ο . ∀ x73 x74 x75 : ι → ι → ι . ∀ x76 : ι → ι . ∀ x77 x78 x79 x80 : ι → ο . ∀ x81 . ∀ x82 : ι → ι → ο . ∀ x83 : ι → ι . ∀ x84 : ι → ι → ο . (∀ x85 . x82 x85 x81 ⟶ (x84 x85 (x83 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x84 (x0 (x83 x85)) x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x84 x86 x85 ⟶ False) ⟶ (x79 x85 ⟶ False) ⟶ (x78 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x1 x86 ⟶ (x86 = x85 ⟶ False) ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x84 x86 x85 ⟶ False) ⟶ (x78 x86 ⟶ False) ⟶ (x79 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x2 x85 x86 ⟶ x1 x86 ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ x84 x86 x85 ⟶ (x1 x86 ⟶ False) ⟶ (x78 x85 ⟶ False) ⟶ (x79 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x85 = x3 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ x84 (x76 x86) x85 ⟶ (x84 (x76 x85) x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ x84 x86 (x76 x85) ⟶ (x84 x85 (x76 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ x84 x86 x85 ⟶ (x1 x85 ⟶ False) ⟶ (x79 x86 ⟶ False) ⟶ (x78 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ x84 x86 x85 ⟶ (x78 x85 ⟶ False) ⟶ x78 x86 ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ x84 x86 x85 ⟶ (x79 x86 ⟶ False) ⟶ x79 x85 ⟶ False) ⟶ (∀ x85 x86 . x82 x85 x86 ⟶ (x1 x86 ⟶ False) ⟶ (x2 x85 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ x84 x86 x85 ⟶ x79 x85 ⟶ (x79 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x76 (x4 x86 x85) = x4 x85 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x76 (x4 x86 x85) = x75 (x76 x86) x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x2 x86 x85 ⟶ (x82 x86 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ x84 x86 x85 ⟶ x78 x86 ⟶ (x78 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x5 x86 ⟶ x5 x85 ⟶ (x7 (x6 x86) (x6 x85) = x7 x85 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x5 x86 ⟶ x5 x85 ⟶ (x74 (x6 x86) (x6 x85) = x6 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 x87 . x5 x87 ⟶ x5 x85 ⟶ x5 x86 ⟶ (x74 (x74 x87 x85) x86 = x74 x87 (x74 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x5 x86 ⟶ x5 x85 ⟶ (x74 x86 (x6 x85) = x7 x86 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x84 x86 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x82 x86 x81 ⟶ x82 x85 x81 ⟶ (x73 x86 x85 = x4 x86 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x0 x85 = x76 x85 ⟶ False) ⟶ False) ⟶ ((x72 x71 ⟶ False) ⟶ False) ⟶ (x8 x71 ⟶ False) ⟶ (x70 x71 ⟶ False) ⟶ (x1 x71 ⟶ False) ⟶ ((x69 x71 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ ((x68 x10 ⟶ False) ⟶ False) ⟶ (x1 x10 ⟶ False) ⟶ ((x67 x66 ⟶ False) ⟶ False) ⟶ (x1 x66 ⟶ False) ⟶ ((x72 x65 ⟶ False) ⟶ False) ⟶ (x8 x65 ⟶ False) ⟶ ((x70 x65 ⟶ False) ⟶ False) ⟶ ((x69 x65 ⟶ False) ⟶ False) ⟶ ((x72 x64 ⟶ False) ⟶ False) ⟶ ((x8 x64 ⟶ False) ⟶ False) ⟶ (x70 x64 ⟶ False) ⟶ ((x69 x64 ⟶ False) ⟶ False) ⟶ ((x72 x63 ⟶ False) ⟶ False) ⟶ ((x8 x63 ⟶ False) ⟶ False) ⟶ ((x70 x63 ⟶ False) ⟶ False) ⟶ ((x69 x63 ⟶ False) ⟶ False) ⟶ ((x62 x61 ⟶ False) ⟶ False) ⟶ (x1 x61 ⟶ False) ⟶ ((x72 x60 ⟶ False) ⟶ False) ⟶ (x1 x60 ⟶ False) ⟶ ((x69 x60 ⟶ False) ⟶ False) ⟶ ((x77 x11 ⟶ False) ⟶ False) ⟶ ((x1 x11 ⟶ False) ⟶ False) ⟶ ((x80 x12 ⟶ False) ⟶ False) ⟶ ((x77 x12 ⟶ False) ⟶ False) ⟶ ((x5 x12 ⟶ False) ⟶ False) ⟶ ((x1 x12 ⟶ False) ⟶ False) ⟶ ((x62 x13 ⟶ False) ⟶ False) ⟶ ((x59 x58 ⟶ False) ⟶ False) ⟶ ((x70 x58 ⟶ False) ⟶ False) ⟶ (x1 x58 ⟶ False) ⟶ ((x14 x58 ⟶ False) ⟶ False) ⟶ ((x57 x58 ⟶ False) ⟶ False) ⟶ ((x15 x58 ⟶ False) ⟶ False) ⟶ ((x56 x58 ⟶ False) ⟶ False) ⟶ ((x69 x58 ⟶ False) ⟶ False) ⟶ ((x55 x58 ⟶ False) ⟶ False) ⟶ ((x79 x16 ⟶ False) ⟶ False) ⟶ ((x77 x16 ⟶ False) ⟶ False) ⟶ ((x80 x17 ⟶ False) ⟶ False) ⟶ ((x79 x17 ⟶ False) ⟶ False) ⟶ ((x77 x17 ⟶ False) ⟶ False) ⟶ ((x5 x17 ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x14 x19 ⟶ False) ⟶ False) ⟶ (x1 x19 ⟶ False) ⟶ (x80 x54 ⟶ False) ⟶ ((x79 x54 ⟶ False) ⟶ False) ⟶ ((x77 x54 ⟶ False) ⟶ False) ⟶ ((x68 x20 ⟶ False) ⟶ False) ⟶ (x1 x20 ⟶ False) ⟶ ((x14 x20 ⟶ False) ⟶ False) ⟶ ((x78 x53 ⟶ False) ⟶ False) ⟶ ((x77 x53 ⟶ False) ⟶ False) ⟶ ((x80 x52 ⟶ False) ⟶ False) ⟶ ((x78 x52 ⟶ False) ⟶ False) ⟶ ((x77 x52 ⟶ False) ⟶ False) ⟶ ((x5 x52 ⟶ False) ⟶ False) ⟶ ((x5 x51 ⟶ False) ⟶ False) ⟶ (x1 x51 ⟶ False) ⟶ (x1 x50 ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ ((x23 x48 ⟶ False) ⟶ False) ⟶ ((x47 x48 ⟶ False) ⟶ False) ⟶ (x1 x48 ⟶ False) ⟶ ((x14 x46 ⟶ False) ⟶ False) ⟶ (x1 x46 ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ (x80 x24 ⟶ False) ⟶ ((x78 x24 ⟶ False) ⟶ False) ⟶ ((x77 x24 ⟶ False) ⟶ False) ⟶ ((x8 x43 ⟶ False) ⟶ False) ⟶ ((x70 x43 ⟶ False) ⟶ False) ⟶ (x1 x43 ⟶ False) ⟶ ((x14 x43 ⟶ False) ⟶ False) ⟶ ((x57 x43 ⟶ False) ⟶ False) ⟶ ((x15 x43 ⟶ False) ⟶ False) ⟶ ((x56 x43 ⟶ False) ⟶ False) ⟶ ((x69 x43 ⟶ False) ⟶ False) ⟶ ((x55 x43 ⟶ False) ⟶ False) ⟶ ((x77 x25 ⟶ False) ⟶ False) ⟶ ((x80 x42 ⟶ False) ⟶ False) ⟶ ((x5 x26 ⟶ False) ⟶ False) ⟶ ((x1 x41 ⟶ False) ⟶ False) ⟶ ((x49 x27 ⟶ False) ⟶ False) ⟶ ((x14 x40 ⟶ False) ⟶ False) ⟶ (x1 x40 ⟶ False) ⟶ ((x68 x39 ⟶ False) ⟶ False) ⟶ (x1 x39 ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x83 (x83 x85) = x83 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x5 x85 ⟶ (x6 (x6 x85) = x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x76 (x76 x85) = x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x0 (x0 x85) = x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 x87 x88 . x80 x88 ⟶ x80 x85 ⟶ x5 x87 ⟶ x5 x86 ⟶ x88 = x87 ⟶ x85 = x86 ⟶ (x4 x88 x85 = x7 x87 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x5 x85 ⟶ x86 = x85 ⟶ (x76 x86 = x6 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 x87 x88 . x80 x88 ⟶ x80 x85 ⟶ x5 x87 ⟶ x5 x86 ⟶ x88 = x87 ⟶ x85 = x86 ⟶ (x75 x88 x85 = x74 x87 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x78 x86 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ x78 (x75 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x78 x86 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . (x79 x86 ⟶ False) ⟶ x80 x86 ⟶ (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ x79 (x74 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x79 x86 ⟶ False) ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ x79 (x75 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x79 x86 ⟶ False) ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ (x80 x86 ⟶ False) ⟶ x77 x85 ⟶ x78 x85 ⟶ (x80 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ (x80 x86 ⟶ False) ⟶ x77 x85 ⟶ x78 x85 ⟶ (x80 x85 ⟶ False) ⟶ (x1 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x80 (x7 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ (x80 x86 ⟶ False) ⟶ x77 x85 ⟶ x79 x85 ⟶ (x80 x85 ⟶ False) ⟶ x80 (x75 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ (x80 x86 ⟶ False) ⟶ x77 x85 ⟶ x79 x85 ⟶ (x80 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . (x1 x85 ⟶ False) ⟶ x5 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . (x1 x85 ⟶ False) ⟶ x5 x85 ⟶ x1 (x6 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ (x80 x86 ⟶ False) ⟶ x77 x85 ⟶ x78 x85 ⟶ (x80 x85 ⟶ False) ⟶ x80 (x75 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ (x80 x86 ⟶ False) ⟶ x77 x85 ⟶ x78 x85 ⟶ (x80 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x80 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x21 x85 ⟶ (x21 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x21 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (x1 x81 ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x77 x85 ⟶ (x80 x85 ⟶ False) ⟶ x80 (x75 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x5 x86 ⟶ x5 x85 ⟶ (x5 (x7 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x62 x86 ⟶ (x1 x85 ⟶ False) ⟶ x62 x85 ⟶ x1 (x74 x85 x86) ⟶ False) ⟶ (∀ x85 x86 . x45 x86 ⟶ x45 x85 ⟶ (x45 (x7 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x80 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x77 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x80 x85 ⟶ (x80 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x80 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x21 x86 ⟶ x21 x85 ⟶ (x21 (x7 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x62 x86 ⟶ (x1 x85 ⟶ False) ⟶ x62 x85 ⟶ x1 (x74 x86 x85) ⟶ False) ⟶ (∀ x85 . x45 x85 ⟶ (x45 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x45 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x80 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x80 x86 ⟶ x80 x85 ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x5 x86 ⟶ x5 x85 ⟶ (x5 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x21 x86 ⟶ x21 x85 ⟶ (x21 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ ((x69 x81 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x78 (x4 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 (x4 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x79 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x79 x86 ⟶ x80 x86 ⟶ (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ (x78 (x7 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x79 (x4 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x4 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x79 x86 ⟶ x80 x86 ⟶ (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ (x79 (x7 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x78 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x78 x86 ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ (x79 (x7 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 . x80 x85 ⟶ (x80 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x80 x85 ⟶ (x77 (x76 x85) ⟶ False) ⟶ False) ⟶ ((x1 x3 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x62 x86 ⟶ x62 x85 ⟶ (x62 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x45 x86 ⟶ x45 x85 ⟶ (x45 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x79 x86 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ x78 (x4 x85 x86) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x79 x86 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x4 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x78 x86 ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ (x78 (x7 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x79 x86 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ x79 (x4 x86 x85) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ (x79 x86 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . (x79 x86 ⟶ False) ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ x78 (x7 x85 x86) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x79 x85 ⟶ (x78 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x79 x85 ⟶ (x77 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . (x79 x86 ⟶ False) ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ x79 (x7 x86 x85) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x78 x85 ⟶ (x79 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x78 x85 ⟶ (x77 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ x78 (x6 x85) ⟶ False) ⟶ (∀ x85 . (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ x78 (x76 x85) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ x79 (x6 x85) ⟶ False) ⟶ (∀ x85 . (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ x79 (x76 x85) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x79 x86 ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ (x79 (x74 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x79 (x75 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x75 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x79 x86 ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ (x79 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x79 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x79 x86 ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ ((x72 x81 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x78 x86 ⟶ x80 x86 ⟶ (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ (x78 (x74 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x78 (x75 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 (x75 x85 x86) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x78 x86 ⟶ x80 x86 ⟶ (x79 x85 ⟶ False) ⟶ x80 x85 ⟶ (x78 (x74 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x78 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x78 x86 ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . (x78 x86 ⟶ False) ⟶ x80 x86 ⟶ (x78 x85 ⟶ False) ⟶ x80 x85 ⟶ x78 (x74 x86 x85) ⟶ False) ⟶ (∀ x85 . (x82 (x28 x85) x85 ⟶ False) ⟶ False) ⟶ ((x1 x38 ⟶ False) ⟶ False) ⟶ (∀ x85 . x5 x85 ⟶ (x5 (x6 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x82 x86 x81 ⟶ x82 x85 x81 ⟶ (x82 (x73 x86 x85) x81 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x77 (x4 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x82 (x83 x85) x81 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x77 (x76 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x82 (x0 x85) x81 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x77 (x75 x86 x85) ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x4 x86 x85 = x75 x86 (x76 x85) ⟶ False) ⟶ False) ⟶ ((x3 = x38 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x84 x86 x85 ⟶ False) ⟶ (x84 x85 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x5 x86 ⟶ x5 x85 ⟶ (x74 x86 x85 = x74 x85 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x77 x86 ⟶ x77 x85 ⟶ (x75 x86 x85 = x75 x85 x86 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ (x29 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ (x14 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x30 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x67 x85 ⟶ (x37 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x1 x85 ⟶ False) ⟶ x29 x85 ⟶ (x70 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x1 x85 ⟶ False) ⟶ x29 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x1 x85 ⟶ False) ⟶ x29 x85 ⟶ (x57 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x79 x85 ⟶ False) ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x79 x85 ⟶ False) ⟶ (x1 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x67 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x1 x85 ⟶ False) ⟶ x31 x85 ⟶ (x8 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x1 x85 ⟶ False) ⟶ x31 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x1 x85 ⟶ False) ⟶ x31 x85 ⟶ (x57 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ x77 x85 ⟶ x79 x85 ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ x77 x85 ⟶ x78 x85 ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ x77 x85 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x62 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x9 x86 ⟶ x82 x85 x86 ⟶ (x68 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ x68 x85 ⟶ (x59 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ x68 x85 ⟶ (x56 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . (x1 x85 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x79 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . (x1 x85 ⟶ False) ⟶ x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x49 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x9 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x29 x85 ⟶ x31 x85 ⟶ (x59 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x29 x85 ⟶ x31 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x79 x85 ⟶ x78 x85 ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x79 x85 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x79 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 x86 . x49 x86 ⟶ x82 x85 x86 ⟶ (x49 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ (x55 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . (x68 x85 ⟶ False) ⟶ x36 x85 ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x59 x85 ⟶ (x31 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x59 x85 ⟶ (x29 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x59 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . (x1 x85 ⟶ False) ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x78 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . (x1 x85 ⟶ False) ⟶ x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x80 x85 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x32 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x36 x85 ⟶ (x68 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ (x1 x85 ⟶ False) ⟶ (x70 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ (x1 x85 ⟶ False) ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ (x1 x85 ⟶ False) ⟶ (x14 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x78 x85 ⟶ x79 x85 ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x78 x85 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ x78 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x80 x85 ⟶ (x5 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x49 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ x79 x85 ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x62 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x15 x85 ⟶ (x56 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x45 x85 ⟶ (x80 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x80 x85 ⟶ False) ⟶ (x79 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x78 x85 ⟶ False) ⟶ (x80 x85 ⟶ False) ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ (x1 x85 ⟶ False) ⟶ x68 x85 ⟶ (x8 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ (x1 x85 ⟶ False) ⟶ x68 x85 ⟶ (x70 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ (x1 x85 ⟶ False) ⟶ x68 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ (x1 x85 ⟶ False) ⟶ x68 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x80 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x5 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x45 x85 ⟶ (x21 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x47 x85 ⟶ x23 x85 ⟶ (x49 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ (x15 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x45 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x18 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x80 x85 ⟶ False) ⟶ (x78 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x77 x85 ⟶ (x79 x85 ⟶ False) ⟶ (x80 x85 ⟶ False) ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x82 x85 x81 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x21 x85 ⟶ (x80 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x49 x85 ⟶ (x23 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x49 x85 ⟶ (x47 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x62 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x62 x85 ⟶ (x49 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ (x57 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x68 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x1 x85 ⟶ (x14 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x8 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x8 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x14 x86 ⟶ x82 x85 x86 ⟶ (x62 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x70 x85 ⟶ x1 x85 ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x70 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x57 x86 ⟶ x82 x85 x86 ⟶ (x45 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x1 x85 ⟶ (x72 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x1 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x15 x86 ⟶ x82 x85 x86 ⟶ (x21 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x59 x85 ⟶ (x56 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x69 x85 ⟶ x59 x85 ⟶ (x69 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x56 x86 ⟶ x82 x85 x86 ⟶ (x80 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ x31 x85 ⟶ (x31 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ x31 x85 ⟶ (x68 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x14 x85 ⟶ x31 x85 ⟶ (x14 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x69 x86 ⟶ x82 x85 x86 ⟶ (x77 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ x59 x85 ⟶ (x68 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x57 x85 ⟶ x59 x85 ⟶ (x57 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x55 x86 ⟶ x82 x85 x86 ⟶ (x5 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ x8 x85 ⟶ (x31 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ x8 x85 ⟶ (x56 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ x70 x85 ⟶ (x29 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 . x56 x85 ⟶ x70 x85 ⟶ (x56 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x67 x86 ⟶ x82 x85 x86 ⟶ (x35 x85 ⟶ False) ⟶ False) ⟶ (∀ x85 x86 . x2 x85 x86 ⟶ x2 x86 x85 ⟶ False) ⟶ (x84 (x73 x33 x34) (x83 (x73 x34 x33)) ⟶ False) ⟶ ((x82 x33 x81 ⟶ False) ⟶ False) ⟶ ((x82 x34 x81 ⟶ False) ⟶ False) ⟶ False (proof)

Proofgold Address