YES
* Step 1: TrivialSCCs YES
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)    -> evalSimpleSingle2entryin(A,B,C,D)       True                                                                             (1,1)
          1.  evalSimpleSingle2entryin(A,B,C,D)  -> evalSimpleSingle2bb4in(0,0,C,D)         True                                                                             (?,1)
          2.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= 1]     (?,1)
          4.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0]               (?,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb1in(A,B,C,D)         [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb2in(A,B,C,D)         [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + C >= 0                                                                     (?,1)
                                                                                             && -1 + B + C >= 0                                                                   
                                                                                             && -1 + -1*B + C >= 0                                                                
                                                                                             && -1 + A + C >= 0                                                                   
                                                                                             && -1 + -1*A + C >= 0                                                                
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0]                                                                           
          8.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2bb3in(A,B,C,D)         [B + -1*C >= 0                                                                   (?,1)
                                                                                             && A + -1*C >= 0                                                                     
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0                                                                            
                                                                                             && D >= 1 + A]                                                                       
          9.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [B + -1*C >= 0                                                                   (?,1)
                                                                                             && A + -1*C >= 0                                                                     
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0                                                                            
                                                                                             && A >= D]                                                                           
          10. evalSimpleSingle2bb3in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + D >= 0                                                                     (?,1)
                                                                                             && -1 + -1*C + D >= 0                                                                
                                                                                             && -1 + B + D >= 0                                                                   
                                                                                             && -1 + -1*B + D >= 0                                                                
                                                                                             && -1 + A + D >= 0                                                                   
                                                                                             && -1 + -1*A + D >= 0                                                                
                                                                                             && B + -1*C >= 0                                                                     
                                                                                             && A + -1*C >= 0                                                                     
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0]                                                                           
          11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D)          [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0]               (?,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4}
          ,11->{}]
        
    + Applied Processor:
        TrivialSCCs
    + Details:
        All trivial SCCs of the transition graph admit timebound 1.
* Step 2: Looptree YES
    + Considered Problem:
        Rules:
          0.  evalSimpleSingle2start(A,B,C,D)    -> evalSimpleSingle2entryin(A,B,C,D)       True                                                                             (1,1)
          1.  evalSimpleSingle2entryin(A,B,C,D)  -> evalSimpleSingle2bb4in(0,0,C,D)         True                                                                             (1,1)
          2.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= 1]     (?,1)
          4.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0]               (1,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb1in(A,B,C,D)         [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb2in(A,B,C,D)         [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + C >= 0                                                                     (?,1)
                                                                                             && -1 + B + C >= 0                                                                   
                                                                                             && -1 + -1*B + C >= 0                                                                
                                                                                             && -1 + A + C >= 0                                                                   
                                                                                             && -1 + -1*A + C >= 0                                                                
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0]                                                                           
          8.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2bb3in(A,B,C,D)         [B + -1*C >= 0                                                                   (?,1)
                                                                                             && A + -1*C >= 0                                                                     
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0                                                                            
                                                                                             && D >= 1 + A]                                                                       
          9.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [B + -1*C >= 0                                                                   (1,1)
                                                                                             && A + -1*C >= 0                                                                     
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0                                                                            
                                                                                             && A >= D]                                                                           
          10. evalSimpleSingle2bb3in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) [-1 + D >= 0                                                                     (?,1)
                                                                                             && -1 + -1*C + D >= 0                                                                
                                                                                             && -1 + B + D >= 0                                                                   
                                                                                             && -1 + -1*B + D >= 0                                                                
                                                                                             && -1 + A + D >= 0                                                                   
                                                                                             && -1 + -1*A + D >= 0                                                                
                                                                                             && B + -1*C >= 0                                                                     
                                                                                             && A + -1*C >= 0                                                                     
                                                                                             && A + -1*B >= 0                                                                     
                                                                                             && B >= 0                                                                            
                                                                                             && A + B >= 0                                                                        
                                                                                             && -1*A + B >= 0                                                                     
                                                                                             && A >= 0]                                                                           
          11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D)          [A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0]               (1,1)
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Flow Graph:
          [0->{1},1->{2,3,4},2->{5,6},3->{5,6},4->{11},5->{7},6->{8,9},7->{2,3,4},8->{10},9->{11},10->{2,3,4}
          ,11->{}]
        
    + Applied Processor:
        Looptree
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11]
          |
          `- p:[2,7,5,3,10,8,6] c: [10]
             |
             `- p:[2,7,5,3] c: [7]

YES