YES Time: 0.000337 TRS: {-(-(neg x, neg x), -(neg y, neg y)) -> -(-(x, y), -(x, y))} RUF: Strict: {} Weak: {} Qed