YES
* Step 1: UnsatPaths 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)          [B >= 1 + C]       (?,1)
          4.  evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)          [0 >= 1 + A]       (?,1)
          5.  evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)             [C >= B && A >= 0] (?,1)
          6.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)             [0 >= 1 + D]       (?,1)
          7.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)             [D >= 1]           (?,1)
          8.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)             True               (?,1)
          9.  evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C) True               (?,1)
          10. evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)     True               (?,1)
          11. 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,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5}
          ,11->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(1,4)]
* Step 2: 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)          [B >= 1 + C]       (?,1)
          4.  evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)          [0 >= 1 + A]       (?,1)
          5.  evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)             [C >= B && A >= 0] (?,1)
          6.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)             [0 >= 1 + D]       (?,1)
          7.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)             [D >= 1]           (?,1)
          8.  evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)             True               (?,1)
          9.  evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C) True               (?,1)
          10. evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)     True               (?,1)
          11. 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,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5},11->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: 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)            [B >= 1 + C]
          evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)            [0 >= 1 + A]
          evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)               [C >= B && A >= 0]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [0 >= 1 + D]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [D >= 1]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)               True
          evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C)   True
          evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)       True
          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,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5},11->{}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11]
          |
          `- p:[5,9,6,7,10,8] c: [5,6,7,8,9,10]
* Step 4: 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)            [B >= 1 + C]
          evalaaron2bb6in(A,B,C)    -> evalaaron2returnin(A,B,C)            [0 >= 1 + A]
          evalaaron2bb6in(A,B,C)    -> evalaaron2bb3in(A,B,C)               [C >= B && A >= 0]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [0 >= 1 + D]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb4in(A,B,C)               [D >= 1]
          evalaaron2bb3in(A,B,C)    -> evalaaron2bb5in(A,B,C)               True
          evalaaron2bb4in(A,B,C)    -> evalaaron2bb6in(A,B,-1 + -1*A + C)   True
          evalaaron2bb5in(A,B,C)    -> evalaaron2bb6in(A,1 + A + B,C)       True
          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,5},2->{11},3->{11},4->{11},5->{6,7,8},6->{9},7->{9},8->{10},9->{3,4,5},10->{3,4,5},11->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11]
          |
          `- p:[5,9,6,7,10,8] c: [5,6,7,8,9,10])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES