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

type
prop

theory
HotG

name
-

proof
PUQdX..

Megalodon
-

proofgold address
TMHWc..

creator
35118 PrPhD../7fb80..

owner
35120 PrPhD../e4676..

term root
885a4..