1. p(X) | ~q(X,Y) | ~s        [9] TRUE
6. q(X,b) | r(X)              [8] FALSE  Subsumed by r(X)
2. ~r(a) | t(Z)               [7] TRUE   Subsumed by t(Z)
5. s                          [2] FALSE
3. ~p(X) | ~s                 [5] TRUE
4. ~t(X) | ~s                 [5] TRUE

5+1 = p(X) | ~q(X,Y)              TRUE   Intermediate
5+3 = ~p(X)                       TRUE   Intermediate
5+4 = ~t(X)                       TRUE   Intermediate

6+1 = p(X) | r(X) | ~s            TRUE   Intermediate
7.  +5 = p(X) | r(X)          [6] FALSE  Subsumed by r(X)

7+3 = ~s | r(X)                   TRUE   Intermediate
8.  +5 = r(X)                 [3] FALSE

9. 8+2 = t(Z)                 [3] FALSE

9+4 = ~s                          TRUE   Intermediate
 +5 = FALSE