SymPy中satisfiable函数返回非预期结果的疑问咨询

我最近在学习使用SymPy，现在正在做下面这些操作：

>>> from sympy import *
>>> x, y, z, t = symbols('x y z t')
>>> k, m, n = symbols('k m n', integer=True)
>>> f, g, h = symbols('f g h', cls=Function)
>>> init_printing()
>>> satisfiable((x > 3) & (x == 1))
False

这个结果是正确的，毕竟x不可能同时大于3和等于1。

但当我把最后一行指令改成这样的时候：

>>> print(satisfiable((x > 3) & (x <= 1)))
{Q.le(x, 1): True, Q.gt(x, 3): True}

我本来预期它会返回False，显然我对SymPy的satisfiable函数有些地方没搞明白，有没有人能给我点提示呀？

备注：内容来源于stack exchange，提问作者thetango