YES
* Step 1: UnsatPaths YES
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f6(0,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                               True         (1,1)
          1. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f6(U,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                           [63 >= B]    (?,1)
          2. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f14(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V[C >= 0]     (?,1)
                                                         ,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1,J1)                                                
          3. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f57(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V[C >= 0]     (?,1)
                                                         ,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1,J1)                                                
          4. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                             [0 >= 1 + C] (?,1)
          5. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f57(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                              [0 >= 1 + C] (?,1)
          6. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f14(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                              [B >= 64]    (?,1)
        Signature:
          {(f0,20);(f101,20);(f14,20);(f57,20);(f6,20)}
        Flow Graph:
          [0->{1,6},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3,4},6->{2,5}]
        
    + Applied Processor:
        UnsatPaths
    + Details:
        We remove following edges from the transition graph: [(0,6),(5,4),(6,5)]
* Step 2: FromIts YES
    + Considered Problem:
        Rules:
          0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f6(0,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                               True         (1,1)
          1. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f6(U,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                           [63 >= B]    (?,1)
          2. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f14(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V[C >= 0]     (?,1)
                                                         ,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1,J1)                                                
          3. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f57(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V[C >= 0]     (?,1)
                                                         ,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1,J1)                                                
          4. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                             [0 >= 1 + C] (?,1)
          5. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> f57(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                              [0 >= 1 + C] (?,1)
          6. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f14(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)                                              [B >= 64]    (?,1)
        Signature:
          {(f0,20);(f101,20);(f14,20);(f57,20);(f6,20)}
        Flow Graph:
          [0->{1},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3},6->{2}]
        
    + Applied Processor:
        FromIts
    + Details:
        ()
* Step 3: Decompose YES
    + Considered Problem:
        Rules:
          f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)   -> f6(0,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          True
          f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)   -> f6(U,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [63 >= B]
          f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f14(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1
          ,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1
          ,J1)                                                                                                                                                                                                              
          [C >= 0]
          f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f57(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1
          ,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1
          ,J1)                                                                                                                                                                                                              
          [C >= 0]
          f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [0 >= 1 + C]
          f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f57(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [0 >= 1 + C]
          f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)   -> f14(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [B >= 64]
        Signature:
          {(f0,20);(f101,20);(f14,20);(f57,20);(f6,20)}
        Rule Graph:
          [0->{1},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3},6->{2}]
    + Applied Processor:
        Decompose NoGreedy
    + Details:
        We construct a looptree:
          P: [0,1,2,3,4,5,6]
          |
          +- p:[1] c: [1]
          |
          +- p:[2] c: [2]
          |
          `- p:[3] c: [3]
* Step 4: CloseWith YES
    + Considered Problem:
        (Rules:
          f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)   -> f6(0,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          True
          f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)   -> f6(U,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [63 >= B]
          f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f14(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1
          ,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1
          ,J1)                                                                                                                                                                                                              
          [C >= 0]
          f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f57(A,B,-1 + C,U + V,W,X + Y,Z,A1 + B1,C1,D1 + E1,F1
          ,D1 + E1 + U + V,-1*D1 + -1*E1 + U + V,A1 + B1 + X + Y,-1*A1 + -1*B1 + X + Y,G1,H1,I1 + J1,J1 + K1
          ,J1)                                                                                                                                                                                                              
          [C >= 0]
          f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [0 >= 1 + C]
          f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)  -> f57(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [0 >= 1 + C]
          f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T)   -> f14(A,B,7,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S
          ,T)                                                                                                                                                                                                               
          [B >= 64]
        Signature:
          {(f0,20);(f101,20);(f14,20);(f57,20);(f6,20)}
        Rule Graph:
          [0->{1},1->{1,6},2->{2,5},3->{3,4},4->{},5->{3},6->{2}]
        ,We construct a looptree:
          P: [0,1,2,3,4,5,6]
          |
          +- p:[1] c: [1]
          |
          +- p:[2] c: [2]
          |
          `- p:[3] c: [3])
    + Applied Processor:
        CloseWith True
    + Details:
        ()

YES