(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C) (RULES f0(A, B, C) -> Com_1(f1(A, B, 2)) [ A >= 0 /\ 3 >= A /\ 3 >= B /\ B >= 0 ] f1(A, B, C) -> Com_1(f1(A, B + 1, C)) [ -C + 2 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 5 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 5 >= 0 /\ C - 2 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 2 >= 0 /\ -A + C + 1 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ C + A >= 2*B + 1 ] f1(A, B, C) -> Com_1(f1(A, B - 1, C)) [ -C + 2 >= 0 /\ B - C + 2 >= 0 /\ -B - C + 5 >= 0 /\ A - C + 2 >= 0 /\ -A - C + 5 >= 0 /\ C - 2 >= 0 /\ B + C - 2 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 2 >= 0 /\ -A + C + 1 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ 2*B >= C + A + 2 ] )