YES
* Step 1: FromIts YES
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D)  -> f6(E,0,C,D)                True                  (1,1)
          1. f6(A,B,C,D)  -> f10(-1 + A,1 + B,C,D)      [-1*B >= 0 && A >= 1] (?,1)
          2. f10(A,B,C,D) -> f14(A,-1 + B,-1 + A,D)     [A >= 0 && B >= 1]    (?,1)
          3. f14(A,B,C,D) -> f14(A,B,-1 + C,0)          [-1 + A + -1*C >= 0   (?,1)
                                                         && 1 + C >= 0             
                                                         && 1 + B + C >= 0         
                                                         && 1 + A + C >= 0         
                                                         && B >= 0                 
                                                         && A + B >= 0             
                                                         && A >= 0                 
                                                         && C >= 1]                
          4. f14(A,B,C,D) -> f14(-1 + A,1 + B,-1 + C,E) [-1 + A + -1*C >= 0   (?,1)
                                                         && 1 + C >= 0             
                                                         && 1 + B + C >= 0         
                                                         && 1 + A + C >= 0         
                                                         && B >= 0                 
                                                         && A + B >= 0             
                                                         && A >= 0                 
                                                         && C >= 1                 
                                                         && 0 >= 1 + E]            
          5. f14(A,B,C,D) -> f14(-1 + A,1 + B,-1 + C,E) [-1 + A + -1*C >= 0   (?,1)
                                                         && 1 + C >= 0             
                                                         && 1 + B + C >= 0         
                                                         && 1 + A + C >= 0         
                                                         && B >= 0                 
                                                         && A + B >= 0             
                                                         && A >= 0                 
                                                         && C >= 1                 
                                                         && E >= 1]                
          6. f14(A,B,C,D) -> f10(A,B,C,D)               [-1 + A + -1*C >= 0   (?,1)
                                                         && 1 + C >= 0             
                                                         && 1 + B + C >= 0         
                                                         && 1 + A + C >= 0         
                                                         && B >= 0                 
                                                         && A + B >= 0             
                                                         && A >= 0                 
                                                         && 0 >= C]                
          7. f10(A,B,C,D) -> f6(A,B,C,D)                [A >= 0 && 0 >= B]    (?,1)
          8. f6(A,B,C,D)  -> f25(A,B,C,D)               [-1*B >= 0 && 0 >= A] (?,1)
        Signature:
          {(f0,4);(f10,4);(f14,4);(f25,4);(f6,4)}
        Flow Graph:
          [0->{1,8},1->{2,7},2->{3,4,5,6},3->{3,4,5,6},4->{3,4,5,6},5->{3,4,5,6},6->{2,7},7->{1,8},8->{}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 2: Decompose YES
    + Considered Problem:
        Rules:
          f0(A,B,C,D)  -> f6(E,0,C,D)                 True
          f6(A,B,C,D)  -> f10(-1 + A,1 + B,C,D)       [-1*B >= 0 && A >= 1]
          f10(A,B,C,D) -> f14(A,-1 + B,-1 + A,D)      [A >= 0 && B >= 1]
          f14(A,B,C,D) -> f14(A,B,-1 + C,0)           [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && C >= 1]
          f14(A,B,C,D) -> f14(-1 + A,1 + B,-1 + C,E)  [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && C >= 1
                                                       && 0 >= 1 + E]
          f14(A,B,C,D) -> f14(-1 + A,1 + B,-1 + C,E)  [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && C >= 1
                                                       && E >= 1]
          f14(A,B,C,D) -> f10(A,B,C,D)                [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && 0 >= C]
          f10(A,B,C,D) -> f6(A,B,C,D)                 [A >= 0 && 0 >= B]
          f6(A,B,C,D)  -> f25(A,B,C,D)                [-1*B >= 0 && 0 >= A]
        Signature:
          {(f0,4);(f10,4);(f14,4);(f25,4);(f6,4)}
        Rule Graph:
          [0->{1,8},1->{2,7},2->{3,4,5,6},3->{3,4,5,6},4->{3,4,5,6},5->{3,4,5,6},6->{2,7},7->{1,8},8->{}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8]
          |
          `- p:[1,7,6,2,3,4,5] c: [1,7]
             |
             `- p:[2,6,3,4,5] c: [2,6]
                |
                `- p:[3,4,5] c: [5]
                   |
                   `- p:[3,4] c: [4]
                      |
                      `- p:[3] c: [3]
* Step 3: CloseWith YES
    + Considered Problem:
        (Rules:
          f0(A,B,C,D)  -> f6(E,0,C,D)                 True
          f6(A,B,C,D)  -> f10(-1 + A,1 + B,C,D)       [-1*B >= 0 && A >= 1]
          f10(A,B,C,D) -> f14(A,-1 + B,-1 + A,D)      [A >= 0 && B >= 1]
          f14(A,B,C,D) -> f14(A,B,-1 + C,0)           [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && C >= 1]
          f14(A,B,C,D) -> f14(-1 + A,1 + B,-1 + C,E)  [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && C >= 1
                                                       && 0 >= 1 + E]
          f14(A,B,C,D) -> f14(-1 + A,1 + B,-1 + C,E)  [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && C >= 1
                                                       && E >= 1]
          f14(A,B,C,D) -> f10(A,B,C,D)                [-1 + A + -1*C >= 0
                                                       && 1 + C >= 0
                                                       && 1 + B + C >= 0
                                                       && 1 + A + C >= 0
                                                       && B >= 0
                                                       && A + B >= 0
                                                       && A >= 0
                                                       && 0 >= C]
          f10(A,B,C,D) -> f6(A,B,C,D)                 [A >= 0 && 0 >= B]
          f6(A,B,C,D)  -> f25(A,B,C,D)                [-1*B >= 0 && 0 >= A]
        Signature:
          {(f0,4);(f10,4);(f14,4);(f25,4);(f6,4)}
        Rule Graph:
          [0->{1,8},1->{2,7},2->{3,4,5,6},3->{3,4,5,6},4->{3,4,5,6},5->{3,4,5,6},6->{2,7},7->{1,8},8->{}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6,7,8]
          |
          `- p:[1,7,6,2,3,4,5] c: [1,7]
             |
             `- p:[2,6,3,4,5] c: [2,6]
                |
                `- p:[3,4,5] c: [5]
                   |
                   `- p:[3,4] c: [4]
                      |
                      `- p:[3] c: [3])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES