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