@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}