Python解决归结反演问题

类似于下图
图中的归结反演要如何用Python表达
涉及鲁滨逊归结原理，归结反演
只见过一元谓词的，下面这种就不会了。