Correcting the size of the smallest grammar

On the method for cut-introduction using maxsat, a
list of grammars is returned because of the
current implementation that supports only grammars
of the type U o S. Since the method needs more
general grammars, i.e., U o S1 o ... o Sn, this is
achieved by having a list of simpler grammars.
Consequently the computation of the size of these
grammars needs some adaptation.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2338 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
LK Equality rules now have a solid foundation grounded in positions. The existing constructors have been modified to use position logic and check for correctness. Additionally, I've added macro rules that automatically choose the right version of an equality rule (i.e. EquationLeft1 or EquationLeft2) and can insert several rules at once if more than one term is exchanged. Several algorithms have been adjusted to use these macro rules in lieu of the elementary equality rules since there are inferences in some of our tests and proof data that don't correspond to single rules.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2340 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Load resources using the classloader, not hard-coded paths.

This allows the tests to be run in IntelliJ.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@2341 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Add missing file from last commit.


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