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