YES
* Step 1: TrivialSCCs YES
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D,E,F)    -> evalfentryin(A,B,C,D,E,F)               True                                                                                                     (1,1)
          1.  evalfentryin(A,B,C,D,E,F)  -> evalfbb9in(B,B,C,D,E,F)                 True                                                                                                     (?,1)
          2.  evalfbb9in(A,B,C,D,E,F)    -> evalfreturnin(A,B,C,D,E,F)              [1 >= B]                                                                                                 (?,1)
          3.  evalfbb9in(A,B,C,D,E,F)    -> evalfbbin(A,B,C,D,E,F)                  [B >= 2]                                                                                                 (?,1)
          4.  evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F)                  [1 + -1*B >= 0]                                                                                          (?,1)
          5.  evalfbbin(A,B,C,D,E,F)     -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F)   [-2 + B >= 0]                                                                                            (?,1)
          6.  evalfbb6in(A,B,C,D,E,F)    -> evalfbb7in(A,B,C,D,E,F)                 [-1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && 1 + -1*B + C >= 0 && -2 + B >= 0 && D >= 1 + C] (?,1)
          7.  evalfbb6in(A,B,C,D,E,F)    -> evalfbb8in(A,B,C,D,E,F)                 [-1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && 1 + -1*B + C >= 0 && -2 + B >= 0 && C >= D]     (?,1)
          8.  evalfbb7in(A,B,C,D,E,F)    -> evalfbb8in(A,B,C,D,E,F)                 [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
          9.  evalfbb7in(A,B,C,D,E,F)    -> evalfbb1in(A,B,C,D,E,F)                 [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0                                                                                               
                                                                                     && G >= 1]                                                                                                   
          10. evalfbb7in(A,B,C,D,E,F)    -> evalfbb1in(A,B,C,D,E,F)                 [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0                                                                                               
                                                                                     && 0 >= 1 + G]                                                                                               
          11. evalfbb8in(A,B,C,D,E,F)    -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) [-1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && 1 + -1*B + C >= 0 && -2 + B >= 0]               (?,1)
          12. evalfbb1in(A,B,C,D,E,F)    -> evalfbb3in(A,B,C,D,C,-1 + D)            [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
          13. evalfbb3in(A,B,C,D,E,F)    -> evalfbb5in(A,B,C,D,E,F)                 [-1 + D + -1*F >= 0                                                                                      (?,1)
                                                                                     && -1 + F >= 0                                                                                               
                                                                                     && -2 + E + F >= 0                                                                                           
                                                                                     && -1*E + F >= 0                                                                                             
                                                                                     && -3 + D + F >= 0                                                                                           
                                                                                     && 1 + -1*D + F >= 0                                                                                         
                                                                                     && -2 + C + F >= 0                                                                                           
                                                                                     && -1*C + F >= 0                                                                                             
                                                                                     && -3 + B + F >= 0                                                                                           
                                                                                     && 1 + -1*B + F >= 0                                                                                         
                                                                                     && -1 + D + -1*E >= 0                                                                                        
                                                                                     && C + -1*E >= 0                                                                                             
                                                                                     && -1 + B + -1*E >= 0                                                                                        
                                                                                     && -1 + E >= 0                                                                                               
                                                                                     && -3 + D + E >= 0                                                                                           
                                                                                     && -2 + C + E >= 0                                                                                           
                                                                                     && -1*C + E >= 0                                                                                             
                                                                                     && -3 + B + E >= 0                                                                                           
                                                                                     && 1 + -1*B + E >= 0                                                                                         
                                                                                     && -2 + D >= 0                                                                                               
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
          14. evalfbb5in(A,B,C,D,E,F)    -> evalfbb6in(A,B,E,-1 + F,E,F)            [-1 + D + -1*F >= 0                                                                                      (?,1)
                                                                                     && -1 + F >= 0                                                                                               
                                                                                     && -2 + E + F >= 0                                                                                           
                                                                                     && -1*E + F >= 0                                                                                             
                                                                                     && -3 + D + F >= 0                                                                                           
                                                                                     && 1 + -1*D + F >= 0                                                                                         
                                                                                     && -2 + C + F >= 0                                                                                           
                                                                                     && -1*C + F >= 0                                                                                             
                                                                                     && -3 + B + F >= 0                                                                                           
                                                                                     && 1 + -1*B + F >= 0                                                                                         
                                                                                     && -1 + D + -1*E >= 0                                                                                        
                                                                                     && C + -1*E >= 0                                                                                             
                                                                                     && -1 + B + -1*E >= 0                                                                                        
                                                                                     && -1 + E >= 0                                                                                               
                                                                                     && -3 + D + E >= 0                                                                                           
                                                                                     && -2 + C + E >= 0                                                                                           
                                                                                     && -1*C + E >= 0                                                                                             
                                                                                     && -3 + B + E >= 0                                                                                           
                                                                                     && 1 + -1*B + E >= 0                                                                                         
                                                                                     && -2 + D >= 0                                                                                               
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
        Signature:
          {(evalfbb1in,6)
          ;(evalfbb3in,6)
          ;(evalfbb5in,6)
          ;(evalfbb6in,6)
          ;(evalfbb7in,6)
          ;(evalfbb8in,6)
          ;(evalfbb9in,6)
          ;(evalfbbin,6)
          ;(evalfentryin,6)
          ;(evalfreturnin,6)
          ;(evalfstart,6)
          ;(evalfstop,6)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4},3->{5},4->{},5->{6,7},6->{8,9,10},7->{11},8->{11},9->{12},10->{12},11->{2,3}
          ,12->{13},13->{14},14->{6,7}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: Looptree YES
    + Considered Problem:
        Rules:
          0.  evalfstart(A,B,C,D,E,F)    -> evalfentryin(A,B,C,D,E,F)               True                                                                                                     (1,1)
          1.  evalfentryin(A,B,C,D,E,F)  -> evalfbb9in(B,B,C,D,E,F)                 True                                                                                                     (1,1)
          2.  evalfbb9in(A,B,C,D,E,F)    -> evalfreturnin(A,B,C,D,E,F)              [1 >= B]                                                                                                 (1,1)
          3.  evalfbb9in(A,B,C,D,E,F)    -> evalfbbin(A,B,C,D,E,F)                  [B >= 2]                                                                                                 (?,1)
          4.  evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F)                  [1 + -1*B >= 0]                                                                                          (1,1)
          5.  evalfbbin(A,B,C,D,E,F)     -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F)   [-2 + B >= 0]                                                                                            (?,1)
          6.  evalfbb6in(A,B,C,D,E,F)    -> evalfbb7in(A,B,C,D,E,F)                 [-1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && 1 + -1*B + C >= 0 && -2 + B >= 0 && D >= 1 + C] (?,1)
          7.  evalfbb6in(A,B,C,D,E,F)    -> evalfbb8in(A,B,C,D,E,F)                 [-1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && 1 + -1*B + C >= 0 && -2 + B >= 0 && C >= D]     (?,1)
          8.  evalfbb7in(A,B,C,D,E,F)    -> evalfbb8in(A,B,C,D,E,F)                 [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
          9.  evalfbb7in(A,B,C,D,E,F)    -> evalfbb1in(A,B,C,D,E,F)                 [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0                                                                                               
                                                                                     && G >= 1]                                                                                                   
          10. evalfbb7in(A,B,C,D,E,F)    -> evalfbb1in(A,B,C,D,E,F)                 [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0                                                                                               
                                                                                     && 0 >= 1 + G]                                                                                               
          11. evalfbb8in(A,B,C,D,E,F)    -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) [-1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && 1 + -1*B + C >= 0 && -2 + B >= 0]               (?,1)
          12. evalfbb1in(A,B,C,D,E,F)    -> evalfbb3in(A,B,C,D,C,-1 + D)            [-2 + D >= 0                                                                                             (?,1)
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
          13. evalfbb3in(A,B,C,D,E,F)    -> evalfbb5in(A,B,C,D,E,F)                 [-1 + D + -1*F >= 0                                                                                      (?,1)
                                                                                     && -1 + F >= 0                                                                                               
                                                                                     && -2 + E + F >= 0                                                                                           
                                                                                     && -1*E + F >= 0                                                                                             
                                                                                     && -3 + D + F >= 0                                                                                           
                                                                                     && 1 + -1*D + F >= 0                                                                                         
                                                                                     && -2 + C + F >= 0                                                                                           
                                                                                     && -1*C + F >= 0                                                                                             
                                                                                     && -3 + B + F >= 0                                                                                           
                                                                                     && 1 + -1*B + F >= 0                                                                                         
                                                                                     && -1 + D + -1*E >= 0                                                                                        
                                                                                     && C + -1*E >= 0                                                                                             
                                                                                     && -1 + B + -1*E >= 0                                                                                        
                                                                                     && -1 + E >= 0                                                                                               
                                                                                     && -3 + D + E >= 0                                                                                           
                                                                                     && -2 + C + E >= 0                                                                                           
                                                                                     && -1*C + E >= 0                                                                                             
                                                                                     && -3 + B + E >= 0                                                                                           
                                                                                     && 1 + -1*B + E >= 0                                                                                         
                                                                                     && -2 + D >= 0                                                                                               
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
          14. evalfbb5in(A,B,C,D,E,F)    -> evalfbb6in(A,B,E,-1 + F,E,F)            [-1 + D + -1*F >= 0                                                                                      (?,1)
                                                                                     && -1 + F >= 0                                                                                               
                                                                                     && -2 + E + F >= 0                                                                                           
                                                                                     && -1*E + F >= 0                                                                                             
                                                                                     && -3 + D + F >= 0                                                                                           
                                                                                     && 1 + -1*D + F >= 0                                                                                         
                                                                                     && -2 + C + F >= 0                                                                                           
                                                                                     && -1*C + F >= 0                                                                                             
                                                                                     && -3 + B + F >= 0                                                                                           
                                                                                     && 1 + -1*B + F >= 0                                                                                         
                                                                                     && -1 + D + -1*E >= 0                                                                                        
                                                                                     && C + -1*E >= 0                                                                                             
                                                                                     && -1 + B + -1*E >= 0                                                                                        
                                                                                     && -1 + E >= 0                                                                                               
                                                                                     && -3 + D + E >= 0                                                                                           
                                                                                     && -2 + C + E >= 0                                                                                           
                                                                                     && -1*C + E >= 0                                                                                             
                                                                                     && -3 + B + E >= 0                                                                                           
                                                                                     && 1 + -1*B + E >= 0                                                                                         
                                                                                     && -2 + D >= 0                                                                                               
                                                                                     && -3 + C + D >= 0                                                                                           
                                                                                     && -1 + -1*C + D >= 0                                                                                        
                                                                                     && -4 + B + D >= 0                                                                                           
                                                                                     && -1*B + D >= 0                                                                                             
                                                                                     && -1 + B + -1*C >= 0                                                                                        
                                                                                     && -1 + C >= 0                                                                                               
                                                                                     && -3 + B + C >= 0                                                                                           
                                                                                     && 1 + -1*B + C >= 0                                                                                         
                                                                                     && -2 + B >= 0]                                                                                              
        Signature:
          {(evalfbb1in,6)
          ;(evalfbb3in,6)
          ;(evalfbb5in,6)
          ;(evalfbb6in,6)
          ;(evalfbb7in,6)
          ;(evalfbb8in,6)
          ;(evalfbb9in,6)
          ;(evalfbbin,6)
          ;(evalfentryin,6)
          ;(evalfreturnin,6)
          ;(evalfstart,6)
          ;(evalfstop,6)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4},3->{5},4->{},5->{6,7},6->{8,9,10},7->{11},8->{11},9->{12},10->{12},11->{2,3}
          ,12->{13},13->{14},14->{6,7}]
        
    + 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:[3,11,7,5,14,13,12,9,6,10,8] c: [14]
             |
             `- p:[3,11,7,5,8,6] c: [11]

YES