Fixed: assertion in Setup::PropagateUnits() to allow non-units.

Setup::PropagateUnits() loops over unit clauses using
lower/upper_bound(). It may encounter a non-unit clause in this loop in
case a resolvent in a previous iteration was non-unit and less then
*last where last is the upper_bound(). The new assertions respect this
case.

Also addded `scalable' unit tests for eventual completeness and
inconsistency.

Also changed the API for generated belief BATs. The k-parameter is now
given to the constructor, which passes it to
Clauses::AddBeliefConditional().