(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f58(5, 16, 0, 0, E, F, G)) f58(A, B, C, D, E, F, G) -> Com_1(f58(A, B, C, C + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ C = D ] f58(A, B, C, D, E, F, G) -> Com_1(f66(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f58(A, B, C, D, E, F, G) -> Com_1(f58(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ D >= C + 1 ] f66(A, B, C, D, E, F, G) -> Com_1(f80(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f66(A, B, C, D, E, F, G) -> Com_1(f69(A, B, C, D, 0, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] f80(A, B, C, D, E, F, G) -> Com_1(f90(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= B ] f80(A, B, C, D, E, F, G) -> Com_1(f80(A, B, C, D + 1, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f80(A, B, C, D, E, F, G) -> Com_1(f86(A, B, C, D, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f69(A, B, C, D, E, F, G) -> Com_1(f66(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 16 >= 0 /\ -B + E + 16 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ E >= B ] f69(A, B, C, D, E, F, G) -> Com_1(f69(A, B, C, D, E + 1, H, I)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 16 >= 0 /\ -B + E + 16 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= E + 1 ] f90(A, B, C, D, E, F, G) -> Com_1(f86(A, B, C, D, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f90(A, B, C, D, E, F, G) -> Com_1(f90(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 16 >= 0 /\ -B + D + 16 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 16 >= 0 /\ -B - C + 16 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 16 >= 0 /\ -B + C + 16 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 16 >= 0 /\ A - B + 11 >= 0 /\ -A - B + 21 >= 0 /\ B - 16 >= 0 /\ A + B - 21 >= 0 /\ -A + B - 11 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] )