YES
* Step 1: TrivialSCCs YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F,G,H)  -> stop(A,B,C,D,E,F,G,H)      [A + -1*H >= 0            (?,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && A >= 5                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          1. start(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,0,G,1 + H) [A + -1*H >= 0            (?,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && 2 >= A                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          2. start(A,B,C,D,E,F,G,H)  -> lbl82(A,0,C,D,E,1,G,H)     [A + -1*H >= 0            (?,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && A >= 3                     
                                                                    && 4 >= A                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          3. lbl92(A,B,C,D,E,F,G,H)  -> stop(A,B,C,D,E,F,G,H)      [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && D >= 4                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          4. lbl92(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,0,G,1 + H) [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && 1 >= D                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          5. lbl92(A,B,C,D,E,F,G,H)  -> lbl82(A,0,C,D,E,1,G,H)     [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && D >= 2                     
                                                                    && 3 >= D                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          6. lbl82(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,F,G,1 + H) [4 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 4 + B + -1*H >= 0          
                                                                    && 8 + -1*A + -1*H >= 0       
                                                                    && -3 + H >= 0                
                                                                    && -4 + F + H >= 0            
                                                                    && -3 + B + H >= 0            
                                                                    && -1*A + H >= 0              
                                                                    && 1 + B + -1*F >= 0          
                                                                    && -1 + F >= 0                
                                                                    && -1 + B + F >= 0            
                                                                    && -1 + -1*B + F >= 0         
                                                                    && 3 + -1*A + F >= 0          
                                                                    && B >= 0                     
                                                                    && 4 + -1*A + B >= 0          
                                                                    && 4 + -1*A >= 0              
                                                                    && H >= A                     
                                                                    && H >= 3                     
                                                                    && 4 >= H                     
                                                                    && F = 10                     
                                                                    && B = 9]                     
          7. lbl82(A,B,C,D,E,F,G,H)  -> lbl82(A,F,C,D,E,1 + F,G,H) [4 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 4 + B + -1*H >= 0          
                                                                    && 8 + -1*A + -1*H >= 0       
                                                                    && -3 + H >= 0                
                                                                    && -4 + F + H >= 0            
                                                                    && -3 + B + H >= 0            
                                                                    && -1*A + H >= 0              
                                                                    && 1 + B + -1*F >= 0          
                                                                    && -1 + F >= 0                
                                                                    && -1 + B + F >= 0            
                                                                    && -1 + -1*B + F >= 0         
                                                                    && 3 + -1*A + F >= 0          
                                                                    && B >= 0                     
                                                                    && 4 + -1*A + B >= 0          
                                                                    && 4 + -1*A >= 0              
                                                                    && H >= 3                     
                                                                    && 8 >= B                     
                                                                    && 9 >= B                     
                                                                    && H >= A                     
                                                                    && 4 >= H                     
                                                                    && F = 1 + B]                 
          8. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A)     True                      (1,1)
        Signature:
          {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
        Flow Graph:
          [0->{},1->{3,4,5},2->{6,7},3->{},4->{3,4,5},5->{6,7},6->{3,4,5},7->{6,7},8->{0,1,2}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: UnsatPaths YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F,G,H)  -> stop(A,B,C,D,E,F,G,H)      [A + -1*H >= 0            (1,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && A >= 5                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          1. start(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,0,G,1 + H) [A + -1*H >= 0            (1,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && 2 >= A                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          2. start(A,B,C,D,E,F,G,H)  -> lbl82(A,0,C,D,E,1,G,H)     [A + -1*H >= 0            (1,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && A >= 3                     
                                                                    && 4 >= A                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          3. lbl92(A,B,C,D,E,F,G,H)  -> stop(A,B,C,D,E,F,G,H)      [5 + -1*H >= 0            (1,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && D >= 4                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          4. lbl92(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,0,G,1 + H) [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && 1 >= D                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          5. lbl92(A,B,C,D,E,F,G,H)  -> lbl82(A,0,C,D,E,1,G,H)     [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && D >= 2                     
                                                                    && 3 >= D                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          6. lbl82(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,F,G,1 + H) [4 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 4 + B + -1*H >= 0          
                                                                    && 8 + -1*A + -1*H >= 0       
                                                                    && -3 + H >= 0                
                                                                    && -4 + F + H >= 0            
                                                                    && -3 + B + H >= 0            
                                                                    && -1*A + H >= 0              
                                                                    && 1 + B + -1*F >= 0          
                                                                    && -1 + F >= 0                
                                                                    && -1 + B + F >= 0            
                                                                    && -1 + -1*B + F >= 0         
                                                                    && 3 + -1*A + F >= 0          
                                                                    && B >= 0                     
                                                                    && 4 + -1*A + B >= 0          
                                                                    && 4 + -1*A >= 0              
                                                                    && H >= A                     
                                                                    && H >= 3                     
                                                                    && 4 >= H                     
                                                                    && F = 10                     
                                                                    && B = 9]                     
          7. lbl82(A,B,C,D,E,F,G,H)  -> lbl82(A,F,C,D,E,1 + F,G,H) [4 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 4 + B + -1*H >= 0          
                                                                    && 8 + -1*A + -1*H >= 0       
                                                                    && -3 + H >= 0                
                                                                    && -4 + F + H >= 0            
                                                                    && -3 + B + H >= 0            
                                                                    && -1*A + H >= 0              
                                                                    && 1 + B + -1*F >= 0          
                                                                    && -1 + F >= 0                
                                                                    && -1 + B + F >= 0            
                                                                    && -1 + -1*B + F >= 0         
                                                                    && 3 + -1*A + F >= 0          
                                                                    && B >= 0                     
                                                                    && 4 + -1*A + B >= 0          
                                                                    && 4 + -1*A >= 0              
                                                                    && H >= 3                     
                                                                    && 8 >= B                     
                                                                    && 9 >= B                     
                                                                    && H >= A                     
                                                                    && 4 >= H                     
                                                                    && F = 1 + B]                 
          8. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A)     True                      (1,1)
        Signature:
          {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
        Flow Graph:
          [0->{},1->{3,4,5},2->{6,7},3->{},4->{3,4,5},5->{6,7},6->{3,4,5},7->{6,7},8->{0,1,2}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,3),(2,6),(4,3),(5,6),(6,4)]
* Step 3: Looptree YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F,G,H)  -> stop(A,B,C,D,E,F,G,H)      [A + -1*H >= 0            (1,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && A >= 5                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          1. start(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,0,G,1 + H) [A + -1*H >= 0            (1,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && 2 >= A                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          2. start(A,B,C,D,E,F,G,H)  -> lbl82(A,0,C,D,E,1,G,H)     [A + -1*H >= 0            (1,1)
                                                                    && -1*A + H >= 0              
                                                                    && F + -1*G >= 0              
                                                                    && -1*F + G >= 0              
                                                                    && D + -1*E >= 0              
                                                                    && -1*D + E >= 0              
                                                                    && B + -1*C >= 0              
                                                                    && -1*B + C >= 0              
                                                                    && A >= 3                     
                                                                    && 4 >= A                     
                                                                    && B = C                      
                                                                    && D = E                      
                                                                    && F = G                      
                                                                    && H = A]                     
          3. lbl92(A,B,C,D,E,F,G,H)  -> stop(A,B,C,D,E,F,G,H)      [5 + -1*H >= 0            (1,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && D >= 4                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          4. lbl92(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,0,G,1 + H) [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && 1 >= D                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          5. lbl92(A,B,C,D,E,F,G,H)  -> lbl82(A,0,C,D,E,1,G,H)     [5 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 15 + -1*F + -1*H >= 0      
                                                                    && 1 + D + -1*H >= 0          
                                                                    && 9 + -1*D + -1*H >= 0       
                                                                    && 9 + -1*A + -1*H >= 0       
                                                                    && -1 + -1*D + H >= 0         
                                                                    && -1 + -1*A + H >= 0         
                                                                    && 10 + -1*F >= 0             
                                                                    && 14 + -1*D + -1*F >= 0      
                                                                    && 14 + -1*A + -1*F >= 0      
                                                                    && F >= 0                     
                                                                    && 2 + -1*D + F >= 0          
                                                                    && 2 + -1*A + F >= 0          
                                                                    && 4 + -1*D >= 0              
                                                                    && 8 + -1*A + -1*D >= 0       
                                                                    && -1*A + D >= 0              
                                                                    && 4 + -1*A >= 0              
                                                                    && D >= 2                     
                                                                    && 3 >= D                     
                                                                    && D >= A                     
                                                                    && 10 + F >= 5*D              
                                                                    && H = 1 + D]                 
          6. lbl82(A,B,C,D,E,F,G,H)  -> lbl92(A,B,C,H,E,F,G,1 + H) [4 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 4 + B + -1*H >= 0          
                                                                    && 8 + -1*A + -1*H >= 0       
                                                                    && -3 + H >= 0                
                                                                    && -4 + F + H >= 0            
                                                                    && -3 + B + H >= 0            
                                                                    && -1*A + H >= 0              
                                                                    && 1 + B + -1*F >= 0          
                                                                    && -1 + F >= 0                
                                                                    && -1 + B + F >= 0            
                                                                    && -1 + -1*B + F >= 0         
                                                                    && 3 + -1*A + F >= 0          
                                                                    && B >= 0                     
                                                                    && 4 + -1*A + B >= 0          
                                                                    && 4 + -1*A >= 0              
                                                                    && H >= A                     
                                                                    && H >= 3                     
                                                                    && 4 >= H                     
                                                                    && F = 10                     
                                                                    && B = 9]                     
          7. lbl82(A,B,C,D,E,F,G,H)  -> lbl82(A,F,C,D,E,1 + F,G,H) [4 + -1*H >= 0            (?,1)
                                                                    && 3 + F + -1*H >= 0          
                                                                    && 4 + B + -1*H >= 0          
                                                                    && 8 + -1*A + -1*H >= 0       
                                                                    && -3 + H >= 0                
                                                                    && -4 + F + H >= 0            
                                                                    && -3 + B + H >= 0            
                                                                    && -1*A + H >= 0              
                                                                    && 1 + B + -1*F >= 0          
                                                                    && -1 + F >= 0                
                                                                    && -1 + B + F >= 0            
                                                                    && -1 + -1*B + F >= 0         
                                                                    && 3 + -1*A + F >= 0          
                                                                    && B >= 0                     
                                                                    && 4 + -1*A + B >= 0          
                                                                    && 4 + -1*A >= 0              
                                                                    && H >= 3                     
                                                                    && 8 >= B                     
                                                                    && 9 >= B                     
                                                                    && H >= A                     
                                                                    && 4 >= H                     
                                                                    && F = 1 + B]                 
          8. start0(A,B,C,D,E,F,G,H) -> start(A,C,C,E,E,G,G,A)     True                      (1,1)
        Signature:
          {(lbl82,8);(lbl92,8);(start,8);(start0,8);(stop,8)}
        Flow Graph:
          [0->{},1->{4,5},2->{7},3->{},4->{4,5},5->{7},6->{3,5},7->{6,7},8->{0,1,2}]
        
    + Applied Processor:
        Looptree
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8]
          |
          +- p:[4] c: [4]
          |
          `- p:[5,6,7] c: [7]

YES