Input TRS:
    1: concat(leaf(),y) -> y
    2: concat(node(u,v),y) -> node(u,concat(v,y))
    3: lessleaves(x,leaf()) -> false()
    4: lessleaves(leaf(),node(w,z)) -> true()
    5: lessleaves(node(u,v),node(w,z)) -> lessleaves(concat(u,v),concat(w,z))
    6: lessleaves(node(u,v),node(w,z)) ->= lessleaves(node(v,u),node(w,z))
    7: lessleaves(node(u,v),node(w,z)) ->= lessleaves(node(u,v),node(z,w))
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 4 1 3 5
 false()	weight: 0
  true()	weight: 0
concat(x1,x2)	weight: (/ 162601 4) + x2 + x1
lessleaves(x1,x2)	weight: x2 + x1
  leaf()	weight: (/ 1 4)
  node(x1,x2)	weight: (/ 325203 8) + x2 + x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 2
 false()	weight: 0
  true()	weight: 0
concat(x1,x2)	weight: (/ 1 4) + x2 + 2 * x1
lessleaves(x1,x2)	weight: x2 + x1
  leaf()	weight: (/ 1 4)
  node(x1,x2)	weight: (/ 1 4) + x2 + x1
Number of strict rules: 0
YES