(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f6(8, 0, 14, -1, E, F, G)) f6(A, B, C, D, E, F, G) -> Com_1(f12(A, B, C, D, I, F, G)) [ -A + 8 >= 0 /\ A - 8 >= 0 /\ C >= B /\ A >= H + 1 ] f6(A, B, C, D, E, F, G) -> Com_1(f12(A, B, C, D, I, F, G)) [ -A + 8 >= 0 /\ A - 8 >= 0 /\ C >= B ] f6(A, B, C, D, E, F, G) -> Com_1(f6(A, B, B - 1, I, H, F, G)) [ -A + 8 >= 0 /\ A - 8 >= 0 /\ C >= B ] f12(A, B, C, D, E, F, G) -> Com_1(f6(A, B, E - 1, D, E, F, G)) [ -B + C >= 0 /\ -A + 8 >= 0 /\ A - 8 >= 0 ] f12(A, B, C, D, E, F, G) -> Com_1(f6(A, E + 1, C, D, E, F, G)) [ -B + C >= 0 /\ -A + 8 >= 0 /\ A - 8 >= 0 ] f6(A, B, C, D, E, F, G) -> Com_1(f20(A, B, C, D, E, D, D)) [ -A + 8 >= 0 /\ A - 8 >= 0 /\ B >= C + 1 ] )