MAYBE

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

Proof:
 DP Processor:
  DPs:
   b#(a(),b(c(z,x,y),a())) -> c#(y,z,a())
   b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a()))
   b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x)
   f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x)
   f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y)
   f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y))
   c#(f(c(a(),y,a())),x,z) -> b#(x,a())
   c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a()))
   c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a())))
   c#(f(c(a(),y,a())),x,z) -> b#(z,z)
   c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a()))))
   c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a())))))
  TRS:
   b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x)
   f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y))
   c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a())))))
  EDG Processor:
   DPs:
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a())
    b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a()))
    b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x)
    f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x)
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y)
    f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y))
    c#(f(c(a(),y,a())),x,z) -> b#(x,a())
    c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a()))
    c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a())))
    c#(f(c(a(),y,a())),x,z) -> b#(z,z)
    c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a()))))
    c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a())))))
   TRS:
    b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x)
    f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y))
    c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a())))))
   graph:
    f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) ->
    f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x)
    f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) ->
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y)
    f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y)) ->
    f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y))
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) ->
    c#(f(c(a(),y,a())),x,z) -> b#(x,a())
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) ->
    c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a()))
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) ->
    c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a())))
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) ->
    c#(f(c(a(),y,a())),x,z) -> b#(z,z)
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) ->
    c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a()))))
    f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y) ->
    c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a())))))
    f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) ->
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a())
    f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) ->
    b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a()))
    f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x) ->
    b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x)
    c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) ->
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a())
    c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) ->
    b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a()))
    c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a())) ->
    b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x)
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) ->
    c#(f(c(a(),y,a())),x,z) -> b#(x,a())
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) ->
    c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a()))
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) ->
    c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a())))
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) ->
    c#(f(c(a(),y,a())),x,z) -> b#(z,z)
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) ->
    c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a()))))
    b#(a(),b(c(z,x,y),a())) -> c#(y,z,a()) ->
    c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a())))))
   Restore Modifier:
    DPs:
     b#(a(),b(c(z,x,y),a())) -> c#(y,z,a())
     b#(a(),b(c(z,x,y),a())) -> b#(z,c(y,z,a()))
     b#(a(),b(c(z,x,y),a())) -> b#(b(z,c(y,z,a())),x)
     f#(c(a(),b(b(z,a()),y),x)) -> b#(z,x)
     f#(c(a(),b(b(z,a()),y),x)) -> c#(x,b(z,x),y)
     f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y))
     c#(f(c(a(),y,a())),x,z) -> b#(x,a())
     c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a()))
     c#(f(c(a(),y,a())),x,z) -> f#(b(y,b(x,a())))
     c#(f(c(a(),y,a())),x,z) -> b#(z,z)
     c#(f(c(a(),y,a())),x,z) -> b#(b(z,z),f(b(y,b(x,a()))))
     c#(f(c(a(),y,a())),x,z) -> f#(b(b(z,z),f(b(y,b(x,a())))))
    TRS:
     b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x)
     f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y))
     c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a())))))
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 21/144
     DPs:
      f#(c(a(),b(b(z,a()),y),x)) -> f#(c(x,b(z,x),y))
     TRS:
      b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x)
      f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y))
      c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a())))))
     Open
     
     DPs:
      c#(f(c(a(),y,a())),x,z) -> b#(y,b(x,a()))
      b#(a(),b(c(z,x,y),a())) -> c#(y,z,a())
     TRS:
      b(a(),b(c(z,x,y),a())) -> b(b(z,c(y,z,a())),x)
      f(c(a(),b(b(z,a()),y),x)) -> f(c(x,b(z,x),y))
      c(f(c(a(),y,a())),x,z) -> f(b(b(z,z),f(b(y,b(x,a())))))
     Open