Bugfixes in Term, Literal, Ewff, Clause, Setup.

* Began the unit test for Setup.
* Fixed: std::vector does not resize automatically when v[i] = x and i
  is out of bounds. (Inconsistenct with map...)
* Fixed: to iterate over same-predicate literals, the right range is
  lower_bound(l.LowerBound()) .. lower_bound(l.UpperBound()), whereas
  I had used upper_bound(.) instead for the second iterator.
* Fixed: For the above to work, Literal::UpperBound() should have
  negative sign, because otherwise there may be literals with the upper
  bound's predicate between l and the upper bound.
* Fixed: Literal::LowerBound() should have negative sign as well
  because we sometimes look for differently signed literals. (Bug
  didn't occur yet, but should be one.)
* Fixed: typo in Ewff::Subsumes led to twice comparing neq_var_ instead
  of once neq_var_ and once neq_name_.
* Fixed: Ewff::Substitute() was vacuously true for two vars X != Y
  where it should have been X == Y.
* Fixed: Clause::Subsumes() should check if substituting only the
  pattern suffices for equality; this is not done in Term::Match
  already because it doesn't work well with general (two-way)
  unification.
* Fixed: Term::Matches() allows no substitutions of *this, i.e., only
  the pattern can be changed.
* Fixed: Box clauses in need be grounded through Setup::GroundBoxes()
  first to avoid infinite unit propagation. Is there a better way to
  fix this? E.g., by restricting the longest action sequence?
  Experiments needed.
* Fixed: Setup::Rel() did not compute the closure correctly (no idea
  what it computed).
* Fixed: PEL = {a | a and ~a in REL} apparently does not suffice.
  Workaround so that PEL is essentially REL. Why doesn't PEL work?
* Fixed: Proper+ compiler swapped sign of literals.
* Fixed: Proper+ compiler created clauses with unsatisfiable ewffs.