MAYBE Problem: f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) cons(x,y) -> x cons(x,y) -> y Proof: DP Processor: DPs: f#(s(a()),s(b()),x) -> f#(x,x,x) g#(f(s(x),s(y),z)) -> f#(x,y,z) g#(f(s(x),s(y),z)) -> g#(f(x,y,z)) TRS: f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) cons(x,y) -> x cons(x,y) -> y TDG Processor: DPs: f#(s(a()),s(b()),x) -> f#(x,x,x) g#(f(s(x),s(y),z)) -> f#(x,y,z) g#(f(s(x),s(y),z)) -> g#(f(x,y,z)) TRS: f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) cons(x,y) -> x cons(x,y) -> y graph: g#(f(s(x),s(y),z)) -> g#(f(x,y,z)) -> g#(f(s(x),s(y),z)) -> g#(f(x,y,z)) g#(f(s(x),s(y),z)) -> g#(f(x,y,z)) -> g#(f(s(x),s(y),z)) -> f#(x,y,z) g#(f(s(x),s(y),z)) -> f#(x,y,z) -> f#(s(a()),s(b()),x) -> f#(x,x,x) f#(s(a()),s(b()),x) -> f#(x,x,x) -> f#(s(a()),s(b()),x) -> f#(x,x,x) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: g#(f(s(x),s(y),z)) -> g#(f(x,y,z)) TRS: f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) cons(x,y) -> x cons(x,y) -> y Open DPs: f#(s(a()),s(b()),x) -> f#(x,x,x) TRS: f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) cons(x,y) -> x cons(x,y) -> y Open