YES
* Step 1: TrivialSCCs YES
    + Considered Problem:
        Rules:
          0.  evalnestedLoopstart(A,B,C,D,E,F,G,H)    -> evalnestedLoopentryin(A,B,C,D,E,F,G,H)   True                         (1,1)
          1.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H)     [A >= 0 && B >= 0 && C >= 0] (?,1)
          2.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [0 >= 1 + A]                 (?,1)
          3.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [0 >= 1 + B]                 (?,1)
          4.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [0 >= 1 + C]                 (?,1)
          5.  evalnestedLoopbb9in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H)     [D >= 0                      (?,1)
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && A + D >= 0                    
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && A + C >= 0                    
                                                                                                   && B >= 0                        
                                                                                                   && A + B >= 0                    
                                                                                                   && A >= 0                        
                                                                                                   && A >= 1 + D]                   
          6.  evalnestedLoopbb9in(A,B,C,D,E,F,G,H)    -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [D >= 0                      (?,1)
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && A + D >= 0                    
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && A + C >= 0                    
                                                                                                   && B >= 0                        
                                                                                                   && A + B >= 0                    
                                                                                                   && A >= 0                        
                                                                                                   && D >= A]                       
          7.  evalnestedLoopbb7in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H)     [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && B + F >= 0                    
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && B + -1*E >= 0                 
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && B + E >= 0                    
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && B >= 0                        
                                                                                                   && -1 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && B >= 1 + E]                   
          8.  evalnestedLoopbb7in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H)     [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && B + F >= 0                    
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && B + -1*E >= 0                 
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && B + E >= 0                    
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && B >= 0                        
                                                                                                   && -1 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && E >= B]                       
          9.  evalnestedLoopbb4in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && -1 + B + C >= 0               
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0]                  
          10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H)     [H >= 0                      (?,1)
                                                                                                   && -1 + G + H >= 0               
                                                                                                   && F + H >= 0                    
                                                                                                   && -1*F + H >= 0                 
                                                                                                   && E + H >= 0                    
                                                                                                   && D + H >= 0                    
                                                                                                   && -1*D + H >= 0                 
                                                                                                   && C + H >= 0                    
                                                                                                   && -1 + B + H >= 0               
                                                                                                   && -1 + A + H >= 0               
                                                                                                   && 1 + E + -1*G >= 0             
                                                                                                   && B + -1*G >= 0                 
                                                                                                   && -1 + G >= 0                   
                                                                                                   && -1 + F + G >= 0               
                                                                                                   && -1 + E + G >= 0               
                                                                                                   && -1 + -1*E + G >= 0            
                                                                                                   && -1 + D + G >= 0               
                                                                                                   && -1 + C + G >= 0               
                                                                                                   && -2 + B + G >= 0               
                                                                                                   && -2 + A + G >= 0               
                                                                                                   && F >= 0                        
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && -1 + B + C >= 0               
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && C >= 1 + H]                   
          11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H)     [H >= 0                      (?,1)
                                                                                                   && -1 + G + H >= 0               
                                                                                                   && F + H >= 0                    
                                                                                                   && -1*F + H >= 0                 
                                                                                                   && E + H >= 0                    
                                                                                                   && D + H >= 0                    
                                                                                                   && -1*D + H >= 0                 
                                                                                                   && C + H >= 0                    
                                                                                                   && -1 + B + H >= 0               
                                                                                                   && -1 + A + H >= 0               
                                                                                                   && 1 + E + -1*G >= 0             
                                                                                                   && B + -1*G >= 0                 
                                                                                                   && -1 + G >= 0                   
                                                                                                   && -1 + F + G >= 0               
                                                                                                   && -1 + E + G >= 0               
                                                                                                   && -1 + -1*E + G >= 0            
                                                                                                   && -1 + D + G >= 0               
                                                                                                   && -1 + C + G >= 0               
                                                                                                   && -2 + B + G >= 0               
                                                                                                   && -2 + A + G >= 0               
                                                                                                   && F >= 0                        
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && -1 + B + C >= 0               
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && H >= C]                       
          12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) [-1 + C + -1*H >= 0          (?,1)
                                                                                                   && H >= 0                        
                                                                                                   && -1 + G + H >= 0               
                                                                                                   && F + H >= 0                    
                                                                                                   && -1*F + H >= 0                 
                                                                                                   && E + H >= 0                    
                                                                                                   && D + H >= 0                    
                                                                                                   && -1*D + H >= 0                 
                                                                                                   && -1 + C + H >= 0               
                                                                                                   && -1 + B + H >= 0               
                                                                                                   && -1 + A + H >= 0               
                                                                                                   && 1 + E + -1*G >= 0             
                                                                                                   && B + -1*G >= 0                 
                                                                                                   && -1 + G >= 0                   
                                                                                                   && -1 + F + G >= 0               
                                                                                                   && -1 + E + G >= 0               
                                                                                                   && -1 + -1*E + G >= 0            
                                                                                                   && -1 + D + G >= 0               
                                                                                                   && -2 + C + G >= 0               
                                                                                                   && -2 + B + G >= 0               
                                                                                                   && -2 + A + G >= 0               
                                                                                                   && -1 + C + -1*F >= 0            
                                                                                                   && F >= 0                        
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && -1 + C + F >= 0               
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && -1 + C + E >= 0               
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + C + -1*D >= 0            
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && -1 + C + D >= 0               
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && -1 + C >= 0                   
                                                                                                   && -2 + B + C >= 0               
                                                                                                   && -2 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0]                  
          13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && B + F >= 0                    
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && B + -1*E >= 0                 
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && B + E >= 0                    
                                                                                                   && -1*B + E >= 0                 
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && B >= 0                        
                                                                                                   && -1 + A + B >= 0               
                                                                                                   && -1 + A >= 0]                  
          14. evalnestedLoopreturnin(A,B,C,D,E,F,G,H) -> evalnestedLoopstop(A,B,C,D,E,F,G,H)      True                         (?,1)
        Signature:
          {(evalnestedLoopbb4in,8)
          ;(evalnestedLoopbb5in,8)
          ;(evalnestedLoopbb6in,8)
          ;(evalnestedLoopbb7in,8)
          ;(evalnestedLoopbb8in,8)
          ;(evalnestedLoopbb9in,8)
          ;(evalnestedLoopentryin,8)
          ;(evalnestedLoopreturnin,8)
          ;(evalnestedLoopstart,8)
          ;(evalnestedLoopstop,8)}
        Flow Graph:
          [0->{1,2,3,4},1->{5,6},2->{14},3->{14},4->{14},5->{7,8},6->{14},7->{9},8->{13},9->{10,11},10->{12},11->{7
          ,8},12->{10,11},13->{5,6},14->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: Looptree YES
    + Considered Problem:
        Rules:
          0.  evalnestedLoopstart(A,B,C,D,E,F,G,H)    -> evalnestedLoopentryin(A,B,C,D,E,F,G,H)   True                         (1,1)
          1.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopbb9in(A,B,C,0,E,F,G,H)     [A >= 0 && B >= 0 && C >= 0] (1,1)
          2.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [0 >= 1 + A]                 (1,1)
          3.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [0 >= 1 + B]                 (1,1)
          4.  evalnestedLoopentryin(A,B,C,D,E,F,G,H)  -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [0 >= 1 + C]                 (1,1)
          5.  evalnestedLoopbb9in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb7in(A,B,C,D,0,D,G,H)     [D >= 0                      (?,1)
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && A + D >= 0                    
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && A + C >= 0                    
                                                                                                   && B >= 0                        
                                                                                                   && A + B >= 0                    
                                                                                                   && A >= 0                        
                                                                                                   && A >= 1 + D]                   
          6.  evalnestedLoopbb9in(A,B,C,D,E,F,G,H)    -> evalnestedLoopreturnin(A,B,C,D,E,F,G,H)  [D >= 0                      (1,1)
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && A + D >= 0                    
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && A + C >= 0                    
                                                                                                   && B >= 0                        
                                                                                                   && A + B >= 0                    
                                                                                                   && A >= 0                        
                                                                                                   && D >= A]                       
          7.  evalnestedLoopbb7in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb4in(A,B,C,D,E,F,G,H)     [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && B + F >= 0                    
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && B + -1*E >= 0                 
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && B + E >= 0                    
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && B >= 0                        
                                                                                                   && -1 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && B >= 1 + E]                   
          8.  evalnestedLoopbb7in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb8in(A,B,C,D,E,F,G,H)     [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && B + F >= 0                    
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && B + -1*E >= 0                 
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && B + E >= 0                    
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && B >= 0                        
                                                                                                   && -1 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && E >= B]                       
          9.  evalnestedLoopbb4in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb6in(A,B,C,D,E,F,1 + E,F) [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && -1 + B + C >= 0               
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0]                  
          10. evalnestedLoopbb6in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb5in(A,B,C,D,E,F,G,H)     [H >= 0                      (?,1)
                                                                                                   && -1 + G + H >= 0               
                                                                                                   && F + H >= 0                    
                                                                                                   && -1*F + H >= 0                 
                                                                                                   && E + H >= 0                    
                                                                                                   && D + H >= 0                    
                                                                                                   && -1*D + H >= 0                 
                                                                                                   && C + H >= 0                    
                                                                                                   && -1 + B + H >= 0               
                                                                                                   && -1 + A + H >= 0               
                                                                                                   && 1 + E + -1*G >= 0             
                                                                                                   && B + -1*G >= 0                 
                                                                                                   && -1 + G >= 0                   
                                                                                                   && -1 + F + G >= 0               
                                                                                                   && -1 + E + G >= 0               
                                                                                                   && -1 + -1*E + G >= 0            
                                                                                                   && -1 + D + G >= 0               
                                                                                                   && -1 + C + G >= 0               
                                                                                                   && -2 + B + G >= 0               
                                                                                                   && -2 + A + G >= 0               
                                                                                                   && F >= 0                        
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && -1 + B + C >= 0               
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && C >= 1 + H]                   
          11. evalnestedLoopbb6in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb7in(A,B,C,D,G,H,G,H)     [H >= 0                      (?,1)
                                                                                                   && -1 + G + H >= 0               
                                                                                                   && F + H >= 0                    
                                                                                                   && -1*F + H >= 0                 
                                                                                                   && E + H >= 0                    
                                                                                                   && D + H >= 0                    
                                                                                                   && -1*D + H >= 0                 
                                                                                                   && C + H >= 0                    
                                                                                                   && -1 + B + H >= 0               
                                                                                                   && -1 + A + H >= 0               
                                                                                                   && 1 + E + -1*G >= 0             
                                                                                                   && B + -1*G >= 0                 
                                                                                                   && -1 + G >= 0                   
                                                                                                   && -1 + F + G >= 0               
                                                                                                   && -1 + E + G >= 0               
                                                                                                   && -1 + -1*E + G >= 0            
                                                                                                   && -1 + D + G >= 0               
                                                                                                   && -1 + C + G >= 0               
                                                                                                   && -2 + B + G >= 0               
                                                                                                   && -2 + A + G >= 0               
                                                                                                   && F >= 0                        
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && -1 + B + C >= 0               
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0                   
                                                                                                   && H >= C]                       
          12. evalnestedLoopbb5in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb6in(A,B,C,D,E,F,G,1 + H) [-1 + C + -1*H >= 0          (?,1)
                                                                                                   && H >= 0                        
                                                                                                   && -1 + G + H >= 0               
                                                                                                   && F + H >= 0                    
                                                                                                   && -1*F + H >= 0                 
                                                                                                   && E + H >= 0                    
                                                                                                   && D + H >= 0                    
                                                                                                   && -1*D + H >= 0                 
                                                                                                   && -1 + C + H >= 0               
                                                                                                   && -1 + B + H >= 0               
                                                                                                   && -1 + A + H >= 0               
                                                                                                   && 1 + E + -1*G >= 0             
                                                                                                   && B + -1*G >= 0                 
                                                                                                   && -1 + G >= 0                   
                                                                                                   && -1 + F + G >= 0               
                                                                                                   && -1 + E + G >= 0               
                                                                                                   && -1 + -1*E + G >= 0            
                                                                                                   && -1 + D + G >= 0               
                                                                                                   && -2 + C + G >= 0               
                                                                                                   && -2 + B + G >= 0               
                                                                                                   && -2 + A + G >= 0               
                                                                                                   && -1 + C + -1*F >= 0            
                                                                                                   && F >= 0                        
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && -1 + C + F >= 0               
                                                                                                   && -1 + B + F >= 0               
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && -1 + B + -1*E >= 0            
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && -1 + C + E >= 0               
                                                                                                   && -1 + B + E >= 0               
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + C + -1*D >= 0            
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && -1 + C + D >= 0               
                                                                                                   && -1 + B + D >= 0               
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && -1 + C >= 0                   
                                                                                                   && -2 + B + C >= 0               
                                                                                                   && -2 + A + C >= 0               
                                                                                                   && -1 + B >= 0                   
                                                                                                   && -2 + A + B >= 0               
                                                                                                   && -1 + A >= 0]                  
          13. evalnestedLoopbb8in(A,B,C,D,E,F,G,H)    -> evalnestedLoopbb9in(A,B,C,1 + F,E,F,G,H) [F >= 0                      (?,1)
                                                                                                   && E + F >= 0                    
                                                                                                   && D + F >= 0                    
                                                                                                   && -1*D + F >= 0                 
                                                                                                   && C + F >= 0                    
                                                                                                   && B + F >= 0                    
                                                                                                   && -1 + A + F >= 0               
                                                                                                   && B + -1*E >= 0                 
                                                                                                   && E >= 0                        
                                                                                                   && D + E >= 0                    
                                                                                                   && C + E >= 0                    
                                                                                                   && B + E >= 0                    
                                                                                                   && -1*B + E >= 0                 
                                                                                                   && -1 + A + E >= 0               
                                                                                                   && -1 + A + -1*D >= 0            
                                                                                                   && D >= 0                        
                                                                                                   && C + D >= 0                    
                                                                                                   && B + D >= 0                    
                                                                                                   && -1 + A + D >= 0               
                                                                                                   && C >= 0                        
                                                                                                   && B + C >= 0                    
                                                                                                   && -1 + A + C >= 0               
                                                                                                   && B >= 0                        
                                                                                                   && -1 + A + B >= 0               
                                                                                                   && -1 + A >= 0]                  
          14. evalnestedLoopreturnin(A,B,C,D,E,F,G,H) -> evalnestedLoopstop(A,B,C,D,E,F,G,H)      True                         (1,1)
        Signature:
          {(evalnestedLoopbb4in,8)
          ;(evalnestedLoopbb5in,8)
          ;(evalnestedLoopbb6in,8)
          ;(evalnestedLoopbb7in,8)
          ;(evalnestedLoopbb8in,8)
          ;(evalnestedLoopbb9in,8)
          ;(evalnestedLoopentryin,8)
          ;(evalnestedLoopreturnin,8)
          ;(evalnestedLoopstart,8)
          ;(evalnestedLoopstop,8)}
        Flow Graph:
          [0->{1,2,3,4},1->{5,6},2->{14},3->{14},4->{14},5->{7,8},6->{14},7->{9},8->{13},9->{10,11},10->{12},11->{7
          ,8},12->{10,11},13->{5,6},14->{}]
        
    + Applied Processor:
        Looptree
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
          |
          `- p:[5,13,8,11,9,7,12,10] c: [13]
             |
             `- p:[7,11,9,12,10] c: [12]
                |
                `- p:[7,11,9] c: [11]

YES