1. Harald Ganzinger (ed.), Automated deduction—CADE-16, in Proceedings of the 16th International Conference held in Trento, July 7–10, 1999, Lecture Notes in Computer Science, vol. 1632, Springer-Verlag, Berlin, 1999, pp. xiv+429.[MR]