MAYBE Problem: f(x,y,f(z,u,v)) -> f(f(x,y,z),u,f(x,y,v)) Proof: DP Processor: DPs: f#(x,y,f(z,u,v)) -> f#(x,y,v) f#(x,y,f(z,u,v)) -> f#(x,y,z) f#(x,y,f(z,u,v)) -> f#(f(x,y,z),u,f(x,y,v)) TRS: f(x,y,f(z,u,v)) -> f(f(x,y,z),u,f(x,y,v)) Restore Modifier: DPs: f#(x,y,f(z,u,v)) -> f#(x,y,v) f#(x,y,f(z,u,v)) -> f#(x,y,z) f#(x,y,f(z,u,v)) -> f#(f(x,y,z),u,f(x,y,v)) TRS: f(x,y,f(z,u,v)) -> f(f(x,y,z),u,f(x,y,v)) SCC Processor: #sccs: 1 #rules: 3 #arcs: 9/9 DPs: f#(x,y,f(z,u,v)) -> f#(x,y,v) f#(x,y,f(z,u,v)) -> f#(x,y,z) f#(x,y,f(z,u,v)) -> f#(f(x,y,z),u,f(x,y,v)) TRS: f(x,y,f(z,u,v)) -> f(f(x,y,z),u,f(x,y,v)) Open