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

8. 5+1 = p(X) | ~q(X,Y)       [7] TRUE
6. 5+3 = ~p(X)                [3] TRUE
7. 5+4 = ~t(X)                [3] TRUE

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

11. 10+6 = r(X)               [3] FALSE

12. 11+2 = t(Z)               [3] FALSE

12+7 = FALSE