The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  P1. (1)  eval_0#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_1#(n, i, j, k, l, t, h, m, p, q, r, true) | n > 0
      (2)  eval_1#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, 1, q, r, up)
      (3)  eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_3#(n, i, j, k, l, t, h, m, p, q, r, up)
      (4)  eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_4#(n, i, j, k, l, t, 1, m, p, q, r, up)
      (5)  eval_4#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_5#(n, i, j, k, l, t, h, n, p, q, r, up)
      (6)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) | up
      (7)  eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_7#(n, 1, j, k, l, t, h, m, p, q, r, up)
      (8)  eval_7#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_8#(n, i, n, k, l, t, h, m, p, q, r, up)
      (9)  eval_8#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_9#(n, i, j, n + 1, l, t, h, n, p, q, r, up)
      (10) eval_9#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, 2 * n, t, h, n, p, q, r, up)
      (11) eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) | not up
      (12) eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_11#(n, i, j, 1, l, t, h, m, p, q, r, up)
      (13) eval_11#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_12#(n, i, j, k, n, t, h, m, p, q, r, up)
      (14) eval_12#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_13#(n, n + 1, j, k, l, t, h, m, p, q, r, up)
      (15) eval_13#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, 2 * n, k, l, t, h, m, p, q, r, up)
      (16) eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up)
      (17) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (18) eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up)
      (19) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (20) eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up)
      (21) eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up)
      (22) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (23) eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up)
      (24) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (25) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up)
      (26) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up)
      (27) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0
      (28) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up)
      (29) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up)
      (30) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (31) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (32) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (33) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up)
      (34) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up)
      (35) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (36) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (37) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (38) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 \/ r <= 0
      (39) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0
      (40) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up)
      (41) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (42) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (43) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (44) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0
      (45) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0
      (46) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up)
      (47) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (48) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (49) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (50) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0
      (51) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up)
      (52) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up)
      (53) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up)
      (54) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_47#(n, i, j, k, t, t, h, m, p, q, r, up) | m <= 0
      (55) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0
      (56) eval_47#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_48#(n, i, j, k, l, t, h, m, p, q, r, not up)
      (57) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_49#(n, i, j, k, l, t, h, m, 2 * p, q, r, up) | p >= n
      (58) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) | p < n
      (59) eval_49#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_50#(n, i, j, k, l, t, h, m, p, q, r, up) | not up
      (60) eval_50#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, 1, j, k, l, t, h, m, p, q, r, up)
      (61) eval_51#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) | i <= n
      (62) eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_53#(n, i, j, k, l, t, h, m, p, q, r, up)
      (63) eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, i + 1, j, k, l, t, h, m, p, q, r, up)

***** We apply the Constraint Modification Processor on P1.

We replace eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 \/ r <= 0 by:

  eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { q, r }
  eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { q, r }

This yields:

  P2. (1)  eval_0#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_1#(n, i, j, k, l, t, h, m, p, q, r, true) | n > 0
      (2)  eval_1#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, 1, q, r, up)
      (3)  eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_3#(n, i, j, k, l, t, h, m, p, q, r, up)
      (4)  eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_4#(n, i, j, k, l, t, 1, m, p, q, r, up)
      (5)  eval_4#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_5#(n, i, j, k, l, t, h, n, p, q, r, up)
      (6)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) | up
      (7)  eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_7#(n, 1, j, k, l, t, h, m, p, q, r, up)
      (8)  eval_7#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_8#(n, i, n, k, l, t, h, m, p, q, r, up)
      (9)  eval_8#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_9#(n, i, j, n + 1, l, t, h, n, p, q, r, up)
      (10) eval_9#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, 2 * n, t, h, n, p, q, r, up)
      (11) eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) | not up
      (12) eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_11#(n, i, j, 1, l, t, h, m, p, q, r, up)
      (13) eval_11#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_12#(n, i, j, k, n, t, h, m, p, q, r, up)
      (14) eval_12#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_13#(n, n + 1, j, k, l, t, h, m, p, q, r, up)
      (15) eval_13#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, 2 * n, k, l, t, h, m, p, q, r, up)
      (16) eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up)
      (17) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (18) eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up)
      (19) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (20) eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up)
      (21) eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up)
      (22) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (23) eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up)
      (24) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (25) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up)
      (26) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up)
      (27) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0
      (28) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up)
      (29) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up)
      (30) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (31) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (32) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (33) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up)
      (34) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up)
      (35) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (36) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (37) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (38) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { q, r }
      (39) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { q, r }
      (40) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0
      (41) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up)
      (42) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (43) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (44) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (45) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0
      (46) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0
      (47) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up)
      (48) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (49) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (50) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (51) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0
      (52) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up)
      (53) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up)
      (54) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up)
      (55) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_47#(n, i, j, k, t, t, h, m, p, q, r, up) | m <= 0
      (56) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0
      (57) eval_47#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_48#(n, i, j, k, l, t, h, m, p, q, r, not up)
      (58) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_49#(n, i, j, k, l, t, h, m, 2 * p, q, r, up) | p >= n
      (59) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) | p < n
      (60) eval_49#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_50#(n, i, j, k, l, t, h, m, p, q, r, up) | not up
      (61) eval_50#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, 1, j, k, l, t, h, m, p, q, r, up)
      (62) eval_51#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) | i <= n
      (63) eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_53#(n, i, j, k, l, t, h, m, p, q, r, up)
      (64) eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, i + 1, j, k, l, t, h, m, p, q, r, up)

***** We apply the Graph Processor on P2.

Considering the 2 SCCs, this DP problem is split into the following new problems.

  P3. (1) eval_51#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) | i <= n
      (2) eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_53#(n, i, j, k, l, t, h, m, p, q, r, up)
      (3) eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, i + 1, j, k, l, t, h, m, p, q, r, up)

  P4. (1)  eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_3#(n, i, j, k, l, t, h, m, p, q, r, up)
      (2)  eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_4#(n, i, j, k, l, t, 1, m, p, q, r, up)
      (3)  eval_4#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_5#(n, i, j, k, l, t, h, n, p, q, r, up)
      (4)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) | up
      (5)  eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_7#(n, 1, j, k, l, t, h, m, p, q, r, up)
      (6)  eval_7#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_8#(n, i, n, k, l, t, h, m, p, q, r, up)
      (7)  eval_8#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_9#(n, i, j, n + 1, l, t, h, n, p, q, r, up)
      (8)  eval_9#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, 2 * n, t, h, n, p, q, r, up)
      (9)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) | not up
      (10) eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_11#(n, i, j, 1, l, t, h, m, p, q, r, up)
      (11) eval_11#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_12#(n, i, j, k, n, t, h, m, p, q, r, up)
      (12) eval_12#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_13#(n, n + 1, j, k, l, t, h, m, p, q, r, up)
      (13) eval_13#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, 2 * n, k, l, t, h, m, p, q, r, up)
      (14) eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up)
      (15) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (16) eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up)
      (17) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (18) eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up)
      (19) eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up)
      (20) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (21) eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up)
      (22) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (23) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up)
      (24) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up)
      (25) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0
      (26) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up)
      (27) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up)
      (28) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (29) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (30) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (31) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up)
      (32) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up)
      (33) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (34) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (35) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (36) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { q, r }
      (37) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { q, r }
      (38) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0
      (39) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up)
      (40) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (41) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (42) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (43) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0
      (44) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0
      (45) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up)
      (46) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (47) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (48) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (49) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0
      (50) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up)
      (51) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up)
      (52) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up)
      (53) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_47#(n, i, j, k, t, t, h, m, p, q, r, up) | m <= 0
      (54) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0
      (55) eval_47#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_48#(n, i, j, k, l, t, h, m, p, q, r, not up)
      (56) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) | p < n

***** We apply the Theory Arguments Processor on P3.

We use the following theory arguments function:

  eval_51# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_52# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_53# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]

This yields the following new DP problems:

  P5. (1) eval_51#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) | i <= n
      (2) eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (3) eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, i + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }

  P6. (1) eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_53#(n, i, j, k, l, t, h, m, p, q, r, up)
      (2) eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, i + 1, j, k, l, t, h, m, p, q, r, up)

***** We apply the Theory Arguments Processor on P4.

We use the following theory arguments function:

  eval_51# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_52# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_53# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]

This yields the following new DP problems:

  P7. (1)  eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_3#(n, i, j, k, l, t, h, m, p, q, r, up)
      (2)  eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_4#(n, i, j, k, l, t, 1, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (3)  eval_4#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_5#(n, i, j, k, l, t, h, n, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (4)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) | up { n, i, j, k, l, t, h, m, p, q, r, up }
      (5)  eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_7#(n, 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (6)  eval_7#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_8#(n, i, n, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (7)  eval_8#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_9#(n, i, j, n + 1, l, t, h, n, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (8)  eval_9#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, 2 * n, t, h, n, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (9)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) | not up { n, i, j, k, l, t, h, m, p, q, r, up }
      (10) eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_11#(n, i, j, 1, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (11) eval_11#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_12#(n, i, j, k, n, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (12) eval_12#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_13#(n, n + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (13) eval_13#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, 2 * n, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (14) eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (15) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p { n, i, j, k, l, t, h, m, p, q, r, up }
      (16) eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (17) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p { n, i, j, k, l, t, h, m, p, q, r, up }
      (18) eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (19) eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (20) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p { n, i, j, k, l, t, h, m, p, q, r, up }
      (21) eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (22) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p { n, i, j, k, l, t, h, m, p, q, r, up }
      (23) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (24) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (25) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (26) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (27) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (28) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (29) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (30) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (31) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (32) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (33) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (34) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (35) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (36) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (37) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (38) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (39) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (40) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (41) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (42) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (43) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (44) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (45) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (46) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (47) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (48) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (49) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (50) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (51) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (52) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (53) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_47#(n, i, j, k, t, t, h, m, p, q, r, up) | m <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (54) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
      (55) eval_47#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_48#(n, i, j, k, l, t, h, m, p, q, r, not up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (56) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) | p < n { n, i, j, k, l, t, h, m, p, q, r, up }

  P8. (1)  eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_4#(n, i, j, k, l, t, 1, m, p, q, r, up)
      (2)  eval_4#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_5#(n, i, j, k, l, t, h, n, p, q, r, up)
      (3)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) | up
      (4)  eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_7#(n, 1, j, k, l, t, h, m, p, q, r, up)
      (5)  eval_7#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_8#(n, i, n, k, l, t, h, m, p, q, r, up)
      (6)  eval_8#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_9#(n, i, j, n + 1, l, t, h, n, p, q, r, up)
      (7)  eval_9#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, 2 * n, t, h, n, p, q, r, up)
      (8)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) | not up
      (9)  eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_11#(n, i, j, 1, l, t, h, m, p, q, r, up)
      (10) eval_11#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_12#(n, i, j, k, n, t, h, m, p, q, r, up)
      (11) eval_12#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_13#(n, n + 1, j, k, l, t, h, m, p, q, r, up)
      (12) eval_13#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, 2 * n, k, l, t, h, m, p, q, r, up)
      (13) eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up)
      (14) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (15) eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up)
      (16) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (17) eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up)
      (18) eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up)
      (19) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
      (20) eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up)
      (21) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
      (22) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up)
      (23) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up)
      (24) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0
      (25) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up)
      (26) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up)
      (27) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (28) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (29) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (30) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up)
      (31) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up)
      (32) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (33) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (34) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (35) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { q, r }
      (36) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { q, r }
      (37) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0
      (38) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up)
      (39) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (40) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
      (41) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
      (42) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0
      (43) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0
      (44) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up)
      (45) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up)
      (46) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
      (47) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
      (48) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0
      (49) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up)
      (50) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up)
      (51) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up)
      (52) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_47#(n, i, j, k, t, t, h, m, p, q, r, up) | m <= 0
      (53) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0
      (54) eval_47#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_48#(n, i, j, k, l, t, h, m, p, q, r, not up)
      (55) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) | p < n

***** We apply the Theory Arguments Processor on P5.

We use the following theory arguments function:

  eval_51# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_52# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_53# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]

This yields the following new DP problems:

  P9. (1) eval_51#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) | i <= n { n, i, j, k, l, t, h, m, p, q, r, up }
      (2) eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
      (3) eval_53#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_51#(n, i + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }

  P10. (1) eval_51#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_52#(n, i, j, k, l, t, h, m, p, q, r, up) | i <= n

***** We apply the Graph Processor on P6.

As there are no SCCs, this DP problem is removed.

***** We apply the Theory Arguments Processor on P7.

We use the following theory arguments function:

  eval_51# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_52# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]
  eval_53# : [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]

This yields the following new DP problems:

  P11. (1)  eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (2)  eval_3#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_4#(n, i, j, k, l, t, 1, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (3)  eval_4#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_5#(n, i, j, k, l, t, h, n, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (4)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) | up { n, i, j, k, l, t, h, m, p, q, r, up }
       (5)  eval_6#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_7#(n, 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (6)  eval_7#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_8#(n, i, n, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (7)  eval_8#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_9#(n, i, j, n + 1, l, t, h, n, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (8)  eval_9#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, 2 * n, t, h, n, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (9)  eval_5#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) | not up { n, i, j, k, l, t, h, m, p, q, r, up }
       (10) eval_10#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_11#(n, i, j, 1, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (11) eval_11#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_12#(n, i, j, k, n, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (12) eval_12#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_13#(n, n + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (13) eval_13#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, 2 * n, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (14) eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (15) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p { n, i, j, k, l, t, h, m, p, q, r, up }
       (16) eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (17) eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p { n, i, j, k, l, t, h, m, p, q, r, up }
       (18) eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (19) eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (20) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p { n, i, j, k, l, t, h, m, p, q, r, up }
       (21) eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (22) eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p { n, i, j, k, l, t, h, m, p, q, r, up }
       (23) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (24) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (25) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (26) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (27) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (28) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (29) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (30) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (31) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (32) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (33) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (34) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (35) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (36) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (37) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (38) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (39) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (40) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (41) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (42) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (43) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (44) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (45) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (46) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (47) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (48) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (49) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (50) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (51) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (52) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (53) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_47#(n, i, j, k, t, t, h, m, p, q, r, up) | m <= 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (54) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0 { n, i, j, k, l, t, h, m, p, q, r, up }
       (55) eval_47#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_48#(n, i, j, k, l, t, h, m, p, q, r, not up) { n, i, j, k, l, t, h, m, p, q, r, up }
       (56) eval_48#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) | p < n { n, i, j, k, l, t, h, m, p, q, r, up }

  P12. (1) eval_2#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_3#(n, i, j, k, l, t, h, m, p, q, r, up)

***** We apply the Graph Processor on P8.

There is only one SCC, so all DPs not inside the SCC can be removed:

  P13. (1)  eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_15#(n, i, j, k, l, t, h, m, p, q, r, up)
       (2)  eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
       (3)  eval_16#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, p, r, up)
       (4)  eval_15#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
       (5)  eval_17#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_18#(n, i, j, k, l, t, h, m, p, m, r, up)
       (6)  eval_18#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_19#(n, i, j, k, l, t, h, m - q, p, q, r, up)
       (7)  eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) | m >= p
       (8)  eval_20#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, p, up)
       (9)  eval_19#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) | m < p
       (10) eval_21#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_22#(n, i, j, k, l, t, h, m, p, q, m, up)
       (11) eval_22#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m - r, p, q, r, up)
       (12) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0 /\ r > 0
       (13) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_25#(n, i, j, k, l, t, h, m, p, q, r, up)
       (14) eval_25#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_26#(n, i, j, k, l, t, h, m, p, q, r, up)
       (15) eval_26#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_27#(n, i, j, k + h, l, t, h, m, p, q, r, up)
       (16) eval_27#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_28#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
       (17) eval_28#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
       (18) eval_24#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_29#(n, i, j, k, l, t, h, m, p, q, r, up)
       (19) eval_29#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_30#(n, i, j, k, l, t, h, m, p, q, r, up)
       (20) eval_30#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_31#(n, i, j, k + h, l, t, h, m, p, q, r, up)
       (21) eval_31#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_32#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
       (22) eval_32#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_23#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
       (23) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0 { q, r }
       (24) eval_23#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0 { q, r }
       (25) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) | r > 0
       (26) eval_34#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_35#(n, i, j, k, l, t, h, m, p, q, r, up)
       (27) eval_35#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_36#(n, i, j, k + h, l, t, h, m, p, q, r, up)
       (28) eval_36#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_37#(n, i, j - 1, k, l, t, h, m, p, q, r, up)
       (29) eval_37#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_33#(n, i, j, k, l, t, h, m, p, q, r - 1, up)
       (30) eval_33#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) | r <= 0
       (31) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) | q > 0
       (32) eval_39#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_40#(n, i, j, k, l, t, h, m, p, q, r, up)
       (33) eval_40#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_41#(n, i, j, k + h, l, t, h, m, p, q, r, up)
       (34) eval_41#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_42#(n, i + 1, j, k, l, t, h, m, p, q, r, up)
       (35) eval_42#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_38#(n, i, j, k, l, t, h, m, p, q - 1, r, up)
       (36) eval_38#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) | q <= 0
       (37) eval_43#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_44#(n, i, j, k, l, t, -h, m, p, q, r, up)
       (38) eval_44#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_45#(n, i, j, k, l, k, h, m, p, q, r, up)
       (39) eval_45#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_46#(n, i, j, l, l, t, h, m, p, q, r, up)
       (40) eval_46#(n, i, j, k, l, t, h, m, p, q, r, up) => eval_14#(n, i, j, k, l, t, h, m, p, q, r, up) | m > 0

***** No progress could be made on DP problem P9.