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