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