TRS: { f(x, y) -> g1(x, x, y), f(x, y) -> g1(y, x, x), f(x, y) -> g2(x, y, y), f(x, y) -> g2(y, y, x), g1(x, x, y) -> h(x, y), g1(y, x, x) -> h(x, y), g2(x, y, y) -> h(x, y), g2(y, y, x) -> h(x, y), h(x, x) -> x} MPO: Prec: g2 > h, g1 > h, f > g2, f > g1 empty Strict: {} Weak: {} Qed