(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E F G H I)
(RULES
  f0(A, B, C, D, E, F, G, H, I) -> Com_1(f7(30, 30, 1, 0, 2, F, G, H, I))
  f7(A, B, C, D, E, F, G, H, I) -> Com_1(f7(A, B, C + D, C, E + 1, C, G, H, I)) [ E - 2 >= 0 /\ D + E - 2 >= 0 /\ C + E - 3 >= 0 /\ B + E - 32 >= 0 /\ -B + E + 28 >= 0 /\ A + E - 32 >= 0 /\ -A + E + 28 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 30 >= 0 /\ -B + D + 30 >= 0 /\ A + D - 30 >= 0 /\ -A + D + 30 >= 0 /\ C - 1 >= 0 /\ B + C - 31 >= 0 /\ -B + C + 29 >= 0 /\ A + C - 31 >= 0 /\ -A + C + 29 >= 0 /\ -B + 30 >= 0 /\ A - B >= 0 /\ -A - B + 60 >= 0 /\ B - 30 >= 0 /\ A + B - 60 >= 0 /\ -A + B >= 0 /\ -A + 30 >= 0 /\ A - 30 >= 0 /\ B >= E ]
  f7(A, B, C, D, E, F, G, H, I) -> Com_1(f19(A, B, C, D, E, F, C, C, C)) [ E - 2 >= 0 /\ D + E - 2 >= 0 /\ C + E - 3 >= 0 /\ B + E - 32 >= 0 /\ -B + E + 28 >= 0 /\ A + E - 32 >= 0 /\ -A + E + 28 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 30 >= 0 /\ -B + D + 30 >= 0 /\ A + D - 30 >= 0 /\ -A + D + 30 >= 0 /\ C - 1 >= 0 /\ B + C - 31 >= 0 /\ -B + C + 29 >= 0 /\ A + C - 31 >= 0 /\ -A + C + 29 >= 0 /\ -B + 30 >= 0 /\ A - B >= 0 /\ -A - B + 60 >= 0 /\ B - 30 >= 0 /\ A + B - 60 >= 0 /\ -A + B >= 0 /\ -A + 30 >= 0 /\ A - 30 >= 0 /\ E >= B + 1 ]
)