Prover9 import should now work again. The biggest issue was that the equality rules didn't cover the case of trivial rules, i.e. the equation is of the form s=s and the auxiliary and main formulas coincide.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2355 85d21ef8-add0-11de-ae77-5bfb9c5a3f34