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

Proofgold Address