The paper as published in AICOM has an error in the condition part of
the inference rule for Clause Subsumption (CS) on the 5th page of the
paper. 

The rule was written as

T    R v S
==========  if \sigma(S)=T for a substitution \sigma
    T

It should be

T    R v S
==========  if \sigma(T)=S for a substitution \sigma
    T

This error has been fixed in the version published on my private
bibliography page. 

- StS