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