YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)             [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A]           (?,1)
          1.  start(A,B,C,D)  -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (?,1)
          2.  start(A,B,C,D)  -> lbl151(A,7 + B,C,1 + D)   [A + -1*D >= 0                                                                                            (?,1)
                                                            && -1*A + D >= 0                                                                                              
                                                            && B + -1*C >= 0                                                                                              
                                                            && -1*B + C >= 0                                                                                              
                                                            && A >= 1 + C                                                                                                 
                                                            && C >= 6                                                                                                     
                                                            && 29 >= A                                                                                                    
                                                            && B = C                                                                                                      
                                                            && D = A]                                                                                                     
          3.  start(A,B,C,D)  -> lbl151(A,2 + B,C,1 + D)   [A + -1*D >= 0                                                                                            (?,1)
                                                            && -1*A + D >= 0                                                                                              
                                                            && B + -1*C >= 0                                                                                              
                                                            && -1*B + C >= 0                                                                                              
                                                            && A >= 1 + C                                                                                                 
                                                            && 5 >= C                                                                                                     
                                                            && 29 >= A                                                                                                    
                                                            && B = C                                                                                                      
                                                            && D = A]                                                                                                     
          4.  lbl171(A,B,C,D) -> stop(A,B,C,D)             [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 30                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          5.  lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && B >= D                                                                                                     
                                                            && 29 >= D                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          6.  lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)   [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && B >= 6                                                                                                     
                                                            && 29 >= D                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          7.  lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)   [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && 5 >= B                                                                                                     
                                                            && 29 >= D                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          8.  lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0                                                                                        (?,1)
                                                            && -1 + -1*A + D >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && B >= D                                                                                                     
                                                            && 6*D >= 7 + 5*A + C                                                                                         
                                                            && B + 5*D >= 7 + 5*A + C                                                                                     
                                                            && D >= 1 + A                                                                                                 
                                                            && 29 >= A                                                                                                    
                                                            && 203 + B >= 5*A + C + 2*D                                                                                   
                                                            && 1561 + 2*B >= 35*A + 7*C + 14*D                                                                            
                                                            && 23*B + 140*D >= 161 + 140*A + 28*C                                                                         
                                                            && 5719 + 23*B >= 140*A + 28*C + 56*D                                                                         
                                                            && 5 + D >= B                                                                                                 
                                                            && C + 7*D >= 7*A + B]                                                                                        
          9.  lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)   [5 + -1*B + D >= 0                                                                                        (?,1)
                                                            && -1 + -1*A + D >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && B >= 6                                                                                                     
                                                            && 6*D >= 7 + 5*A + C                                                                                         
                                                            && B + 5*D >= 7 + 5*A + C                                                                                     
                                                            && D >= 1 + A                                                                                                 
                                                            && 29 >= A                                                                                                    
                                                            && 203 + B >= 5*A + C + 2*D                                                                                   
                                                            && 1561 + 2*B >= 35*A + 7*C + 14*D                                                                            
                                                            && 23*B + 140*D >= 161 + 140*A + 28*C                                                                         
                                                            && 5719 + 23*B >= 140*A + 28*C + 56*D                                                                         
                                                            && 5 + D >= B                                                                                                 
                                                            && C + 7*D >= 7*A + B]                                                                                        
          10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)   [5 + -1*B + D >= 0                                                                                        (?,1)
                                                            && -1 + -1*A + D >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && 5 >= B                                                                                                     
                                                            && 6*D >= 7 + 5*A + C                                                                                         
                                                            && B + 5*D >= 7 + 5*A + C                                                                                     
                                                            && D >= 1 + A                                                                                                 
                                                            && 29 >= A                                                                                                    
                                                            && 203 + B >= 5*A + C + 2*D                                                                                   
                                                            && 1561 + 2*B >= 35*A + 7*C + 14*D                                                                            
                                                            && 23*B + 140*D >= 161 + 140*A + 28*C                                                                         
                                                            && 5719 + 23*B >= 140*A + 28*C + 56*D                                                                         
                                                            && 5 + D >= B                                                                                                 
                                                            && C + 7*D >= 7*A + B]                                                                                        
          11. start0(A,B,C,D) -> start(A,C,C,A)            True                                                                                                      (1,1)
        Signature:
          {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{4,5,6,7},2->{8,9,10},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8
          ,9,10},10->{8,9,10},11->{0,1,2,3}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(2,10),(6,10),(8,5),(9,10)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  start(A,B,C,D)  -> stop(A,B,C,D)             [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A]           (?,1)
          1.  start(A,B,C,D)  -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (?,1)
          2.  start(A,B,C,D)  -> lbl151(A,7 + B,C,1 + D)   [A + -1*D >= 0                                                                                            (?,1)
                                                            && -1*A + D >= 0                                                                                              
                                                            && B + -1*C >= 0                                                                                              
                                                            && -1*B + C >= 0                                                                                              
                                                            && A >= 1 + C                                                                                                 
                                                            && C >= 6                                                                                                     
                                                            && 29 >= A                                                                                                    
                                                            && B = C                                                                                                      
                                                            && D = A]                                                                                                     
          3.  start(A,B,C,D)  -> lbl151(A,2 + B,C,1 + D)   [A + -1*D >= 0                                                                                            (?,1)
                                                            && -1*A + D >= 0                                                                                              
                                                            && B + -1*C >= 0                                                                                              
                                                            && -1*B + C >= 0                                                                                              
                                                            && A >= 1 + C                                                                                                 
                                                            && 5 >= C                                                                                                     
                                                            && 29 >= A                                                                                                    
                                                            && B = C                                                                                                      
                                                            && D = A]                                                                                                     
          4.  lbl171(A,B,C,D) -> stop(A,B,C,D)             [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 30                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          5.  lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && B >= D                                                                                                     
                                                            && 29 >= D                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          6.  lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)   [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && B >= 6                                                                                                     
                                                            && 29 >= D                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          7.  lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)   [12 + B + -1*D >= 0                                                                                       (?,1)
                                                            && -2 + -1*A + D >= 0                                                                                         
                                                            && 10 + -1*A + B >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && 5 >= B                                                                                                     
                                                            && 29 >= D                                                                                                    
                                                            && 29 >= A                                                                                                    
                                                            && B + 5*D >= 5*A + C                                                                                         
                                                            && C + 7*D >= 24 + 7*A + B                                                                                    
                                                            && 1674 + 7*B >= 35*A + 7*C + 19*D                                                                            
                                                            && 12 + B >= D]                                                                                               
          8.  lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0                                                                                        (?,1)
                                                            && -1 + -1*A + D >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && B >= D                                                                                                     
                                                            && 6*D >= 7 + 5*A + C                                                                                         
                                                            && B + 5*D >= 7 + 5*A + C                                                                                     
                                                            && D >= 1 + A                                                                                                 
                                                            && 29 >= A                                                                                                    
                                                            && 203 + B >= 5*A + C + 2*D                                                                                   
                                                            && 1561 + 2*B >= 35*A + 7*C + 14*D                                                                            
                                                            && 23*B + 140*D >= 161 + 140*A + 28*C                                                                         
                                                            && 5719 + 23*B >= 140*A + 28*C + 56*D                                                                         
                                                            && 5 + D >= B                                                                                                 
                                                            && C + 7*D >= 7*A + B]                                                                                        
          9.  lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)   [5 + -1*B + D >= 0                                                                                        (?,1)
                                                            && -1 + -1*A + D >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && B >= 6                                                                                                     
                                                            && 6*D >= 7 + 5*A + C                                                                                         
                                                            && B + 5*D >= 7 + 5*A + C                                                                                     
                                                            && D >= 1 + A                                                                                                 
                                                            && 29 >= A                                                                                                    
                                                            && 203 + B >= 5*A + C + 2*D                                                                                   
                                                            && 1561 + 2*B >= 35*A + 7*C + 14*D                                                                            
                                                            && 23*B + 140*D >= 161 + 140*A + 28*C                                                                         
                                                            && 5719 + 23*B >= 140*A + 28*C + 56*D                                                                         
                                                            && 5 + D >= B                                                                                                 
                                                            && C + 7*D >= 7*A + B]                                                                                        
          10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)   [5 + -1*B + D >= 0                                                                                        (?,1)
                                                            && -1 + -1*A + D >= 0                                                                                         
                                                            && 29 + -1*A >= 0                                                                                             
                                                            && D >= 1 + B                                                                                                 
                                                            && 5 >= B                                                                                                     
                                                            && 6*D >= 7 + 5*A + C                                                                                         
                                                            && B + 5*D >= 7 + 5*A + C                                                                                     
                                                            && D >= 1 + A                                                                                                 
                                                            && 29 >= A                                                                                                    
                                                            && 203 + B >= 5*A + C + 2*D                                                                                   
                                                            && 1561 + 2*B >= 35*A + 7*C + 14*D                                                                            
                                                            && 23*B + 140*D >= 161 + 140*A + 28*C                                                                         
                                                            && 5719 + 23*B >= 140*A + 28*C + 56*D                                                                         
                                                            && 5 + D >= B                                                                                                 
                                                            && C + 7*D >= 7*A + B]                                                                                        
          11. start0(A,B,C,D) -> start(A,C,C,A)            True                                                                                                      (1,1)
        Signature:
          {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
        Flow Graph:
          [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9}
          ,10->{8,9,10},11->{0,1,2,3}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          start(A,B,C,D)  -> stop(A,B,C,D)              [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && A >= 30
                                                         && B = C
                                                         && D = A]
          start(A,B,C,D)  -> lbl171(A,-10 + B,C,2 + D)  [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && C >= A
                                                         && 29 >= A
                                                         && B = C
                                                         && D = A]
          start(A,B,C,D)  -> lbl151(A,7 + B,C,1 + D)    [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && A >= 1 + C
                                                         && C >= 6
                                                         && 29 >= A
                                                         && B = C
                                                         && D = A]
          start(A,B,C,D)  -> lbl151(A,2 + B,C,1 + D)    [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && A >= 1 + C
                                                         && 5 >= C
                                                         && 29 >= A
                                                         && B = C
                                                         && D = A]
          lbl171(A,B,C,D) -> stop(A,B,C,D)              [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 30
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D)  [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && B >= D
                                                         && 29 >= D
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)    [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && B >= 6
                                                         && 29 >= D
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)    [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && 5 >= B
                                                         && 29 >= D
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D)  [5 + -1*B + D >= 0
                                                         && -1 + -1*A + D >= 0
                                                         && 29 + -1*A >= 0
                                                         && B >= D
                                                         && 6*D >= 7 + 5*A + C
                                                         && B + 5*D >= 7 + 5*A + C
                                                         && D >= 1 + A
                                                         && 29 >= A
                                                         && 203 + B >= 5*A + C + 2*D
                                                         && 1561 + 2*B >= 35*A + 7*C + 14*D
                                                         && 23*B + 140*D >= 161 + 140*A + 28*C
                                                         && 5719 + 23*B >= 140*A + 28*C + 56*D
                                                         && 5 + D >= B
                                                         && C + 7*D >= 7*A + B]
          lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)    [5 + -1*B + D >= 0
                                                         && -1 + -1*A + D >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && B >= 6
                                                         && 6*D >= 7 + 5*A + C
                                                         && B + 5*D >= 7 + 5*A + C
                                                         && D >= 1 + A
                                                         && 29 >= A
                                                         && 203 + B >= 5*A + C + 2*D
                                                         && 1561 + 2*B >= 35*A + 7*C + 14*D
                                                         && 23*B + 140*D >= 161 + 140*A + 28*C
                                                         && 5719 + 23*B >= 140*A + 28*C + 56*D
                                                         && 5 + D >= B
                                                         && C + 7*D >= 7*A + B]
          lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)    [5 + -1*B + D >= 0
                                                         && -1 + -1*A + D >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && 5 >= B
                                                         && 6*D >= 7 + 5*A + C
                                                         && B + 5*D >= 7 + 5*A + C
                                                         && D >= 1 + A
                                                         && 29 >= A
                                                         && 203 + B >= 5*A + C + 2*D
                                                         && 1561 + 2*B >= 35*A + 7*C + 14*D
                                                         && 23*B + 140*D >= 161 + 140*A + 28*C
                                                         && 5719 + 23*B >= 140*A + 28*C + 56*D
                                                         && 5 + D >= B
                                                         && C + 7*D >= 7*A + B]
          start0(A,B,C,D) -> start(A,C,C,A)             True
        Signature:
          {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9}
          ,10->{8,9,10},11->{0,1,2,3}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11]
          |
          +- p:[5] c: [5]
          |
          `- p:[6,8,7,9,10] c: [10]
             |
             `- p:[6,8,7,9] c: [9]
                |
                `- p:[6,8,7] c: [6,7,8]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          start(A,B,C,D)  -> stop(A,B,C,D)              [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && A >= 30
                                                         && B = C
                                                         && D = A]
          start(A,B,C,D)  -> lbl171(A,-10 + B,C,2 + D)  [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && C >= A
                                                         && 29 >= A
                                                         && B = C
                                                         && D = A]
          start(A,B,C,D)  -> lbl151(A,7 + B,C,1 + D)    [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && A >= 1 + C
                                                         && C >= 6
                                                         && 29 >= A
                                                         && B = C
                                                         && D = A]
          start(A,B,C,D)  -> lbl151(A,2 + B,C,1 + D)    [A + -1*D >= 0
                                                         && -1*A + D >= 0
                                                         && B + -1*C >= 0
                                                         && -1*B + C >= 0
                                                         && A >= 1 + C
                                                         && 5 >= C
                                                         && 29 >= A
                                                         && B = C
                                                         && D = A]
          lbl171(A,B,C,D) -> stop(A,B,C,D)              [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 30
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D)  [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && B >= D
                                                         && 29 >= D
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)    [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && B >= 6
                                                         && 29 >= D
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)    [12 + B + -1*D >= 0
                                                         && -2 + -1*A + D >= 0
                                                         && 10 + -1*A + B >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && 5 >= B
                                                         && 29 >= D
                                                         && 29 >= A
                                                         && B + 5*D >= 5*A + C
                                                         && C + 7*D >= 24 + 7*A + B
                                                         && 1674 + 7*B >= 35*A + 7*C + 19*D
                                                         && 12 + B >= D]
          lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D)  [5 + -1*B + D >= 0
                                                         && -1 + -1*A + D >= 0
                                                         && 29 + -1*A >= 0
                                                         && B >= D
                                                         && 6*D >= 7 + 5*A + C
                                                         && B + 5*D >= 7 + 5*A + C
                                                         && D >= 1 + A
                                                         && 29 >= A
                                                         && 203 + B >= 5*A + C + 2*D
                                                         && 1561 + 2*B >= 35*A + 7*C + 14*D
                                                         && 23*B + 140*D >= 161 + 140*A + 28*C
                                                         && 5719 + 23*B >= 140*A + 28*C + 56*D
                                                         && 5 + D >= B
                                                         && C + 7*D >= 7*A + B]
          lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D)    [5 + -1*B + D >= 0
                                                         && -1 + -1*A + D >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && B >= 6
                                                         && 6*D >= 7 + 5*A + C
                                                         && B + 5*D >= 7 + 5*A + C
                                                         && D >= 1 + A
                                                         && 29 >= A
                                                         && 203 + B >= 5*A + C + 2*D
                                                         && 1561 + 2*B >= 35*A + 7*C + 14*D
                                                         && 23*B + 140*D >= 161 + 140*A + 28*C
                                                         && 5719 + 23*B >= 140*A + 28*C + 56*D
                                                         && 5 + D >= B
                                                         && C + 7*D >= 7*A + B]
          lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D)    [5 + -1*B + D >= 0
                                                         && -1 + -1*A + D >= 0
                                                         && 29 + -1*A >= 0
                                                         && D >= 1 + B
                                                         && 5 >= B
                                                         && 6*D >= 7 + 5*A + C
                                                         && B + 5*D >= 7 + 5*A + C
                                                         && D >= 1 + A
                                                         && 29 >= A
                                                         && 203 + B >= 5*A + C + 2*D
                                                         && 1561 + 2*B >= 35*A + 7*C + 14*D
                                                         && 23*B + 140*D >= 161 + 140*A + 28*C
                                                         && 5719 + 23*B >= 140*A + 28*C + 56*D
                                                         && 5 + D >= B
                                                         && C + 7*D >= 7*A + B]
          start0(A,B,C,D) -> start(A,C,C,A)             True
        Signature:
          {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)}
        Rule Graph:
          [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9}
          ,10->{8,9,10},11->{0,1,2,3}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11]
          |
          +- p:[5] c: [5]
          |
          `- p:[6,8,7,9,10] c: [10]
             |
             `- p:[6,8,7,9] c: [9]
                |
                `- p:[6,8,7] c: [6,7,8])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES