KB implements (almost) LBF semantics.

* Splitting is done at a fixed point: after reducing conjunctive
  operators (more precisely, negated disjunctions and negated
  existentials).
* Added transform_range(), filter_range().
* Fixed missing Setup::Minimize() in Setup::PropagateUnit().
* Printing now sorts clauses and setups.