(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f49(5, 13, 0, 0, E, F, G)) f49(A, B, C, D, E, F, G) -> Com_1(f49(A, B, C, C + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ C = D ] f49(A, B, C, D, E, F, G) -> Com_1(f57(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f49(A, B, C, D, E, F, G) -> Com_1(f49(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ D >= C + 1 ] f57(A, B, C, D, E, F, G) -> Com_1(f71(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f57(A, B, C, D, E, F, G) -> Com_1(f60(A, B, C, D, 0, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] f71(A, B, C, D, E, F, G) -> Com_1(f81(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= B ] f71(A, B, C, D, E, F, G) -> Com_1(f71(A, B, C, D + 1, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f71(A, B, C, D, E, F, G) -> Com_1(f77(A, B, C, D, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f60(A, B, C, D, E, F, G) -> Com_1(f57(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 13 >= 0 /\ -B + E + 13 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ E >= B ] f60(A, B, C, D, E, F, G) -> Com_1(f60(A, B, C, D, E + 1, H, I)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 13 >= 0 /\ -B + E + 13 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= E + 1 ] f81(A, B, C, D, E, F, G) -> Com_1(f77(A, B, C, D, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f81(A, B, C, D, E, F, G) -> Com_1(f81(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 13 >= 0 /\ -B + D + 13 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 13 >= 0 /\ -B - C + 13 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 13 >= 0 /\ -B + C + 13 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 13 >= 0 /\ A - B + 8 >= 0 /\ -A - B + 18 >= 0 /\ B - 13 >= 0 /\ A + B - 18 >= 0 /\ -A + B - 8 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] )