YES
Termination proof succeeded
Used the following cutpoint-specific lexicographic rank functions:
 * For cutpoint 26, used the following rank functions/bounds (in descending priority order):
    - RF -2*seq_0-pos_0+2*n_0, bound -1
    - RF -pos_0+pi_0, bound 0
    - RF z_0+m_0, bound 2
    - RF -pos_0, bound 0
    - RF z_0, bound 1
Errors: