I have seen this patent while searching for many-sorted theorem provers. And was surprised, as there are descriptions of full many-sorted resolutions far before that time. http://link.springer.com/chapter/10.1007%2F978-3-642-83739-5_4 http://books.google.co.jp/books/about/A_many_sorted_calculus_based_on_resoluti.html?id=twUnAAAAMAAJ&redir_esc=y etc.
This question is missing information necessary to easily research this patent application. Please add missing information to this prior art request, including: a patent number, at least one independent claim, a priority date (the date before which the prior art is needed) and a plain English description of the independent claim. See the prior art request template for more information and an example.