Input TRS:
    1: lessElements(l,t) -> lessE(l,t,0())
    2: lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
    3: if(true(),b,l,t,n) -> l
    4: if(false(),true(),l,t,n) -> t
    5: if(false(),false(),l,t,n) -> lessE(l,t,s(n))
    6: length(nil()) -> 0()
    7: length(cons(n,l)) -> s(length(l))
    8: toList(leaf()) -> nil()
    9: toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
    10: append(nil(),l2) -> l2
    11: append(cons(n,l1),l2) -> cons(n,append(l1,l2))
    12: le(s(n),0()) -> false()
    13: le(0(),m) -> true()
    14: le(s(n),s(m)) -> le(n,m)
    15: a() -> c()
    16: a() -> d()
Number of strict rules: 16
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #lessE(l,t,n) -> #if(le(length(l),n),le(length(toList(t)),n),l,t,n)
   #2: #lessE(l,t,n) -> #le(length(l),n)
   #3: #lessE(l,t,n) -> #length(l)
   #4: #lessE(l,t,n) -> #le(length(toList(t)),n)
   #5: #lessE(l,t,n) -> #length(toList(t))
   #6: #lessE(l,t,n) -> #toList(t)
   #7: #toList(node(t1,n,t2)) -> #append(toList(t1),cons(n,toList(t2)))
   #8: #toList(node(t1,n,t2)) -> #toList(t1)
   #9: #toList(node(t1,n,t2)) -> #toList(t2)
   #10: #append(cons(n,l1),l2) -> #append(l1,l2)
   #11: #le(s(n),s(m)) -> #le(n,m)
   #12: #length(cons(n,l)) -> #length(l)
   #13: #if(false(),false(),l,t,n) -> #lessE(l,t,s(n))
   #14: #lessElements(l,t) -> #lessE(l,t,0())
Number of SCCs: 5, DPs: 7, edges: 9
	SCC { #12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: 0
  #le(x1,x2)	weight: 0
#append(x1,x2)	weight: 0
 lessE(x1,x2,x3)	weight: 0
 false()	weight: 0
     c()	weight: 0
  true()	weight: 0
toList(x1)	weight: 0
lessElements(x1,x2)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
#toList(x1)	weight: 0
   nil()	weight: 0
#lessE(x1,x2,x3)	weight: 0
#lessElements(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
  #if(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
  leaf()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: x1
  node(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #12
Number of SCCs: 4, DPs: 6, edges: 8
	SCC { #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: x2
#append(x1,x2)	weight: 0
 lessE(x1,x2,x3)	weight: 0
 false()	weight: 0
     c()	weight: 0
  true()	weight: 0
toList(x1)	weight: 0
lessElements(x1,x2)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
#toList(x1)	weight: 0
   nil()	weight: 0
#lessE(x1,x2,x3)	weight: 0
#lessElements(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2)
  #if(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
  leaf()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
  node(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #11
Number of SCCs: 3, DPs: 5, edges: 7
	SCC { #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2)
  #le(x1,x2)	weight: 0
#append(x1,x2)	weight: x1
 lessE(x1,x2,x3)	weight: 0
 false()	weight: 0
     c()	weight: 0
  true()	weight: 0
toList(x1)	weight: 0
lessElements(x1,x2)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
#toList(x1)	weight: 0
   nil()	weight: 0
#lessE(x1,x2,x3)	weight: 0
#lessElements(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
  #if(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
  leaf()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
  node(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 2, DPs: 4, edges: 6
	SCC { #8 #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
    le(x1,x2)	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2)
  #le(x1,x2)	weight: 0
#append(x1,x2)	weight: 0
 lessE(x1,x2,x3)	weight: 0
 false()	weight: 0
     c()	weight: 0
  true()	weight: 0
toList(x1)	weight: 0
lessElements(x1,x2)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5)	weight: 0
#toList(x1)	weight: x1
   nil()	weight: 0
#lessE(x1,x2,x3)	weight: 0
#lessElements(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2)
  #if(x1,x2,x3,x4,x5)	weight: 0
   #a()	weight: 0
  leaf()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
  node(x1,x2,x3)	weight: (/ 1 2) + x1 + x3
    Usable rules: { }
    Removed DPs: #8 #9
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #1 #13 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE