Fix relating to issue #250. To avoid name clashes between the variables of the cut formula and variables in the expansion trees, the variables in the cut formula now have the format β_n.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1769 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
splitting cut-intro stats phase gcomp into termex, dtg, and dtr

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1770 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
removed david's debug output from struct computation, compile time should go down form 22 to 15 mins again; bugfixes to definition elimination, it handles the n-tape proof now. fixes to the n-tape proof, we had two different notions of infinity in there.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1771 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
some redestribution in definition elimination, less debug output, starting changes to struct creation (automatic trivial tautology elimination and treating arguments of plus as set; atm computing the clause set of the n-tape proof fails with a stack overflow)

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