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

Proofgold Address