Input TRS:
    1: flatten(nil()) -> nil()
    2: flatten(unit(x)) -> flatten(x)
    3: flatten(++(x,y)) -> ++(flatten(x),flatten(y))
    4: flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
    5: flatten(flatten(x)) -> flatten(x)
    6: rev(nil()) -> nil()
    7: rev(unit(x)) -> unit(x)
    8: rev(++(x,y)) -> ++(rev(y),rev(x))
    9: rev(rev(x)) -> x
    10: ++(x,nil()) -> x
    11: ++(nil(),y) -> y
    12: ++(++(x,y),z) -> ++(x,++(y,z))
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 4 10 11 2
flatten(x1)	weight: x1
    ++(x1,x2)	weight: (/ 1 8) + x1 + x2
  unit(x1)	weight: (/ 1 8) + 2 * x1
   nil()	weight: 0
   rev(x1)	weight: x1
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 7
flatten(x1)	weight: x1
    ++(x1,x2)	weight: x1 + x2
  unit(x1)	weight: (/ 1 4) + 2 * x1
   nil()	weight: 0
   rev(x1)	weight: 2 * x1
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... removes: 8 9 6
flatten(x1)	weight: x1
    ++(x1,x2)	weight: (/ 2647 2) + x1 + x2
  unit(x1)	weight: (/ 1 4) + x1
   nil()	weight: 0
   rev(x1)	weight: (/ 5293 4) + 2 * x1
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 12
flatten(x1)	weight: x1
    ++(x1,x2)	weight: (/ 2647 2) + 2 * x1 + x2
  unit(x1)	weight: (/ 1 4) + x1
   nil()	weight: 0
   rev(x1)	weight: (/ 2647 4) + 2 * x1
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 1 3 5
flatten(x1)	weight: (/ 1 8) + 2 * x1
    ++(x1,x2)	weight: (/ 1 4) + x1 + x2
  unit(x1)	weight: x1
   nil()	weight: 0
   rev(x1)	weight: (/ 1 8) + 2 * x1
Number of strict rules: 0
YES