YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G,H,I)  -> f17(0,J,K,0,E,F,G,H,I)     True      (1,1)
          1.  f17(A,B,C,D,E,F,G,H,I) -> f17(A,B,C,1 + D,E,F,G,H,I) [49 >= D] (?,1)
          2.  f27(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,1 + E,F,G,H,I) [49 >= E] (?,1)
          3.  f37(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,1 + F,G,H,I) [49 >= F] (?,1)
          4.  f45(A,B,C,D,E,F,G,H,I) -> f45(1 + A,B,C,D,E,F,G,H,I) [49 >= A] (?,1)
          5.  f55(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,1 + G,H,I) [49 >= G] (?,1)
          6.  f65(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,1 + H,I) [49 >= H] (?,1)
          7.  f75(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,1 + I) [49 >= I] (?,1)
          8.  f83(A,B,C,D,E,F,G,H,I) -> f83(1 + A,B,C,D,E,F,G,H,I) [49 >= A] (?,1)
          9.  f83(A,B,C,D,E,F,G,H,I) -> f93(A,B,C,D,E,F,G,H,I)     [A >= 50] (?,1)
          10. f75(A,B,C,D,E,F,G,H,I) -> f83(0,B,C,D,E,F,G,H,I)     [I >= 50] (?,1)
          11. f65(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,0)     [H >= 50] (?,1)
          12. f55(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,0,I)     [G >= 50] (?,1)
          13. f45(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,0,H,I)     [A >= 50] (?,1)
          14. f37(A,B,C,D,E,F,G,H,I) -> f45(0,B,C,D,E,F,G,H,I)     [F >= 50] (?,1)
          15. f27(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,0,G,H,I)     [E >= 50] (?,1)
          16. f17(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,0,F,G,H,I)     [D >= 50] (?,1)
        Signature:
          {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)}
        Flow Graph:
          [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9}
          ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,16)
                                                             ,(10,9)
                                                             ,(11,10)
                                                             ,(12,11)
                                                             ,(13,12)
                                                             ,(14,13)
                                                             ,(15,14)
                                                             ,(16,15)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C,D,E,F,G,H,I)  -> f17(0,J,K,0,E,F,G,H,I)     True      (1,1)
          1.  f17(A,B,C,D,E,F,G,H,I) -> f17(A,B,C,1 + D,E,F,G,H,I) [49 >= D] (?,1)
          2.  f27(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,1 + E,F,G,H,I) [49 >= E] (?,1)
          3.  f37(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,1 + F,G,H,I) [49 >= F] (?,1)
          4.  f45(A,B,C,D,E,F,G,H,I) -> f45(1 + A,B,C,D,E,F,G,H,I) [49 >= A] (?,1)
          5.  f55(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,1 + G,H,I) [49 >= G] (?,1)
          6.  f65(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,1 + H,I) [49 >= H] (?,1)
          7.  f75(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,1 + I) [49 >= I] (?,1)
          8.  f83(A,B,C,D,E,F,G,H,I) -> f83(1 + A,B,C,D,E,F,G,H,I) [49 >= A] (?,1)
          9.  f83(A,B,C,D,E,F,G,H,I) -> f93(A,B,C,D,E,F,G,H,I)     [A >= 50] (?,1)
          10. f75(A,B,C,D,E,F,G,H,I) -> f83(0,B,C,D,E,F,G,H,I)     [I >= 50] (?,1)
          11. f65(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,0)     [H >= 50] (?,1)
          12. f55(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,0,I)     [G >= 50] (?,1)
          13. f45(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,0,H,I)     [A >= 50] (?,1)
          14. f37(A,B,C,D,E,F,G,H,I) -> f45(0,B,C,D,E,F,G,H,I)     [F >= 50] (?,1)
          15. f27(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,0,G,H,I)     [E >= 50] (?,1)
          16. f17(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,0,F,G,H,I)     [D >= 50] (?,1)
        Signature:
          {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)}
        Flow Graph:
          [0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8}
          ,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          f0(A,B,C,D,E,F,G,H,I)  -> f17(0,J,K,0,E,F,G,H,I)      True
          f17(A,B,C,D,E,F,G,H,I) -> f17(A,B,C,1 + D,E,F,G,H,I)  [49 >= D]
          f27(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,1 + E,F,G,H,I)  [49 >= E]
          f37(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,1 + F,G,H,I)  [49 >= F]
          f45(A,B,C,D,E,F,G,H,I) -> f45(1 + A,B,C,D,E,F,G,H,I)  [49 >= A]
          f55(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,1 + G,H,I)  [49 >= G]
          f65(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,1 + H,I)  [49 >= H]
          f75(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,1 + I)  [49 >= I]
          f83(A,B,C,D,E,F,G,H,I) -> f83(1 + A,B,C,D,E,F,G,H,I)  [49 >= A]
          f83(A,B,C,D,E,F,G,H,I) -> f93(A,B,C,D,E,F,G,H,I)      [A >= 50]
          f75(A,B,C,D,E,F,G,H,I) -> f83(0,B,C,D,E,F,G,H,I)      [I >= 50]
          f65(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,0)      [H >= 50]
          f55(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,0,I)      [G >= 50]
          f45(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,0,H,I)      [A >= 50]
          f37(A,B,C,D,E,F,G,H,I) -> f45(0,B,C,D,E,F,G,H,I)      [F >= 50]
          f27(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,0,G,H,I)      [E >= 50]
          f17(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,0,F,G,H,I)      [D >= 50]
        Signature:
          {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)}
        Rule Graph:
          [0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8}
          ,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}]
    + 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,15,16]
          |
          +- p:[1] c: [1]
          |
          +- p:[2] c: [2]
          |
          +- p:[3] c: [3]
          |
          +- p:[4] c: [4]
          |
          +- p:[5] c: [5]
          |
          +- p:[6] c: [6]
          |
          +- p:[7] c: [7]
          |
          `- p:[8] c: [8]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          f0(A,B,C,D,E,F,G,H,I)  -> f17(0,J,K,0,E,F,G,H,I)      True
          f17(A,B,C,D,E,F,G,H,I) -> f17(A,B,C,1 + D,E,F,G,H,I)  [49 >= D]
          f27(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,1 + E,F,G,H,I)  [49 >= E]
          f37(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,1 + F,G,H,I)  [49 >= F]
          f45(A,B,C,D,E,F,G,H,I) -> f45(1 + A,B,C,D,E,F,G,H,I)  [49 >= A]
          f55(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,1 + G,H,I)  [49 >= G]
          f65(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,1 + H,I)  [49 >= H]
          f75(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,1 + I)  [49 >= I]
          f83(A,B,C,D,E,F,G,H,I) -> f83(1 + A,B,C,D,E,F,G,H,I)  [49 >= A]
          f83(A,B,C,D,E,F,G,H,I) -> f93(A,B,C,D,E,F,G,H,I)      [A >= 50]
          f75(A,B,C,D,E,F,G,H,I) -> f83(0,B,C,D,E,F,G,H,I)      [I >= 50]
          f65(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,0)      [H >= 50]
          f55(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,0,I)      [G >= 50]
          f45(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,0,H,I)      [A >= 50]
          f37(A,B,C,D,E,F,G,H,I) -> f45(0,B,C,D,E,F,G,H,I)      [F >= 50]
          f27(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,0,G,H,I)      [E >= 50]
          f17(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,0,F,G,H,I)      [D >= 50]
        Signature:
          {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)}
        Rule Graph:
          [0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8}
          ,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
          |
          +- p:[1] c: [1]
          |
          +- p:[2] c: [2]
          |
          +- p:[3] c: [3]
          |
          +- p:[4] c: [4]
          |
          +- p:[5] c: [5]
          |
          +- p:[6] c: [6]
          |
          +- p:[7] c: [7]
          |
          `- p:[8] c: [8])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES