Installation requirements and usage instructions: README.md

Theories are parsed in this script to so that each axiom is represented as an element in a list. The list contains all axioms in the theory and removes all comments from the original file. All comments must be ended by a period in order for axioms to be parsed correctly.

The last two functions are called when relation definitions are needed. Unique relation names are identified and retrieved from the theory, then the definitions that are provided by the user are added to the theory.

Mace4 cooked models are parsed in this script. Model pairs are stored in a list so they can be used for Prover9/Mace4. Constants must contain alphabetical letters (can be alphabetical or alphanumeric) to work with Mace4, so all numeric constants are replaced by a unique letter in the alphabet (i.e., 0 -> 'a', 1 -> 'b', etc.). Inequalities for each constant are then appended to the list (will not change model file in place, but instead will work at runtime). Finally, a closure axiom is added to the end of the model.