Fixed the cases where cutIntro was successful while cutIntroG failed, reporting uncompressible proofs. 

* Fixed a bug in case 3 of ManyVariableDelta: new variables would only be created when the function symbol was unary. They are now only created if it is NOT unary.
* Fixed the grammar size calculation in the folding of the delta table for the generalized delta vector: the function ssize(S) was calculating sum(S.map(length)) instead of S.head.length. This penalized grammars with more than one variable and led to proofs being falsely labelled as uncompressible.

  As a side effect, some of the proofs in ProofSequences.scala are now compressible for smaller n. An example is SumExampleProof(n), which now works for n=4, but used to require n=8.
* Reinstated variable sanitizing in the cut formulas of cutIntroG: the first 6 variables are named x,y,z,u,v,w instead of x_0,...,x_6 for readability. The variables after w are x_6,x_7,...

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