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