Disequality might not eliminate when `(!= (_0 _0))`

Question

When a unification constraint and a disequality constraint are applied to the same lvars they might eliminate possibilities.

`
(run 1 [q]
(fresh [v n]
(== q v)
(!= q v)))

;=> ()
`

However when a separate disequality is interleaved the possibility is not eliminated.

`
(run 1 [q]
(fresh [v n]

(== q v)
(!= q n)
(!= q v)))

;=> ((_0 :- (!= (_0 _0)) (!= (_0 _1))))
`

I expected this to also return '().

Answer 1

Reference: https://clojure.atlassian.net/browse/LOGIC-175 (reported by xeqi)