Subsumption of clauses with ewffs.

* Clause::Subsumes() now takes Clause objects as arguments, not
  SimpleClause. That is necessary to defer grounding as long as
  possible.
* Added family of Match functions similar to Unify functions, but Match
  performs only one-way unification. More precisely, x.Match(y)
  performs pattern matching by checking if variables in y can be
  substituted so that the result equals x.
* Made SimpleClause a class (instead of a typedef) and moved several
  methods from Clause there. A SimpleClause is not boxed and has no
  ewff, but it may have variables.
  (Thanks for inherited constructors, C++.)
* Clause::PrependActions is called Clause::InstantiateBox() and sets
  box_ to false now.
* Made TermSeq a class (instead of a typedef).
* Clause::BoxUnify() is now essentially moved to TermSeq::IsSuffixOf().
* Added [Term|Atom|Literal]::[MIN|MAX].

Todo: more unit tests