MAYBE

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

Proof:
 DP Processor:
  DPs:
   f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
   f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
   f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
   f#(b(b(x,f(y)),z)) -> f#(a())
   f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
   f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
  TRS:
   f(c(c(a(),y,a()),b(x,z),a())) -> b(y,f(c(f(a()),z,z)))
   f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
   c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
  Usable Rule Processor:
   DPs:
    f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
    f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
    f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
    f#(b(b(x,f(y)),z)) -> f#(a())
    f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
    f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
   TRS:
    f6(x,y) -> x
    f6(x,y) -> y
    f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
    c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
   TDG Processor:
    DPs:
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
     f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
     f#(b(b(x,f(y)),z)) -> f#(a())
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
     f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
    TRS:
     f6(x,y) -> x
     f6(x,y) -> y
     f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
     c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
    graph:
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
     f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
     f#(b(b(x,f(y)),z)) -> f#(a())
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
     f#(b(b(x,f(y)),z)) -> f#(a()) ->
     f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
     f#(b(b(x,f(y)),z)) -> f#(a()) ->
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
     f#(b(b(x,f(y)),z)) -> f#(a()) -> f#(b(b(x,f(y)),z)) -> f#(a())
     f#(b(b(x,f(y)),z)) -> f#(a()) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
     f#(b(b(x,f(y)),z)) -> f#(a()) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
     f#(b(b(x,f(y)),z)) -> f#(a()) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z)) ->
     f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z)) ->
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z)) ->
     f#(b(b(x,f(y)),z)) -> f#(a())
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z)) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z)) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z)) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a()) ->
     f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a()) ->
     f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a()) ->
     f#(b(b(x,f(y)),z)) -> f#(a())
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a()) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a()) ->
     f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
     f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a()) -> f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
    EDG Processor:
     DPs:
      f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
      f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
      f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
      f#(b(b(x,f(y)),z)) -> f#(a())
      f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
      f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
     TRS:
      f6(x,y) -> x
      f6(x,y) -> y
      f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
      c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
     graph:
      f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
      f#(b(b(x,f(y)),z)) -> f#(a())
      f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
      f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
      f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y)) ->
      f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
     Restore Modifier:
      DPs:
       f#(c(c(a(),y,a()),b(x,z),a())) -> f#(a())
       f#(c(c(a(),y,a()),b(x,z),a())) -> c#(f(a()),z,z)
       f#(c(c(a(),y,a()),b(x,z),a())) -> f#(c(f(a()),z,z))
       f#(b(b(x,f(y)),z)) -> f#(a())
       f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
       f#(b(b(x,f(y)),z)) -> c#(z,x,f(b(b(f(a()),y),y)))
      TRS:
       f(c(c(a(),y,a()),b(x,z),a())) -> b(y,f(c(f(a()),z,z)))
       f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
       c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
      SCC Processor:
       #sccs: 1
       #rules: 1
       #arcs: 3/36
       DPs:
        f#(b(b(x,f(y)),z)) -> f#(b(b(f(a()),y),y))
       TRS:
        f(c(c(a(),y,a()),b(x,z),a())) -> b(y,f(c(f(a()),z,z)))
        f(b(b(x,f(y)),z)) -> c(z,x,f(b(b(f(a()),y),y)))
        c(b(a(),a()),b(y,z),x) -> b(a(),b(z,z))
       Open