MAYBE
Time: 0.434499
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), A()) -> f'' foldf(triple(cons(A(), a), nil(), c), b),
  f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
  f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
       f'' triple(a, b, c) -> foldf(triple(a, b, nil()), c)}
 DP:
  DP:
   {    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), 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), B()) -> f#(triple(a, b, c), A()),
         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), A()) -> f'' foldf(triple(cons(A(), a), nil(), c), b),
   f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
   f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
        f'' triple(a, b, c) -> foldf(triple(a, b, nil()), c)}
  UR:
   {                   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), A()) -> f'' foldf(triple(cons(A(), a), nil(), c), b),
    f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
    f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
         f'' triple(a, b, c) -> foldf(triple(a, b, nil()), c)}
   EDG:
    {(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))
     (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))
     (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)
     (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()) -> foldf#(triple(cons(A(), a), nil(), c), b))
     (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), B()) -> f#(triple(a, b, c), A()))
     (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> g# x)
     (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g x))
     (f''# triple(a, b, c) -> foldf#(triple(a, b, nil()), c), foldf#(x, cons(y, z)) -> foldf#(x, z))
     (f''# triple(a, b, c) -> foldf#(triple(a, b, nil()), c), foldf#(x, cons(y, z)) -> f#(foldf(x, z), y))}
    STATUS:
     arrows: 0.781250
     SCCS (1):
      Scc:
       {    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), 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), B()) -> f#(triple(a, b, c), A()),
             f''# triple(a, b, c) -> foldf#(triple(a, b, nil()), c)}
      
      SCC (7):
       Strict:
        {    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), 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), B()) -> f#(triple(a, b, c), A()),
              f''# triple(a, b, c) -> foldf#(triple(a, b, nil()), c)}
       Weak:
       {                   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), A()) -> f'' foldf(triple(cons(A(), a), nil(), c), b),
        f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
        f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
             f'' triple(a, b, c) -> foldf(triple(a, b, nil()), c)}
       Open