(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(lbl42(A, B - 1, 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 /\ A >= 0 /\ C >= 0 /\ B = C /\ D = A /\ E = F /\ G = H ] start(A, B, C, D, E, F, G, H) -> Com_1(cut(A, B, C, D - 1, 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 /\ A >= 0 /\ B = C /\ D = A /\ E = F /\ G = H ] start(A, B, C, D, E, F, G, H) -> Com_1(lbl72(A, B + 1, C, D - 1, B, 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 /\ H >= C /\ A >= 0 /\ B = C /\ D = A /\ E = F /\ G = H ] lbl72(A, B, C, D, E, F, G, H) -> Com_1(cut(A, B, C, D, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ -E + H >= 0 /\ -B + H + 1 >= 0 /\ -E + G >= 0 /\ -B + G + 1 >= 0 /\ B - E - 1 >= 0 /\ -B + E + 1 >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ A + D + 1 >= 0 /\ A >= 0 /\ A >= D + 1 /\ H + 1 >= B /\ E + 1 = B /\ G = H ] lbl72(A, B, C, D, E, F, G, H) -> Com_1(lbl72(A, B + 1, C, D, B, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ -E + H >= 0 /\ -B + H + 1 >= 0 /\ -E + G >= 0 /\ -B + G + 1 >= 0 /\ B - E - 1 >= 0 /\ -B + E + 1 >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ A + D + 1 >= 0 /\ A >= 0 /\ H >= B /\ A >= D + 1 /\ H + 1 >= B /\ E + 1 = B /\ G = H ] lbl42(A, B, C, D, E, F, G, H) -> Com_1(lbl42(A, B - 1, C, D, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - D >= 0 /\ D >= 0 /\ B + D + 1 >= 0 /\ A + D >= 0 /\ B + 1 >= 0 /\ A + B + 1 >= 0 /\ A >= 0 /\ B >= 0 /\ A >= D /\ G = H ] lbl42(A, B, C, D, E, F, G, H) -> Com_1(cut(A, B, C, D - 1, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - D >= 0 /\ D >= 0 /\ B + D + 1 >= 0 /\ A + D >= 0 /\ B + 1 >= 0 /\ A + B + 1 >= 0 /\ A >= 0 /\ A >= D /\ G = H ] lbl42(A, B, C, D, E, F, G, H) -> Com_1(lbl72(A, B + 1, C, D - 1, B, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - D >= 0 /\ D >= 0 /\ B + D + 1 >= 0 /\ A + D >= 0 /\ B + 1 >= 0 /\ A + B + 1 >= 0 /\ A >= 0 /\ H >= B /\ A >= D /\ G = H ] cut(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 - D - 1 >= 0 /\ D + 1 >= 0 /\ A + D + 1 >= 0 /\ A >= 0 /\ D + 1 = 0 /\ G = H ] cut(A, B, C, D, E, F, G, H) -> Com_1(lbl42(A, B - 1, C, D, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ A + D + 1 >= 0 /\ A >= 0 /\ D >= 0 /\ B >= 0 /\ A >= D + 1 /\ G = H ] cut(A, B, C, D, E, F, G, H) -> Com_1(cut(A, B, C, D - 1, E, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ A + D + 1 >= 0 /\ A >= 0 /\ D >= 0 /\ A >= D + 1 /\ G = H ] cut(A, B, C, D, E, F, G, H) -> Com_1(lbl72(A, B + 1, C, D - 1, B, F, G, H)) [ G - H >= 0 /\ -G + H >= 0 /\ A - D - 1 >= 0 /\ D + 1 >= 0 /\ A + D + 1 >= 0 /\ A >= 0 /\ H >= B /\ D >= 0 /\ A >= D + 1 /\ G = H ] start0(A, B, C, D, E, F, G, H) -> Com_1(start(A, C, C, A, F, F, H, H)) )