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