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

type
prop

theory
HotG

name
-

proof
PULdr..

Megalodon
-

proofgold address
TMKcR..

creator
35133 PrPhD../97ac4..

owner
35137 PrPhD../4ff05..

term root
33913..