- Added a top level function (getDecompositions) that returns a list with all the
  decompositions (sorted by size).
- Now the function "improveCanonicalSolution" in CLI returns a list of the
  possible simplifications sorted by size.
- The main code for cut introduction now uses the improved solution.
- Should we change "decomposition" to "grammar" (at least at the top level so
  not to confuse the user)?
- Tried to fix the bug pointed out by Stefan in r1361. Now ForgetfulResolution
  finds the solution he proposed (¬P(x)∨P(s^3(x))) but it states that it is not
  a valid solution. Is it? I haven't checked.


git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1384 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Hardcoded example for cade paper: a typo.


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