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

type
prop

theory
HotG

name
-

proof
PUZLD..

Megalodon
-

proofgold address
TMbEN..

creator
35162 PrPhD../f6ddd..

owner
35168 PrPhD../9e3f1..

term root
e8df5..