Add support for spass extension, FO lower units algorithm

Algorithm not yet implemented; just a stub
Clean UnifyingResolution(MRR)
Add first version of FOLowerUnits

Untested; too many 'vars' instead of 'vals' too.