为什么解码出错，已经尝试了各种方法，还是不行

苏格拉底符号化及论证

用代码块功能插入代码，请勿粘贴截图

import nltk
lp = nltk.sem.logic.LogicParser()
P = lp.parse('man(Socrates)')
Q = lp.parse('all x(man(x) -> mortal(x))')
R = lp.parse('mortal(Socrates)')

prover1 = nltk.inference.prover9.Prover9()
print(prover1.prove(R, [P, Q]))

运行结果及报错内容

Traceback (most recent call last):
  File "F:\python\project\demo\shiyan2.py", line 9, in 
    print(prover1.prove(R, [P, Q]))
  File "D:\ANACONDA\ANA\envs\know\lib\site-packages\nltk\inference\api.py", line 37, in prove
    return self._prove(goal, assumptions, verbose)[0]
  File "D:\ANACONDA\ANA\envs\know\lib\site-packages\nltk\inference\prover9.py", line 327, in _prove
    stdout, returncode = self._call_prover9(
  File "D:\ANACONDA\ANA\envs\know\lib\site-packages\nltk\inference\prover9.py", line 356, in _call_prover9
    stdout, returncode = self._call(
  File "D:\ANACONDA\ANA\envs\know\lib\site-packages\nltk\inference\prover9.py", line 219, in _call
    return (stdout.decode("utf-8"), p.returncode)
UnicodeDecodeError: 'utf-8' codec can't decode byte 0xb1 in position 222: invalid start byte