YES

Problem:
 g(A()) -> A()
 g(B()) -> A()
 g(B()) -> B()
 g(C()) -> A()
 g(C()) -> B()
 g(C()) -> C()
 foldf(x,nil()) -> x
 foldf(x,cons(y,z)) -> f(foldf(x,z),y)
 f(t,x) -> f'(t,g(x))
 f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
 f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
 f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
 f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)

Proof:
 DP Processor:
  DPs:
   foldf#(x,cons(y,z)) -> foldf#(x,z)
   foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
   f#(t,x) -> g#(x)
   f#(t,x) -> f'#(t,g(x))
   f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
   f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
   f'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
   f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
  TRS:
   g(A()) -> A()
   g(B()) -> A()
   g(B()) -> B()
   g(C()) -> A()
   g(C()) -> B()
   g(C()) -> C()
   foldf(x,nil()) -> x
   foldf(x,cons(y,z)) -> f(foldf(x,z),y)
   f(t,x) -> f'(t,g(x))
   f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
   f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
   f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
   f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
  TDG Processor:
   DPs:
    foldf#(x,cons(y,z)) -> foldf#(x,z)
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
    f#(t,x) -> g#(x)
    f#(t,x) -> f'#(t,g(x))
    f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
    f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
    f'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
    f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
   TRS:
    g(A()) -> A()
    g(B()) -> A()
    g(B()) -> B()
    g(C()) -> A()
    g(C()) -> B()
    g(C()) -> C()
    foldf(x,nil()) -> x
    foldf(x,cons(y,z)) -> f(foldf(x,z),y)
    f(t,x) -> f'(t,g(x))
    f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
    f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
    f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
    f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
   graph:
    f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c) ->
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
    f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c) ->
    foldf#(x,cons(y,z)) -> foldf#(x,z)
    f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) ->
    f#(t,x) -> f'#(t,g(x))
    f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A()) ->
    f#(t,x) -> g#(x)
    f'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b)) ->
    f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
    f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b) ->
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
    f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b) ->
    foldf#(x,cons(y,z)) -> foldf#(x,z)
    f#(t,x) -> f'#(t,g(x)) ->
    f'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
    f#(t,x) -> f'#(t,g(x)) ->
    f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
    f#(t,x) -> f'#(t,g(x)) ->
    f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y) ->
    f#(t,x) -> f'#(t,g(x))
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y) -> f#(t,x) -> g#(x)
    foldf#(x,cons(y,z)) -> foldf#(x,z) ->
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
    foldf#(x,cons(y,z)) -> foldf#(x,z) -> foldf#(x,cons(y,z)) -> foldf#(x,z)
   SCC Processor:
    #sccs: 1
    #rules: 7
    #arcs: 14/64
    DPs:
     f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
     foldf#(x,cons(y,z)) -> foldf#(x,z)
     foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
     f#(t,x) -> f'#(t,g(x))
     f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
     f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
     f'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
    TRS:
     g(A()) -> A()
     g(B()) -> A()
     g(B()) -> B()
     g(C()) -> A()
     g(C()) -> B()
     g(C()) -> C()
     foldf(x,nil()) -> x
     foldf(x,cons(y,z)) -> f(foldf(x,z),y)
     f(t,x) -> f'(t,g(x))
     f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
     f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
     f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
     f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [f''#](x0) = x0,
      
      [f'#](x0, x1) = x0 + x1,
      
      [f#](x0, x1) = x0 + 6x1 + 2,
      
      [foldf#](x0, x1) = x0 + x1,
      
      [f''](x0) = x0 + 2,
      
      [triple](x0, x1, x2) = 4x1 + x2,
      
      [f'](x0, x1) = x0 + 2,
      
      [f](x0, x1) = x0 + 2,
      
      [cons](x0, x1) = 6x0 + x1 + 2,
      
      [foldf](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [C] = 0,
      
      [B] = 2,
      
      [g](x0) = 6x0 + 2,
      
      [A] = 0
     orientation:
      f''#(triple(a,b,c)) = 4b + c >= 4b + c = foldf#(triple(a,b,nil()),c)
      
      foldf#(x,cons(y,z)) = x + 6y + z + 2 >= x + z = foldf#(x,z)
      
      foldf#(x,cons(y,z)) = x + 6y + z + 2 >= x + 6y + z + 2 = f#(foldf(x,z),y)
      
      f#(t,x) = t + 6x + 2 >= t + 6x + 2 = f'#(t,g(x))
      
      f'#(triple(a,b,c),B()) = 4b + c + 2 >= 4b + c + 2 = f#(triple(a,b,c),A())
      
      f'#(triple(a,b,c),A()) = 4b + c >= b + c = foldf#(triple(cons(A(),a),nil(),c),b)
      
      f'#(triple(a,b,c),A()) = 4b + c >= b + c = f''#(foldf(triple(cons(A(),a),nil(),c),b))
      
      g(A()) = 2 >= 0 = A()
      
      g(B()) = 14 >= 0 = A()
      
      g(B()) = 14 >= 2 = B()
      
      g(C()) = 2 >= 0 = A()
      
      g(C()) = 2 >= 2 = B()
      
      g(C()) = 2 >= 0 = C()
      
      foldf(x,nil()) = x >= x = x
      
      foldf(x,cons(y,z)) = x + 6y + z + 2 >= x + z + 2 = f(foldf(x,z),y)
      
      f(t,x) = t + 2 >= t + 2 = f'(t,g(x))
      
      f'(triple(a,b,c),C()) = 4b + c + 2 >= 4b + c + 2 = triple(a,b,cons(C(),c))
      
      f'(triple(a,b,c),B()) = 4b + c + 2 >= 4b + c + 2 = f(triple(a,b,c),A())
      
      f'(triple(a,b,c),A()) = 4b + c + 2 >= b + c + 2 = f''(foldf(triple(cons(A(),a),nil(),c),b))
      
      f''(triple(a,b,c)) = 4b + c + 2 >= 4b + c = foldf(triple(a,b,nil()),c)
     problem:
      DPs:
       f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
       foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
       f#(t,x) -> f'#(t,g(x))
       f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
       f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
       f'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
      TRS:
       g(A()) -> A()
       g(B()) -> A()
       g(B()) -> B()
       g(C()) -> A()
       g(C()) -> B()
       g(C()) -> C()
       foldf(x,nil()) -> x
       foldf(x,cons(y,z)) -> f(foldf(x,z),y)
       f(t,x) -> f'(t,g(x))
       f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
       f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
       f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
       f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [f''#](x0) = x0,
       
       [f'#](x0, x1) = x0 + x1,
       
       [f#](x0, x1) = x0 + x1,
       
       [foldf#](x0, x1) = x0 + 2x1,
       
       [f''](x0) = x0 + 2,
       
       [triple](x0, x1, x2) = 3x1 + 2x2,
       
       [f'](x0, x1) = x0 + 2x1 + 2,
       
       [f](x0, x1) = x0 + 2x1 + 2,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [foldf](x0, x1) = x0 + 2x1 + 2,
       
       [nil] = 0,
       
       [C] = 4,
       
       [B] = 4,
       
       [g](x0) = x0,
       
       [A] = 4
      orientation:
       f''#(triple(a,b,c)) = 3b + 2c >= 3b + 2c = foldf#(triple(a,b,nil()),c)
       
       foldf#(x,cons(y,z)) = x + 2y + 2z + 2 >= x + y + 2z + 2 = f#(foldf(x,z),y)
       
       f#(t,x) = t + x >= t + x = f'#(t,g(x))
       
       f'#(triple(a,b,c),B()) = 3b + 2c + 4 >= 3b + 2c + 4 = f#(triple(a,b,c),A())
       
       f'#(triple(a,b,c),A()) = 3b + 2c + 4 >= 2b + 2c = foldf#(triple(cons(A(),a),nil(),c),b)
       
       f'#(triple(a,b,c),A()) = 3b + 2c + 4 >= 2b + 2c + 2 = f''#(foldf(triple(cons(A(),a),nil(),c),b))
       
       g(A()) = 4 >= 4 = A()
       
       g(B()) = 4 >= 4 = A()
       
       g(B()) = 4 >= 4 = B()
       
       g(C()) = 4 >= 4 = A()
       
       g(C()) = 4 >= 4 = B()
       
       g(C()) = 4 >= 4 = C()
       
       foldf(x,nil()) = x + 2 >= x = x
       
       foldf(x,cons(y,z)) = x + 2y + 2z + 4 >= x + 2y + 2z + 4 = f(foldf(x,z),y)
       
       f(t,x) = t + 2x + 2 >= t + 2x + 2 = f'(t,g(x))
       
       f'(triple(a,b,c),C()) = 3b + 2c + 10 >= 3b + 2c + 10 = triple(a,b,cons(C(),c))
       
       f'(triple(a,b,c),B()) = 3b + 2c + 10 >= 3b + 2c + 10 = f(triple(a,b,c),A())
       
       f'(triple(a,b,c),A()) = 3b + 2c + 10 >= 2b + 2c + 4 = f''(foldf(triple(cons(A(),a),nil(),c),b))
       
       f''(triple(a,b,c)) = 3b + 2c + 2 >= 3b + 2c + 2 = foldf(triple(a,b,nil()),c)
      problem:
       DPs:
        f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
        foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
        f#(t,x) -> f'#(t,g(x))
        f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
       TRS:
        g(A()) -> A()
        g(B()) -> A()
        g(B()) -> B()
        g(C()) -> A()
        g(C()) -> B()
        g(C()) -> C()
        foldf(x,nil()) -> x
        foldf(x,cons(y,z)) -> f(foldf(x,z),y)
        f(t,x) -> f'(t,g(x))
        f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
        f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
        f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
        f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
      SCC Processor:
       #sccs: 1
       #rules: 2
       #arcs: 12/16
       DPs:
        f#(t,x) -> f'#(t,g(x))
        f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
       TRS:
        g(A()) -> A()
        g(B()) -> A()
        g(B()) -> B()
        g(C()) -> A()
        g(C()) -> B()
        g(C()) -> C()
        foldf(x,nil()) -> x
        foldf(x,cons(y,z)) -> f(foldf(x,z),y)
        f(t,x) -> f'(t,g(x))
        f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
        f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
        f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
        f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [f'#](x0, x1) = x1,
         
         [f#](x0, x1) = 1x1,
         
         [f''](x0) = 0,
         
         [triple](x0, x1, x2) = 0,
         
         [f'](x0, x1) = x0 + 0,
         
         [f](x0, x1) = x0 + 0,
         
         [cons](x0, x1) = 5x1 + 0,
         
         [foldf](x0, x1) = x0 + 0,
         
         [nil] = 0,
         
         [C] = 1,
         
         [B] = 1,
         
         [g](x0) = x0,
         
         [A] = 0
        orientation:
         f#(t,x) = 1x >= x = f'#(t,g(x))
         
         f'#(triple(a,b,c),B()) = 1 >= 1 = f#(triple(a,b,c),A())
         
         g(A()) = 0 >= 0 = A()
         
         g(B()) = 1 >= 0 = A()
         
         g(B()) = 1 >= 1 = B()
         
         g(C()) = 1 >= 0 = A()
         
         g(C()) = 1 >= 1 = B()
         
         g(C()) = 1 >= 1 = C()
         
         foldf(x,nil()) = x + 0 >= x = x
         
         foldf(x,cons(y,z)) = x + 0 >= x + 0 = f(foldf(x,z),y)
         
         f(t,x) = t + 0 >= t + 0 = f'(t,g(x))
         
         f'(triple(a,b,c),C()) = 0 >= 0 = triple(a,b,cons(C(),c))
         
         f'(triple(a,b,c),B()) = 0 >= 0 = f(triple(a,b,c),A())
         
         f'(triple(a,b,c),A()) = 0 >= 0 = f''(foldf(triple(cons(A(),a),nil(),c),b))
         
         f''(triple(a,b,c)) = 0 >= 0 = foldf(triple(a,b,nil()),c)
        problem:
         DPs:
          f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
         TRS:
          g(A()) -> A()
          g(B()) -> A()
          g(B()) -> B()
          g(C()) -> A()
          g(C()) -> B()
          g(C()) -> C()
          foldf(x,nil()) -> x
          foldf(x,cons(y,z)) -> f(foldf(x,z),y)
          f(t,x) -> f'(t,g(x))
          f'(triple(a,b,c),C()) -> triple(a,b,cons(C(),c))
          f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
          f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
          f''(triple(a,b,c)) -> foldf(triple(a,b,nil()),c)
        SCC Processor:
         #sccs: 0
         #rules: 0
         #arcs: 2/1