Gandalf is an automated theorem proving (ATP) system ... is particularly strong at large problems, decidable classes and model building according to the
CASC competition, probably the best there is for these kinds of tasks.
The person behind it, Tanel Tammet, is looking to get in touch with people doing implementation work for using first order provers for semantic web tasks.