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