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 x57 x58 : ι → ο . ∀ x59 : ι → ι → ι → ο . ∀ x60 x61 x62 . ∀ x63 : ι → ι → ι . ∀ x64 x65 : ι → ο . ∀ x66 . ∀ x67 : ι → ι → ο . ∀ x68 : ι → ο . ∀ x69 x70 . ∀ x71 x72 : ι → ο . ∀ x73 : ι → ι . ∀ x74 : ι → ο . ∀ x75 : ι → ι → ι → ο . ∀ x76 x77 x78 . ∀ x79 : ι → ο . (∀ x80 x81 . x79 x81 ⟶ (x81 = x80 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x80 x81 ⟶ x2 x81 (x1 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x2 x82 (x1 x80) ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 x80 ⟶ (x2 x81 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 x80) ⟶ (x3 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ ((x2 x78 x4 ⟶ False) ⟶ False) ⟶ ((x2 x76 x77 ⟶ False) ⟶ False) ⟶ ((x2 x76 x5 ⟶ False) ⟶ False) ⟶ ((x75 x76 x77 x5 ⟶ False) ⟶ False) ⟶ ((x6 x76 ⟶ False) ⟶ False) ⟶ (x79 x76 ⟶ False) ⟶ (∀ x80 . (x3 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x82) ⟶ x2 x81 x80 ⟶ (x75 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x82) ⟶ x75 x81 x82 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ ((x5 = x4 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x11 x82 ⟶ x2 x81 (x8 x82) ⟶ x2 x80 (x8 x82) ⟶ (x10 x82 x81 x80 = x9 x82 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x74 x80 ⟶ False) ⟶ x72 x80 ⟶ x79 (x73 x80) ⟶ False) ⟶ (∀ x80 . (x74 x80 ⟶ False) ⟶ x72 x80 ⟶ (x2 (x73 x80) (x1 (x8 x80)) ⟶ False) ⟶ False) ⟶ ((x71 x70 ⟶ False) ⟶ False) ⟶ ((x12 x70 ⟶ False) ⟶ False) ⟶ (x79 x70 ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ (x79 x13 ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x72 x80 ⟶ x15 (x16 x80) ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x72 x80 ⟶ (x2 (x16 x80) (x1 (x8 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x74 x80 ⟶ False) ⟶ x72 x80 ⟶ (x15 (x17 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x74 x80 ⟶ False) ⟶ x72 x80 ⟶ x79 (x17 x80) ⟶ False) ⟶ (∀ x80 . (x74 x80 ⟶ False) ⟶ x72 x80 ⟶ (x2 (x17 x80) (x1 (x8 x80)) ⟶ False) ⟶ False) ⟶ ((x14 x69 ⟶ False) ⟶ False) ⟶ (x74 x69 ⟶ False) ⟶ ((x68 x69 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x18 (x19 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x67 (x19 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x20 (x19 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 (x19 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x2 (x19 x80 x81) (x1 (x21 x81 x80)) ⟶ False) ⟶ False) ⟶ ((x12 x66 ⟶ False) ⟶ False) ⟶ (x79 x66 ⟶ False) ⟶ (∀ x80 . (x65 x80 ⟶ False) ⟶ x72 x80 ⟶ x64 (x8 x80) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x72 x80 ⟶ (x64 (x8 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x14 x80 ⟶ x72 x80 ⟶ (x15 (x8 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x14 x80 ⟶ False) ⟶ x72 x80 ⟶ x15 (x8 x80) ⟶ False) ⟶ ((x12 x4 ⟶ False) ⟶ False) ⟶ ((x71 x4 ⟶ False) ⟶ False) ⟶ ((x71 x77 ⟶ False) ⟶ False) ⟶ ((x22 x77 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x74 x80 ⟶ False) ⟶ x72 x80 ⟶ x79 (x8 x80) ⟶ False) ⟶ (∀ x80 . x74 x80 ⟶ x72 x80 ⟶ (x79 (x8 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ (x75 (x63 x80 x81) x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x23 x80) x80 ⟶ False) ⟶ False) ⟶ ((x68 x62 ⟶ False) ⟶ False) ⟶ ((x24 x25 ⟶ False) ⟶ False) ⟶ ((x72 x61 ⟶ False) ⟶ False) ⟶ ((x26 x27 ⟶ False) ⟶ False) ⟶ ((x11 x60 ⟶ False) ⟶ False) ⟶ (∀ x80 . x26 x80 ⟶ (x2 (x28 x80) (x1 (x21 (x21 x77 (x8 x80)) (x8 x80))) ⟶ False) ⟶ False) ⟶ (∀ x80 . x26 x80 ⟶ (x59 (x28 x80) (x21 x77 (x8 x80)) (x8 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x26 x80 ⟶ (x29 (x28 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x82) ⟶ x75 x81 x82 x80 ⟶ (x2 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x68 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x24 x80 ⟶ (x11 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x24 x80 ⟶ (x68 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x26 x80 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x11 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ ((x2 x5 (x1 x77) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x11 x82 ⟶ x2 x81 (x8 x82) ⟶ x2 x80 (x8 x82) ⟶ (x2 (x10 x82 x81 x80) (x8 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . (x74 x83 ⟶ False) ⟶ x51 x83 ⟶ x7 x83 ⟶ x52 x83 ⟶ x58 x83 ⟶ x53 x83 ⟶ x57 x83 ⟶ x54 x83 ⟶ x56 x83 ⟶ x26 x83 ⟶ x2 x82 (x8 x83) ⟶ x2 x80 (x8 x83) ⟶ x2 x81 (x8 x83) ⟶ (x2 (x55 x83 x82 x80 x81) x77 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . (x74 x83 ⟶ False) ⟶ x51 x83 ⟶ x7 x83 ⟶ x52 x83 ⟶ x58 x83 ⟶ x53 x83 ⟶ x57 x83 ⟶ x54 x83 ⟶ x56 x83 ⟶ x26 x83 ⟶ x2 x82 (x8 x83) ⟶ x2 x80 (x8 x83) ⟶ x2 x81 (x8 x83) ⟶ (x2 (x30 x83 x82 x80 x81) x77 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x74 x82 ⟶ False) ⟶ x26 x82 ⟶ x2 x81 (x8 x82) ⟶ x49 x80 ⟶ (x2 (x50 x82 x81 x80) (x8 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x11 x82 ⟶ x2 x80 (x8 x82) ⟶ x2 x81 (x8 x82) ⟶ (x2 (x9 x82 x80 x81) (x8 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . (x74 x85 ⟶ False) ⟶ x51 x85 ⟶ x7 x85 ⟶ x52 x85 ⟶ x58 x85 ⟶ x53 x85 ⟶ x57 x85 ⟶ x54 x85 ⟶ x56 x85 ⟶ x26 x85 ⟶ x2 x84 (x8 x85) ⟶ x2 x80 (x8 x85) ⟶ x2 x83 (x8 x85) ⟶ x48 x85 x84 x80 ⟶ x2 x82 x77 ⟶ x2 x81 x77 ⟶ x83 = x10 x85 (x50 x85 x84 x81) (x50 x85 x80 x82) ⟶ (x82 = x55 x85 x84 x80 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . (x74 x84 ⟶ False) ⟶ x51 x84 ⟶ x7 x84 ⟶ x52 x84 ⟶ x58 x84 ⟶ x53 x84 ⟶ x57 x84 ⟶ x54 x84 ⟶ x56 x84 ⟶ x26 x84 ⟶ x2 x83 (x8 x84) ⟶ x2 x80 (x8 x84) ⟶ x2 x82 (x8 x84) ⟶ x48 x84 x83 x80 ⟶ x2 x81 x77 ⟶ x81 = x55 x84 x83 x80 x82 ⟶ (x82 = x10 x84 (x50 x84 x83 (x31 x81 x82 x80 x83 x84)) (x50 x84 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . (x74 x84 ⟶ False) ⟶ x51 x84 ⟶ x7 x84 ⟶ x52 x84 ⟶ x58 x84 ⟶ x53 x84 ⟶ x57 x84 ⟶ x54 x84 ⟶ x56 x84 ⟶ x26 x84 ⟶ x2 x83 (x8 x84) ⟶ x2 x80 (x8 x84) ⟶ x2 x82 (x8 x84) ⟶ x48 x84 x83 x80 ⟶ x2 x81 x77 ⟶ x81 = x55 x84 x83 x80 x82 ⟶ (x2 (x31 x81 x82 x80 x83 x84) x77 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . (x74 x85 ⟶ False) ⟶ x51 x85 ⟶ x7 x85 ⟶ x52 x85 ⟶ x58 x85 ⟶ x53 x85 ⟶ x57 x85 ⟶ x54 x85 ⟶ x56 x85 ⟶ x26 x85 ⟶ x2 x84 (x8 x85) ⟶ x2 x80 (x8 x85) ⟶ x2 x83 (x8 x85) ⟶ x48 x85 x84 x80 ⟶ x2 x82 x77 ⟶ x2 x81 x77 ⟶ x83 = x10 x85 (x50 x85 x84 x82) (x50 x85 x80 x81) ⟶ (x82 = x30 x85 x84 x80 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . (x74 x84 ⟶ False) ⟶ x51 x84 ⟶ x7 x84 ⟶ x52 x84 ⟶ x58 x84 ⟶ x53 x84 ⟶ x57 x84 ⟶ x54 x84 ⟶ x56 x84 ⟶ x26 x84 ⟶ x2 x83 (x8 x84) ⟶ x2 x80 (x8 x84) ⟶ x2 x82 (x8 x84) ⟶ x48 x84 x83 x80 ⟶ x2 x81 x77 ⟶ x81 = x30 x84 x83 x80 x82 ⟶ (x82 = x10 x84 (x50 x84 x83 x81) (x50 x84 x80 (x47 x81 x82 x80 x83 x84)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . (x74 x84 ⟶ False) ⟶ x51 x84 ⟶ x7 x84 ⟶ x52 x84 ⟶ x58 x84 ⟶ x53 x84 ⟶ x57 x84 ⟶ x54 x84 ⟶ x56 x84 ⟶ x26 x84 ⟶ x2 x83 (x8 x84) ⟶ x2 x80 (x8 x84) ⟶ x2 x82 (x8 x84) ⟶ x48 x84 x83 x80 ⟶ x2 x81 x77 ⟶ x81 = x30 x84 x83 x80 x82 ⟶ (x2 (x47 x81 x82 x80 x83 x84) x77 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x74 x82 ⟶ False) ⟶ x26 x82 ⟶ x2 x81 (x8 x82) ⟶ x49 x80 ⟶ (x50 x82 x81 x80 = x46 (x28 x82) x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x7 x82 ⟶ x11 x82 ⟶ x2 x81 (x8 x82) ⟶ x2 x80 (x8 x82) ⟶ (x10 x82 x81 x80 = x10 x82 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x45 x80 x78 ⟶ (x74 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x74 x80 ⟶ (x45 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 (x1 x77) ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x65 x80 ⟶ False) ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x14 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x65 x80 ⟶ False) ⟶ x65 x80 ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x65 x80 ⟶ False) ⟶ x74 x80 ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x74 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x74 x80 ⟶ (x74 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x21 x81 x82)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x21 x82 x81)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x34 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x14 x80 ⟶ False) ⟶ x74 x80 ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x21 x80 x81)) ⟶ (x18 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x21 x81 x80)) ⟶ (x67 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x35 x80 ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x71 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x2 x80 x5 ⟶ (x12 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x12 x81 ⟶ x2 x80 (x1 x81) ⟶ (x12 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x35 x81 ⟶ x2 x80 (x1 x81) ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ x2 x80 (x1 x81) ⟶ (x34 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x22 x81 ⟶ x2 x80 (x1 x81) ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x33 x81 ⟶ x2 x80 (x1 x81) ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x74 x80 ⟶ (x14 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x21 x80 x81)) ⟶ (x20 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x12 x80 ⟶ (x35 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x32 x81 ⟶ x2 x80 (x1 x81) ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x12 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x14 x80 ⟶ False) ⟶ x74 x80 ⟶ False) ⟶ (∀ x80 x81 . x12 x81 ⟶ x2 x80 x81 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x35 x81 ⟶ x2 x80 x81 ⟶ (x44 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x34 x81 ⟶ x2 x80 x81 ⟶ (x37 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x22 x81 ⟶ x2 x80 x81 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x33 x81 ⟶ x2 x80 x81 ⟶ (x38 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x32 x81 ⟶ x2 x80 x81 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x45 x80 x76 ⟶ (x14 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x45 x80 x76 ⟶ x74 x80 ⟶ False) ⟶ (∀ x80 . x2 x80 (x1 x5) ⟶ (x12 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x74 x80 ⟶ False) ⟶ x14 x80 ⟶ (x45 x80 x76 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x0 x81 x80 ⟶ False) ⟶ (x39 = x10 x42 (x50 x42 x40 (x30 x42 x40 x41 x39)) (x50 x42 x41 (x55 x42 x40 x41 x39)) ⟶ False) ⟶ ((x48 x42 x40 x41 ⟶ False) ⟶ False) ⟶ ((x2 x39 (x8 x42) ⟶ False) ⟶ False) ⟶ ((x2 x41 (x8 x42) ⟶ False) ⟶ False) ⟶ ((x2 x40 (x8 x42) ⟶ False) ⟶ False) ⟶ ((x26 x42 ⟶ False) ⟶ False) ⟶ ((x56 x42 ⟶ False) ⟶ False) ⟶ ((x54 x42 ⟶ False) ⟶ False) ⟶ ((x57 x42 ⟶ False) ⟶ False) ⟶ ((x53 x42 ⟶ False) ⟶ False) ⟶ ((x58 x42 ⟶ False) ⟶ False) ⟶ ((x52 x42 ⟶ False) ⟶ False) ⟶ ((x7 x42 ⟶ False) ⟶ False) ⟶ ((x51 x42 ⟶ False) ⟶ False) ⟶ (x74 x42 ⟶ False) ⟶ False

type
prop

theory
HotG

name
-

proof
PUXXr..

Megalodon
-

proofgold address
TMHA1..

creator
35120 PrPhD../33842..

owner
35122 PrPhD../93755..

term root
c3995..