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

type
prop

theory
HotG

name
-

proof
PUSbm..

Megalodon
t6_xregular

proofgold address
TMStL..^t6_xregular

creator
11992 PrJLy../bd9a3..

owner
12103 PrJLy../e107d..

term root
2c8d4..