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