Fixed bug in encoding the final conflict during interpolation. Refactored Interpolation and BUP out of SATRefutation.