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