MAYBE

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

Proof:
 DP Processor:
  DPs:
   c#(z,x,a()) -> f#(z)
   c#(z,x,a()) -> b#(f(z),z)
   c#(z,x,a()) -> b#(b(f(z),z),x)
   c#(z,x,a()) -> f#(b(b(f(z),z),x))
   b#(y,b(z,a())) -> f#(a())
   b#(y,b(z,a())) -> c#(f(a()),y,z)
   b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
   b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
  TRS:
   c(z,x,a()) -> f(b(b(f(z),z),x))
   b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
   f(c(c(z,a(),a()),x,a())) -> z
  TDG Processor:
   DPs:
    c#(z,x,a()) -> f#(z)
    c#(z,x,a()) -> b#(f(z),z)
    c#(z,x,a()) -> b#(b(f(z),z),x)
    c#(z,x,a()) -> f#(b(b(f(z),z),x))
    b#(y,b(z,a())) -> f#(a())
    b#(y,b(z,a())) -> c#(f(a()),y,z)
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
   TRS:
    c(z,x,a()) -> f(b(b(f(z),z),x))
    b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
    f(c(c(z,a(),a()),x,a())) -> z
   graph:
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> c#(f(a()),y,z)
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) ->
    b#(y,b(z,a())) -> f#(a())
    b#(y,b(z,a())) -> c#(f(a()),y,z) ->
    c#(z,x,a()) -> f#(b(b(f(z),z),x))
    b#(y,b(z,a())) -> c#(f(a()),y,z) ->
    c#(z,x,a()) -> b#(b(f(z),z),x)
    b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> b#(f(z),z)
    b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> f#(z)
    c#(z,x,a()) -> b#(b(f(z),z),x) ->
    b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    c#(z,x,a()) -> b#(b(f(z),z),x) ->
    b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    c#(z,x,a()) -> b#(b(f(z),z),x) ->
    b#(y,b(z,a())) -> c#(f(a()),y,z)
    c#(z,x,a()) -> b#(b(f(z),z),x) -> b#(y,b(z,a())) -> f#(a())
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> c#(f(a()),y,z)
    c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> f#(a())
   Restore Modifier:
    DPs:
     c#(z,x,a()) -> f#(z)
     c#(z,x,a()) -> b#(f(z),z)
     c#(z,x,a()) -> b#(b(f(z),z),x)
     c#(z,x,a()) -> f#(b(b(f(z),z),x))
     b#(y,b(z,a())) -> f#(a())
     b#(y,b(z,a())) -> c#(f(a()),y,z)
     b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
     b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z))
    TRS:
     c(z,x,a()) -> f(b(b(f(z),z),x))
     b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
     f(c(c(z,a(),a()),x,a())) -> z
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 16/64
     DPs:
      b#(y,b(z,a())) -> b#(c(f(a()),y,z),z)
      b#(y,b(z,a())) -> c#(f(a()),y,z)
      c#(z,x,a()) -> b#(f(z),z)
      c#(z,x,a()) -> b#(b(f(z),z),x)
     TRS:
      c(z,x,a()) -> f(b(b(f(z),z),x))
      b(y,b(z,a())) -> f(b(c(f(a()),y,z),z))
      f(c(c(z,a(),a()),x,a())) -> z
     Open