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