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