Altered length function

Changed the length function from using a generated conjecture to using
nested quantifiers. The nested quantifier approach works better, but
only if we are checking for "UNSAT" results. Checking for a "SAT" result
will always return "UNKNOWN".
Fixed bug with the set functions

The bug involved generating the incorrect type due to a hardcoded type
rather than generated.

Also altered the timeout method during verification.