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