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