1. t(a)                      [5]
6. ~t(Z) | q(Z) | r(Z)       [12]
2. ~q(W) | ~p(W)             [8]
4. p(X) | ~t(a)              [9] Subsumed by p(X)
3. ~r(Y) | ~p(Y)             [8]

w: predicates = 3, functions = 2, variables = 1
p: reverse alphabetic

5. 4+1 = p(X)               [4]
4+2 =                           Sibling subsumed parent

7. 6+1 = q(a) | r(a)        [10]

8. 7+3 = q(a) | ~p(a)       [10]

9. 8+2 ~p(a) | ~p(a)        [10]

9+5 = FALSE