Setup::Subsumes() holds for valid clauses.

So far, Solver had to handle this case. It is now the Setups
responsibility as this follows exactly the theory.

There's something wrong with Setup::LocallyConsistent() and its use
in Solver::Assign(): it should close the set of literals only under
the unsubsumed clauses; and the starting set of literals should only
be the literals from the clauses.