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

type
prop

theory
HotG

name
-

proof
PUbQp..

Megalodon
-

proofgold address
TMPhH..

creator
35121 PrPhD../c8c28..

owner
35124 PrPhD../59bb9..

term root
a9ed3..