YES(?,O(n^1))
* Step 1: TrivialSCCs WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (?,1)
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (?,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (?,1)
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (?,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (1,1)
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (1,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (?,1)
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (1,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        We apply a polynomial interpretation of shape linear:
               p(a) = x4     
               p(b) = 1 + x4 
           p(cont1) = x4     
           p(start) = x4     
          p(start0) = x1     
           p(stop1) = x4     
           p(stop2) = x3 + x4
           p(stop3) = 1 + x4 
        
        Following rules are strictly oriented:
        [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D] ==>               
                                        b(A,B,C,D)   = 1 + D         
                                                     > D             
                                                     = start(A,B,C,D)
        
        
        Following rules are weakly oriented:
                             [A >= 0 && B >= 0 && C >= 0 && D = 0] ==>                    
                                                    start(A,B,C,D)   = D                  
                                                                    >= D                  
                                                                     = stop1(A,B,C,D)     
        
        [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] ==>                    
                                                    start(A,B,C,D)   = D                  
                                                                    >= D                  
                                                                     = cont1(A,B,C,D)     
        
                             [D >= 1 && B >= 0 && A >= D && C = 0] ==>                    
                                                    cont1(A,B,C,D)   = D                  
                                                                    >= D                  
                                                                     = stop2(A,B,1,-1 + D)
        
                  [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D] ==>                    
                                                    cont1(A,B,C,D)   = D                  
                                                                    >= D                  
                                                                     = a(A,B,-1 + C,D)    
        
                            [A >= D && B >= 0 && C >= 0 && D >= 1] ==>                    
                                                        a(A,B,C,D)   = D                  
                                                                    >= D                  
                                                                     = b(A,B,E,-1 + D)    
        
                    [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D] ==>                    
                                                        b(A,B,C,D)   = 1 + D              
                                                                    >= 1 + D              
                                                                     = stop3(A,B,C,D)     
        
                                                [A >= 0 && B >= 0] ==>                    
                                                   start0(A,B,C,D)   = A                  
                                                                    >= A                  
                                                                     = start(A,B,B,A)     
        
        
* Step 3: KnowledgePropagation WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (1,1)
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (?,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (1,1)
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (?,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (?,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (A,1)
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (1,1)
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        
    + Applied Processor:
        KnowledgePropagation
    + Details:
        We propagate bounds from predecessors.
* Step 4: PolyRank WORST_CASE(?,O(n^1))
    + Considered Problem:
        Rules:
          0. start(A,B,C,D)  -> stop1(A,B,C,D)      [A >= 0 && B >= 0 && C >= 0 && D = 0]                      (1,1)    
          1. start(A,B,C,D)  -> cont1(A,B,C,D)      [D >= 1 && A >= 0 && B >= 0 && C >= 0 && D >= 0 && A >= D] (1 + A,1)
          2. cont1(A,B,C,D)  -> stop2(A,B,1,-1 + D) [D >= 1 && B >= 0 && A >= D && C = 0]                      (1,1)    
          3. cont1(A,B,C,D)  -> a(A,B,-1 + C,D)     [C >= 1 && D >= 1 && C >= 0 && B >= 0 && A >= D]           (1 + A,1)
          4. a(A,B,C,D)      -> b(A,B,E,-1 + D)     [A >= D && B >= 0 && C >= 0 && D >= 1]                     (1 + A,1)
          5. b(A,B,C,D)      -> start(A,B,C,D)      [C >= 0 && D >= 0 && B >= 0 && A >= 1 + D]                 (A,1)    
          6. b(A,B,C,D)      -> stop3(A,B,C,D)      [0 >= 1 + C && D >= 0 && B >= 0 && A >= 1 + D]             (1,1)    
          7. start0(A,B,C,D) -> start(A,B,B,A)      [A >= 0 && B >= 0]                                         (1,1)    
        Signature:
          {(a,4);(b,4);(cont1,4);(start,4);(start0,4);(stop1,4);(stop2,4);(stop3,4)}
        Flow Graph:
          [0->{},1->{2,3},2->{},3->{4},4->{5,6},5->{0,1},6->{},7->{0,1}]
        
    + Applied Processor:
        PolyRank {useFarkas = True, withSizebounds = [], shape = Linear}
    + Details:
        The problem is already solved.

YES(?,O(n^1))