(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f10(1, 1, H, 0, 2, 1, G)) [ H >= 0 ] f10(A, B, C, D, E, F, G) -> Com_1(f21(A, B - 1, C, D, E, F, 0)) [ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ F >= 1 /\ E >= F /\ B >= 1 /\ 0 >= C ] f10(A, B, C, D, E, F, G) -> Com_1(f21(A + 1, A + 1, H, D, E, F, I)) [ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ I >= 0 /\ 1 >= I /\ H >= 0 /\ F >= 1 /\ E >= F /\ 0 >= B /\ 0 >= C ] f10(A, B, C, D, E, F, G) -> Com_1(f21(A, B, C - 1, D, E, F, H)) [ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ H >= 0 /\ 1 >= H /\ F >= 1 /\ C >= 1 /\ E >= F ] f21(A, B, C, D, E, F, G) -> Com_1(f10(A, B, C, D, E, F - 1, G)) [ -G + 1 >= 0 /\ F - G >= 0 /\ -F - G + 3 >= 0 /\ E - G - 1 >= 0 /\ -E - G + 3 >= 0 /\ D - G + 1 >= 0 /\ -D - G + 1 >= 0 /\ C - G + 1 >= 0 /\ A - G >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 2 >= 0 /\ E + G - 2 >= 0 /\ -E + G + 2 >= 0 /\ D + G >= 0 /\ -D + G >= 0 /\ C + G >= 0 /\ A + G - 1 >= 0 /\ -F + 2 >= 0 /\ E - F >= 0 /\ -E - F + 4 >= 0 /\ D - F + 2 >= 0 /\ -D - F + 2 >= 0 /\ C - F + 2 >= 0 /\ A - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 3 >= 0 /\ -E + F + 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 1 >= 0 /\ C + F - 1 >= 0 /\ A + F - 2 >= 0 /\ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ 0 >= G ] f21(A, B, C, D, E, F, G) -> Com_1(f10(A, B, C, D, E, F + 1, G)) [ -G + 1 >= 0 /\ F - G >= 0 /\ -F - G + 3 >= 0 /\ E - G - 1 >= 0 /\ -E - G + 3 >= 0 /\ D - G + 1 >= 0 /\ -D - G + 1 >= 0 /\ C - G + 1 >= 0 /\ A - G >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ -F + G + 2 >= 0 /\ E + G - 2 >= 0 /\ -E + G + 2 >= 0 /\ D + G >= 0 /\ -D + G >= 0 /\ C + G >= 0 /\ A + G - 1 >= 0 /\ -F + 2 >= 0 /\ E - F >= 0 /\ -E - F + 4 >= 0 /\ D - F + 2 >= 0 /\ -D - F + 2 >= 0 /\ C - F + 2 >= 0 /\ A - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 3 >= 0 /\ -E + F + 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F - 1 >= 0 /\ C + F - 1 >= 0 /\ A + F - 2 >= 0 /\ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ G >= 1 ] f10(A, B, C, D, E, F, G) -> Com_1(f31(A, B, C, D, E, F, G)) [ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ 0 >= F /\ E >= F ] f10(A, B, C, D, E, F, G) -> Com_1(f31(A, B, C, D, E, F, G)) [ -E + 2 >= 0 /\ D - E + 2 >= 0 /\ -D - E + 2 >= 0 /\ C - E + 2 >= 0 /\ A - E + 1 >= 0 /\ E - 2 >= 0 /\ D + E - 2 >= 0 /\ -D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ A + E - 3 >= 0 /\ -D >= 0 /\ C - D >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ F >= E + 1 ] )