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

type
prop

theory
HotG

name
-

proof
PUYvF..

Megalodon
-

proofgold address
TMcbc..

creator
35133 PrPhD../9e27a..

owner
35137 PrPhD../601dc..

term root
d9b4d..