YES(?,O(n^1))
TRS:
 {
        minus minus x -> x,
  +(minus x, +(x, y)) -> y,
  +(+(x, y), minus y) -> x,
        minux +(x, y) -> +(minus y, minus x)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
          minus minus x -> x,
    +(minus x, +(x, y)) -> y,
    +(+(x, y), minus y) -> x,
          minux +(x, y) -> +(minus y, minus x)
   }
  Natural interpretation:
   Strict:
    {
           minus minus x -> x,
     +(minus x, +(x, y)) -> y,
     +(+(x, y), minus y) -> x,
           minux +(x, y) -> +(minus y, minus x)
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [minux](X0) = + 1*X0 + 3
   [+](X1, X0) = + 1*X0 + 1*X1 + 6
   [minus](X0) = + 1*X0 + 1
   
   Qed