Input TRS:
    1: minus(minus(x)) -> x
    2: minux(+(x,y)) -> +(minus(y),minus(x))
    3: +(minus(x),+(x,y)) -> y
    4: +(+(x,y),minus(y)) -> x
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 4 1 3 2
 minus(x1)	weight: (/ 1 4) + 2 * x1
 minux(x1)	weight: (/ 1 2) + 2 * x1
     +(x1,x2)	weight: (/ 1 4) + x1 + x2
Number of strict rules: 0
YES