(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D E F G H) (RULES start(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 101 /\ B = C /\ D = E /\ F = A /\ G = H ] start(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ E >= C + 1 /\ B = C /\ D = E /\ F = A /\ G = H ] start(A, B, C, D, E, F, G, H) -> Com_1(lbl72(A, B - 1, C, F + 1, E, D, F, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - F >= 0 /\ -A + F >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ C >= E /\ 100 >= A /\ B = C /\ D = E /\ F = A /\ G = H ] lbl72(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ -G + 100 >= 0 /\ D - G - 1 >= 0 /\ -D - G + 201 >= 0 /\ -A - G + 200 >= 0 /\ -D + G + 1 >= 0 /\ C - E >= 0 /\ -D + 101 >= 0 /\ -A - D + 201 >= 0 /\ -B + C - 1 >= 0 /\ -A + 100 >= 0 /\ F >= 101 /\ 100 >= A /\ F + B + 101 >= A + E + C /\ B + 1 >= F /\ C >= B + 1 /\ C >= E /\ G + F + B + 1 = A + E + C /\ D + F + B = A + E + C ] lbl72(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ -G + 100 >= 0 /\ D - G - 1 >= 0 /\ -D - G + 201 >= 0 /\ -A - G + 200 >= 0 /\ -D + G + 1 >= 0 /\ C - E >= 0 /\ -D + 101 >= 0 /\ -A - D + 201 >= 0 /\ -B + C - 1 >= 0 /\ -A + 100 >= 0 /\ A + E + C >= F + 2*B + 1 /\ 100 >= A /\ F + B + 101 >= A + E + C /\ B + 1 >= F /\ C >= B + 1 /\ C >= E /\ G + F + B + 1 = A + E + C /\ D + F + B = A + E + C ] lbl72(A, B, C, D, E, F, G, H) -> Com_1(lbl72(A, B - 1, C, F + 1, E, D, F, H)) [ -G + 100 >= 0 /\ D - G - 1 >= 0 /\ -D - G + 201 >= 0 /\ -A - G + 200 >= 0 /\ -D + G + 1 >= 0 /\ C - E >= 0 /\ -D + 101 >= 0 /\ -A - D + 201 >= 0 /\ -B + C - 1 >= 0 /\ -A + 100 >= 0 /\ 2*B + F >= A + E + C /\ 100 >= F /\ 100 >= A /\ F + B + 101 >= A + E + C /\ B + 1 >= F /\ C >= B + 1 /\ C >= E /\ G + F + B + 1 = A + E + C /\ D + F + B = A + E + C ] start0(A, B, C, D, E, F, G, H) -> Com_1(start(A, C, C, E, E, A, H, H)) )