(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C) (RULES f6(A, B, C) -> Com_1(f9(A, D, C)) [ -C >= 0 /\ C >= 0 /\ 0 >= A + 1 ] f6(A, B, C) -> Com_1(f9(A, D, C)) [ -C >= 0 /\ C >= 0 /\ A >= 1 ] f6(A, B, C) -> Com_1(f17(0, B, C)) [ -C >= 0 /\ C >= 0 /\ A = 0 ] f17(A, B, C) -> Com_1(f24(A, B, C)) [ -C + 1 >= 0 /\ C >= 0 /\ 0 >= C ] f17(A, B, C) -> Com_1(f24(A, B, 0)) [ -C + 1 >= 0 /\ C >= 0 /\ C = 1 ] f9(A, B, C) -> Com_1(f17(A, 0, 1)) [ -C >= 0 /\ C >= 0 /\ B = 0 ] f9(A, B, C) -> Com_1(f6(D, B, C)) [ -C >= 0 /\ C >= 0 /\ 0 >= B + 1 ] f9(A, B, C) -> Com_1(f6(D, B, C)) [ -C >= 0 /\ C >= 0 /\ B >= 1 ] f0(A, B, C) -> Com_1(f6(D, B, 0)) )