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