(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS start0))
(VAR A B C D E F)
(RULES
  start(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ 0 >= A /\ B = C /\ D = A /\ E = F ]
  start(A, B, C, D, E, F) -> Com_1(lbl6(A, B, C, D, E, F)) [ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 1 /\ A >= C /\ B = C /\ D = A /\ E = F ]
  start(A, B, C, D, E, F) -> Com_1(lbl121(A, B, C, D, B - D, F)) [ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ -B + C >= 0 /\ A >= 1 /\ C >= A + 1 /\ B = C /\ D = A /\ E = F ]
  lbl6(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ E - F >= 0 /\ -E + F >= 0 /\ A - D >= 0 /\ D - 1 >= 0 /\ -C + D >= 0 /\ -B + D >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ A - C >= 0 /\ -B + C >= 0 /\ A - B >= 0 /\ A - 1 >= 0 /\ A >= 1 /\ A >= C /\ E = F /\ D = A /\ B = C ]
  lbl111(A, B, C, D, E, F) -> Com_1(cut(A, B, C, D, E, F)) [ D - E - 2 >= 0 /\ C - E - 3 >= 0 /\ B - E - 3 >= 0 /\ A - E - 2 >= 0 /\ E >= 0 /\ D + E - 2 >= 0 /\ C + E - 3 >= 0 /\ B + E - 3 >= 0 /\ A + E - 2 >= 0 /\ C - D - 1 >= 0 /\ B - D - 1 >= 0 /\ A - D >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ B + D - 5 >= 0 /\ A + D - 4 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ C - 3 >= 0 /\ B + C - 6 >= 0 /\ -B + C >= 0 /\ A + C - 5 >= 0 /\ -A + C - 1 >= 0 /\ B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B - 1 >= 0 /\ A - 2 >= 0 /\ C >= A + 1 /\ A >= 2 /\ E = 0 /\ D = A /\ B = C ]
  lbl111(A, B, C, D, E, F) -> Com_1(lbl111(A, B, C, D, E - 1, F)) [ D - E - 2 >= 0 /\ C - E - 3 >= 0 /\ B - E - 3 >= 0 /\ A - E - 2 >= 0 /\ E >= 0 /\ D + E - 2 >= 0 /\ C + E - 3 >= 0 /\ B + E - 3 >= 0 /\ A + E - 2 >= 0 /\ C - D - 1 >= 0 /\ B - D - 1 >= 0 /\ A - D >= 0 /\ D - 2 >= 0 /\ C + D - 5 >= 0 /\ B + D - 5 >= 0 /\ A + D - 4 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ C - 3 >= 0 /\ B + C - 6 >= 0 /\ -B + C >= 0 /\ A + C - 5 >= 0 /\ -A + C - 1 >= 0 /\ B - 3 >= 0 /\ A + B - 5 >= 0 /\ -A + B - 1 >= 0 /\ A - 2 >= 0 /\ E >= 1 /\ A >= E + 1 /\ C >= E + A + 1 /\ A >= E + 2 /\ D = A /\ B = C ]
  lbl121(A, B, C, D, E, F) -> Com_1(cut(A, B, C, D, E, F)) [ C - E - 1 >= 0 /\ B - E - 1 >= 0 /\ C - D - 1 >= 0 /\ B - D - 1 >= 0 /\ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 3 >= 0 /\ B + D - 3 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ C >= A + 1 /\ A >= 1 /\ C >= A /\ E = 0 /\ D = A /\ B = C ]
  lbl121(A, B, C, D, E, F) -> Com_1(lbl111(A, B, C, D, E - 1, F)) [ C - E - 1 >= 0 /\ B - E - 1 >= 0 /\ C - D - 1 >= 0 /\ B - D - 1 >= 0 /\ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 3 >= 0 /\ B + D - 3 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ E >= 1 /\ A >= E + 1 /\ C >= A + 1 /\ A >= 1 /\ E >= 0 /\ C >= E + A /\ D = A /\ B = C ]
  lbl121(A, B, C, D, E, F) -> Com_1(lbl121(A, B, C, D, E - D, F)) [ C - E - 1 >= 0 /\ B - E - 1 >= 0 /\ C - D - 1 >= 0 /\ B - D - 1 >= 0 /\ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 3 >= 0 /\ B + D - 3 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ E >= 1 /\ E >= A /\ C >= A + 1 /\ A >= 1 /\ E >= 0 /\ C >= E + A /\ D = A /\ B = C ]
  cut(A, B, C, D, E, F) -> Com_1(stop(A, B, C, D, E, F)) [ -E >= 0 /\ D - E - 1 >= 0 /\ C - E - 2 >= 0 /\ B - E - 2 >= 0 /\ A - E - 1 >= 0 /\ E >= 0 /\ D + E - 1 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ A + E - 1 >= 0 /\ C - D - 1 >= 0 /\ B - D - 1 >= 0 /\ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 3 >= 0 /\ B + D - 3 >= 0 /\ A + D - 2 >= 0 /\ -A + D >= 0 /\ B - C >= 0 /\ C - 2 >= 0 /\ B + C - 4 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ A - 1 >= 0 /\ A >= 1 /\ C >= A + 1 /\ E = 0 /\ D = A /\ B = C ]
  start0(A, B, C, D, E, F) -> Com_1(start(A, C, C, A, F, F))
)