% -----------------------------------------------------------------
unify1(A,B) :- unify([A],[B]).
% -----------------------------------------------------------------

unify([],[]).

unify([A|A1],[B|B1]) :- A==B, !, unify(A1,B1).

unify([A|A1],[B|B1]) :- var(A), !, not_in(A,B), A=B, unify(A1,B1).
unify([A|A1],[B|B1]) :- var(B), !, not_in(B,A), A=B, unify(A1,B1).

unify([A|A1],[B|B1]) :- A=..[F|ArgA], B=..[F|ArgB],
    length(ArgA,N), length(ArgB,N), unify(ArgA,ArgB),unify(A1,B1).

% -----------------------------------------------------------------
not_in(A,B) :- term_variables(B,L), \+ (member(X,L), X==A).
% -----------------------------------------------------------------