MAYBE Problem: f(f(a(),b()),x) -> f(b(),f(a(),f(c(),f(b(),f(a(),x))))) f(x,f(y,z)) -> f(f(x,y),z) Proof: DP Processor: DPs: f#(f(a(),b()),x) -> f#(a(),x) f#(f(a(),b()),x) -> f#(b(),f(a(),x)) f#(f(a(),b()),x) -> f#(c(),f(b(),f(a(),x))) f#(f(a(),b()),x) -> f#(a(),f(c(),f(b(),f(a(),x)))) f#(f(a(),b()),x) -> f#(b(),f(a(),f(c(),f(b(),f(a(),x))))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(a(),b()),x) -> f(b(),f(a(),f(c(),f(b(),f(a(),x))))) f(x,f(y,z)) -> f(f(x,y),z) SCC Processor: #sccs: 1 #rules: 7 #arcs: 49/49 DPs: f#(f(a(),b()),x) -> f#(a(),x) f#(f(a(),b()),x) -> f#(b(),f(a(),x)) f#(f(a(),b()),x) -> f#(c(),f(b(),f(a(),x))) f#(f(a(),b()),x) -> f#(a(),f(c(),f(b(),f(a(),x)))) f#(f(a(),b()),x) -> f#(b(),f(a(),f(c(),f(b(),f(a(),x))))) f#(x,f(y,z)) -> f#(x,y) f#(x,f(y,z)) -> f#(f(x,y),z) TRS: f(f(a(),b()),x) -> f(b(),f(a(),f(c(),f(b(),f(a(),x))))) f(x,f(y,z)) -> f(f(x,y),z) Open