(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f25(5, 5, 0, 0, E, F, G)) f25(A, B, C, D, E, F, G) -> Com_1(f25(A, B, C, C + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ C = D ] f25(A, B, C, D, E, F, G) -> Com_1(f33(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f25(A, B, C, D, E, F, G) -> Com_1(f25(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ D >= C + 1 ] f33(A, B, C, D, E, F, G) -> Com_1(f47(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f33(A, B, C, D, E, F, G) -> Com_1(f36(A, B, C, D, 0, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] f47(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 - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= B ] f47(A, B, C, D, E, F, G) -> Com_1(f47(A, B, C, D + 1, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f47(A, B, C, D, E, F, G) -> Com_1(f53(A, B, C, D, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f36(A, B, C, D, E, F, G) -> Com_1(f33(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 5 >= 0 /\ -B + E + 5 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ E >= B ] f36(A, B, C, D, E, F, G) -> Com_1(f36(A, B, C, D, E + 1, H, I)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 5 >= 0 /\ -B + E + 5 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= E + 1 ] f57(A, B, C, D, E, F, G) -> Com_1(f53(A, B, C, D, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f57(A, B, C, D, E, F, G) -> Com_1(f57(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 5 >= 0 /\ -B + D + 5 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 5 >= 0 /\ -B - C + 5 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 5 >= 0 /\ -B + C + 5 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 5 >= 0 /\ A - B >= 0 /\ -A - B + 10 >= 0 /\ B - 5 >= 0 /\ A + B - 10 >= 0 /\ -A + B >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] )