1. They, e.g., do not entail the saturation and reflexivity properties given below.

2. The calculus in Kohlhase 1998 is technically still flawed; e.g., to guarantee soundness Skolemization must be used in rule \(\textit{SIM}(\textit{fun})\).

3. RUE stands for resolution by unification and equality.

4. Different to what is claimed, the presented rules fail to capture an exhaustive extensionality treatment, and so did their implementation in the prover HOT (Konrad 1998); see the respective comment on this in Benzmüller 1997; there are also some soundness issues.