YES
O(n)
TRS:
 {-(-(neg(x), neg(x)), -(neg(y), neg(y))) -> -(-(x, y), -(x, y))}
 DUP: We consider a non-duplicating system.
  Trs:
   {-(-(neg(x), neg(x)), -(neg(y), neg(y))) -> -(-(x, y), -(x, y))}
  BOUND:
   Automaton:
    {
      neg_0(6) -> 3,
      neg_0(3) -> 3,
      neg_0(2) -> 3,
     -_1(6, 6) -> 6 | 5 | 4 | 2,
     -_1(6, 5) -> 2,
     -_1(6, 3) -> 2,
     -_1(6, 2) -> 6 | 5 | 4 | 2,
     -_1(4, 6) -> 2,
     -_1(4, 5) -> 2,
     -_1(3, 6) -> 2,
     -_1(3, 3) -> 2,
     -_1(3, 2) -> 2,
     -_1(2, 6) -> 6 | 5 | 4 | 2,
     -_1(2, 3) -> 2,
     -_1(2, 2) -> 6 | 5 | 4 | 2,
     -_0(6, 6) -> 2,
     -_0(6, 3) -> 2,
     -_0(6, 2) -> 2,
     -_0(3, 6) -> 2,
     -_0(3, 3) -> 2,
     -_0(3, 2) -> 2,
     -_0(2, 6) -> 2,
     -_0(2, 3) -> 2,
     -_0(2, 2) -> 2
    }
   Strict:
    {}
   Qed