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