Created TPTP based test suite to help validate R_complete_simplify satisfiability logic

[GoogleCodeExporter]

There is a subset of problems in the TPTP:

http://www.cs.miami.edu/~tptp/

library, termed Pure Equality (PEQ), which could be used to help validate the 
satisfiability logic in R_complete_simplify. These problems comprise a single 
equality predicate but also functions, whereby it should be possible to 
transform these problems to the R_complete_simplify representation by using 
skolemization on the functions to free variables instead of unique constants 
(i.e. we can already get around unique names assumption in R_complete_simplify 
because that's basically what a free variable is: a "constant" that can be 
equal to other "constants". This takes care of using this suite of tests in our 
algorithm. However for the other way around, that is, converting our problems 
for other algorithms in which we do have constants, we need to add the 
constraints that they are pairwise distinct). 

Original issue reported on code.google.com by [email protected] on 23 Apr 2013 at 5:32