We consider universal computability of the LCTRS with only rule scheme Calc:

  Signature: eval_0   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> o -> Int -> Int -> o -> o
             eval_1   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> o -> Int -> Int -> Bool -> o
             eval_10  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_11  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_12  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_13  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_14  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_15  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_16  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_17  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_18  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_19  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_2   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_20  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_21  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_22  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_23  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_24  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_25  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_26  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_27  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_28  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_29  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_3   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_30  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_31  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_32  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_33  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_34  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_35  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_36  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_37  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_38  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_39  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_4   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_40  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_41  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_42  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_43  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_44  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_45  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_46  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_47  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_48  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_49  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_5   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_50  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_51  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_52  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_53  :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_6   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_7   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_8   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_9   :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o
             eval_end :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Bool -> o

  Rules: 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
         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)
         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)
         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)
         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)
         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
         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)
         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)
         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)
         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)
         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
         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)
         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)
         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)
         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)
         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)
         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
         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)
         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
         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)
         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)
         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
         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)
         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
         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)
         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)
         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
         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)
         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)
         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)
         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)
         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)
         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)
         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)
         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)
         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)
         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)
         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
         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
         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)
         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)
         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)
         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)
         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
         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
         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)
         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)
         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)
         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)
         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
         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)
         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)
         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)
         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
         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
         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)
         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
         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
         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
         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)
         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
         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)
         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)
         eval_51(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up) | i > n
         eval_49(n, i, j, k, l, t, h, m, p, q, r, up) -> eval_end(n, i, j, k, l, t, h, m, p, q, r, up) | up

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

We start by computing the initial DP problem D1 = (P1, R UNION R_?, f, c), where:

  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 D1 = (P1, R UNION R_?, f, c).

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 { r, q }
  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 { r, q }

Processor output: { D2 = (P2, R UNION R_?, f, c) }, where:

  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 { r, q }
      (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 { r, q }
      (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 D2 = (P2, R UNION R_?, f, c).

We compute a graph approximation with the following edges:

  1:  2 
  2:  3 
  3:  4 
  4:  5 
  5:  6 11 
  6:  7 
  7:  8 
  8:  9 
  9:  10 
  10: 16 
  11: 12 
  12: 13 
  13: 14 
  14: 15 
  15: 16 
  16: 17 19 
  17: 18 
  18: 21 
  19: 20 
  20: 21 
  21: 22 24 
  22: 23 
  23: 26 
  24: 25 
  25: 26 
  26: 27 38 39 
  27: 28 33 
  28: 29 
  29: 30 
  30: 31 
  31: 32 
  32: 27 38 39 
  33: 34 
  34: 35 
  35: 36 
  36: 37 
  37: 27 38 39 
  38: 40 45 
  39: 45 
  40: 41 
  41: 42 
  42: 43 
  43: 44 
  44: 40 45 
  45: 46 51 
  46: 47 
  47: 48 
  48: 49 
  49: 50 
  50: 46 51 
  51: 52 
  52: 53 
  53: 54 
  54: 55 56 
  55: 57 
  56: 16 
  57: 58 59 
  58: 60 
  59: 3 
  60: 61 
  61: 62 
  62: 63 
  63: 64 
  64: 62 

There are 2 SCCs.

Processor output: { D3 = (P3, R UNION R_?, f, c) ; D4 = (P4, R UNION R_?, f, c) }, where:

  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 { r, q }
      (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 { r, q }
      (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 D3 = (P3, R UNION R_?, f, c).

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]

Processor output: { D5 = (P5, R UNION R_?, f, c) ; D6 = (P6, R UNION R_?, f, c) }, where:

  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 D4 = (P4, R UNION R_?, f, c).

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]

Processor output: { D7 = (P7, R UNION R_?, f, c) ; D8 = (P8, R UNION R_?, f, c) }, where:

  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 { r, q }
      (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 { r, q }
      (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 D5 = (P5, R UNION R_?, f, c).

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]

Processor output: { D9 = (P9, R UNION R_?, f, c) ; D10 = (P10, R UNION R_?, f, c) }, where:

  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 D6 = (P6, R UNION R_?, f, c).

We compute a graph approximation with the following edges:

  1: 2 
  2:

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

Processor output: { }.

***** We apply the Theory Arguments Processor on D7 = (P7, R UNION R_?, f, c).

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]

Processor output: { D11 = (P11, R UNION R_?, f, c) ; D12 = (P12, R UNION R_?, f, c) }, where:

  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 D8 = (P8, R UNION R_?, f, c).

We compute a graph approximation with the following edges:

  1:  2 
  2:  3 8 
  3:  4 
  4:  5 
  5:  6 
  6:  7 
  7:  13 
  8:  9 
  9:  10 
  10: 11 
  11: 12 
  12: 13 
  13: 14 16 
  14: 15 
  15: 18 
  16: 17 
  17: 18 
  18: 19 21 
  19: 20 
  20: 23 
  21: 22 
  22: 23 
  23: 24 35 36 
  24: 25 30 
  25: 26 
  26: 27 
  27: 28 
  28: 29 
  29: 24 35 36 
  30: 31 
  31: 32 
  32: 33 
  33: 34 
  34: 24 35 36 
  35: 37 42 
  36: 42 
  37: 38 
  38: 39 
  39: 40 
  40: 41 
  41: 37 42 
  42: 43 48 
  43: 44 
  44: 45 
  45: 46 
  46: 47 
  47: 43 48 
  48: 49 
  49: 50 
  50: 51 
  51: 52 53 
  52: 54 
  53: 13 
  54: 55 
  55:

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

Processor output: { D13 = (P13, R UNION R_?, f, c) }, where:

  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 { r, q }
       (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 { r, q }
       (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 D9 = (P9, R UNION R_?, f, c).