The paper presents an efficient unification algorithm for first-order predicate calculus, which is derived from a nondeterministic algorithm. The new algorithm efficiently embeds an acyclicity test, improving performance in various scenarios. The authors define the unification problem as solving a system of equations and provide a nondeterministic algorithm to transform the system into an equivalent set of equations in solved form. They then extend this formalism to multiequations, allowing for the grouping of multiple equations to be unified. This extension includes transformations such as multiequation reduction and compactification to handle complex systems. The main algorithm, UNIFY, selects multiequations based on a partial ordering to avoid unnecessary substitutions, ensuring efficient and concise solutions. The paper also discusses efficient multiequation selection and improvements for nonunifying data, including early detection of clashes. Finally, a PASCAL implementation is provided, and the algorithm's performance is compared with other well-known algorithms, showing superior performance in all tested cases.The paper presents an efficient unification algorithm for first-order predicate calculus, which is derived from a nondeterministic algorithm. The new algorithm efficiently embeds an acyclicity test, improving performance in various scenarios. The authors define the unification problem as solving a system of equations and provide a nondeterministic algorithm to transform the system into an equivalent set of equations in solved form. They then extend this formalism to multiequations, allowing for the grouping of multiple equations to be unified. This extension includes transformations such as multiequation reduction and compactification to handle complex systems. The main algorithm, UNIFY, selects multiequations based on a partial ordering to avoid unnecessary substitutions, ensuring efficient and concise solutions. The paper also discusses efficient multiequation selection and improvements for nonunifying data, including early detection of clashes. Finally, a PASCAL implementation is provided, and the algorithm's performance is compared with other well-known algorithms, showing superior performance in all tested cases.