根据归结原理编写程序（编程语言不限），要求给出完整python代码： 求子句集：(1) ¬P(x) Q(x) (2) ¬P(y) R(y) (3)P(a) (4)S(a) (5) ¬S(z) ¬ R(z) (¬G)

# 定义子句集
clauses = [
(set(['¬P(x)', 'Q(x)'])),
(set(['¬P(y)', 'R(y)'])),
(set(['P(a)'])),
(set(['S(a)'])),
(set(['¬S(z)', '¬R(z)'])),
(set(['¬G']))
]

# 定义归结函数
def resolve(ci, cj):
resolvents = []
for li in ci:
for lj in cj:
if li == '¬' + lj or lj == '¬' + li:
resolvent = (ci | cj) - set([li, lj])
if not resolvent:
resolvent.add('EMPTY_CLAUSE')
resolvents.append(resolvent)
return resolvents

# 定义归结循环
def resolution(clauses):
new = set()
while True:
for i in range(len(clauses)):
for j in range(i + 1, len(clauses)):
resolvents = resolve(clauses[i], clauses[j])
if set(['EMPTY_CLAUSE']) in resolvents:
return True
new = new.union(set(resolvents))
if new.issubset(clauses):
return False
clauses = clauses.union(new)

# 输出判断结果
if resolution(set(frozenset(c) for c in clauses)):
print('可以从给定子句集推导出空子句，即子句集不可满足')
else:
print('不能从给定子句集推导出空子句，即子句集可满足')