YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0.  evalrealbubblestart(A,B,C,D)    -> evalrealbubbleentryin(A,B,C,D)    True         (1,1)
          1.  evalrealbubbleentryin(A,B,C,D)  -> evalrealbubblebb7in(-1 + A,B,C,D) True         (?,1)
          2.  evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblebb4in(A,0,0,D)      [A >= 1]     (?,1)
          3.  evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)   [0 >= A]     (?,1)
          4.  evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb1in(A,B,C,D)      [A >= 1 + B] (?,1)
          5.  evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb5in(A,B,C,D)      [B >= A]     (?,1)
          6.  evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb2in(A,B,C,D)      [E >= 1 + F] (?,1)
          7.  evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,C)      [F >= E]     (?,1)
          8.  evalrealbubblebb2in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,1)      True         (?,1)
          9.  evalrealbubblebb3in(A,B,C,D)    -> evalrealbubblebb4in(A,1 + B,D,D)  True         (?,1)
          10. evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)   [C = 0]      (?,1)
          11. evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)      [0 >= 1 + C] (?,1)
          12. evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)      [C >= 1]     (?,1)
          13. evalrealbubblebb6in(A,B,C,D)    -> evalrealbubblebb7in(-1 + A,B,C,D) True         (?,1)
          14. evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D)       True         (?,1)
        Signature:
          {(evalrealbubblebb1in,4)
          ;(evalrealbubblebb2in,4)
          ;(evalrealbubblebb3in,4)
          ;(evalrealbubblebb4in,4)
          ;(evalrealbubblebb5in,4)
          ;(evalrealbubblebb6in,4)
          ;(evalrealbubblebb7in,4)
          ;(evalrealbubbleentryin,4)
          ;(evalrealbubblereturnin,4)
          ;(evalrealbubblestart,4)
          ;(evalrealbubblestop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4,5},3->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13}
          ,12->{13},13->{2,3},14->{}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(2,5)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  evalrealbubblestart(A,B,C,D)    -> evalrealbubbleentryin(A,B,C,D)    True         (1,1)
          1.  evalrealbubbleentryin(A,B,C,D)  -> evalrealbubblebb7in(-1 + A,B,C,D) True         (?,1)
          2.  evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblebb4in(A,0,0,D)      [A >= 1]     (?,1)
          3.  evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)   [0 >= A]     (?,1)
          4.  evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb1in(A,B,C,D)      [A >= 1 + B] (?,1)
          5.  evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb5in(A,B,C,D)      [B >= A]     (?,1)
          6.  evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb2in(A,B,C,D)      [E >= 1 + F] (?,1)
          7.  evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,C)      [F >= E]     (?,1)
          8.  evalrealbubblebb2in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,1)      True         (?,1)
          9.  evalrealbubblebb3in(A,B,C,D)    -> evalrealbubblebb4in(A,1 + B,D,D)  True         (?,1)
          10. evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)   [C = 0]      (?,1)
          11. evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)      [0 >= 1 + C] (?,1)
          12. evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)      [C >= 1]     (?,1)
          13. evalrealbubblebb6in(A,B,C,D)    -> evalrealbubblebb7in(-1 + A,B,C,D) True         (?,1)
          14. evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D)       True         (?,1)
        Signature:
          {(evalrealbubblebb1in,4)
          ;(evalrealbubblebb2in,4)
          ;(evalrealbubblebb3in,4)
          ;(evalrealbubblebb4in,4)
          ;(evalrealbubblebb5in,4)
          ;(evalrealbubblebb6in,4)
          ;(evalrealbubblebb7in,4)
          ;(evalrealbubbleentryin,4)
          ;(evalrealbubblereturnin,4)
          ;(evalrealbubblestart,4)
          ;(evalrealbubblestop,4)}
        Flow Graph:
          [0->{1},1->{2,3},2->{4},3->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13}
          ,12->{13},13->{2,3},14->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          evalrealbubblestart(A,B,C,D)    -> evalrealbubbleentryin(A,B,C,D)      True
          evalrealbubbleentryin(A,B,C,D)  -> evalrealbubblebb7in(-1 + A,B,C,D)   True
          evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblebb4in(A,0,0,D)        [A >= 1]
          evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)     [0 >= A]
          evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb1in(A,B,C,D)        [A >= 1 + B]
          evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb5in(A,B,C,D)        [B >= A]
          evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb2in(A,B,C,D)        [E >= 1 + F]
          evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,C)        [F >= E]
          evalrealbubblebb2in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,1)        True
          evalrealbubblebb3in(A,B,C,D)    -> evalrealbubblebb4in(A,1 + B,D,D)    True
          evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)     [C = 0]
          evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)        [0 >= 1 + C]
          evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)        [C >= 1]
          evalrealbubblebb6in(A,B,C,D)    -> evalrealbubblebb7in(-1 + A,B,C,D)   True
          evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D)         True
        Signature:
          {(evalrealbubblebb1in,4)
          ;(evalrealbubblebb2in,4)
          ;(evalrealbubblebb3in,4)
          ;(evalrealbubblebb4in,4)
          ;(evalrealbubblebb5in,4)
          ;(evalrealbubblebb6in,4)
          ;(evalrealbubblebb7in,4)
          ;(evalrealbubbleentryin,4)
          ;(evalrealbubblereturnin,4)
          ;(evalrealbubblestart,4)
          ;(evalrealbubblestop,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4},3->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13}
          ,12->{13},13->{2,3},14->{}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
          |
          `- p:[2,13,11,5,9,7,4,8,6,12] c: [2,5,11,12,13]
             |
             `- p:[4,9,7,8,6] c: [4,6,7,8,9]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          evalrealbubblestart(A,B,C,D)    -> evalrealbubbleentryin(A,B,C,D)      True
          evalrealbubbleentryin(A,B,C,D)  -> evalrealbubblebb7in(-1 + A,B,C,D)   True
          evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblebb4in(A,0,0,D)        [A >= 1]
          evalrealbubblebb7in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)     [0 >= A]
          evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb1in(A,B,C,D)        [A >= 1 + B]
          evalrealbubblebb4in(A,B,C,D)    -> evalrealbubblebb5in(A,B,C,D)        [B >= A]
          evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb2in(A,B,C,D)        [E >= 1 + F]
          evalrealbubblebb1in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,C)        [F >= E]
          evalrealbubblebb2in(A,B,C,D)    -> evalrealbubblebb3in(A,B,C,1)        True
          evalrealbubblebb3in(A,B,C,D)    -> evalrealbubblebb4in(A,1 + B,D,D)    True
          evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblereturnin(A,B,C,D)     [C = 0]
          evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)        [0 >= 1 + C]
          evalrealbubblebb5in(A,B,C,D)    -> evalrealbubblebb6in(A,B,C,D)        [C >= 1]
          evalrealbubblebb6in(A,B,C,D)    -> evalrealbubblebb7in(-1 + A,B,C,D)   True
          evalrealbubblereturnin(A,B,C,D) -> evalrealbubblestop(A,B,C,D)         True
        Signature:
          {(evalrealbubblebb1in,4)
          ;(evalrealbubblebb2in,4)
          ;(evalrealbubblebb3in,4)
          ;(evalrealbubblebb4in,4)
          ;(evalrealbubblebb5in,4)
          ;(evalrealbubblebb6in,4)
          ;(evalrealbubblebb7in,4)
          ;(evalrealbubbleentryin,4)
          ;(evalrealbubblereturnin,4)
          ;(evalrealbubblestart,4)
          ;(evalrealbubblestop,4)}
        Rule Graph:
          [0->{1},1->{2,3},2->{4},3->{14},4->{6,7},5->{10,11,12},6->{8},7->{9},8->{9},9->{4,5},10->{14},11->{13}
          ,12->{13},13->{2,3},14->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
          |
          `- p:[2,13,11,5,9,7,4,8,6,12] c: [2,5,11,12,13]
             |
             `- p:[4,9,7,8,6] c: [4,6,7,8,9])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES