(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C)
(RULES
  f2(A, B, C) -> Com_1(f2(A + 1, B, C)) [ C - 1 >= 0 /\ A + C - 1 >= 0 /\ A >= 0 ]
  f3(A, B, C) -> Com_1(f3(A, B - 1, C)) [ -C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ -A >= 0 /\ A >= 0 /\ B >= 1 ]
  f5(A, B, C) -> Com_1(f5(A, B, 1)) [ -B >= 0 /\ A - B >= 0 /\ -A - B >= 0 /\ -A >= 0 /\ A >= 0 ]
  f0(A, B, C) -> Com_1(f2(0, B, C)) [ C >= 1 ]
  f0(A, B, C) -> Com_1(f3(0, B, C)) [ 0 >= C ]
  f3(A, B, C) -> Com_1(f5(0, B, C)) [ -C >= 0 /\ A - C >= 0 /\ -A - C >= 0 /\ -A >= 0 /\ A >= 0 /\ 0 >= B ]
)