(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 /\ A >= 5 /\ B = C /\ D = E /\ F = G /\ H = A ] start(A, B, C, D, E, F, G, H) -> Com_1(lbl92(A, B, C, H, E, 0, G, H + 1)) [ A - H >= 0 /\ -A + H >= 0 /\ F - G >= 0 /\ -F + G >= 0 /\ D - E >= 0 /\ -D + E >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ 2 >= A /\ B = C /\ D = E /\ F = G /\ H = A ] start(A, B, C, D, E, F, G, H) -> Com_1(lbl82(A, 0, C, D, E, 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 >= 3 /\ 4 >= A /\ B = C /\ D = E /\ F = G /\ H = A ] lbl92(A, B, C, D, E, F, G, H) -> Com_1(stop(A, B, C, D, E, F, G, H)) [ -H + 5 >= 0 /\ F - H + 3 >= 0 /\ -F - H + 15 >= 0 /\ D - H + 1 >= 0 /\ -D - H + 9 >= 0 /\ -A - H + 9 >= 0 /\ -D + H - 1 >= 0 /\ -A + H - 1 >= 0 /\ -F + 10 >= 0 /\ -D - F + 14 >= 0 /\ -A - F + 14 >= 0 /\ F >= 0 /\ -D + F + 2 >= 0 /\ -A + F + 2 >= 0 /\ -D + 4 >= 0 /\ -A - D + 8 >= 0 /\ -A + D >= 0 /\ -A + 4 >= 0 /\ D >= 4 /\ D >= A /\ F + 10 >= 5*D /\ H = D + 1 ] lbl92(A, B, C, D, E, F, G, H) -> Com_1(lbl92(A, B, C, H, E, 0, G, H + 1)) [ -H + 5 >= 0 /\ F - H + 3 >= 0 /\ -F - H + 15 >= 0 /\ D - H + 1 >= 0 /\ -D - H + 9 >= 0 /\ -A - H + 9 >= 0 /\ -D + H - 1 >= 0 /\ -A + H - 1 >= 0 /\ -F + 10 >= 0 /\ -D - F + 14 >= 0 /\ -A - F + 14 >= 0 /\ F >= 0 /\ -D + F + 2 >= 0 /\ -A + F + 2 >= 0 /\ -D + 4 >= 0 /\ -A - D + 8 >= 0 /\ -A + D >= 0 /\ -A + 4 >= 0 /\ 1 >= D /\ D >= A /\ F + 10 >= 5*D /\ H = D + 1 ] lbl92(A, B, C, D, E, F, G, H) -> Com_1(lbl82(A, 0, C, D, E, 1, G, H)) [ -H + 5 >= 0 /\ F - H + 3 >= 0 /\ -F - H + 15 >= 0 /\ D - H + 1 >= 0 /\ -D - H + 9 >= 0 /\ -A - H + 9 >= 0 /\ -D + H - 1 >= 0 /\ -A + H - 1 >= 0 /\ -F + 10 >= 0 /\ -D - F + 14 >= 0 /\ -A - F + 14 >= 0 /\ F >= 0 /\ -D + F + 2 >= 0 /\ -A + F + 2 >= 0 /\ -D + 4 >= 0 /\ -A - D + 8 >= 0 /\ -A + D >= 0 /\ -A + 4 >= 0 /\ D >= 2 /\ 3 >= D /\ D >= A /\ F + 10 >= 5*D /\ H = D + 1 ] lbl82(A, B, C, D, E, F, G, H) -> Com_1(lbl92(A, B, C, H, E, F, G, H + 1)) [ -H + 4 >= 0 /\ F - H + 3 >= 0 /\ B - H + 4 >= 0 /\ -A - H + 8 >= 0 /\ H - 3 >= 0 /\ F + H - 4 >= 0 /\ B + H - 3 >= 0 /\ -A + H >= 0 /\ B - F + 1 >= 0 /\ F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F - 1 >= 0 /\ -A + F + 3 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ H >= A /\ H >= 3 /\ 4 >= H /\ F = 10 /\ B = 9 ] lbl82(A, B, C, D, E, F, G, H) -> Com_1(lbl82(A, F, C, D, E, F + 1, G, H)) [ -H + 4 >= 0 /\ F - H + 3 >= 0 /\ B - H + 4 >= 0 /\ -A - H + 8 >= 0 /\ H - 3 >= 0 /\ F + H - 4 >= 0 /\ B + H - 3 >= 0 /\ -A + H >= 0 /\ B - F + 1 >= 0 /\ F - 1 >= 0 /\ B + F - 1 >= 0 /\ -B + F - 1 >= 0 /\ -A + F + 3 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ H >= 3 /\ 8 >= B /\ 9 >= B /\ H >= A /\ 4 >= H /\ F = B + 1 ] start0(A, B, C, D, E, F, G, H) -> Com_1(start(A, C, C, E, E, G, G, A)) )