prolog - different/2 - does a pure, determinate definition exist?

Question

different(Xs, Ys) :-
   member(X, Xs),
   non_member(X, Ys).
different(Xs, Ys) :-
   member(Y, Ys),
   non_member(Y, Xs).

While this definition using member/2 and non_member/2 is almost¹ perfect from a declarative viewpoint, it produces redundant solutions for certain queries and leaves choice points all around.

What is a definition that improves upon this (in a pure manner probably using if_/3 and (=)/3) such that exactly the same set of solutions is described by different/2 but is determinate at least for ground queries (thus does not leave any useless choice points open) and omits (if possible) any redundant answer?

---

¹ _{Actually, different([a|nonlist],[]), different([],[b|nonlist]) succeeds. It could equally fail. So a solution that fails for both is fine (maybe even finer).}

Answer 1

First try!

The following code is based on the meta-predicates tfilter/3 and tpartition/4, the monotone if-then-else control construct if_/3, the reified unary logical connective not_t/3, and the reified term equality predicate (=)/3:

different([],[_|_]).
different([X|Xs0],Ys0) :-
   tpartition(=(X),Ys0,Es,Ys1),
   if_(Es=[], true, (tfilter(not_t(=(X)),Xs0,Xs1),different(Xs1,Ys1))).

Sample query:

?- different([A,B],[X,Y]).
                A=Y ,           dif(B,Y),     X=Y
;     A=X           ,     B=X           , dif(X,Y)
;     A=X           , dif(B,X), dif(B,Y), dif(X,Y)
;               A=Y ,               B=Y , dif(X,Y)
;               A=Y , dif(B,X), dif(B,Y), dif(X,Y)
; dif(A,X), dif(A,Y).

Let's observe determinism when working with ground data:

?- different([5,4],[1,2]).
true.

The above approach feels like a step in the right direction... But, as-is, I wouldn't call it perfect.