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