(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E)
(RULES
  f0(A, B, C, D, E) -> Com_1(f7(400, 0, C, D, E))
  f7(A, B, C, D, E) -> Com_1(f10(A, B, 0, D, E)) [ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ 4 >= B ]
  f10(A, B, C, D, E) -> Com_1(f13(A, B, C, 0, E)) [ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ 4 >= C ]
  f13(A, B, C, D, E) -> Com_1(f16(A, B, C, D, 0)) [ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 400 >= 0 /\ -A + D + 400 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ 4 >= D ]
  f16(A, B, C, D, E) -> Com_1(f16(A, B, C, D, E + 1)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 400 >= 0 /\ -A + E + 400 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 400 >= 0 /\ -A + D + 400 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ 4 >= E /\ A >= F + 1 ]
  f16(A, B, C, D, E) -> Com_1(f16(A, B, C, D, E + 1)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 400 >= 0 /\ -A + E + 400 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 400 >= 0 /\ -A + D + 400 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ 4 >= E ]
  f16(A, B, C, D, E) -> Com_1(f31(A, B, C, D, E)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 400 >= 0 /\ -A + E + 400 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 400 >= 0 /\ -A + D + 400 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ 4 >= E ]
  f16(A, B, C, D, E) -> Com_1(f13(A, B, C, D + 1, E)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 400 >= 0 /\ -A + E + 400 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 400 >= 0 /\ -A + D + 400 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ E >= 5 ]
  f13(A, B, C, D, E) -> Com_1(f10(A, B, C + 1, D, E)) [ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 400 >= 0 /\ -A + D + 400 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ D >= 5 ]
  f10(A, B, C, D, E) -> Com_1(f7(A, B + 1, C, D, E)) [ C >= 0 /\ B + C >= 0 /\ A + C - 400 >= 0 /\ -A + C + 400 >= 0 /\ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ C >= 5 ]
  f7(A, B, C, D, E) -> Com_1(f31(A, B, C, D, E)) [ B >= 0 /\ A + B - 400 >= 0 /\ -A + B + 400 >= 0 /\ -A + 400 >= 0 /\ A - 400 >= 0 /\ B >= 5 ]
)