1. p(X) | ~q(X,Y) | ~s        [9] TRUE   Subsumed by intermediate p(X) | ~q(X,Y)
7. 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   Subsumed by intermediate ~s
4. ~t(X) | ~s                 [5] TRUE   Subsumed by intermediate ~s

6. 5+1 = p(X) | ~q(X,Y)       [7] TRUE  Intermediate

8. 7+6 = r(X) | p(X)          [6] FALSE Subsumed by r(X)

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

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

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