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