在`(!= (_0 _0))`中，不等式可能不会消除

Question

当将统一约束和不等式约束应用于相同的lvars时，可能会消除可能性。

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

;=> ()
`

然而，当单独的不等式被插入时，可能性不会被消除。

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

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

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

我原本预期这也会返回'()。

Answer 1

参考：https://clojure.atlassian.net/browse/LOGIC-175（由xeqi报告）