pushed to latest library versions, added an alternative clause set generation algorithm which handles bigger structs better(cvetan's algorithm was a normlization procedure on structs, which can create deep nestings which overflow the call stack)

git-svn-id: https://gapt.googlecode.com/svn/trunk@2344 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed a compiler warning in fol matching (an Option[X] was compared to [X]). Corrected the code, but i'm not 100% sure if this what should have been compared in the first place.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2345 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Implementing a more general grammar

The Grammar class goes from supporting only
grammars of the type U o S to supporting the more
genral grammar format U o S1 o ... o Sn, which is
needed for the introduction of many cuts.

Thanks to Christoph Spoerk for this change.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2346 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added glue code (partial reversing of hol2fol) to ntape tests, bugfixes in robinson2ral and ceres omega.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2347 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed cutIntro integration tests
added scala doc to Grammar class for the constructor

git-svn-id: https://gapt.googlecode.com/svn/trunk@2348 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
ntape proof acnf and et computed in ntape test

git-svn-id: https://gapt.googlecode.com/svn/trunk@2349 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
some more bugfixes to ceres omega

git-svn-id: https://gapt.googlecode.com/svn/trunk@2350 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
implemented (hopefully correct) skolem symbol merging. et calculation is working now.

git-svn-id: https://gapt.googlecode.com/svn/trunk@2351 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
sorry for breaking the build, this should fix it

git-svn-id: https://gapt.googlecode.com/svn/trunk@2352 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
I renamed the "ancestors" member of FormulaOccurrence to "parents" to reflect that it only contains immediate predecessors. I also added a function "ancestors" that returns the actual ancestors.


git-svn-id: https://gapt.googlecode.com/svn/trunk@2353 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fixing path of prover9 minitests

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