Ｈｅｎｓｃｈｅｎ和Ｗｏｓ在［２］中的定理１和定理２分别证明了不可满足的Ｈｏｒｎ集有严格－正的－单元反驳和严格－输入反驳，如果子句（ｃｌａｕｓｅ）集合Ｓ是一个Ｒ－不可满足的Ｈｏｒｎ集，该集合包含子句Ｒｘ，ｘ和它的函数反身公理，当Ω由调换（ｐａｒａｍｏｄｕｌａｔｉｏｎ）、归结（ｒｅｓｏｌｕｔｉｏｎ）和因子（ｆａｃｔｏｒｉｎｇ）三个推理规律组成时，Ｈｅｎｓｃｈｅｎ和Ｗｏｓ在［２］中的定理３证明了：利用这三个推理规律从该子句集可以得到一个输入反驳（ｉｎｐｕｔｒｅｔｕｔａｔｉｏｎ）Ｄ１和一个单元反驳（ｕｎｉｔｒｅｆ
