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

type
prop

theory
HotG

name
-

proof
PURHq..

Megalodon
-

proofgold address
TMScg..

creator
35145 PrPhD../d8821..

owner
35148 PrPhD../e6125..

term root
0849c..