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

type
prop

theory
HotG

name
-

proof
PUSp5..

Megalodon
-

proofgold address
TMUYQ..

creator
35133 PrPhD../924ec..

owner
35137 PrPhD../f6647..

term root
85e3b..