(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f70(5, 20, 0, 0, E, F, G)) f70(A, B, C, D, E, F, G) -> Com_1(f70(A, B, C, C + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ C = D ] f70(A, B, C, D, E, F, G) -> Com_1(f78(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f70(A, B, C, D, E, F, G) -> Com_1(f70(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ D >= C + 1 ] f78(A, B, C, D, E, F, G) -> Com_1(f92(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f78(A, B, C, D, E, F, G) -> Com_1(f81(A, B, C, D, 0, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] f92(A, B, C, D, E, F, G) -> Com_1(f102(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= B ] f92(A, B, C, D, E, F, G) -> Com_1(f92(A, B, C, D + 1, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f92(A, B, C, D, E, F, G) -> Com_1(f98(A, B, C, D, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f81(A, B, C, D, E, F, G) -> Com_1(f78(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 20 >= 0 /\ -B + E + 20 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ E >= B ] f81(A, B, C, D, E, F, G) -> Com_1(f81(A, B, C, D, E + 1, H, I)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 20 >= 0 /\ -B + E + 20 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= E + 1 ] f102(A, B, C, D, E, F, G) -> Com_1(f98(A, B, C, D, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f102(A, B, C, D, E, F, G) -> Com_1(f102(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 20 >= 0 /\ -B + D + 20 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 20 >= 0 /\ -B - C + 20 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 20 >= 0 /\ -B + C + 20 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 20 >= 0 /\ A - B + 15 >= 0 /\ -A - B + 25 >= 0 /\ B - 20 >= 0 /\ A + B - 25 >= 0 /\ -A + B - 15 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] )