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.