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