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