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