(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C) (RULES f4(A, B, C) -> Com_1(f5(A, B, 1)) [ -C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ -A + C >= 0 /\ -A >= 0 /\ 0 >= A /\ 0 >= B ] f0(A, B, C) -> Com_1(f2(A, B, 1)) [ A >= 1 ] f4(A, B, C) -> Com_1(f4(A, B - 1, C)) [ -C >= 0 /\ -A - C >= 0 /\ C >= 0 /\ -A + C >= 0 /\ -A >= 0 /\ B >= 1 ] f0(A, B, C) -> Com_1(f4(A, B, 0)) [ 0 >= A ] )