(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f30)) (VAR A B C D E) (RULES f4(A, B, C, D, E) -> Com_1(f5(A, 1, C, D, E)) [ -C + 2 >= 0 /\ A - C >= 0 /\ C - 2 >= 0 /\ A + C - 4 >= 0 /\ A - 2 >= 0 /\ A >= 2 ] f30(A, B, C, D, E) -> Com_1(f4(2, B, 2, F, E)) f5(A, B, C, D, E) -> Com_1(f4(A + 1, B, C, F, E)) [ -C + 2 >= 0 /\ B - C + 1 >= 0 /\ -B - C + 3 >= 0 /\ A - C >= 0 /\ C - 2 >= 0 /\ B + C - 3 >= 0 /\ -B + C - 1 >= 0 /\ A + C - 4 >= 0 /\ -B + 1 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 3 >= 0 /\ A - 2 >= 0 /\ F >= 1 ] )