YES Time: 0.000335 TRS: { f(x, x) -> a(), f(g x, y) -> f(x, y)} RUF: Strict: {f(x, x) -> a()} Weak: {} RUF: Strict: {} Weak: {} Qed