MAYBE

Problem:
 c(c(z,y,a()),a(),a()) -> b(z,y)
 f(c(x,y,z)) -> c(z,f(b(y,z)),a())
 b(z,b(c(a(),y,a()),f(f(x)))) -> c(c(y,a(),z),z,x)

Proof:
 DP Processor:
  DPs:
   c#(c(z,y,a()),a(),a()) -> b#(z,y)
   f#(c(x,y,z)) -> b#(y,z)
   f#(c(x,y,z)) -> f#(b(y,z))
   f#(c(x,y,z)) -> c#(z,f(b(y,z)),a())
   b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z)
   b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x)
  TRS:
   c(c(z,y,a()),a(),a()) -> b(z,y)
   f(c(x,y,z)) -> c(z,f(b(y,z)),a())
   b(z,b(c(a(),y,a()),f(f(x)))) -> c(c(y,a(),z),z,x)
  CDG Processor:
   DPs:
    c#(c(z,y,a()),a(),a()) -> b#(z,y)
    f#(c(x,y,z)) -> b#(y,z)
    f#(c(x,y,z)) -> f#(b(y,z))
    f#(c(x,y,z)) -> c#(z,f(b(y,z)),a())
    b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z)
    b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x)
   TRS:
    c(c(z,y,a()),a(),a()) -> b(z,y)
    f(c(x,y,z)) -> c(z,f(b(y,z)),a())
    b(z,b(c(a(),y,a()),f(f(x)))) -> c(c(y,a(),z),z,x)
   graph:
    f#(c(x,y,z)) -> f#(b(y,z)) -> f#(c(x,y,z)) -> b#(y,z)
    f#(c(x,y,z)) -> f#(b(y,z)) -> f#(c(x,y,z)) -> f#(b(y,z))
    f#(c(x,y,z)) -> f#(b(y,z)) -> f#(c(x,y,z)) -> c#(z,f(b(y,z)),a())
    f#(c(x,y,z)) -> b#(y,z) -> b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z)
    f#(c(x,y,z)) -> b#(y,z) ->
    b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x)
    b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x) ->
    c#(c(z,y,a()),a(),a()) -> b#(z,y)
    b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z) ->
    c#(c(z,y,a()),a(),a()) -> b#(z,y)
    c#(c(z,y,a()),a(),a()) -> b#(z,y) ->
    b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z)
    c#(c(z,y,a()),a(),a()) -> b#(z,y) -> b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x)
   Restore Modifier:
    DPs:
     c#(c(z,y,a()),a(),a()) -> b#(z,y)
     f#(c(x,y,z)) -> b#(y,z)
     f#(c(x,y,z)) -> f#(b(y,z))
     f#(c(x,y,z)) -> c#(z,f(b(y,z)),a())
     b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z)
     b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x)
    TRS:
     c(c(z,y,a()),a(),a()) -> b(z,y)
     f(c(x,y,z)) -> c(z,f(b(y,z)),a())
     b(z,b(c(a(),y,a()),f(f(x)))) -> c(c(y,a(),z),z,x)
    SCC Processor:
     #sccs: 2
     #rules: 4
     #arcs: 9/36
     DPs:
      f#(c(x,y,z)) -> f#(b(y,z))
     TRS:
      c(c(z,y,a()),a(),a()) -> b(z,y)
      f(c(x,y,z)) -> c(z,f(b(y,z)),a())
      b(z,b(c(a(),y,a()),f(f(x)))) -> c(c(y,a(),z),z,x)
     Open
     
     DPs:
      b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(c(y,a(),z),z,x)
      c#(c(z,y,a()),a(),a()) -> b#(z,y)
      b#(z,b(c(a(),y,a()),f(f(x)))) -> c#(y,a(),z)
     TRS:
      c(c(z,y,a()),a(),a()) -> b(z,y)
      f(c(x,y,z)) -> c(z,f(b(y,z)),a())
      b(z,b(c(a(),y,a()),f(f(x)))) -> c(c(y,a(),z),z,x)
     Open