Input TRS:
    1: concat(leaf(),Y) -> Y
    2: concat(cons(U,V),Y) -> cons(U,concat(V,Y))
    3: lessleaves(X,leaf()) -> false()
    4: lessleaves(leaf(),cons(W,Z)) -> true()
    5: lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 4 1 3 5
 false()	weight: 0
  true()	weight: 0
concat(x1,x2)	weight: (/ 1 4) + x1 + x2
  cons(x1,x2)	weight: (/ 1 3) + x1 + x2
lessleaves(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
  leaf()	weight: 0
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 2
 false()	weight: 0
  true()	weight: 0
concat(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
lessleaves(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
  leaf()	weight: 0
Number of strict rules: 0
YES