tEnqueueLiteral for decisions fixed
parallel execution enabled in build.sbt
Added a test from a diamond example.

The congruence closure algorithm doesn't detect the inconsistency, leading to
a SAT result from the DPLL engine. The test case implements the model found by
the DPLL procedure.
Various fixes, mainly in the DPLL algorithm

Fixed a match error in the congruence closure algorithm.

Main fix in DPLL algorithm is in conflictAnalysis, when searching for the UIP.
confl is allowed to be null, when c <= 1. status reset after backtracking does
not override a possible conflict found when enqueueing the decision literal in
the opposite polarity any more.