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

type
prop

theory
HotG

name
-

proof
PUeQB..

Megalodon
-

proofgold address
TMbqC..

creator
35132 PrPhD../30bed..

owner
35137 PrPhD../204e6..

term root
0cff1..