(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D) (RULES f0(A, B, C, D) -> Com_1(f19(A, 999, C, 1)) f19(A, B, C, D) -> Com_1(f19(A, B - 1, C, D)) [ -D + 1 >= 0 /\ -B - D + 1000 >= 0 /\ D - 1 >= 0 /\ -B + D + 998 >= 0 /\ -B + 999 >= 0 /\ B >= 0 ] f19(A, B, C, D) -> Com_1(f28(A, B, 999, D)) [ -D + 1 >= 0 /\ -B - D + 1000 >= 0 /\ D - 1 >= 0 /\ -B + D + 998 >= 0 /\ -B + 999 >= 0 /\ 0 >= B + 1 ] f28(A, B, C, D) -> Com_1(f28(A, B, C - 1, D)) [ -D + 1 >= 0 /\ -C - D + 1000 >= 0 /\ -B - D >= 0 /\ D - 1 >= 0 /\ -C + D + 998 >= 0 /\ -B + D - 2 >= 0 /\ -C + 999 >= 0 /\ -B - C + 998 >= 0 /\ -B - 1 >= 0 /\ C >= 0 ] f28(A, B, C, D) -> Com_1(f36(A, B, C, D)) [ -D + 1 >= 0 /\ -C - D + 1000 >= 0 /\ -B - D >= 0 /\ D - 1 >= 0 /\ -C + D + 998 >= 0 /\ -B + D - 2 >= 0 /\ -C + 999 >= 0 /\ -B - C + 998 >= 0 /\ -B - 1 >= 0 /\ 0 >= C + 1 ] )