(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E F G H I J K)
(RULES
  f63(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f11(A, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 2 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 2 >= 0 /\ -A + G + 20 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 1 >= 0 /\ -A - F + 21 >= 0 /\ F - 1 >= 0 /\ -E + F + 19 >= 0 /\ D + F - 2 >= 0 /\ C + F - 21 >= 0 /\ -C + F + 19 >= 0 /\ B + F - 11 >= 0 /\ -B + F + 9 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 18 >= 0 /\ -A - E + 39 >= 0 /\ -A + E + 1 >= 0 /\ J - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 3 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 18 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 22 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 8 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 12 >= 0 /\ -A + B + 10 >= 0 /\ J - 2 >= 0 /\ -A + J + 18 >= 0 /\ -A + 20 >= 0 /\ A >= B + 1 ]
  f0(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f11(A, 10, 20, 1, 20, 0, 0, H, I, J, K))
  f11(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f11(A, B, C, D, E, F, 1, H, I, J, K)) [ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ -B + 10 >= 0 /\ B - 10 >= 0 /\ D >= E /\ G = 0 ]
  f11(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f11(A, B, C, D, D + 1, F, 1, H, I, J, K)) [ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ -B + 10 >= 0 /\ B - 10 >= 0 /\ E = D + 1 /\ G = 0 ]
  f11(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f11(A, B, C, D, D + 1, F, 1, N, I, J, K)) [ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ -B + 10 >= 0 /\ B - 10 >= 0 /\ L >= M + 1 /\ E = D + 1 /\ G = 0 ]
  f11(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f40(E, B, C, D, E, F, 0, N, L, D + 1, M)) [ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ -B + 10 >= 0 /\ B - 10 >= 0 /\ E >= D + 2 /\ G = 0 ]
  f40(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f59(A, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 2 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 2 >= 0 /\ -A + G + 20 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 1 >= 0 /\ -A - F + 21 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 2 >= 0 /\ -A + F + 20 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 18 >= 0 /\ -A - E + 40 >= 0 /\ -A + E >= 0 /\ J - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 3 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 18 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 22 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 8 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 12 >= 0 /\ -A + B + 10 >= 0 /\ J - 2 >= 0 /\ -A + J + 18 >= 0 /\ -A + 20 >= 0 /\ F >= 1 ]
  f40(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f43(A, B, C, D, E, 0, G, H, I, J + 1, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 2 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 2 >= 0 /\ -A + G + 20 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 1 >= 0 /\ -A - F + 21 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 2 >= 0 /\ -A + F + 20 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 18 >= 0 /\ -A - E + 40 >= 0 /\ -A + E >= 0 /\ J - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 3 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 18 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 22 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 8 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 12 >= 0 /\ -A + B + 10 >= 0 /\ J - 2 >= 0 /\ -A + J + 18 >= 0 /\ -A + 20 >= 0 /\ F = 0 ]
  f43(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f43(A, B, C, D, E, F, G, H, I, J + 1, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 20 >= 0 /\ -F >= 0 /\ -E - F + 20 >= 0 /\ D - F - 1 >= 0 /\ C - F - 20 >= 0 /\ -C - F + 20 >= 0 /\ B - F - 10 >= 0 /\ -B - F + 10 >= 0 /\ J - F - 3 >= 0 /\ -A - F + 20 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 20 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 40 >= 0 /\ -A + E >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 10 >= 0 /\ J - 3 >= 0 /\ -A + J + 17 >= 0 /\ -A + 20 >= 0 /\ K >= N + 1 ]
  f48(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f48(A - 1, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 19 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 19 >= 0 /\ -F >= 0 /\ -E - F + 20 >= 0 /\ D - F - 1 >= 0 /\ C - F - 20 >= 0 /\ -C - F + 20 >= 0 /\ B - F - 10 >= 0 /\ -B - F + 10 >= 0 /\ J - F - 3 >= 0 /\ -A - F + 19 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 39 >= 0 /\ -A + E - 1 >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 18 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 39 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C - 1 >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 29 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 9 >= 0 /\ J - 3 >= 0 /\ -A + J + 16 >= 0 /\ -A + 19 >= 0 ]
  f54(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f40(A, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 19 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 19 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 2 >= 0 /\ -A - F + 20 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 39 >= 0 /\ -A + E - 1 >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 18 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 39 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C - 1 >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 29 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 9 >= 0 /\ J - 3 >= 0 /\ -A + J + 16 >= 0 /\ -A + 19 >= 0 /\ F >= 1 ]
  f54(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f40(A, B, C, D, E, 0, G, N, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 19 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 19 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 2 >= 0 /\ -A - F + 20 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 39 >= 0 /\ -A + E - 1 >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 18 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 39 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C - 1 >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 29 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 9 >= 0 /\ J - 3 >= 0 /\ -A + J + 16 >= 0 /\ -A + 19 >= 0 /\ F = 0 ]
  f59(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f63(A, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 2 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 2 >= 0 /\ -A + G + 20 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 1 >= 0 /\ -A - F + 21 >= 0 /\ F - 1 >= 0 /\ -E + F + 19 >= 0 /\ D + F - 2 >= 0 /\ C + F - 21 >= 0 /\ -C + F + 19 >= 0 /\ B + F - 11 >= 0 /\ -B + F + 9 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 18 >= 0 /\ -A - E + 40 >= 0 /\ -A + E >= 0 /\ J - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 3 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 18 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 22 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 8 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 12 >= 0 /\ -A + B + 10 >= 0 /\ J - 2 >= 0 /\ -A + J + 18 >= 0 /\ -A + 20 >= 0 /\ B >= A + 1 ]
  f59(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f63(A, B, C, D, A - 1, F, G, H, I, J, K)) [ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 2 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 2 >= 0 /\ -A + G + 20 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 1 >= 0 /\ -A - F + 21 >= 0 /\ F - 1 >= 0 /\ -E + F + 19 >= 0 /\ D + F - 2 >= 0 /\ C + F - 21 >= 0 /\ -C + F + 19 >= 0 /\ B + F - 11 >= 0 /\ -B + F + 9 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 18 >= 0 /\ -A - E + 40 >= 0 /\ -A + E >= 0 /\ J - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 3 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 18 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 22 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 8 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 12 >= 0 /\ -A + B + 10 >= 0 /\ J - 2 >= 0 /\ -A + J + 18 >= 0 /\ -A + 20 >= 0 /\ A >= B ]
  f63(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f11(A, B, C, J, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G - 1 >= 0 /\ -F - G + 1 >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 2 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 2 >= 0 /\ -A + G + 20 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ J - F - 1 >= 0 /\ -A - F + 21 >= 0 /\ F - 1 >= 0 /\ -E + F + 19 >= 0 /\ D + F - 2 >= 0 /\ C + F - 21 >= 0 /\ -C + F + 19 >= 0 /\ B + F - 11 >= 0 /\ -B + F + 9 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 18 >= 0 /\ -A - E + 39 >= 0 /\ -A + E + 1 >= 0 /\ J - D - 1 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 3 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 18 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 22 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 8 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 12 >= 0 /\ -A + B + 10 >= 0 /\ J - 2 >= 0 /\ -A + J + 18 >= 0 /\ -A + 20 >= 0 /\ B >= A ]
  f48(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f54(A, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 19 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 19 >= 0 /\ -F >= 0 /\ -E - F + 20 >= 0 /\ D - F - 1 >= 0 /\ C - F - 20 >= 0 /\ -C - F + 20 >= 0 /\ B - F - 10 >= 0 /\ -B - F + 10 >= 0 /\ J - F - 3 >= 0 /\ -A - F + 19 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 39 >= 0 /\ -A + E - 1 >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 18 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 39 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C - 1 >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 29 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 9 >= 0 /\ J - 3 >= 0 /\ -A + J + 16 >= 0 /\ -A + 19 >= 0 /\ A >= J ]
  f48(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f54(A, B, C, D, E, 1, G, H, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 19 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 19 >= 0 /\ -F >= 0 /\ -E - F + 20 >= 0 /\ D - F - 1 >= 0 /\ C - F - 20 >= 0 /\ -C - F + 20 >= 0 /\ B - F - 10 >= 0 /\ -B - F + 10 >= 0 /\ J - F - 3 >= 0 /\ -A - F + 19 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 19 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 39 >= 0 /\ -A + E - 1 >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 18 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 39 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C - 1 >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 29 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 9 >= 0 /\ J - 3 >= 0 /\ -A + J + 16 >= 0 /\ -A + 19 >= 0 /\ J >= A + 1 ]
  f43(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f48(A - 1, B, C, D, E, F, G, H, I, J, K)) [ -G >= 0 /\ F - G >= 0 /\ -F - G >= 0 /\ -E - G + 20 >= 0 /\ D - G - 1 >= 0 /\ C - G - 20 >= 0 /\ -C - G + 20 >= 0 /\ B - G - 10 >= 0 /\ -B - G + 10 >= 0 /\ J - G - 3 >= 0 /\ -A - G + 20 >= 0 /\ G >= 0 /\ F + G >= 0 /\ -F + G >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ J + G - 3 >= 0 /\ -A + G + 20 >= 0 /\ -F >= 0 /\ -E - F + 20 >= 0 /\ D - F - 1 >= 0 /\ C - F - 20 >= 0 /\ -C - F + 20 >= 0 /\ B - F - 10 >= 0 /\ -B - F + 10 >= 0 /\ J - F - 3 >= 0 /\ -A - F + 20 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ J + F - 3 >= 0 /\ -A + F + 20 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ J - E + 17 >= 0 /\ -A - E + 40 >= 0 /\ -A + E >= 0 /\ J - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ J + D - 4 >= 0 /\ -A + D + 19 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ J - C + 17 >= 0 /\ -A - C + 40 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ J + C - 23 >= 0 /\ -A + C >= 0 /\ -B + 10 >= 0 /\ J - B + 7 >= 0 /\ -A - B + 30 >= 0 /\ B - 10 >= 0 /\ J + B - 13 >= 0 /\ -A + B + 10 >= 0 /\ J - 3 >= 0 /\ -A + J + 17 >= 0 /\ -A + 20 >= 0 ]
  f11(A, B, C, D, E, F, G, H, I, J, K) -> Com_1(f69(A, B, C, D, E, F, G, H, I, J, K)) [ G >= 0 /\ F + G >= 0 /\ -F + G + 1 >= 0 /\ -E + G + 20 >= 0 /\ D + G - 1 >= 0 /\ C + G - 20 >= 0 /\ -C + G + 20 >= 0 /\ B + G - 10 >= 0 /\ -B + G + 10 >= 0 /\ -F + 1 >= 0 /\ -E - F + 21 >= 0 /\ D - F >= 0 /\ C - F - 19 >= 0 /\ -C - F + 21 >= 0 /\ B - F - 9 >= 0 /\ -B - F + 11 >= 0 /\ F >= 0 /\ -E + F + 20 >= 0 /\ D + F - 1 >= 0 /\ C + F - 20 >= 0 /\ -C + F + 20 >= 0 /\ B + F - 10 >= 0 /\ -B + F + 10 >= 0 /\ -E + 20 >= 0 /\ D - E + 19 >= 0 /\ C - E >= 0 /\ -C - E + 40 >= 0 /\ B - E + 10 >= 0 /\ -B - E + 30 >= 0 /\ D - 1 >= 0 /\ C + D - 21 >= 0 /\ -C + D + 19 >= 0 /\ B + D - 11 >= 0 /\ -B + D + 9 >= 0 /\ -C + 20 >= 0 /\ B - C + 10 >= 0 /\ -B - C + 30 >= 0 /\ C - 20 >= 0 /\ B + C - 30 >= 0 /\ -B + C - 10 >= 0 /\ -B + 10 >= 0 /\ B - 10 >= 0 /\ G >= 1 ]
)