@MISC{FB-MPB-MB-AZ:AAR1989:ENprover,
AUTHOR = "Fabio Baj and Bonacina, Maria Paola
and Massimo Bruschi and Antonella Zanzi",
TITLE = "Another term rewriting based proof of the `non-obvious' theorem",
HOWPUBLISHED = "Newsletter of the Association for Automated Reasoning,
No. 13, pages 4--8",
MONTH = "September",
YEAR = 1989}