MAYBE Problem: a(x1) -> x1 a(x1) -> b(c(x1)) b(b(x1)) -> a(a(x1)) c(c(c(x1))) -> b(x1) Proof: DP Processor: DPs: a#(x1) -> c#(x1) a#(x1) -> b#(c(x1)) b#(b(x1)) -> a#(x1) b#(b(x1)) -> a#(a(x1)) c#(c(c(x1))) -> b#(x1) TRS: a(x1) -> x1 a(x1) -> b(c(x1)) b(b(x1)) -> a(a(x1)) c(c(c(x1))) -> b(x1) Open