(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS start0))
(VAR A B C D)
(RULES
  start(A, B, C, D) -> Com_1(lbl51(E, B, 0, D)) [ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ A = B /\ C = D ]
  lbl51(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ C >= 0 /\ C >= A /\ 9 >= C ]
  lbl51(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ C >= 0 /\ A >= C + 3 /\ 9 >= C ]
  lbl51(A, B, C, D) -> Com_1(cut(A, B, C, D)) [ C >= 0 /\ A >= C + 1 /\ C + 2 >= A /\ 9 >= A /\ 9 >= C ]
  lbl51(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ C >= 0 /\ A >= 10 /\ A >= C + 1 /\ C + 2 >= A /\ 9 >= C ]
  cut(A, B, C, D) -> Com_1(lbl51(E, B, A, D)) [ -C + 8 >= 0 /\ A - C - 1 >= 0 /\ -A - C + 17 >= 0 /\ C >= 0 /\ A + C - 1 >= 0 /\ -A + C + 2 >= 0 /\ -A + 9 >= 0 /\ A - 1 >= 0 /\ C + 2 >= A /\ 9 >= A /\ A >= C + 1 ]
  start0(A, B, C, D) -> Com_1(start(B, B, D, D))
)