(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E F G)
(RULES
  f0(A, B, C, D, E, F, G) -> Com_1(f14(2*I + 1, H, 0, D, H, 2*I + 1, I)) [ H >= 1 /\ 2*I >= 0 ]
  f14(A, B, C, D, E, F, G) -> Com_1(f14(A - 1, B, C, H, E, F, G)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ C + G >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 1 >= 0 /\ C >= 0 /\ 0 >= H /\ A >= 1 /\ A >= B + 1 ]
  f14(A, B, C, D, E, F, G) -> Com_1(f14(A - 1, B - 1, C + 1, H, E, F, G)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ C + G >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 1 >= 0 /\ C >= 0 /\ A >= 1 /\ H >= 1 ]
  f14(A, B, C, D, E, F, G) -> Com_1(f24(A, B, C, D, E, F, G)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ C + G >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ C + F - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 1 >= 0 /\ C >= 0 /\ 0 >= A ]
  f24(A, B, C, D, E, F, G) -> Com_1(f24(A, B, C, D, E, F, G)) [ G >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ C + G >= 0 /\ -A + G >= 0 /\ F - 1 >= 0 /\ E + F - 2 >= 0 /\ C + F - 1 >= 0 /\ -A + F - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 1 >= 0 /\ -A + E - 1 >= 0 /\ C >= 0 /\ -A + C >= 0 /\ -A >= 0 ]
)