YES
* Step 1: UnsatRules YES
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)      [0 >= 1 + A && B = C && D = A]                                   (?,1)
          1.  start(A,B,C,D)  -> stop(A,B,C,D)      [0 >= 1 + C && B = C && D = A]                                   (?,1)
          2.  start(A,B,C,D)  -> stop(A,B,C,D)      [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (?,1)
          3.  start(A,B,C,D)  -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A]                         (?,1)
          4.  start(A,B,C,D)  -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A]                         (?,1)
          5.  lbl81(A,B,C,D)  -> stop(A,B,C,D)      [C >= 3 + A && A >= 0 && 2 + D = C && B = C]                     (?,1)
          6.  lbl81(A,B,C,D)  -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C]      (?,1)
          7.  lbl81(A,B,C,D)  -> lbl91(A,1 + B,C,D) [D >= 3 + C && D >= 1 + A && A >= 0 && C >= 2 + D && B = C]      (?,1)
          8.  lbl91(A,B,C,D)  -> stop(A,B,C,D)      [A >= 3 + C && C >= 0 && 2 + B = A && D = A]                     (?,1)
          9.  lbl91(A,B,C,D)  -> lbl81(A,B,C,1 + D) [B >= 3 + A && A >= 2 + B && B >= 1 + C && C >= 0 && D = A]      (?,1)
          10. lbl91(A,B,C,D)  -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A]      (?,1)
          11. start0(A,B,C,D) -> start(A,C,C,A)     True                                                             (1,1)
        Signature:
          {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{},2->{},3->{5,6,7},4->{8,9,10},5->{},6->{5,6,7},7->{8,9,10},8->{},9->{5,6,7},10->{8,9,10}
          ,11->{0,1,2,3,4}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        Following transitions have unsatisfiable constraints and are removed:  [7,9]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)      [0 >= 1 + A && B = C && D = A]                                   (?,1)
          1.  start(A,B,C,D)  -> stop(A,B,C,D)      [0 >= 1 + C && B = C && D = A]                                   (?,1)
          2.  start(A,B,C,D)  -> stop(A,B,C,D)      [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A] (?,1)
          3.  start(A,B,C,D)  -> lbl81(A,B,C,1 + D) [A >= 0 && C >= 3 + A && B = C && D = A]                         (?,1)
          4.  start(A,B,C,D)  -> lbl91(A,1 + B,C,D) [A >= 3 + C && C >= 0 && B = C && D = A]                         (?,1)
          5.  lbl81(A,B,C,D)  -> stop(A,B,C,D)      [C >= 3 + A && A >= 0 && 2 + D = C && B = C]                     (?,1)
          6.  lbl81(A,B,C,D)  -> lbl81(A,B,C,1 + D) [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C]      (?,1)
          8.  lbl91(A,B,C,D)  -> stop(A,B,C,D)      [A >= 3 + C && C >= 0 && 2 + B = A && D = A]                     (?,1)
          10. lbl91(A,B,C,D)  -> lbl91(A,1 + B,C,D) [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A]      (?,1)
          11. start0(A,B,C,D) -> start(A,C,C,A)     True                                                             (1,1)
        Signature:
          {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{},2->{},3->{5,6},4->{8,10},5->{},6->{5,6},8->{},10->{8,10},11->{0,1,2,3,4}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          start(A,B,C,D)  -> stop(A,B,C,D)       [0 >= 1 + A && B = C && D = A]
          start(A,B,C,D)  -> stop(A,B,C,D)       [0 >= 1 + C && B = C && D = A]
          start(A,B,C,D)  -> stop(A,B,C,D)       [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A]
          start(A,B,C,D)  -> lbl81(A,B,C,1 + D)  [A >= 0 && C >= 3 + A && B = C && D = A]
          start(A,B,C,D)  -> lbl91(A,1 + B,C,D)  [A >= 3 + C && C >= 0 && B = C && D = A]
          lbl81(A,B,C,D)  -> stop(A,B,C,D)       [C >= 3 + A && A >= 0 && 2 + D = C && B = C]
          lbl81(A,B,C,D)  -> lbl81(A,B,C,1 + D)  [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C]
          lbl91(A,B,C,D)  -> stop(A,B,C,D)       [A >= 3 + C && C >= 0 && 2 + B = A && D = A]
          lbl91(A,B,C,D)  -> lbl91(A,1 + B,C,D)  [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A]
          start0(A,B,C,D) -> start(A,C,C,A)      True
        Signature:
          {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{},1->{},2->{},3->{5,6},4->{8,10},5->{},6->{5,6},8->{},10->{8,10},11->{0,1,2,3,4}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,8,10,11]
          |
          +- p:[10] c: [10]
          |
          `- p:[6] c: [6]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          start(A,B,C,D)  -> stop(A,B,C,D)       [0 >= 1 + A && B = C && D = A]
          start(A,B,C,D)  -> stop(A,B,C,D)       [0 >= 1 + C && B = C && D = A]
          start(A,B,C,D)  -> stop(A,B,C,D)       [A >= 0 && 2 + A >= C && C >= 0 && 2 + C >= A && B = C && D = A]
          start(A,B,C,D)  -> lbl81(A,B,C,1 + D)  [A >= 0 && C >= 3 + A && B = C && D = A]
          start(A,B,C,D)  -> lbl91(A,1 + B,C,D)  [A >= 3 + C && C >= 0 && B = C && D = A]
          lbl81(A,B,C,D)  -> stop(A,B,C,D)       [C >= 3 + A && A >= 0 && 2 + D = C && B = C]
          lbl81(A,B,C,D)  -> lbl81(A,B,C,1 + D)  [C >= 3 + D && D >= 1 + A && A >= 0 && C >= 2 + D && B = C]
          lbl91(A,B,C,D)  -> stop(A,B,C,D)       [A >= 3 + C && C >= 0 && 2 + B = A && D = A]
          lbl91(A,B,C,D)  -> lbl91(A,1 + B,C,D)  [A >= 3 + B && A >= 2 + B && B >= 1 + C && C >= 0 && D = A]
          start0(A,B,C,D) -> start(A,C,C,A)      True
        Signature:
          {(lbl81,4);(lbl91,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{},1->{},2->{},3->{5,6},4->{8,10},5->{},6->{5,6},8->{},10->{8,10},11->{0,1,2,3,4}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,8,10,11]
          |
          +- p:[10] c: [10]
          |
          `- p:[6] c: [6])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES