MAYBE Problem: f(s(x),y) -> f(x,s(x)) f(x,s(y)) -> f(y,x) Proof: DP Processor: DPs: f#(s(x),y) -> f#(x,s(x)) f#(x,s(y)) -> f#(y,x) TRS: f(s(x),y) -> f(x,s(x)) f(x,s(y)) -> f(y,x) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(s(x),y) -> f#(x,s(x)) f#(x,s(y)) -> f#(y,x) TRS: f(s(x),y) -> f(x,s(x)) f(x,s(y)) -> f(y,x) Open