如何实现 not_all_equal/1 谓词

如何实施not_all_equal/1谓词，如果给定列表包含至少 2 个不同的元素，则该谓词成功，否则失败？

这是我的尝试（不是很纯粹的尝试）：

not_all_equal(L) :-
    (   member(H1, L), member(H2, L), H1 \= H2 -> true
    ;   list_to_set(L, S),
        not_all_equal_(S)
    ).

not_all_equal_([H|T]) :-
    (   member(H1, T), dif(H, H1)
    ;   not_all_equal_(T)
    ).

然而，这并不总是具有最佳行为：

?- not_all_equal([A,B,C]), A = a, B = b.
A = a,
B = b ;
A = a,
B = b,
dif(a, C) ;
A = a,
B = b,
dif(b, C) ;
false.

在这个例子中，只有第一个答案应该出现，其他两个答案是多余的。

这是使用的部分实现library(reif) for SICStus http://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/sicstus/reif.pl|SWI http://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/swi/reif.pl。这当然是正确的，因为当它无法继续时会产生错误。但它缺乏我们想要的通用性。

not_all_equalp([A,B]) :-
   dif(A,B).
not_all_equalp([A,B,C]) :-
   if_(( dif(A,B) ; dif(A,C) ; dif(B,C) ), true, false ).
not_all_equalp([A,B,C,D]) :-
   if_(( dif(A,B) ; dif(A,C) ; dif(A,D) ; dif(B,C) ; dif(B,D) ), true, false ).
not_all_equalp([_,_,_,_,_|_]) :-
   throw(error(representation_error(reified_disjunction),'C\'est trop !')).

?- not_all_equalp(L).
   L = [_A,_B], dif(_A,_B)
;  L = [_A,_A,_B], dif(_A,_B)
;  L = [_A,_B,_C], dif(_A,_B)
;  L = [_A,_A,_A,_B], dif(_A,_B)
;  L = [_A,_A,_B,_C], dif(_A,_B)
;  L = [_A,_B,_C,_D], dif(_A,_B)
;  error(representation_error(reified_disjunction),'C\'est trop !').
?- not_all_equalp([A,B,C]), A = a, B = b.
   A = a, B = b
;  false.

编辑：现在我意识到我不需要添加那么多dif/2根本没有目标！就足够了one变量与第一个不同！无需相互排斥！删除还是觉得有点不安全感dif(B,C)目标...

not_all_equalp([A,B]) :-
   dif(A,B).
not_all_equalp([A,B,C]) :-
   if_(( dif(A,B) ; dif(A,C) ), true, false ).
not_all_equalp([A,B,C,D]) :-
   if_(( dif(A,B) ; dif(A,C) ; dif(A,D) ), true, false ).
not_all_equalp([_,_,_,_,_|_]) :-
   throw(error(representation_error(reified_disjunction),'C\'est trop !')).

答案是完全相同的......我认为这里发生了什么。这个版本是否较弱，一致性较差？