MAYBE Problem: f(g(x,y),x,z) -> f(z,z,z) g(x,y) -> x g(x,y) -> y Proof: DP Processor: DPs: f#(g(x,y),x,z) -> f#(z,z,z) TRS: f(g(x,y),x,z) -> f(z,z,z) g(x,y) -> x g(x,y) -> y Usable Rule Processor: DPs: f#(g(x,y),x,z) -> f#(z,z,z) TRS: f4(x,y) -> x f4(x,y) -> y Restore Modifier: DPs: f#(g(x,y),x,z) -> f#(z,z,z) TRS: f(g(x,y),x,z) -> f(z,z,z) g(x,y) -> x g(x,y) -> y SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(g(x,y),x,z) -> f#(z,z,z) TRS: f(g(x,y),x,z) -> f(z,z,z) g(x,y) -> x g(x,y) -> y Open