YES
* Step 1: TrivialSCCs YES
    + Considered Problem:
        Rules:
          0.  evalwcet1start(A,B,C,D)    -> evalwcet1entryin(A,B,C,D)    True                   (1,1)
          1.  evalwcet1entryin(A,B,C,D)  -> evalwcet1bbin(A,0,A,D)       [A >= 1]               (?,1)
          2.  evalwcet1entryin(A,B,C,D)  -> evalwcet1returnin(A,B,C,D)   [0 >= A]               (?,1)
          3.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 0 >= 1 + E]             
          4.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && E >= 1]                 
          5.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb4in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0]            
          6.  evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 1 + B >= A]             
          7.  evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,1 + B)  [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && A >= 2 + B]             
          8.  evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb5in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 1 >= B]                 
          9.  evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,-1 + B) [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && B >= 2]                 
          10. evalwcet1bb5in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -1*B + C >= 0           
                                                                          && -2 + A + C >= 0         
                                                                          && 1 + -1*B >= 0           
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0]            
          11. evalwcet1bb6in(A,B,C,D)    -> evalwcet1bbin(A,D,-1 + C,D)  [1 + B + -1*D >= 0     (?,1)
                                                                          && -1 + A + -1*D >= 0      
                                                                          && D >= 0                  
                                                                          && -1 + C + D >= 0         
                                                                          && B + D >= 0              
                                                                          && -1 + A + D >= 0         
                                                                          && A + -1*C >= 0           
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && C >= 2]                 
          12. evalwcet1bb6in(A,B,C,D)    -> evalwcet1returnin(A,B,C,D)   [1 + B + -1*D >= 0     (?,1)
                                                                          && -1 + A + -1*D >= 0      
                                                                          && D >= 0                  
                                                                          && -1 + C + D >= 0         
                                                                          && B + D >= 0              
                                                                          && -1 + A + D >= 0         
                                                                          && A + -1*C >= 0           
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 1 >= C]                 
          13. evalwcet1returnin(A,B,C,D) -> evalwcet1stop(A,B,C,D)       True                   (?,1)
        Signature:
          {(evalwcet1bb1in,4)
          ;(evalwcet1bb4in,4)
          ;(evalwcet1bb5in,4)
          ;(evalwcet1bb6in,4)
          ;(evalwcet1bbin,4)
          ;(evalwcet1entryin,4)
          ;(evalwcet1returnin,4)
          ;(evalwcet1start,4)
          ;(evalwcet1stop,4)}
        Flow Graph:
          [0->{1,2},1->{3,4,5},2->{13},3->{6,7},4->{6,7},5->{8,9},6->{11,12},7->{11,12},8->{10},9->{11,12},10->{11
          ,12},11->{3,4,5},12->{13},13->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: Looptree YES
    + Considered Problem:
        Rules:
          0.  evalwcet1start(A,B,C,D)    -> evalwcet1entryin(A,B,C,D)    True                   (1,1)
          1.  evalwcet1entryin(A,B,C,D)  -> evalwcet1bbin(A,0,A,D)       [A >= 1]               (1,1)
          2.  evalwcet1entryin(A,B,C,D)  -> evalwcet1returnin(A,B,C,D)   [0 >= A]               (1,1)
          3.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 0 >= 1 + E]             
          4.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && E >= 1]                 
          5.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb4in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0]            
          6.  evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 1 + B >= A]             
          7.  evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,1 + B)  [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && A >= 2 + B]             
          8.  evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb5in(A,B,C,D)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 1 >= B]                 
          9.  evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,-1 + B) [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && B >= 2]                 
          10. evalwcet1bb5in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)      [A + -1*C >= 0         (?,1)
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -1*B + C >= 0           
                                                                          && -2 + A + C >= 0         
                                                                          && 1 + -1*B >= 0           
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0]            
          11. evalwcet1bb6in(A,B,C,D)    -> evalwcet1bbin(A,D,-1 + C,D)  [1 + B + -1*D >= 0     (?,1)
                                                                          && -1 + A + -1*D >= 0      
                                                                          && D >= 0                  
                                                                          && -1 + C + D >= 0         
                                                                          && B + D >= 0              
                                                                          && -1 + A + D >= 0         
                                                                          && A + -1*C >= 0           
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && C >= 2]                 
          12. evalwcet1bb6in(A,B,C,D)    -> evalwcet1returnin(A,B,C,D)   [1 + B + -1*D >= 0     (1,1)
                                                                          && -1 + A + -1*D >= 0      
                                                                          && D >= 0                  
                                                                          && -1 + C + D >= 0         
                                                                          && B + D >= 0              
                                                                          && -1 + A + D >= 0         
                                                                          && A + -1*C >= 0           
                                                                          && -1 + C >= 0             
                                                                          && -1 + B + C >= 0         
                                                                          && -2 + A + C >= 0         
                                                                          && -1 + A + -1*B >= 0      
                                                                          && B >= 0                  
                                                                          && -1 + A + B >= 0         
                                                                          && -1 + A >= 0             
                                                                          && 1 >= C]                 
          13. evalwcet1returnin(A,B,C,D) -> evalwcet1stop(A,B,C,D)       True                   (1,1)
        Signature:
          {(evalwcet1bb1in,4)
          ;(evalwcet1bb4in,4)
          ;(evalwcet1bb5in,4)
          ;(evalwcet1bb6in,4)
          ;(evalwcet1bbin,4)
          ;(evalwcet1entryin,4)
          ;(evalwcet1returnin,4)
          ;(evalwcet1start,4)
          ;(evalwcet1stop,4)}
        Flow Graph:
          [0->{1,2},1->{3,4,5},2->{13},3->{6,7},4->{6,7},5->{8,9},6->{11,12},7->{11,12},8->{10},9->{11,12},10->{11
          ,12},11->{3,4,5},12->{13},13->{}]
        
    + Applied Processor:
        Looptree
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13]
          |
          `- p:[3,11,6,4,7,9,5,10,8] c: [11]

YES