Fix FORPILU

Check for unification changed to only use variables in the aux formulae
Clean FORPILU

Since last change, the unifiableVariables set was not necessary in a 
lot of places; it's been removed.