MAYBE Problem: f() -> b() b() -> f() Proof: DP Processor: DPs: f#() -> b#() b#() -> f#() TRS: f() -> b() b() -> f() Usable Rule Processor: DPs: f#() -> b#() b#() -> f#() TRS: Open