(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D) (RULES f0(A, B, C, D) -> Com_1(f6(E, 0, C, D)) f6(A, B, C, D) -> Com_1(f10(A - 1, B + 1, C, D)) [ -B >= 0 /\ A >= 1 ] f10(A, B, C, D) -> Com_1(f14(A, B - 1, A - 1, D)) [ A >= 0 /\ B >= 1 ] f14(A, B, C, D) -> Com_1(f14(A, B, C - 1, 0)) [ A - C - 1 >= 0 /\ C + 1 >= 0 /\ B + C + 1 >= 0 /\ A + C + 1 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= 1 ] f14(A, B, C, D) -> Com_1(f14(A - 1, B + 1, C - 1, E)) [ A - C - 1 >= 0 /\ C + 1 >= 0 /\ B + C + 1 >= 0 /\ A + C + 1 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= 1 /\ 0 >= E + 1 ] f14(A, B, C, D) -> Com_1(f14(A - 1, B + 1, C - 1, E)) [ A - C - 1 >= 0 /\ C + 1 >= 0 /\ B + C + 1 >= 0 /\ A + C + 1 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= 1 /\ E >= 1 ] f14(A, B, C, D) -> Com_1(f10(A, B, C, D)) [ A - C - 1 >= 0 /\ C + 1 >= 0 /\ B + C + 1 >= 0 /\ A + C + 1 >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ 0 >= C ] f10(A, B, C, D) -> Com_1(f6(A, B, C, D)) [ A >= 0 /\ 0 >= B ] f6(A, B, C, D) -> Com_1(f25(A, B, C, D)) [ -B >= 0 /\ 0 >= A ] )