Improved efficency of Clause::Subsumes().

Added [Atom|Literal]::[Lower|Upper]Bound().
Clause::Subsumes() first estimates whether subsumption is even possible
and only then attempts the necessary unifications. Both checks are now
more efficient (from O(n*m) to O(n+m) where n, m are the lengths of the
clauses) through use of lower/upper bounds.