Like SWI Prolog's unifiable/3, but maintains the left-right order of the terms in the unifier, rather than placing variables on the left.

unifier.pl

%!  unifier(@Term1, @Term2, ?Unifier) is semidet.
%
%   Like SWI Prolog's unifiable/3, but maintains the left-right order of the terms in the unifier, rather than placing variables on the left.
unifier(A, B, Unifier) :-
    rb_empty(Seen),
    unifier_(Seen, A, B, [], Unifier0),
    exclude(unifier_is_reflexive, Unifier0, Unifier1),
    sort(Unifier1, Unifier).

unifier_(Seen0, A, B, Unifier0, Unifier) :-
    (var(A) ; var(B))
    -> Unifier = [A=B|Unifier0]
    ;  rb_insert_new(Seen0, A-B, true, Seen)
       -> A =.. [F|As],
	  B =.. [F|Bs],
	  foldl(unifier_(Seen), As, Bs, Unifier0, Unifier)
    ; Unifier = Unifier0.

unifier_is_reflexive(A=B) :- A == B.

% unifier_list_ uses a list instead of an rbtree to check visited pairs.
%% unifier_list_(Seen, A, B, Unifier0, Unifier) :-
%%     (var(A) ; var(B))
%%     -> Unifier = [A=B|Unifier0]
%%     ;  memberchk_eq(A-B, Seen)
%%        -> Unifier = Unifier0
%%     ;  A =.. [F|As],
%%        B =.. [F|Bs],
%%        foldl(unifier_list_([A-B|Seen]), As, Bs, Unifier0, Unifier).

%% memberchk_eq(X, [A|As]) :-
%%     X == A
%%     -> true
%%     ;  memberchk_eq(X, As).