(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f)) (VAR A B C) (RULES f(A, B, C) -> Com_1(g(1, 1, C)) g(A, B, C) -> Com_1(g(A + B, A + B, C - 1)) [ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ C > 0 ] g(A, B, C) -> Com_1(h(A, B, C)) [ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ C <= 0 ] h(A, B, C) -> Com_1(h(A, B - 1, C)) [ -C >= 0 /\ A - C - 1 >= 0 /\ A - 1 >= 0 /\ B > 0 ] )