Estou brincando com restrições no prólogo (swi) usando a biblioteca clpfd.

Estou tentando identificar quando um conjunto de restrições encapsula ou substitui o outro, por exemplo X <4 encapsula X <7, pois sempre que o primeiro é verdadeiro, o último é verdadeiro. Isso pode ser facilmente representado usando implicação lógica. No entanto, não consegui que o operador # ==> me desse o resultado que desejava, então comecei a não usar (Co1 # / \ # \ Co2) onde Co1 e Co2 são restrições. Isso é bom para restrições individuais, mas eu queria passar uma conjunção de restrições para Co1 e Co2.

Agora, aqui está o problema. Quando eu tento

X#<7 #/\ #\X#<4.

eu voltei

X in 4..6,
X+1#=_G822,
X+1#=_G834,
_G822 in 5..7,
_G834 in 5..7.

(curiosamente, fazer isso no Sicstus resulta em uma falha de segmentação)

Quando eu passo

X#<7,X#<4

Eu recebo o desejado

X in inf..3.

Obviamente, não posso passar o último para não (Co1 # / \ # \ Co2), mas o primeiro não me dá o resultado que desejo. Alguém pode explicar por que as duas abordagens produzem resultados diferentes e como posso fazer com que a primeira aja como a segunda?