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