(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D) (RULES f0(A, B, C, D) -> Com_1(f4(0, B, C, D)) f4(A, B, C, D) -> Com_1(f8(A + 1, B, 0, D)) [ A >= 0 /\ B >= A + 1 ] f8(A, B, C, D) -> Com_1(f16(A, B, C, 0)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ B >= A + 1 ] f8(A, B, C, D) -> Com_1(f16(A, B, C, D)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ A >= B ] f8(A, B, C, D) -> Com_1(f8(A + 1, B, C + 1, E)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ B >= A + 1 /\ 0 >= E + 1 ] f8(A, B, C, D) -> Com_1(f8(A + 1, B, C + 1, E)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ B >= A + 1 /\ E >= 1 ] f16(A, B, C, D) -> Com_1(f4(A, B, C, D)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ 0 >= C ] f16(A, B, C, D) -> Com_1(f4(A - 1, B, C, D)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ C >= 1 ] f4(A, B, C, D) -> Com_1(f20(A, B, C, D)) [ A >= 0 /\ A >= B ] )