YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C)  -> f10(1,B,C)     True     (1,1)
          1.  f10(A,B,C) -> f13(A,1,C)     [5 >= A] (?,1)
          2.  f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1)
          3.  f21(A,B,C) -> f24(A,1,C)     [5 >= A] (?,1)
          4.  f24(A,B,C) -> f27(A,B,1)     [5 >= B] (?,1)
          5.  f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1)
          6.  f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1)
          7.  f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1)
          8.  f21(A,B,C) -> f39(A,B,C)     [A >= 6] (?,1)
          9.  f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1)
          10. f10(A,B,C) -> f21(1,B,C)     [A >= 6] (?,1)
        Signature:
          {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)}
        Flow Graph:
          [0->{1,10},1->{2,9},2->{2,9},3->{4,7},4->{5,6},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3,8}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,10),(1,9),(3,7),(4,6),(10,8)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0.  f0(A,B,C)  -> f10(1,B,C)     True     (1,1)
          1.  f10(A,B,C) -> f13(A,1,C)     [5 >= A] (?,1)
          2.  f13(A,B,C) -> f13(A,1 + B,C) [5 >= B] (?,1)
          3.  f21(A,B,C) -> f24(A,1,C)     [5 >= A] (?,1)
          4.  f24(A,B,C) -> f27(A,B,1)     [5 >= B] (?,1)
          5.  f27(A,B,C) -> f27(A,B,1 + C) [5 >= C] (?,1)
          6.  f27(A,B,C) -> f24(A,1 + B,C) [C >= 6] (?,1)
          7.  f24(A,B,C) -> f21(1 + A,B,C) [B >= 6] (?,1)
          8.  f21(A,B,C) -> f39(A,B,C)     [A >= 6] (?,1)
          9.  f13(A,B,C) -> f10(1 + A,B,C) [B >= 6] (?,1)
          10. f10(A,B,C) -> f21(1,B,C)     [A >= 6] (?,1)
        Signature:
          {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)}
        Flow Graph:
          [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          f0(A,B,C)  -> f10(1,B,C)      True
          f10(A,B,C) -> f13(A,1,C)      [5 >= A]
          f13(A,B,C) -> f13(A,1 + B,C)  [5 >= B]
          f21(A,B,C) -> f24(A,1,C)      [5 >= A]
          f24(A,B,C) -> f27(A,B,1)      [5 >= B]
          f27(A,B,C) -> f27(A,B,1 + C)  [5 >= C]
          f27(A,B,C) -> f24(A,1 + B,C)  [C >= 6]
          f24(A,B,C) -> f21(1 + A,B,C)  [B >= 6]
          f21(A,B,C) -> f39(A,B,C)      [A >= 6]
          f13(A,B,C) -> f10(1 + A,B,C)  [B >= 6]
          f10(A,B,C) -> f21(1,B,C)      [A >= 6]
        Signature:
          {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)}
        Rule Graph:
          [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10]
          |
          +- p:[1,9,2] c: [1,9]
          |  |
          |  `- p:[2] c: [2]
          |
          `- p:[3,7,6,5,4] c: [3,7]
             |
             `- p:[4,6,5] c: [4,6]
                |
                `- p:[5] c: [5]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          f0(A,B,C)  -> f10(1,B,C)      True
          f10(A,B,C) -> f13(A,1,C)      [5 >= A]
          f13(A,B,C) -> f13(A,1 + B,C)  [5 >= B]
          f21(A,B,C) -> f24(A,1,C)      [5 >= A]
          f24(A,B,C) -> f27(A,B,1)      [5 >= B]
          f27(A,B,C) -> f27(A,B,1 + C)  [5 >= C]
          f27(A,B,C) -> f24(A,1 + B,C)  [C >= 6]
          f24(A,B,C) -> f21(1 + A,B,C)  [B >= 6]
          f21(A,B,C) -> f39(A,B,C)      [A >= 6]
          f13(A,B,C) -> f10(1 + A,B,C)  [B >= 6]
          f10(A,B,C) -> f21(1,B,C)      [A >= 6]
        Signature:
          {(f0,3);(f10,3);(f13,3);(f21,3);(f24,3);(f27,3);(f39,3)}
        Rule Graph:
          [0->{1},1->{2},2->{2,9},3->{4},4->{5},5->{5,6},6->{4,7},7->{3,8},8->{},9->{1,10},10->{3}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8,9,10]
          |
          +- p:[1,9,2] c: [1,9]
          |  |
          |  `- p:[2] c: [2]
          |
          `- p:[3,7,6,5,4] c: [3,7]
             |
             `- p:[4,6,5] c: [4,6]
                |
                `- p:[5] c: [5])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES