Proof.apply is duplicating nodes

[ceilican]

> skeptik -a RP -a D examples/proofs/TraceCheck/trace2.tc
[info] Compiling 125 Scala sources to /Users/Bruno/Dropbox/Code/Skeptik/target/scala-2.11/classes...
[warn] there was one inliner warning; re-run with -Yinline-warnings for details
[warn] one warning found
[info] Running at.logic.skeptik.ProofCompressionCLI -a RP -a D examples/proofs/TraceCheck/trace2.tc

Reading and checking proof 'examples/proofs/TraceCheck/trace2.tc' ... (completed in 111ms)
29
29
Measuring... (completed in 4ms)

        Compressing with algorithm: RP... (completed in 9ms)
        Measuring... (completed in 0ms)

        Compressing with algorithm: D... (completed in 9ms)
        Measuring... (completed in 0ms)


Proof                                  length       coreSize     height       space        time    
======================================================================================================
examples/proofs/TraceCheck/trace2      29           15           6            5            111     
examples/proofs/TraceCheck/trace2-RP   23 (79.3%)   12 (80.0%)   5 (83.3%)    5 (100.0%)   9 (8.1%)
examples/proofs/TraceCheck/trace2-D    20 (69.0%)   8 (53.3%)    6 (100.0%)   6 (120.0%)   9 (8.1%)

trace2.tc has length 20. But our Proof.apply constructor makes it have length 29! This is then corrected by DAGify.

[ceilican]

The bug seems to emerge from the interaction of the methods "resolveClauses" and "getNode".

A simpler proof where this wrong behavior can be see is trace4.tc. It should have 6 nodes, but it ends up having 7 nodes.