YES
* Step 1: FromIts YES
    + Considered Problem:
        Rules:
          0.  evalaaron2start(A,B,C)    -> evalaaron2entryin(A,B,C)           True                                    (1,1)
          1.  evalaaron2entryin(A,B,C)  -> evalaaron2bb6in(A,C,B)             [A >= 0]                                (?,1)
          2.  evalaaron2entryin(A,B,C)  -> evalaaron2returnin(A,B,C)          [0 >= 1 + A]                            (?,1)
          3.  evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)          [A >= 0 && B >= 1 + C]                  (?,1)
          4.  evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)             [A >= 0 && C >= B]                      (?,1)
          5.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)             [-1*B + C >= 0 && A >= 0 && 0 >= 1 + D] (?,1)
          6.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)             [-1*B + C >= 0 && A >= 0 && D >= 1]     (?,1)
          7.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)             [-1*B + C >= 0 && A >= 0]               (?,1)
          8.  evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C) [-1*B + C >= 0 && A >= 0]               (?,1)
          9.  evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)     [-1*B + C >= 0 && A >= 0]               (?,1)
          10. evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C)              True                                    (?,1)
        Signature:
          {(evalaaron2bb3in,3)
          ;(evalaaron2bb4in,3)
          ;(evalaaron2bb5in,3)
          ;(evalaaron2bb6in,3)
          ;(evalaaron2entryin,3)
          ;(evalaaron2returnin,3)
          ;(evalaaron2start,3)
          ;(evalaaron2stop,3)}
        Flow Graph:
          [0->{1,2},1->{3,4},2->{10},3->{10},4->{5,6,7},5->{8},6->{8},7->{9},8->{3,4},9->{3,4},10->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: Decompose YES
    + Considered Problem:
        Rules:
          evalaaron2start(A,B,C)    -> evalaaron2entryin(A,B,C)             True
          evalaaron2entryin(A,B,C)  -> evalaaron2bb6in(A,C,B)               [A >= 0]
          evalaaron2entryin(A,B,C)  -> evalaaron2returnin(A,B,C)            [0 >= 1 + A]
          evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)            [A >= 0 && B >= 1 + C]
          evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)               [A >= 0 && C >= B]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [-1*B + C >= 0 && A >= 0 && 0 >= 1 + D]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [-1*B + C >= 0 && A >= 0 && D >= 1]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)               [-1*B + C >= 0 && A >= 0]
          evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C)   [-1*B + C >= 0 && A >= 0]
          evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)       [-1*B + C >= 0 && A >= 0]
          evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C)                True
        Signature:
          {(evalaaron2bb3in,3)
          ;(evalaaron2bb4in,3)
          ;(evalaaron2bb5in,3)
          ;(evalaaron2bb6in,3)
          ;(evalaaron2entryin,3)
          ;(evalaaron2returnin,3)
          ;(evalaaron2start,3)
          ;(evalaaron2stop,3)}
        Rule Graph:
          [0->{1,2},1->{3,4},2->{10},3->{10},4->{5,6,7},5->{8},6->{8},7->{9},8->{3,4},9->{3,4},10->{}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10]
          |
          `- p:[4,8,5,6,9,7] c: [7,9]
             |
             `- p:[4,8,5,6] c: [4,5,6,8]
* Step 3: CloseWith YES
    + Considered Problem:
        (Rules:
          evalaaron2start(A,B,C)    -> evalaaron2entryin(A,B,C)             True
          evalaaron2entryin(A,B,C)  -> evalaaron2bb6in(A,C,B)               [A >= 0]
          evalaaron2entryin(A,B,C)  -> evalaaron2returnin(A,B,C)            [0 >= 1 + A]
          evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)            [A >= 0 && B >= 1 + C]
          evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)               [A >= 0 && C >= B]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [-1*B + C >= 0 && A >= 0 && 0 >= 1 + D]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [-1*B + C >= 0 && A >= 0 && D >= 1]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)               [-1*B + C >= 0 && A >= 0]
          evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C)   [-1*B + C >= 0 && A >= 0]
          evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)       [-1*B + C >= 0 && A >= 0]
          evalaaron2returnin(A,B,C) -> evalaaron2stop(A,B,C)                True
        Signature:
          {(evalaaron2bb3in,3)
          ;(evalaaron2bb4in,3)
          ;(evalaaron2bb5in,3)
          ;(evalaaron2bb6in,3)
          ;(evalaaron2entryin,3)
          ;(evalaaron2returnin,3)
          ;(evalaaron2start,3)
          ;(evalaaron2stop,3)}
        Rule Graph:
          [0->{1,2},1->{3,4},2->{10},3->{10},4->{5,6,7},5->{8},6->{8},7->{9},8->{3,4},9->{3,4},10->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10]
          |
          `- p:[4,8,5,6,9,7] c: [7,9]
             |
             `- p:[4,8,5,6] c: [4,5,6,8])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES