(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 /\ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ 0 >= A + 1 /\ B = C /\ D = A /\ E = F /\ G = H ] start(A, B, C, D, E, F, G, H) -> Com_1(lbl82(A, B, C, D, 2*D, F, 2*D - 1, H)) [ G - H >= 0 /\ -G + H >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ B = C /\ D = A /\ E = F /\ G = H ] start(A, B, C, D, E, F, G, H) -> Com_1(lbl121(A, 2*D, C, D, 2*D - 1, F, 2*D - 1, H)) [ G - H >= 0 /\ -G + H >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ B = C /\ D = A /\ E = F /\ G = H ] lbl82(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ G + 1 >= 0 /\ E + G + 1 >= 0 /\ D + G + 1 >= 0 /\ -D + G + 1 >= 0 /\ A + G + 1 >= 0 /\ -A + G + 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ A - D >= 0 /\ D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ A >= 0 /\ E >= A /\ 2*A >= E /\ D = A /\ G + 1 = A ] lbl82(A, B, C, D, E, F, G, H) -> Com_1(lbl82(A, B, C, D, E, F, G - 1, H)) [ G + 1 >= 0 /\ E + G + 1 >= 0 /\ D + G + 1 >= 0 /\ -D + G + 1 >= 0 /\ A + G + 1 >= 0 /\ -A + G + 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ A - D >= 0 /\ D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ A >= 0 /\ G >= A /\ E >= G + 1 /\ 2*A >= E /\ G + 1 >= A /\ D = A ] lbl82(A, B, C, D, E, F, G, H) -> Com_1(lbl121(A, G, C, D, E - 1, F, E - 1, H)) [ G + 1 >= 0 /\ E + G + 1 >= 0 /\ D + G + 1 >= 0 /\ -D + G + 1 >= 0 /\ A + G + 1 >= 0 /\ -A + G + 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ A + E >= 0 /\ -A + E >= 0 /\ A - D >= 0 /\ D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ A >= 0 /\ G >= A /\ E >= G + 1 /\ 2*A >= E /\ G + 1 >= A /\ D = A ] lbl121(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ G + 1 >= 0 /\ E + G + 2 >= 0 /\ D + G + 1 >= 0 /\ -D + G + 1 >= 0 /\ B + G + 1 >= 0 /\ A + G + 1 >= 0 /\ -A + G + 1 >= 0 /\ E + 1 >= 0 /\ D + E + 1 >= 0 /\ -D + E + 1 >= 0 /\ B + E + 1 >= 0 /\ A + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ B - D >= 0 /\ A - D >= 0 /\ D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ A >= E + 1 /\ 2*A >= E + 1 /\ B >= A /\ E + 1 >= B /\ G = E /\ D = A ] lbl121(A, B, C, D, E, F, G, H) -> Com_1(lbl82(A, B, C, D, E, F, G - 1, H)) [ G + 1 >= 0 /\ E + G + 2 >= 0 /\ D + G + 1 >= 0 /\ -D + G + 1 >= 0 /\ B + G + 1 >= 0 /\ A + G + 1 >= 0 /\ -A + G + 1 >= 0 /\ E + 1 >= 0 /\ D + E + 1 >= 0 /\ -D + E + 1 >= 0 /\ B + E + 1 >= 0 /\ A + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ B - D >= 0 /\ A - D >= 0 /\ D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ E >= A /\ 2*A >= E + 1 /\ B >= A /\ E + 1 >= B /\ G = E /\ D = A ] lbl121(A, B, C, D, E, F, G, H) -> Com_1(lbl121(A, G, C, D, E - 1, F, E - 1, H)) [ G + 1 >= 0 /\ E + G + 2 >= 0 /\ D + G + 1 >= 0 /\ -D + G + 1 >= 0 /\ B + G + 1 >= 0 /\ A + G + 1 >= 0 /\ -A + G + 1 >= 0 /\ E + 1 >= 0 /\ D + E + 1 >= 0 /\ -D + E + 1 >= 0 /\ B + E + 1 >= 0 /\ A + E + 1 >= 0 /\ -A + E + 1 >= 0 /\ B - D >= 0 /\ A - D >= 0 /\ D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ -A + D >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 /\ E >= A /\ 2*A >= E + 1 /\ B >= A /\ E + 1 >= B /\ G = E /\ D = A ] start0(A, B, C, D, E, F, G, H) -> Com_1(start(A, C, C, A, F, F, H, H)) )