Then we can use 13.2 along the way to derive the empty clause if possible. Using 13.1 first and specifying that set of support must be used greatly reduces the search space. There are at least a couple possibilities to improve the search efficiency. Use the more specific approach first, then try resolution. Incorporate resolution and the more specific approach to take advantage of any helpful hints obtained by the more specific approach.
Nonmonotonic inference is a bit more complicated and is left to the students to read.