MAYBE Problem: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) Proof: DP Processor: DPs: f#(g(X)) -> f#(X) f#(g(X)) -> f#(f(X)) TRS: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) Restore Modifier: DPs: f#(g(X)) -> f#(X) f#(g(X)) -> f#(f(X)) TRS: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: f#(g(X)) -> f#(X) f#(g(X)) -> f#(f(X)) TRS: f(g(X)) -> g(f(f(X))) f(h(X)) -> h(g(X)) Open