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