MAYBE TRS: {f(x, f(y, a())) -> h(f(a(), f(f(x, a()), y)))} DP: Strict: {f#(x, f(y, a())) -> f#(x, a()), f#(x, f(y, a())) -> f#(f(x, a()), y), f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y))} Weak: {f(x, f(y, a())) -> h(f(a(), f(f(x, a()), y)))} EDG: {(f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y)), f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y))) (f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y)), f#(x, f(y, a())) -> f#(f(x, a()), y)) (f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y)), f#(x, f(y, a())) -> f#(x, a())) (f#(x, f(y, a())) -> f#(f(x, a()), y), f#(x, f(y, a())) -> f#(x, a())) (f#(x, f(y, a())) -> f#(f(x, a()), y), f#(x, f(y, a())) -> f#(f(x, a()), y)) (f#(x, f(y, a())) -> f#(f(x, a()), y), f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y)))} SCCS: Scc: {f#(x, f(y, a())) -> f#(f(x, a()), y), f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y))} SCC: Strict: {f#(x, f(y, a())) -> f#(f(x, a()), y), f#(x, f(y, a())) -> f#(a(), f(f(x, a()), y))} Weak: {f(x, f(y, a())) -> h(f(a(), f(f(x, a()), y)))} Fail