added cli command to check lk proofs up isomorphic rules. bugfix for skolem expansion tree extraction.

git-svn-id: http://gapt.googlecode.com/svn/trunk@2123 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
less outermost parenthesis in prooftool, relaxed paramodulation rules in llk format

git-svn-id: http://gapt.googlecode.com/svn/trunk@2124 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Updated ProofSequences.scala in examples to fit current state of gapt

git-svn-id: http://gapt.googlecode.com/svn/trunk@2125 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Removing unreachable code (duplicated case)


git-svn-id: http://gapt.googlecode.com/svn/trunk@2126 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Removing another unreachable line.


git-svn-id: http://gapt.googlecode.com/svn/trunk@2127 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
poshed scala maven plugin to latest version, compile without zinc works again

git-svn-id: http://gapt.googlecode.com/svn/trunk@2128 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
a (hopefully correct) bugfix for prover9 parsing with nonclausal input formulas - before the formulas extracted came from a step before skolemization happened. 

git-svn-id: http://gapt.googlecode.com/svn/trunk@2129 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
adding focuing on a subproof as an alternative to zooming to the sunburst view

git-svn-id: http://gapt.googlecode.com/svn/trunk@2130 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
sunburst viewer shows all axiom formulas as primary formula in th einference view

git-svn-id: http://gapt.googlecode.com/svn/trunk@2131 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
pushing to version 1.9

git-svn-id: http://gapt.googlecode.com/svn/trunk@2132 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
adding ntape to examples

git-svn-id: http://gapt.googlecode.com/svn/trunk@2133 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
changed example name to match paper

git-svn-id: http://gapt.googlecode.com/svn/trunk@2134 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added prime proofs to examples

git-svn-id: http://gapt.googlecode.com/svn/trunk@2135 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
changed usage/help output in GAPShell
changed ncutIntro result to list of canonical solutions
added time logging to debug output in TreeGrammarDecomposition and MaxSAT
fixed a bug in TreeGrammarDecomposition leading to possible incomplete set of keys in case of n>=2
added a prettyPrinter function to abbreviate latex output of MCS formulation
refactored debugs/traces

git-svn-id: http://gapt.googlecode.com/svn/trunk@2136 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Added some helpful debug outputs in MaxSAT Interface

git-svn-id: http://gapt.googlecode.com/svn/trunk@2137 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Refactored CNFp generation and
added some helpful debug outputs in MaxSAT Interface

git-svn-id: http://gapt.googlecode.com/svn/trunk@2138 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
implemented Tseitin transformation to cnf for FOLFormulas
Note: this may not be an implementation of high performance
added additional debug output to maxsat

git-svn-id: http://gapt.googlecode.com/svn/trunk@2139 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
added propositional decomposition rules to ral, a bit of code cleanup in ral, started with embedding of prover9 proofs into ral

git-svn-id: http://gapt.googlecode.com/svn/trunk@2142 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
fixed prover9 detection code

git-svn-id: http://gapt.googlecode.com/svn/trunk@2143 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fix issue 267 (Error on solve propositional)


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