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

type
prop

theory
HotG

name
-

proof
PUaXw..

Megalodon
-

proofgold address
TMG1k..

creator
35159 PrPhD../7de67..

owner
35162 PrPhD../62c5b..

term root
6238e..