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 . x34 x36 ⟶ (x36 = x35 ⟶ False) ⟶ x34 x35 ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x34 x36 ⟶ False) ⟶ (∀ x35 . x34 x35 ⟶ (x35 = x33 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x0 x35 x36 ⟶ x2 x36 (x1 x37) ⟶ x34 x37 ⟶ False) ⟶ (∀ x35 x36 x37 . x0 x36 x37 ⟶ x2 x37 (x1 x35) ⟶ (x2 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x3 x36 x35 ⟶ (x2 x36 (x1 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 x35) ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x35 x36 ⟶ (x34 x36 ⟶ False) ⟶ (x0 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x36 x35 ⟶ (x2 x36 x35 ⟶ False) ⟶ False) ⟶ (x34 x4 ⟶ False) ⟶ (∀ x35 . (x3 x35 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ (x7 (x6 x35) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ (x2 (x6 x35) (x1 (x32 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x10 x35 ⟶ x34 (x9 x35) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x10 x35 ⟶ (x2 (x9 x35) (x1 (x32 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x11 x35 ⟶ False) ⟶ x10 x35 ⟶ x12 (x13 x35) ⟶ False) ⟶ (∀ x35 . (x11 x35 ⟶ False) ⟶ x10 x35 ⟶ (x2 (x13 x35) (x1 (x32 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x10 x35 ⟶ (x12 (x14 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x10 x35 ⟶ x34 (x14 x35) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x10 x35 ⟶ (x2 (x14 x35) (x1 (x32 x35)) ⟶ False) ⟶ False) ⟶ ((x31 x30 ⟶ False) ⟶ False) ⟶ ((x5 x30 ⟶ False) ⟶ False) ⟶ ((x31 x29 ⟶ False) ⟶ False) ⟶ ((x8 x29 ⟶ False) ⟶ False) ⟶ ((x5 x29 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x2 x37 (x1 (x1 x38)) ⟶ x15 x38 x37 = x15 x36 x35 ⟶ (x37 = x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . x2 x37 (x1 (x1 x38)) ⟶ x15 x38 x37 = x15 x35 x36 ⟶ (x38 = x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x16 x35 ⟶ False) ⟶ x10 x35 ⟶ x17 (x32 x35) ⟶ False) ⟶ (∀ x35 x36 . (x34 x36 ⟶ False) ⟶ x2 x35 (x1 (x1 x36)) ⟶ (x31 (x15 x36 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x34 x36 ⟶ False) ⟶ x2 x35 (x1 (x1 x36)) ⟶ x8 (x15 x36 x35) ⟶ False) ⟶ (∀ x35 . x16 x35 ⟶ x10 x35 ⟶ (x17 (x32 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . x11 x35 ⟶ x10 x35 ⟶ (x12 (x32 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x5 x35 ⟶ (x31 (x15 (x32 x35) (x28 x35)) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x5 x35 ⟶ x8 (x15 (x32 x35) (x28 x35)) ⟶ False) ⟶ (∀ x35 . (x11 x35 ⟶ False) ⟶ x10 x35 ⟶ x12 (x32 x35) ⟶ False) ⟶ (∀ x35 . (x8 x35 ⟶ False) ⟶ x10 x35 ⟶ x34 (x32 x35) ⟶ False) ⟶ (∀ x35 . x8 x35 ⟶ x10 x35 ⟶ (x34 (x32 x35) ⟶ False) ⟶ False) ⟶ (∀ x35 . (x2 (x18 x35) x35 ⟶ False) ⟶ False) ⟶ ((x10 x27 ⟶ False) ⟶ False) ⟶ ((x5 x19 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ (x2 (x28 x35) (x1 (x1 (x32 x35))) ⟶ False) ⟶ False) ⟶ ((x34 x20 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ (x10 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 (x1 x35)) ⟶ (x5 (x15 x35 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 (x1 x35)) ⟶ (x31 (x15 x35 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 (x21 x35 x36) x35 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 (x21 x35 x36) x36 ⟶ False) ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . x3 x36 x37 ⟶ x0 x35 x36 ⟶ (x0 x35 x37 ⟶ False) ⟶ False) ⟶ ((x33 = x20 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x5 x36 ⟶ x2 x35 (x1 (x32 x36)) ⟶ x0 x35 (x28 x36) ⟶ (x22 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x5 x36 ⟶ x2 x35 (x1 (x32 x36)) ⟶ x22 x35 x36 ⟶ (x0 x35 (x28 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x3 x36 x35 ⟶ x3 x35 x36 ⟶ (x36 = x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x35 = x36 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x36 = x35 ⟶ (x3 x36 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x26 x35 x33 ⟶ (x8 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ x8 x35 ⟶ (x23 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x8 x35 ⟶ (x26 x35 x33 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ (x16 x35 ⟶ False) ⟶ x11 x35 ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x11 x35 ⟶ (x16 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ (x16 x35 ⟶ False) ⟶ x16 x35 ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ (x16 x35 ⟶ False) ⟶ x8 x35 ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x8 x35 ⟶ (x16 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x8 x35 ⟶ (x8 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x5 x36 ⟶ x2 x35 (x1 (x32 x36)) ⟶ x34 x35 ⟶ (x7 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ (x11 x35 ⟶ False) ⟶ x8 x35 ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x8 x35 ⟶ (x11 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ (x11 x35 ⟶ False) ⟶ x8 x35 ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x26 x35 x4 ⟶ (x11 x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ x26 x35 x4 ⟶ x8 x35 ⟶ False) ⟶ (∀ x35 . x10 x35 ⟶ (x8 x35 ⟶ False) ⟶ x11 x35 ⟶ (x26 x35 x4 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x0 x35 x36 ⟶ x0 x36 x35 ⟶ False) ⟶ (∀ x35 . x5 x35 ⟶ x31 x35 ⟶ (x35 = x15 (x32 x35) (x28 x35) ⟶ False) ⟶ False) ⟶ (x15 (x32 x25) (x28 x25) = x15 (x32 x24) (x28 x24) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 (x32 x25)) ⟶ x2 x35 (x1 (x32 x24)) ⟶ x36 = x35 ⟶ x22 x35 x24 ⟶ (x22 x36 x25 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . x2 x36 (x1 (x32 x25)) ⟶ x2 x35 (x1 (x32 x24)) ⟶ x36 = x35 ⟶ x22 x36 x25 ⟶ (x22 x35 x24 ⟶ False) ⟶ False) ⟶ ((x32 x25 = x32 x24 ⟶ False) ⟶ False) ⟶ ((x5 x24 ⟶ False) ⟶ False) ⟶ ((x5 x25 ⟶ False) ⟶ False) ⟶ False

type
prop

theory
HotG

name
-

proof
PULJn..

Megalodon
-

proofgold address
TMc5N..

creator
35164 PrPhD../f6efe..

owner
35169 PrPhD../46f9f..

term root
cebd7..