/** Thorem-Solver
** 
**  @author Jason Allen
**
**  Accepts a file containing a knowledge base and a goal clause, and attempts to perform
**  resolution.  Can parse any number of knowledge base and goal clause pairs as long as
**  the file presented is in a similar format to 'test-prover.lisp'.  The default behavior
**  is to read from 'test-prover.lisp' when the program begins, but you may provide your 
**  own file to read from by entering -1 as your selection and entering the file name when
**  prompted.  The result from each test will be printed to a file Solutions_'testNum'_'type'.txt
**
**  See prog2.pdf for project specifications
*/