MAYBE

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)
  EDG 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)) -> foldf#(x,z)
    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),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),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)) -> foldf#(x,z)
    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#(t,x) -> f'#(t,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),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))
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y) ->
    f#(t,x) -> g#(x)
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y) ->
    f#(t,x) -> f'#(t,g(x))
    foldf#(x,cons(y,z)) -> foldf#(x,z) ->
    foldf#(x,cons(y,z)) -> foldf#(x,z)
    foldf#(x,cons(y,z)) -> foldf#(x,z) -> foldf#(x,cons(y,z)) -> f#(foldf(x,z),y)
   Restore Modifier:
    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)
    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)) -> 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),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
      foldf#(x,cons(y,z)) -> foldf#(x,z)
      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)
     Open