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