使用归结和调解的输入反驳与单元反驳不等价

Chang和Lee在文献1]中给出了如下结果: 定理8.4 如果子句集S有使用归结和调解的输入反驳,则S与函数自反公理集的并集有使用归结和调解的单元反驳。