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