code cleanup in lk quantifier rules -- weak quantfier rules now throw an LKQuantificationException with the relevant formulas if the main formula does not fit to the inferred formula after inserting the replaced term. added testcases for weak quantifier rules in lk.

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