* Replace various instances of output and finishOutput by an OutputManager trait.

* Simple Propositional solver (trivial) now can accept arbitrary number of premises.
Correction of many bugs related to the propositional solver,
and a crash in the kernel proof checker when using LeftOr and RightAnd on empty premises.