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