This directory contains a paper by Larry Wos and an companion file containing three appendices. Title: Automating the Search for Elegant Proofs, and Related Topics Abstract In this report, we focus on methodology for seeking more elegant proofs. Although the emphasis is on the aspect of proof length, we also touch on proof structure with regard to the nature of the terms in use. In particular, after discussing the impracticality of algorithmically attacking the problem, we show how an automated reasoning program can be used to systematically seek shorter and still shorter proofs when given an initial proof. Regarding proof structure, we show, for example, how one can use such a program to avoid the use of terms of the form n(n(t)), where t is any term and n denotes negation. Our objectives include demonstrating the power of McCune's reasoning program OTTER as a research assistant, presenting some techniques gleaned from almost thirty years of experimentation, giving some insight regarding the use of an automated reasoning program, and offering topics for research. Since history shows that new approaches often arise from attempting to meet a challenge, we also offer a theorem whose proof has never been obtained by an automated reasoning program without a substantially sophisticated approach. To promote research, we include input and output files and statistics. The file paper.text.roff is the text of the paper without appendices. To print the file, one writes eqn filename | ptroff -me -Pprintername The current paper.text.roff is not yet a complete version of the text of the paper. The file of appendices is paper.apps.tex. It is a TeX file that can be read on line, for it contains few TeX commands.