YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)        [A >= 1 + B && C >= 0]                         (?,1)
          1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R)                [U >= 1 + T && E >= 1 && F >= 0]               (?,1)
          2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R)       [T >= U && E >= 0 && F >= 0 && H = 0]          (?,1)
          3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R)               [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] (?,1)
          4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [C >= 2 && B >= A && Y >= Z]                   (?,1)
          5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R)               True                                           (1,1)
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Flow Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0,4}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(5,4)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)        [A >= 1 + B && C >= 0]                         (?,1)
          1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R)                [U >= 1 + T && E >= 1 && F >= 0]               (?,1)
          2. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R)       [T >= U && E >= 0 && F >= 0 && H = 0]          (?,1)
          3. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R)               [X >= T && E >= 0 && F >= 0 && N = 0 && H = 0] (?,1)
          4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C) [C >= 2 && B >= A && Y >= Z]                   (?,1)
          5. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R)               True                                           (1,1)
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Flow Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)         
          [A >= 1 + B && C >= 0]
          f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R)                 
          [U >= 1 + T && E >= 1 && F >= 0]
          f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R)         [T >= U
                                                                                                                && E >= 0
                                                                                                                && F >= 0
                                                                                                                && H = 0]
          f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R)                 [X >= T
                                                                                                                && E >= 0
                                                                                                                && F >= 0
                                                                                                                && N = 0
                                                                                                                && H = 0]
          f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C)   [C >= 2
                                                                                                                && B >= A
                                                                                                                && Y >= Z]
          f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R)                 True
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Rule Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5]
          |
          +- p:[0] c: [0]
          |
          `- p:[2] c: [2]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f9(A,1 + B,1 + C,S,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)         
          [A >= 1 + B && C >= 0]
          f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f0(A,B,C,D,E,F,S,G,V,W,X,L,M,N,O,P,Q,R)                 
          [U >= 1 + T && E >= 1 && F >= 0]
          f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f5(A,B,C,D,1 + E,-1 + F,M,0,W,X,K,M,N,V,S,E,Q,R)         [T >= U
                                                                                                                && E >= 0
                                                                                                                && F >= 0
                                                                                                                && H = 0]
          f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f12(A,B,C,D,E,F,G,0,V,W,K,M,M,0,O,E,S,R)                 [X >= T
                                                                                                                && E >= 0
                                                                                                                && F >= 0
                                                                                                                && N = 0
                                                                                                                && H = 0]
          f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f5(A,B,C,D,1,-3 + C + T,S,0,U,A1,K,S,V,X,W,P,D,-2 + C)   [C >= 2
                                                                                                                && B >= A
                                                                                                                && Y >= Z]
          f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R)  -> f9(17,1,0,S,E,F,G,H,I,J,K,V,M,N,O,P,Q,R)                 True
        Signature:
          {(f0,18);(f12,18);(f5,18);(f6,18);(f9,18)}
        Rule Graph:
          [0->{0,4},1->{},2->{1,2,3},3->{},4->{1,2,3},5->{0}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5]
          |
          +- p:[0] c: [0]
          |
          `- p:[2] c: [2])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES