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