YES
* Step 1: UnsatRules YES
    + Considered Problem:
        Rules:
          0.  evalEx1start(A,B,C,D)    -> evalEx1entryin(A,B,C,D)        True                   (1,1)
          1.  evalEx1entryin(A,B,C,D)  -> evalEx1bb6in(0,A,C,D)          True                   (?,1)
          2.  evalEx1bb6in(A,B,C,D)    -> evalEx1bbin(A,B,C,D)           [B >= 1 + A]           (?,1)
          3.  evalEx1bb6in(A,B,C,D)    -> evalEx1returnin(A,B,C,D)       [A >= B]               (?,1)
          4.  evalEx1bbin(A,B,C,D)     -> evalEx1bb4in(A,B,1 + A,B)      True                   (?,1)
          5.  evalEx1bb4in(A,B,C,D)    -> evalEx1bb1in(A,B,C,D)          [D >= 1 + C]           (?,1)
          6.  evalEx1bb4in(A,B,C,D)    -> evalEx1bb5in(A,B,C,D)          [C >= D]               (?,1)
          7.  evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)     [0 >= 1 + E]           (?,1)
          8.  evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)     [0 >= 1 + E && E >= 1] (?,1)
          9.  evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)     [E >= 1]               (?,1)
          10. evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,D)          [0 >= 1]               (?,1)
          11. evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,D)          [0 >= 1]               (?,1)
          12. evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,1 + C,-1 + D) [0 >= 1]               (?,1)
          13. evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,1 + C,-1 + D) [0 >= 1]               (?,1)
          14. evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,1 + C,D)      True                   (?,1)
          15. evalEx1bb5in(A,B,C,D)    -> evalEx1bb6in(1 + A,D,C,D)      True                   (?,1)
          16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D)           True                   (?,1)
        Signature:
          {(evalEx1bb1in,4)
          ;(evalEx1bb4in,4)
          ;(evalEx1bb5in,4)
          ;(evalEx1bb6in,4)
          ;(evalEx1bbin,4)
          ;(evalEx1entryin,4)
          ;(evalEx1returnin,4)
          ;(evalEx1start,4)
          ;(evalEx1stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,8,9,10,11,12,13,14},6->{15},7->{5,6},8->{5,6},9->{5,6}
          ,10->{5,6},11->{5,6},12->{5,6},13->{5,6},14->{5,6},15->{2,3},16->{}]
        
    + Applied Processor:
        UnsatRules
    + Details:
        Following transitions have unsatisfiable constraints and are removed:  [8,10,11,12,13]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  evalEx1start(A,B,C,D)    -> evalEx1entryin(A,B,C,D)    True         (1,1)
          1.  evalEx1entryin(A,B,C,D)  -> evalEx1bb6in(0,A,C,D)      True         (?,1)
          2.  evalEx1bb6in(A,B,C,D)    -> evalEx1bbin(A,B,C,D)       [B >= 1 + A] (?,1)
          3.  evalEx1bb6in(A,B,C,D)    -> evalEx1returnin(A,B,C,D)   [A >= B]     (?,1)
          4.  evalEx1bbin(A,B,C,D)     -> evalEx1bb4in(A,B,1 + A,B)  True         (?,1)
          5.  evalEx1bb4in(A,B,C,D)    -> evalEx1bb1in(A,B,C,D)      [D >= 1 + C] (?,1)
          6.  evalEx1bb4in(A,B,C,D)    -> evalEx1bb5in(A,B,C,D)      [C >= D]     (?,1)
          7.  evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D) [0 >= 1 + E] (?,1)
          9.  evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D) [E >= 1]     (?,1)
          14. evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,1 + C,D)  True         (?,1)
          15. evalEx1bb5in(A,B,C,D)    -> evalEx1bb6in(1 + A,D,C,D)  True         (?,1)
          16. evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D)       True         (?,1)
        Signature:
          {(evalEx1bb1in,4)
          ;(evalEx1bb4in,4)
          ;(evalEx1bb5in,4)
          ;(evalEx1bb6in,4)
          ;(evalEx1bbin,4)
          ;(evalEx1entryin,4)
          ;(evalEx1returnin,4)
          ;(evalEx1start,4)
          ;(evalEx1stop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,9,14},6->{15},7->{5,6},9->{5,6},14->{5,6},15->{2,3},16->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          evalEx1start(A,B,C,D)    -> evalEx1entryin(A,B,C,D)     True
          evalEx1entryin(A,B,C,D)  -> evalEx1bb6in(0,A,C,D)       True
          evalEx1bb6in(A,B,C,D)    -> evalEx1bbin(A,B,C,D)        [B >= 1 + A]
          evalEx1bb6in(A,B,C,D)    -> evalEx1returnin(A,B,C,D)    [A >= B]
          evalEx1bbin(A,B,C,D)     -> evalEx1bb4in(A,B,1 + A,B)   True
          evalEx1bb4in(A,B,C,D)    -> evalEx1bb1in(A,B,C,D)       [D >= 1 + C]
          evalEx1bb4in(A,B,C,D)    -> evalEx1bb5in(A,B,C,D)       [C >= D]
          evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)  [0 >= 1 + E]
          evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)  [E >= 1]
          evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,1 + C,D)   True
          evalEx1bb5in(A,B,C,D)    -> evalEx1bb6in(1 + A,D,C,D)   True
          evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D)        True
        Signature:
          {(evalEx1bb1in,4)
          ;(evalEx1bb4in,4)
          ;(evalEx1bb5in,4)
          ;(evalEx1bb6in,4)
          ;(evalEx1bbin,4)
          ;(evalEx1entryin,4)
          ;(evalEx1returnin,4)
          ;(evalEx1start,4)
          ;(evalEx1stop,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,9,14},6->{15},7->{5,6},9->{5,6},14->{5,6},15->{2,3},16->{}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,9,14,15,16]
          |
          `- p:[2,15,6,4,7,5,9,14] c: [2,4,6,15]
             |
             `- p:[5,7,9,14] c: [5,7,9,14]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          evalEx1start(A,B,C,D)    -> evalEx1entryin(A,B,C,D)     True
          evalEx1entryin(A,B,C,D)  -> evalEx1bb6in(0,A,C,D)       True
          evalEx1bb6in(A,B,C,D)    -> evalEx1bbin(A,B,C,D)        [B >= 1 + A]
          evalEx1bb6in(A,B,C,D)    -> evalEx1returnin(A,B,C,D)    [A >= B]
          evalEx1bbin(A,B,C,D)     -> evalEx1bb4in(A,B,1 + A,B)   True
          evalEx1bb4in(A,B,C,D)    -> evalEx1bb1in(A,B,C,D)       [D >= 1 + C]
          evalEx1bb4in(A,B,C,D)    -> evalEx1bb5in(A,B,C,D)       [C >= D]
          evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)  [0 >= 1 + E]
          evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,C,-1 + D)  [E >= 1]
          evalEx1bb1in(A,B,C,D)    -> evalEx1bb4in(A,B,1 + C,D)   True
          evalEx1bb5in(A,B,C,D)    -> evalEx1bb6in(1 + A,D,C,D)   True
          evalEx1returnin(A,B,C,D) -> evalEx1stop(A,B,C,D)        True
        Signature:
          {(evalEx1bb1in,4)
          ;(evalEx1bb4in,4)
          ;(evalEx1bb5in,4)
          ;(evalEx1bb6in,4)
          ;(evalEx1bbin,4)
          ;(evalEx1entryin,4)
          ;(evalEx1returnin,4)
          ;(evalEx1start,4)
          ;(evalEx1stop,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4},3->{16},4->{5,6},5->{7,9,14},6->{15},7->{5,6},9->{5,6},14->{5,6},15->{2,3},16->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,9,14,15,16]
          |
          `- p:[2,15,6,4,7,5,9,14] c: [2,4,6,15]
             |
             `- p:[5,7,9,14] c: [5,7,9,14])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES