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

type
prop

theory
HotG

name
-

proof
PUPYb..

Megalodon
-

proofgold address
TMXzU..

creator
35162 PrPhD../c3c80..

owner
35168 PrPhD../bdc6b..

term root
a2c7d..