(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C) (RULES f0(A, B, C) -> Com_1(f8(0, B, C)) f8(A, B, C) -> Com_1(f14(A, A, C)) [ A >= 0 /\ 0 >= A /\ 0 >= D ] f8(A, B, C) -> Com_1(f14(A, A, C)) [ A >= 0 /\ 0 >= A ] f23(A, B, C) -> Com_1(f28(A, B, D)) [ A >= 0 /\ 0 >= A /\ 0 >= E + 1 ] f23(A, B, C) -> Com_1(f28(A, B, D)) [ A >= 0 /\ 0 >= A ] f23(A, B, C) -> Com_1(f23(A + 1, B, C)) [ A >= 0 /\ 0 >= A ] f28(A, B, C) -> Com_1(f23(A + 1, B, C)) [ -A >= 0 /\ A >= 0 ] f28(A, B, C) -> Com_1(f23(A + 1, B, C)) [ -A >= 0 /\ A >= 0 /\ 0 >= D + 1 ] f23(A, B, C) -> Com_1(f38(A, B, C)) [ A >= 0 /\ A >= 1 ] f8(A, B, C) -> Com_1(f8(A + 1, A, C)) [ A >= 0 /\ 0 >= A ] f14(A, B, C) -> Com_1(f8(A + 1, B, C)) [ -B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -A >= 0 /\ A >= 0 ] f14(A, B, C) -> Com_1(f8(A + 1, B, C)) [ -B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ -A >= 0 /\ A >= 0 /\ 0 >= D + 1 ] f8(A, B, C) -> Com_1(f23(0, B, C)) [ A >= 0 /\ A >= 1 ] )