Fixed an oversight in the end condition of find-mgu and added methods for explicit unification of literals.