(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f2))
(VAR A B C D E F G H)
(RULES
  f2(A, B, C, D, E, F, G, H) -> Com_1(f1(A, B, C, D, E, F, J, J))
  f1(A, B, C, D, E, F, G, H) -> Com_1(f300(A, B, J, D, E, I, G, H)) [ B >= A ]
  f1(A, B, C, D, E, F, G, H) -> Com_1(f1(A, B, J, 0, E, F, G, H)) [ A >= B + 1 ]
  f1(A, B, C, D, E, F, G, H) -> Com_1(f1(A, B, J, I, K, F, G, H)) [ 0 >= I + 1 /\ A >= B + 1 ]
  f1(A, B, C, D, E, F, G, H) -> Com_1(f1(A, B, J, I, K, F, G, H)) [ I >= 1 /\ A >= B + 1 ]
)