(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C) (RULES f0(A, B, C) -> Com_1(f8(0, 10, 0)) f8(A, B, C) -> Com_1(f8(A + 2, B, C + 1)) [ A - C >= 0 /\ C >= 0 /\ B + C - 10 >= 0 /\ -B + C + 10 >= 0 /\ A + C >= 0 /\ -B + 10 >= 0 /\ A - B + 10 >= 0 /\ B - 10 >= 0 /\ A + B - 10 >= 0 /\ A >= 0 /\ B >= C + 1 ] f8(A, B, C) -> Com_1(f6(A, B, C)) [ A - C >= 0 /\ C >= 0 /\ B + C - 10 >= 0 /\ -B + C + 10 >= 0 /\ A + C >= 0 /\ -B + 10 >= 0 /\ A - B + 10 >= 0 /\ B - 10 >= 0 /\ A + B - 10 >= 0 /\ A >= 0 /\ 2*B >= A + 1 /\ C >= B ] f8(A, B, C) -> Com_1(f6(A, B, C)) [ A - C >= 0 /\ C >= 0 /\ B + C - 10 >= 0 /\ -B + C + 10 >= 0 /\ A + C >= 0 /\ -B + 10 >= 0 /\ A - B + 10 >= 0 /\ B - 10 >= 0 /\ A + B - 10 >= 0 /\ A >= 0 /\ A >= 2*B /\ C >= B ] )