MAYBE

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

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