MAYBE

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

Proof:
 DP Processor:
  DPs:
   b#(x,y) -> a#(0(),x)
   b#(x,y) -> a#(c(y),a(0(),x))
   a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
   a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
   a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
  TRS:
   b(x,y) -> c(a(c(y),a(0(),x)))
   a(y,x) -> y
   a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
  CDG Processor:
   DPs:
    b#(x,y) -> a#(0(),x)
    b#(x,y) -> a#(c(y),a(0(),x))
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
   TRS:
    b(x,y) -> c(a(c(y),a(0(),x)))
    a(y,x) -> y
    a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
   graph:
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) ->
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0()) ->
    b#(x,y) -> a#(0(),x)
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0()) ->
    b#(x,y) -> a#(c(y),a(0(),x))
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y) ->
    b#(x,y) -> a#(0(),x)
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y) -> b#(x,y) -> a#(c(y),a(0(),x))
    b#(x,y) -> a#(0(),x) -> a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    b#(x,y) -> a#(0(),x) -> a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    b#(x,y) -> a#(0(),x) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
    b#(x,y) -> a#(c(y),a(0(),x)) ->
    a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
    b#(x,y) -> a#(c(y),a(0(),x)) ->
    a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
    b#(x,y) -> a#(c(y),a(0(),x)) -> a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
   Restore Modifier:
    DPs:
     b#(x,y) -> a#(0(),x)
     b#(x,y) -> a#(c(y),a(0(),x))
     a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
     a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
     a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
    TRS:
     b(x,y) -> c(a(c(y),a(0(),x)))
     a(y,x) -> y
     a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
    SCC Processor:
     #sccs: 1
     #rules: 5
     #arcs: 13/25
     DPs:
      a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x)
      a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0())
      b#(x,y) -> a#(c(y),a(0(),x))
      a#(y,c(b(a(0(),x),0()))) -> b#(0(),y)
      b#(x,y) -> a#(0(),x)
     TRS:
      b(x,y) -> c(a(c(y),a(0(),x)))
      a(y,x) -> y
      a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0())
     Open