Combining A1 and AC1 Unification

From International Center for Computational Logic