(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I J K L) (RULES f63(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f71(A, B, C, 0, E, F, G, H, I, J, K, 1)) [ F - 11 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 10 >= 0 /\ -C + F - 10 >= 0 /\ B + F - 23 >= 0 /\ -B + F + 1 >= 0 /\ -A + F - 10 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ D = 0 ] f63(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f71(A, B, C, D, E, F, G, H, I, J, K, 0)) [ F - 11 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 10 >= 0 /\ -C + F - 10 >= 0 /\ B + F - 23 >= 0 /\ -B + F + 1 >= 0 /\ -A + F - 10 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ D >= 1 ] f63(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f71(A, B, C, D, E, F, G, H, I, J, K, 0)) [ F - 11 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 10 >= 0 /\ -C + F - 10 >= 0 /\ B + F - 23 >= 0 /\ -B + F + 1 >= 0 /\ -A + F - 10 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ 0 >= D + 1 ] f62(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f71(0, B, C, D, E, F, G, H, I, J, K, 1)) [ F - 11 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 10 >= 0 /\ -C + F - 10 >= 0 /\ B + F - 23 >= 0 /\ -B + F + 1 >= 0 /\ -A + F - 10 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A = 0 ] f62(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f63(A, B, C, D, E, F, G, H, I, J, K, L)) [ F - 11 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 10 >= 0 /\ -C + F - 10 >= 0 /\ B + F - 23 >= 0 /\ -B + F + 1 >= 0 /\ -A + F - 10 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A >= 1 ] f62(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f63(A, B, C, D, E, F, G, H, I, J, K, L)) [ F - 11 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 10 >= 0 /\ -C + F - 10 >= 0 /\ B + F - 23 >= 0 /\ -B + F + 1 >= 0 /\ -A + F - 10 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ 0 >= A + 1 ] f48(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f48(A, B, C, 0, E, F + 1, G, H, I, M, 0, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ B >= F + 2 /\ D = 0 ] f48(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f71(A, B, 0, D, E, F, G, H, I, J, K, 1)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ F + 1 >= B /\ C = 0 ] f48(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f62(A, B, C, D, E, F, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ C >= 1 /\ F + 1 >= B ] f48(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f62(A, B, C, D, E, F, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ 0 >= C + 1 /\ F + 1 >= B ] f52(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f48(A, B, C, 0, E, F + 1, G, H, I, J, 0, L)) [ -F + 10 >= 0 /\ D - F + 19 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D + 9 >= 0 /\ -C + D + 10 >= 0 /\ B + D - 3 >= 0 /\ -B + D + 21 >= 0 /\ -A + D + 10 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 ] f52(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f48(A, B, C, 0, E, F + 1, G, H, I, 0, 0, L)) [ -F + 10 >= 0 /\ D - F + 19 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D + 9 >= 0 /\ -C + D + 10 >= 0 /\ B + D - 3 >= 0 /\ -B + D + 21 >= 0 /\ -A + D + 10 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ J = 0 ] f52(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f48(A, B, C, 1, E, F + 1, G, H, I, J, 1, L)) [ -F + 10 >= 0 /\ D - F + 19 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D + 9 >= 0 /\ -C + D + 10 >= 0 /\ B + D - 3 >= 0 /\ -B + D + 21 >= 0 /\ -A + D + 10 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ J >= 1 ] f52(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f48(A, B, C, 1, E, F + 1, G, H, I, J, 1, L)) [ -F + 10 >= 0 /\ D - F + 19 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D + 9 >= 0 /\ -C + D + 10 >= 0 /\ B + D - 3 >= 0 /\ -B + D + 21 >= 0 /\ -A + D + 10 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ 0 >= J + 1 ] f48(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f52(A, B, C, D, E, F, G, H, I, M, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ D >= 1 /\ B >= F + 2 ] f32(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f48(A, B, C, D, E, 0, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ F + 1 >= B ] f35(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f32(A, B, C, D, E, F + 1, G, H, I, J, K, L)) [ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ H >= B ] f38(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f35(0, B, C, D, E, F, G, H + 1, 0, J, K, L)) [ -H + 11 >= 0 /\ F - H + 11 >= 0 /\ -F - H + 21 >= 0 /\ D - H + 10 >= 0 /\ -D - H + 12 >= 0 /\ -C - H + 12 >= 0 /\ B - H - 1 >= 0 /\ -B - H + 23 >= 0 /\ -A - H + 12 >= 0 /\ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ -F + 10 >= 0 /\ D - F + 9 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 ] f38(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f35(1, B, C, D, E, F, G, H + 1, 1, J, K, L)) [ -H + 11 >= 0 /\ F - H + 11 >= 0 /\ -F - H + 21 >= 0 /\ D - H + 10 >= 0 /\ -D - H + 12 >= 0 /\ -C - H + 12 >= 0 /\ B - H - 1 >= 0 /\ -B - H + 23 >= 0 /\ -A - H + 12 >= 0 /\ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ -F + 10 >= 0 /\ D - F + 9 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 ] f38(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f35(1, B, C, D, E, F, G, H + 1, 1, J, K, L)) [ -H + 11 >= 0 /\ F - H + 11 >= 0 /\ -F - H + 21 >= 0 /\ D - H + 10 >= 0 /\ -D - H + 12 >= 0 /\ -C - H + 12 >= 0 /\ B - H - 1 >= 0 /\ -B - H + 23 >= 0 /\ -A - H + 12 >= 0 /\ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ -F + 10 >= 0 /\ D - F + 9 >= 0 /\ -D - F + 11 >= 0 /\ -C - F + 11 >= 0 /\ B - F - 2 >= 0 /\ -B - F + 22 >= 0 /\ -A - F + 11 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ M >= N + 1 ] f35(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f35(0, B, C, D, E, F, G, H + 1, 0, J, K, L)) [ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ B >= H + 1 /\ A = 0 ] f35(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K, L)) [ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A >= 1 /\ B >= H + 1 ] f35(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f38(A, B, C, D, E, F, G, H, I, J, K, L)) [ H - 1 >= 0 /\ F + H - 1 >= 0 /\ -F + H - 1 >= 0 /\ D + H - 2 >= 0 /\ -D + H >= 0 /\ -C + H >= 0 /\ B + H - 13 >= 0 /\ -B + H + 11 >= 0 /\ -A + H >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ 0 >= A + 1 /\ B >= H + 1 ] f32(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f35(A, B, C, D, E, F, G, F + 1, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ B >= F + 2 ] f19(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f19(A, B, 0, D, E, F + 1, 0, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ B >= F + 1 /\ C = 0 ] f19(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f32(A, B, C, D, E, 0, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ F >= B ] f22(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f19(A, B, 0, D, E, F + 1, 0, H, I, J, K, L)) [ -F + 11 >= 0 /\ D - F + 10 >= 0 /\ -D - F + 12 >= 0 /\ C - F + 21 >= 0 /\ -C - F + 12 >= 0 /\ B - F - 1 >= 0 /\ -B - F + 23 >= 0 /\ A - F + 10 >= 0 /\ -A - F + 12 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ C - D + 11 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ C + D + 9 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ C + 10 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 22 >= 0 /\ A + C + 9 >= 0 /\ -A + C + 11 >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ 0 >= M + 1 ] f22(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f19(A, B, 0, D, E, F + 1, 0, H, I, J, K, L)) [ -F + 11 >= 0 /\ D - F + 10 >= 0 /\ -D - F + 12 >= 0 /\ C - F + 21 >= 0 /\ -C - F + 12 >= 0 /\ B - F - 1 >= 0 /\ -B - F + 23 >= 0 /\ A - F + 10 >= 0 /\ -A - F + 12 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ C - D + 11 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ C + D + 9 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ C + 10 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 22 >= 0 /\ A + C + 9 >= 0 /\ -A + C + 11 >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ M >= 0 ] f22(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f19(A, B, 1, D, E, F + 1, 1, H, I, J, K, L)) [ -F + 11 >= 0 /\ D - F + 10 >= 0 /\ -D - F + 12 >= 0 /\ C - F + 21 >= 0 /\ -C - F + 12 >= 0 /\ B - F - 1 >= 0 /\ -B - F + 23 >= 0 /\ A - F + 10 >= 0 /\ -A - F + 12 >= 0 /\ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ C - D + 11 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ C + D + 9 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ C + 10 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 22 >= 0 /\ A + C + 9 >= 0 /\ -A + C + 11 >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ M >= 0 /\ B >= N + 1 ] f19(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f22(A, B, C, D, E, F, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ C >= 1 /\ B >= F + 1 ] f13(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f19(A, B, C, D, E, 0, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ C - D >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ C - 1 >= 0 /\ B + C - 13 >= 0 /\ -B + C + 11 >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ F >= B ] f13(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f13(A, B, C, D, E, F + 1, G, H, I, J, K, L)) [ F >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ C + F - 1 >= 0 /\ -C + F + 1 >= 0 /\ B + F - 12 >= 0 /\ -B + F + 12 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 1 >= 0 /\ -D + 1 >= 0 /\ C - D >= 0 /\ -C - D + 2 >= 0 /\ B - D - 11 >= 0 /\ -B - D + 13 >= 0 /\ A - D >= 0 /\ -A - D + 2 >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 11 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ -C + 1 >= 0 /\ B - C - 11 >= 0 /\ -B - C + 13 >= 0 /\ A - C >= 0 /\ -A - C + 2 >= 0 /\ C - 1 >= 0 /\ B + C - 13 >= 0 /\ -B + C + 11 >= 0 /\ A + C - 2 >= 0 /\ -A + C >= 0 /\ -B + 12 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 13 >= 0 /\ B - 12 >= 0 /\ A + B - 13 >= 0 /\ -A + B - 11 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 /\ B >= F + 1 ] f0(A, B, C, D, E, F, G, H, I, J, K, L) -> Com_1(f13(1, 12, 1, 1, M, 0, G, H, I, J, K, L)) )