Cleanup ml prover 5

@dwightguth @andreistefanescu please review
because ```orientSubstitution``` now returns a boolean to indicate whether the orientation succeeds (the orientation is possible and the resulting constraint is not false). If so, then there is no need to check ```unificationConstraint.substitution().keySet().containsAll(variables)```.  If not, then the substitution will remain unchanged.