YES
* Step 1: FromIts 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)      [0 >= 1 + E] (?,1)
          4.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)      [E >= 1]     (?,1)
          5.  evalwcet1bbin(A,B,C,D)     -> evalwcet1bb4in(A,B,C,D)      True         (?,1)
          6.  evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)      [1 + B >= A] (?,1)
          7.  evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,1 + B)  [A >= 2 + B] (?,1)
          8.  evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb5in(A,B,C,D)      [1 >= B]     (?,1)
          9.  evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,-1 + B) [B >= 2]     (?,1)
          10. evalwcet1bb5in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)      True         (?,1)
          11. evalwcet1bb6in(A,B,C,D)    -> evalwcet1bbin(A,D,-1 + C,D)  [C >= 2]     (?,1)
          12. evalwcet1bb6in(A,B,C,D)    -> evalwcet1returnin(A,B,C,D)   [1 >= C]     (?,1)
          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:
        FromIts
    + Details:
        ()
* Step 2: Decompose YES
    + Considered Problem:
        Rules:
          evalwcet1start(A,B,C,D)    -> evalwcet1entryin(A,B,C,D)     True
          evalwcet1entryin(A,B,C,D)  -> evalwcet1bbin(A,0,A,D)        [A >= 1]
          evalwcet1entryin(A,B,C,D)  -> evalwcet1returnin(A,B,C,D)    [0 >= A]
          evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)       [0 >= 1 + E]
          evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)       [E >= 1]
          evalwcet1bbin(A,B,C,D)     -> evalwcet1bb4in(A,B,C,D)       True
          evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)       [1 + B >= A]
          evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,1 + B)   [A >= 2 + B]
          evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb5in(A,B,C,D)       [1 >= B]
          evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,-1 + B)  [B >= 2]
          evalwcet1bb5in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)       True
          evalwcet1bb6in(A,B,C,D)    -> evalwcet1bbin(A,D,-1 + C,D)   [C >= 2]
          evalwcet1bb6in(A,B,C,D)    -> evalwcet1returnin(A,B,C,D)    [1 >= C]
          evalwcet1returnin(A,B,C,D) -> evalwcet1stop(A,B,C,D)        True
        Signature:
          {(evalwcet1bb1in,4)
          ;(evalwcet1bb4in,4)
          ;(evalwcet1bb5in,4)
          ;(evalwcet1bb6in,4)
          ;(evalwcet1bbin,4)
          ;(evalwcet1entryin,4)
          ;(evalwcet1returnin,4)
          ;(evalwcet1start,4)
          ;(evalwcet1stop,4)}
        Rule 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:
        Decompose NoGreedy
    + 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: [3,4,5,6,7,8,9,10,11]
* Step 3: CloseWith YES
    + Considered Problem:
        (Rules:
          evalwcet1start(A,B,C,D)    -> evalwcet1entryin(A,B,C,D)     True
          evalwcet1entryin(A,B,C,D)  -> evalwcet1bbin(A,0,A,D)        [A >= 1]
          evalwcet1entryin(A,B,C,D)  -> evalwcet1returnin(A,B,C,D)    [0 >= A]
          evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)       [0 >= 1 + E]
          evalwcet1bbin(A,B,C,D)     -> evalwcet1bb1in(A,B,C,D)       [E >= 1]
          evalwcet1bbin(A,B,C,D)     -> evalwcet1bb4in(A,B,C,D)       True
          evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)       [1 + B >= A]
          evalwcet1bb1in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,1 + B)   [A >= 2 + B]
          evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb5in(A,B,C,D)       [1 >= B]
          evalwcet1bb4in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,-1 + B)  [B >= 2]
          evalwcet1bb5in(A,B,C,D)    -> evalwcet1bb6in(A,B,C,0)       True
          evalwcet1bb6in(A,B,C,D)    -> evalwcet1bbin(A,D,-1 + C,D)   [C >= 2]
          evalwcet1bb6in(A,B,C,D)    -> evalwcet1returnin(A,B,C,D)    [1 >= C]
          evalwcet1returnin(A,B,C,D) -> evalwcet1stop(A,B,C,D)        True
        Signature:
          {(evalwcet1bb1in,4)
          ;(evalwcet1bb4in,4)
          ;(evalwcet1bb5in,4)
          ;(evalwcet1bb6in,4)
          ;(evalwcet1bbin,4)
          ;(evalwcet1entryin,4)
          ;(evalwcet1returnin,4)
          ;(evalwcet1start,4)
          ;(evalwcet1stop,4)}
        Rule 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->{}]
        ,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: [3,4,5,6,7,8,9,10,11])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES