(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(H, 0, C, D, E, F, G)) f10(A, B, C, D, E, F, G) -> Com_1(f10(A, B + 1, C, D, E, F, G)) [ B >= 0 /\ C >= B + 1 ] f18(A, B, C, D, E, F, G) -> Com_1(f21(A, B, C, D, E, 0, G)) [ B - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ -C + D >= 0 /\ B - C >= 0 /\ B >= 0 /\ D >= E + 2 ] f21(A, B, C, D, E, F, G) -> Com_1(f21(A, B, C, D, E, F + 1, G)) [ F >= 0 /\ E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 2 >= 0 /\ B + F - 2 >= 0 /\ D - E - 2 >= 0 /\ C - E - 2 >= 0 /\ B - E - 2 >= 0 /\ E >= 0 /\ D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ D - 2 >= 0 /\ C + D - 4 >= 0 /\ -C + D >= 0 /\ B + D - 4 >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ B - 2 >= 0 /\ D >= E + F + 2 ] f21(A, B, C, D, E, F, G) -> Com_1(f21(A, B, C, D, E, F + 1, H)) [ F >= 0 /\ E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 2 >= 0 /\ B + F - 2 >= 0 /\ D - E - 2 >= 0 /\ C - E - 2 >= 0 /\ B - E - 2 >= 0 /\ E >= 0 /\ D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ D - 2 >= 0 /\ C + D - 4 >= 0 /\ -C + D >= 0 /\ B + D - 4 >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ B - 2 >= 0 /\ D >= E + F + 2 ] f32(A, B, C, D, E, F, G) -> Com_1(f32(A, B, C, D, E + 1, F, G)) [ B - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ -C + D >= 0 /\ B - C >= 0 /\ B >= 0 /\ D >= E + 2 ] f32(A, B, C, D, E, F, G) -> Com_1(f41(A, B, C, D, E, F, G)) [ B - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ -C + D >= 0 /\ B - C >= 0 /\ B >= 0 /\ E + 1 >= D ] f21(A, B, C, D, E, F, G) -> Com_1(f18(A, B, C, D, E + 1, F, G)) [ F >= 0 /\ E + F >= 0 /\ D + F - 2 >= 0 /\ C + F - 2 >= 0 /\ B + F - 2 >= 0 /\ D - E - 2 >= 0 /\ C - E - 2 >= 0 /\ B - E - 2 >= 0 /\ E >= 0 /\ D + E - 2 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ D - 2 >= 0 /\ C + D - 4 >= 0 /\ -C + D >= 0 /\ B + D - 4 >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ B - 2 >= 0 /\ F + E + 1 >= D ] f18(A, B, C, D, E, F, G) -> Com_1(f32(A, B, C, D, 0, F, G)) [ B - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ C - D >= 0 /\ B - D >= 0 /\ -C + D >= 0 /\ B - C >= 0 /\ B >= 0 /\ E + 1 >= D ] f10(A, B, C, D, E, F, G) -> Com_1(f18(A, B, C, C, 0, F, G)) [ B >= 0 /\ B >= C ] )