Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity.  Minor cleanup.
Adding example proof signatures for LFSC.