z3 - Z3-Py を使用して量指定子を削除するには?

Question

次のコードを使用して、量指定子のない数式を取得しようとしています。

S, E, I, R = Reals('S E I R')
b, n, s, g, m = Reals('b n s g m')
SS = Then('qe', 'smt').solver()
SS.add(Exists([S,E,I,R], And(m+g*R-m*S-b*I*S == 0,
   b*I*S-(m+s)*E==0, s*E-(n+m)*I==0, n*I-(m+g)*R==0,
   S > 0, I > 0, E > 0, R >0)))
SS.add(b > 0, n > 0, s >0 , g >0, m>0)
print SS
print SS.check()

しかし、私は出力を取得しています:

unknown

私のコードで何が起こるか教えてください。どうもありがとう。