(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS start0))
(VAR A B C D)
(RULES
  start(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ 0 >= A + 1 /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ 0 >= C + 1 /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ A + 2 >= C /\ C >= 0 /\ C + 2 >= A /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(lbl81(A, B, C, D + 1)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 0 /\ C >= A + 3 /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(lbl91(A, B + 1, C, D)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= C + 3 /\ C >= 0 /\ B = C /\ D = A ]
  lbl81(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ C - D - 2 >= 0 /\ B - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ B + D - 4 >= 0 /\ A + D - 1 >= 0 /\ -A + D - 1 >= 0 /\ B - C >= 0 /\ C - 3 >= 0 /\ B + C - 6 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ -A + C - 3 >= 0 /\ B - 3 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 3 >= 0 /\ A >= 0 /\ C >= A + 3 /\ D + 2 = C /\ B = C ]
  lbl81(A, B, C, D) -> Com_1(lbl81(A, B, C, D + 1)) [ C - D - 2 >= 0 /\ B - D - 2 >= 0 /\ D - 1 >= 0 /\ C + D - 4 >= 0 /\ B + D - 4 >= 0 /\ A + D - 1 >= 0 /\ -A + D - 1 >= 0 /\ B - C >= 0 /\ C - 3 >= 0 /\ B + C - 6 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ -A + C - 3 >= 0 /\ B - 3 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 3 >= 0 /\ A >= 0 /\ C >= D + 3 /\ D >= A + 1 /\ C >= D + 2 /\ B = C ]
  lbl91(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ A - D >= 0 /\ D - 3 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 3 >= 0 /\ B + D - 4 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 6 >= 0 /\ -A + D >= 0 /\ B - C - 1 >= 0 /\ A - C - 3 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 3 >= 0 /\ A - B - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ A >= C + 3 /\ B + 2 = A /\ D = A ]
  lbl91(A, B, C, D) -> Com_1(lbl91(A, B + 1, C, D)) [ A - D >= 0 /\ D - 3 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 3 >= 0 /\ B + D - 4 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 6 >= 0 /\ -A + D >= 0 /\ B - C - 1 >= 0 /\ A - C - 3 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 3 >= 0 /\ A - B - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 4 >= 0 /\ A - 3 >= 0 /\ A >= B + 3 /\ A >= B + 2 /\ B >= C + 1 /\ D = A ]
  start0(A, B, C, D) -> Com_1(start(A, C, C, A))
)