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