(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 /\ A >= 30 /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(lbl171(A, B - 10, C, D + 2)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ C >= A /\ 29 >= A /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(lbl151(A, B + 7, C, D + 1)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= C + 1 /\ C >= 6 /\ 29 >= A /\ B = C /\ D = A ]
  start(A, B, C, D) -> Com_1(lbl151(A, B + 2, C, D + 1)) [ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= C + 1 /\ 5 >= C /\ 29 >= A /\ B = C /\ D = A ]
  lbl171(A, B, C, D) -> Com_1(stop(A, B, C, D)) [ B - D + 12 >= 0 /\ -A + D - 2 >= 0 /\ -A + B + 10 >= 0 /\ -A + 29 >= 0 /\ D >= 30 /\ 29 >= A /\ 5*D + B >= 5*A + C /\ 7*D + C >= B + 7*A + 24 /\ 7*B + 1674 >= 19*D + 35*A + 7*C /\ B + 12 >= D ]
  lbl171(A, B, C, D) -> Com_1(lbl171(A, B - 10, C, D + 2)) [ B - D + 12 >= 0 /\ -A + D - 2 >= 0 /\ -A + B + 10 >= 0 /\ -A + 29 >= 0 /\ B >= D /\ 29 >= D /\ 29 >= A /\ 5*D + B >= 5*A + C /\ 7*D + C >= B + 7*A + 24 /\ 7*B + 1674 >= 19*D + 35*A + 7*C /\ B + 12 >= D ]
  lbl171(A, B, C, D) -> Com_1(lbl151(A, B + 7, C, D + 1)) [ B - D + 12 >= 0 /\ -A + D - 2 >= 0 /\ -A + B + 10 >= 0 /\ -A + 29 >= 0 /\ D >= B + 1 /\ B >= 6 /\ 29 >= D /\ 29 >= A /\ 5*D + B >= 5*A + C /\ 7*D + C >= B + 7*A + 24 /\ 7*B + 1674 >= 19*D + 35*A + 7*C /\ B + 12 >= D ]
  lbl171(A, B, C, D) -> Com_1(lbl151(A, B + 2, C, D + 1)) [ B - D + 12 >= 0 /\ -A + D - 2 >= 0 /\ -A + B + 10 >= 0 /\ -A + 29 >= 0 /\ D >= B + 1 /\ 5 >= B /\ 29 >= D /\ 29 >= A /\ 5*D + B >= 5*A + C /\ 7*D + C >= B + 7*A + 24 /\ 7*B + 1674 >= 19*D + 35*A + 7*C /\ B + 12 >= D ]
  lbl151(A, B, C, D) -> Com_1(lbl171(A, B - 10, C, D + 2)) [ -B + D + 5 >= 0 /\ -A + D - 1 >= 0 /\ -A + 29 >= 0 /\ B >= D /\ 6*D >= 5*A + C + 7 /\ 5*D + B >= 5*A + C + 7 /\ D >= A + 1 /\ 29 >= A /\ B + 203 >= 2*D + 5*A + C /\ 2*B + 1561 >= 14*D + 35*A + 7*C /\ 140*D + 23*B >= 140*A + 28*C + 161 /\ 23*B + 5719 >= 56*D + 140*A + 28*C /\ D + 5 >= B /\ 7*D + C >= B + 7*A ]
  lbl151(A, B, C, D) -> Com_1(lbl151(A, B + 7, C, D + 1)) [ -B + D + 5 >= 0 /\ -A + D - 1 >= 0 /\ -A + 29 >= 0 /\ D >= B + 1 /\ B >= 6 /\ 6*D >= 5*A + C + 7 /\ 5*D + B >= 5*A + C + 7 /\ D >= A + 1 /\ 29 >= A /\ B + 203 >= 2*D + 5*A + C /\ 2*B + 1561 >= 14*D + 35*A + 7*C /\ 140*D + 23*B >= 140*A + 28*C + 161 /\ 23*B + 5719 >= 56*D + 140*A + 28*C /\ D + 5 >= B /\ 7*D + C >= B + 7*A ]
  lbl151(A, B, C, D) -> Com_1(lbl151(A, B + 2, C, D + 1)) [ -B + D + 5 >= 0 /\ -A + D - 1 >= 0 /\ -A + 29 >= 0 /\ D >= B + 1 /\ 5 >= B /\ 6*D >= 5*A + C + 7 /\ 5*D + B >= 5*A + C + 7 /\ D >= A + 1 /\ 29 >= A /\ B + 203 >= 2*D + 5*A + C /\ 2*B + 1561 >= 14*D + 35*A + 7*C /\ 140*D + 23*B >= 140*A + 28*C + 161 /\ 23*B + 5719 >= 56*D + 140*A + 28*C /\ D + 5 >= B /\ 7*D + C >= B + 7*A ]
  start0(A, B, C, D) -> Com_1(start(A, C, C, A))
)