z3 - Z3Py は特定の証拠を作成できませんか?

Question

私はそれを証明しようとしています

4*n^3*m+4*n*m^3 <= n^4+6*n^2*m^2+m^4

すべてのn、m実数。Z3Py をオンラインで使用します。

私はコードを使用しています：

n, m = Reals('n m')

s = Solver()

s.add(ForAll([n, m], n**4+6*n**2*m**2+m**4 >= 4*n**3*m+4*n*m**3))

print s.check()

出力は : unknownです。

Z3が入手できない理由を教えてください "sat"。