Proofgold Proposition

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

type
prop

theory
HotG

name
-

proof
PUWC6..

Megalodon
-

proofgold address
TMEq4..

creator
35130 PrPhD../b6726..

owner
35137 PrPhD../9ab3b..

term root
e24d2..