This paper is an introduction to an automated reasoning program developed at Northern Illinois University and Argonne National Laboratory over the past nine years. Recently the program has reached the stage where it can be considered a useful research tool in a variety of disciplines. It has solved open problems in mathematics and participated in the design of new electronic circuits. Here we describe the general types of capabilities provided to the user by the program and give examples of how they are currently being used in diverse areas of investigation.