(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D) (RULES f6(A, B, C, D) -> Com_1(f16(A, B, C, D)) [ A + 1 >= B ] f6(A, B, C, D) -> Com_1(f6(E, B, C, E)) [ B >= A + 2 /\ C >= E^2 ] f6(A, B, C, D) -> Com_1(f6(A, E, C, E)) [ B >= A + 2 /\ E^2 >= C + 1 ] f0(A, B, C, D) -> Com_1(f6(1, C, C, D)) )