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