Add first draft of proof exporter using VeriT's format
Add dependency on scopt
Improve VeriT parsers

Now there is a trait, as usual in the Scala combinator parsing library
Refactor draft proof exporter
Add draft CLI for proof compression
Change command line interfaces
Move Axiom and CutIC out of lk.scala
Remove inefficient computation of ancestor relation
Remove inefficient computation of ancestor relation
Clean CutIC
Add UncheckedInference

This will be useful to parse VeriT's theory inferences.
Create abstract proof parser
Clean ProofParser and ProofParserVeriT
Add draft parser for a yet-to-be-defined proof format for Skeptik
Simplify ProofParserVeriT
Fix UncheckedInference
Prepare ProofParserVeriT to use UncheckedInference instead of Axiom for unknown inferences
Clean
Make RPI work with UncheckedInference
Make ProofExporterVeriT export unchecked inference