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

type
prop

theory
HotG

name
-

proof
PUV3T..

Megalodon
-

proofgold address
TMQje..

creator
35144 PrPhD../746ef..

owner
35145 PrPhD../2662e..

term root
a305b..