YES
* Step 1: FromIts 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)          [0 >= 1 + E] (?,1)
          3.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2bbin(A,B,C,D)          [E >= 1]     (?,1)
          4.  evalSimpleSingle2bb4in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      True         (?,1)
          5.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb1in(A,B,C,D)         [C >= 1 + B] (?,1)
          6.  evalSimpleSingle2bbin(A,B,C,D)     -> evalSimpleSingle2bb2in(A,B,C,D)         [B >= C]     (?,1)
          7.  evalSimpleSingle2bb1in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          8.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2bb3in(A,B,C,D)         [D >= 1 + A] (?,1)
          9.  evalSimpleSingle2bb2in(A,B,C,D)    -> evalSimpleSingle2returnin(A,B,C,D)      [A >= D]     (?,1)
          10. evalSimpleSingle2bb3in(A,B,C,D)    -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D) True         (?,1)
          11. evalSimpleSingle2returnin(A,B,C,D) -> evalSimpleSingle2stop(A,B,C,D)          True         (?,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:
        FromIts
    + Details:
        ()
* Step 2: Decompose YES
    + Considered Problem:
        Rules:
          evalSimpleSingle2start(A,B,C,D)     -> evalSimpleSingle2entryin(A,B,C,D)         True
          evalSimpleSingle2entryin(A,B,C,D)   -> evalSimpleSingle2bb4in(0,0,C,D)           True
          evalSimpleSingle2bb4in(A,B,C,D)     -> evalSimpleSingle2bbin(A,B,C,D)            [0 >= 1 + E]
          evalSimpleSingle2bb4in(A,B,C,D)     -> evalSimpleSingle2bbin(A,B,C,D)            [E >= 1]
          evalSimpleSingle2bb4in(A,B,C,D)     -> evalSimpleSingle2returnin(A,B,C,D)        True
          evalSimpleSingle2bbin(A,B,C,D)      -> evalSimpleSingle2bb1in(A,B,C,D)           [C >= 1 + B]
          evalSimpleSingle2bbin(A,B,C,D)      -> evalSimpleSingle2bb2in(A,B,C,D)           [B >= C]
          evalSimpleSingle2bb1in(A,B,C,D)     -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D)   True
          evalSimpleSingle2bb2in(A,B,C,D)     -> evalSimpleSingle2bb3in(A,B,C,D)           [D >= 1 + A]
          evalSimpleSingle2bb2in(A,B,C,D)     -> evalSimpleSingle2returnin(A,B,C,D)        [A >= D]
          evalSimpleSingle2bb3in(A,B,C,D)     -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D)   True
          evalSimpleSingle2returnin(A,B,C,D)  -> evalSimpleSingle2stop(A,B,C,D)            True
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Rule 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:
        Decompose NoGreedy
    + 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: [5,7]
             |
             `- p:[2,10,8,6,3] c: [2,3,6,8,10]
* Step 3: CloseWith YES
    + Considered Problem:
        (Rules:
          evalSimpleSingle2start(A,B,C,D)     -> evalSimpleSingle2entryin(A,B,C,D)         True
          evalSimpleSingle2entryin(A,B,C,D)   -> evalSimpleSingle2bb4in(0,0,C,D)           True
          evalSimpleSingle2bb4in(A,B,C,D)     -> evalSimpleSingle2bbin(A,B,C,D)            [0 >= 1 + E]
          evalSimpleSingle2bb4in(A,B,C,D)     -> evalSimpleSingle2bbin(A,B,C,D)            [E >= 1]
          evalSimpleSingle2bb4in(A,B,C,D)     -> evalSimpleSingle2returnin(A,B,C,D)        True
          evalSimpleSingle2bbin(A,B,C,D)      -> evalSimpleSingle2bb1in(A,B,C,D)           [C >= 1 + B]
          evalSimpleSingle2bbin(A,B,C,D)      -> evalSimpleSingle2bb2in(A,B,C,D)           [B >= C]
          evalSimpleSingle2bb1in(A,B,C,D)     -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D)   True
          evalSimpleSingle2bb2in(A,B,C,D)     -> evalSimpleSingle2bb3in(A,B,C,D)           [D >= 1 + A]
          evalSimpleSingle2bb2in(A,B,C,D)     -> evalSimpleSingle2returnin(A,B,C,D)        [A >= D]
          evalSimpleSingle2bb3in(A,B,C,D)     -> evalSimpleSingle2bb4in(1 + A,1 + B,C,D)   True
          evalSimpleSingle2returnin(A,B,C,D)  -> evalSimpleSingle2stop(A,B,C,D)            True
        Signature:
          {(evalSimpleSingle2bb1in,4)
          ;(evalSimpleSingle2bb2in,4)
          ;(evalSimpleSingle2bb3in,4)
          ;(evalSimpleSingle2bb4in,4)
          ;(evalSimpleSingle2bbin,4)
          ;(evalSimpleSingle2entryin,4)
          ;(evalSimpleSingle2returnin,4)
          ;(evalSimpleSingle2start,4)
          ;(evalSimpleSingle2stop,4)}
        Rule 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->{}]
        ,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: [5,7]
             |
             `- p:[2,10,8,6,3] c: [2,3,6,8,10])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES