YES
* Step 1: TrivialSCCs YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F,G,H)  -> a(A,B,C,D,E,F,G,H)      [G + -1*H >= 0         (?,1)
                                                                 && -1*G + H >= 0           
                                                                 && E + -1*F >= 0           
                                                                 && -1*E + F >= 0           
                                                                 && C + -1*D >= 0           
                                                                 && -1*C + D >= 0           
                                                                 && A + -1*B >= 0           
                                                                 && -1*A + B >= 0           
                                                                 && A >= 1                  
                                                                 && B = A                   
                                                                 && C = D                   
                                                                 && E = F                   
                                                                 && G = H]                  
          1. a(A,B,C,D,E,F,G,H)      -> d(A,B,1,D,E,F,G,H)      [G + -1*H >= 0         (?,1)
                                                                 && -1*G + H >= 0           
                                                                 && E + -1*F >= 0           
                                                                 && -1*E + F >= 0           
                                                                 && C + -1*D >= 0           
                                                                 && -1*C + D >= 0           
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1                  
                                                                 && G = H                   
                                                                 && E = F                   
                                                                 && C = D                   
                                                                 && B = A]                  
          2. d(A,B,C,D,E,F,G,H)      -> b(A,B,C,D,E,F,1 + C,H)  [B + -1*C >= 0         (?,1)
                                                                 && A + -1*C >= 0           
                                                                 && -1 + C >= 0             
                                                                 && -2 + B + C >= 0         
                                                                 && -2 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1 + C              
                                                                 && A >= C                  
                                                                 && A >= 1                  
                                                                 && C >= 1                  
                                                                 && B = A]                  
          3. d(A,B,C,D,E,F,G,H)      -> halt(A,B,C,D,E,F,G,H)   [B + -1*C >= 0         (?,1)
                                                                 && A + -1*C >= 0           
                                                                 && -1 + C >= 0             
                                                                 && -2 + B + C >= 0         
                                                                 && -2 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1                  
                                                                 && C = A                   
                                                                 && B = A]                  
          4. b(A,B,C,D,E,F,G,H)      -> d(A,B,1 + C,D,E,F,G,H)  [1 + B + -1*G >= 0     (?,1)
                                                                 && 1 + A + -1*G >= 0       
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= 1 + C              
                                                                 && C >= 1                  
                                                                 && A >= C                  
                                                                 && G = 1 + A               
                                                                 && B = A]                  
          5. b(A,B,C,D,E,F,G,H)      -> c(A,B,C,D,B,F,G,H)      [1 + B + -1*G >= 0     (?,1)
                                                                 && 1 + A + -1*G >= 0       
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= G                  
                                                                 && 1 + A >= G              
                                                                 && A >= 1 + C              
                                                                 && C >= 1                  
                                                                 && G >= 1 + C              
                                                                 && B = A]                  
          6. c(A,B,C,D,E,F,G,H)      -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0         (?,1)
                                                                 && A + -1*G >= 0           
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && B + -1*E >= 0           
                                                                 && A + -1*E >= 0           
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && E >= 1 + C              
                                                                 && A >= E                  
                                                                 && A >= G                  
                                                                 && C >= 1                  
                                                                 && E >= C                  
                                                                 && G >= 1 + C              
                                                                 && B = A]                  
          7. c(A,B,C,D,E,F,G,H)      -> b(A,B,C,D,E,F,1 + G,H)  [B + -1*G >= 0         (?,1)
                                                                 && A + -1*G >= 0           
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && B + -1*E >= 0           
                                                                 && A + -1*E >= 0           
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= E                  
                                                                 && A >= G                  
                                                                 && E >= 1                  
                                                                 && G >= 1 + E              
                                                                 && C = E                   
                                                                 && B = A]                  
          8. start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H)  True                   (1,1)
        Signature:
          {(a,8);(b,8);(c,8);(d,8);(halt,8);(start,8);(start0,8)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{},4->{2,3},5->{6,7},6->{6,7},7->{4,5},8->{0}]
        
    + 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)  -> a(A,B,C,D,E,F,G,H)      [G + -1*H >= 0         (1,1)
                                                                 && -1*G + H >= 0           
                                                                 && E + -1*F >= 0           
                                                                 && -1*E + F >= 0           
                                                                 && C + -1*D >= 0           
                                                                 && -1*C + D >= 0           
                                                                 && A + -1*B >= 0           
                                                                 && -1*A + B >= 0           
                                                                 && A >= 1                  
                                                                 && B = A                   
                                                                 && C = D                   
                                                                 && E = F                   
                                                                 && G = H]                  
          1. a(A,B,C,D,E,F,G,H)      -> d(A,B,1,D,E,F,G,H)      [G + -1*H >= 0         (1,1)
                                                                 && -1*G + H >= 0           
                                                                 && E + -1*F >= 0           
                                                                 && -1*E + F >= 0           
                                                                 && C + -1*D >= 0           
                                                                 && -1*C + D >= 0           
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1                  
                                                                 && G = H                   
                                                                 && E = F                   
                                                                 && C = D                   
                                                                 && B = A]                  
          2. d(A,B,C,D,E,F,G,H)      -> b(A,B,C,D,E,F,1 + C,H)  [B + -1*C >= 0         (?,1)
                                                                 && A + -1*C >= 0           
                                                                 && -1 + C >= 0             
                                                                 && -2 + B + C >= 0         
                                                                 && -2 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1 + C              
                                                                 && A >= C                  
                                                                 && A >= 1                  
                                                                 && C >= 1                  
                                                                 && B = A]                  
          3. d(A,B,C,D,E,F,G,H)      -> halt(A,B,C,D,E,F,G,H)   [B + -1*C >= 0         (1,1)
                                                                 && A + -1*C >= 0           
                                                                 && -1 + C >= 0             
                                                                 && -2 + B + C >= 0         
                                                                 && -2 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1                  
                                                                 && C = A                   
                                                                 && B = A]                  
          4. b(A,B,C,D,E,F,G,H)      -> d(A,B,1 + C,D,E,F,G,H)  [1 + B + -1*G >= 0     (?,1)
                                                                 && 1 + A + -1*G >= 0       
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= 1 + C              
                                                                 && C >= 1                  
                                                                 && A >= C                  
                                                                 && G = 1 + A               
                                                                 && B = A]                  
          5. b(A,B,C,D,E,F,G,H)      -> c(A,B,C,D,B,F,G,H)      [1 + B + -1*G >= 0     (?,1)
                                                                 && 1 + A + -1*G >= 0       
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= G                  
                                                                 && 1 + A >= G              
                                                                 && A >= 1 + C              
                                                                 && C >= 1                  
                                                                 && G >= 1 + C              
                                                                 && B = A]                  
          6. c(A,B,C,D,E,F,G,H)      -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0         (?,1)
                                                                 && A + -1*G >= 0           
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && B + -1*E >= 0           
                                                                 && A + -1*E >= 0           
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && E >= 1 + C              
                                                                 && A >= E                  
                                                                 && A >= G                  
                                                                 && C >= 1                  
                                                                 && E >= C                  
                                                                 && G >= 1 + C              
                                                                 && B = A]                  
          7. c(A,B,C,D,E,F,G,H)      -> b(A,B,C,D,E,F,1 + G,H)  [B + -1*G >= 0         (?,1)
                                                                 && A + -1*G >= 0           
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && B + -1*E >= 0           
                                                                 && A + -1*E >= 0           
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= E                  
                                                                 && A >= G                  
                                                                 && E >= 1                  
                                                                 && G >= 1 + E              
                                                                 && C = E                   
                                                                 && B = A]                  
          8. start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H)  True                   (1,1)
        Signature:
          {(a,8);(b,8);(c,8);(d,8);(halt,8);(start,8);(start0,8)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{},4->{2,3},5->{6,7},6->{6,7},7->{4,5},8->{0}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(2,4),(5,7)]
* Step 3: Looptree YES
    + Considered Problem:
        Rules:
          0. start(A,B,C,D,E,F,G,H)  -> a(A,B,C,D,E,F,G,H)      [G + -1*H >= 0         (1,1)
                                                                 && -1*G + H >= 0           
                                                                 && E + -1*F >= 0           
                                                                 && -1*E + F >= 0           
                                                                 && C + -1*D >= 0           
                                                                 && -1*C + D >= 0           
                                                                 && A + -1*B >= 0           
                                                                 && -1*A + B >= 0           
                                                                 && A >= 1                  
                                                                 && B = A                   
                                                                 && C = D                   
                                                                 && E = F                   
                                                                 && G = H]                  
          1. a(A,B,C,D,E,F,G,H)      -> d(A,B,1,D,E,F,G,H)      [G + -1*H >= 0         (1,1)
                                                                 && -1*G + H >= 0           
                                                                 && E + -1*F >= 0           
                                                                 && -1*E + F >= 0           
                                                                 && C + -1*D >= 0           
                                                                 && -1*C + D >= 0           
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1                  
                                                                 && G = H                   
                                                                 && E = F                   
                                                                 && C = D                   
                                                                 && B = A]                  
          2. d(A,B,C,D,E,F,G,H)      -> b(A,B,C,D,E,F,1 + C,H)  [B + -1*C >= 0         (?,1)
                                                                 && A + -1*C >= 0           
                                                                 && -1 + C >= 0             
                                                                 && -2 + B + C >= 0         
                                                                 && -2 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1 + C              
                                                                 && A >= C                  
                                                                 && A >= 1                  
                                                                 && C >= 1                  
                                                                 && B = A]                  
          3. d(A,B,C,D,E,F,G,H)      -> halt(A,B,C,D,E,F,G,H)   [B + -1*C >= 0         (1,1)
                                                                 && A + -1*C >= 0           
                                                                 && -1 + C >= 0             
                                                                 && -2 + B + C >= 0         
                                                                 && -2 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -1 + B >= 0             
                                                                 && -2 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -1 + A >= 0             
                                                                 && A >= 1                  
                                                                 && C = A                   
                                                                 && B = A]                  
          4. b(A,B,C,D,E,F,G,H)      -> d(A,B,1 + C,D,E,F,G,H)  [1 + B + -1*G >= 0     (?,1)
                                                                 && 1 + A + -1*G >= 0       
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= 1 + C              
                                                                 && C >= 1                  
                                                                 && A >= C                  
                                                                 && G = 1 + A               
                                                                 && B = A]                  
          5. b(A,B,C,D,E,F,G,H)      -> c(A,B,C,D,B,F,G,H)      [1 + B + -1*G >= 0     (?,1)
                                                                 && 1 + A + -1*G >= 0       
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= G                  
                                                                 && 1 + A >= G              
                                                                 && A >= 1 + C              
                                                                 && C >= 1                  
                                                                 && G >= 1 + C              
                                                                 && B = A]                  
          6. c(A,B,C,D,E,F,G,H)      -> c(A,B,C,D,-1 + E,F,G,H) [B + -1*G >= 0         (?,1)
                                                                 && A + -1*G >= 0           
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && B + -1*E >= 0           
                                                                 && A + -1*E >= 0           
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && E >= 1 + C              
                                                                 && A >= E                  
                                                                 && A >= G                  
                                                                 && C >= 1                  
                                                                 && E >= C                  
                                                                 && G >= 1 + C              
                                                                 && B = A]                  
          7. c(A,B,C,D,E,F,G,H)      -> b(A,B,C,D,E,F,1 + G,H)  [B + -1*G >= 0         (?,1)
                                                                 && A + -1*G >= 0           
                                                                 && -2 + G >= 0             
                                                                 && -3 + C + G >= 0         
                                                                 && -1 + -1*C + G >= 0      
                                                                 && -4 + B + G >= 0         
                                                                 && -4 + A + G >= 0         
                                                                 && B + -1*E >= 0           
                                                                 && A + -1*E >= 0           
                                                                 && -1 + B + -1*C >= 0      
                                                                 && -1 + A + -1*C >= 0      
                                                                 && -1 + C >= 0             
                                                                 && -3 + B + C >= 0         
                                                                 && -3 + A + C >= 0         
                                                                 && A + -1*B >= 0           
                                                                 && -2 + B >= 0             
                                                                 && -4 + A + B >= 0         
                                                                 && -1*A + B >= 0           
                                                                 && -2 + A >= 0             
                                                                 && A >= E                  
                                                                 && A >= G                  
                                                                 && E >= 1                  
                                                                 && G >= 1 + E              
                                                                 && C = E                   
                                                                 && B = A]                  
          8. start0(A,B,C,D,E,F,G,H) -> start(A,A,D,D,F,F,H,H)  True                   (1,1)
        Signature:
          {(a,8);(b,8);(c,8);(d,8);(halt,8);(start,8);(start0,8)}
        Flow Graph:
          [0->{1},1->{2,3},2->{5},3->{},4->{2,3},5->{6},6->{6,7},7->{4,5},8->{0}]
        
    + Applied Processor:
        Looptree
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8]
          |
          `- p:[2,4,7,6,5] c: [4]
             |
             `- p:[5,7,6] c: [7]
                |
                `- p:[6] c: [6]

YES