An erratum for some errata to ATP problems (Q679255)

In 1986 \textit{F. J. Pelletier} published [ibid. 2, 191-216 (1986; Zbl 0642.68147)] an annotated list of 75 logic problems for testing ATP systems. The problems are presented in a natural first-order form (FOF), and most of them are also given in an equivalent negated conclusion clause normal form (CNF). The CNF versions are available in the TPTP Problem Library [\textit{G. Sutcliffe}, \textit{C. Suttner} and \textit{T. Yemenis}, ``The TPTP problem library'', in: A. Bundy (ed.), Proceedings of the 12th International Conference on Automated Deduction, Sci., Lect. Notes Artif. Intell. 814, 252-266 (1994)]. Shortly after the publication of Pelletier's paper [loc. cit.], some errata were published [ibid. 4, 235-236 (1988; Zbl 0642.68148)]. In particular, Problem 62 was `corrected'. Recently, howeve, it has been discovered that both the CNF and FOF versions of Problem 62 in the errata are incorrect (although the FOF, unlike the CNF, is still a theorem). The correct version of Problem 62 is given.