Input TRS:
    1: a__zeros() -> cons(0(),zeros())
    2: a__U11(tt(),L) -> a__U12(tt(),L)
    3: a__U12(tt(),L) -> s(a__length(mark(L)))
    4: a__length(nil()) -> 0()
    5: a__length(cons(N,L)) -> a__U11(tt(),L)
    6: mark(zeros()) -> a__zeros()
    7: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
    8: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
    9: mark(length(X)) -> a__length(mark(X))
    10: mark(cons(X1,X2)) -> cons(mark(X1),X2)
    11: mark(0()) -> 0()
    12: mark(tt()) -> tt()
    13: mark(s(X)) -> s(mark(X))
    14: mark(nil()) -> nil()
    15: a__zeros() -> zeros()
    16: a__U11(X1,X2) -> U11(X1,X2)
    17: a__U12(X1,X2) -> U12(X1,X2)
    18: a__length(X) -> length(X)
Number of strict rules: 18
Direct Order(PosReal,>,Poly) ... removes: 4
   U11(x1,x2)	weight: 9726 + x1 + 2 * x2
     s(x1)	weight: x1
 zeros()	weight: 0
   U12(x1,x2)	weight: 9726 + 2 * x1 + 2 * x2
     0()	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
a__U11(x1,x2)	weight: 9726 + x1 + 2 * x2
a__U12(x1,x2)	weight: 9726 + 2 * x1 + 2 * x2
  cons(x1,x2)	weight: x1 + 2 * x2
    tt()	weight: 0
length(x1)	weight: 9726 + x1
a__zeros()	weight: 0
a__length(x1)	weight: 9726 + x1
Number of strict rules: 17
Direct Order(PosReal,>,Poly) ... removes: 18 8 16 17 7 9
   U11(x1,x2)	weight: 17067 + x1 + x2
     s(x1)	weight: x1
 zeros()	weight: 0
   U12(x1,x2)	weight: 8534 + x1 + x2
     0()	weight: 0
   nil()	weight: 0
  mark(x1)	weight: 2 * x1
a__U11(x1,x2)	weight: (/ 34135 2) + x1 + 2 * x2
a__U12(x1,x2)	weight: (/ 34135 2) + x1 + 2 * x2
  cons(x1,x2)	weight: x1 + 2 * x2
    tt()	weight: 0
length(x1)	weight: 17067 + x1
a__zeros()	weight: 0
a__length(x1)	weight: (/ 34135 2) + x1
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... failed.
Freezing a__U12 a__U11
1: a__zeros() -> cons(0(),zeros())
2: a__U11❆1_tt(L) -> a__U12❆1_tt(L)
3: a__U12❆1_tt(L) -> s(a__length(mark(L)))
5: a__length(cons(N,L)) -> a__U11❆1_tt(L)
6: mark(zeros()) -> a__zeros()
10: mark(cons(X1,X2)) -> cons(mark(X1),X2)
11: mark(0()) -> 0()
12: mark(tt()) -> tt()
13: mark(s(X)) -> s(mark(X))
14: mark(nil()) -> nil()
15: a__zeros() -> zeros()
19: a__U11(tt(),_1) ->= a__U11❆1_tt(_1)
20: a__U12(tt(),_1) ->= a__U12❆1_tt(_1)
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 19 20
a__U11❆1_tt(x1)	weight: (/ 1 4) + 2 * x1
   U11(x1,x2)	weight: x1 + x2
     s(x1)	weight: x1
 zeros()	weight: 0
   U12(x1,x2)	weight: x1 + x2
     0()	weight: 0
   nil()	weight: 0
  mark(x1)	weight: 2 * x1
a__U11(x1,x2)	weight: (/ 1 2) + x1 + 2 * x2
a__U12(x1,x2)	weight: (/ 1 2) + x1 + 2 * x2
  cons(x1,x2)	weight: x1 + 2 * x2
    tt()	weight: 0
a__U12❆1_tt(x1)	weight: (/ 1 4) + 2 * x1
length(x1)	weight: x1
a__zeros()	weight: 0
a__length(x1)	weight: (/ 1 4) + x1
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #a__U11❆1_tt(L) -> #a__U12❆1_tt(L)
   #2: #mark(zeros()) -> #a__zeros()
   #3: #mark(s(X)) -> #mark(X)
   #4: #mark(cons(X1,X2)) -> #mark(X1)
   #5: #a__length(cons(N,L)) -> #a__U11❆1_tt(L)
   #6: #a__U12❆1_tt(L) -> #a__length(mark(L))
   #7: #a__U12❆1_tt(L) -> #mark(L)
Number of SCCs: 2, DPs: 5, edges: 7
	SCC { #3 #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
a__U11❆1_tt(x1)	weight: 0
   U11(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 zeros()	weight: 0
   U12(x1,x2)	weight: 0
#a__U12❆1_tt(x1)	weight: 0
#mark(x1)	weight: x1
     0()	weight: 0
#a__zeros()	weight: 0
   nil()	weight: 0
  mark(x1)	weight: 0
a__U11(x1,x2)	weight: 0
#a__length(x1)	weight: 0
a__U12(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x1
    tt()	weight: 0
a__U12❆1_tt(x1)	weight: 0
length(x1)	weight: 0
#a__U11❆1_tt(x1)	weight: 0
a__zeros()	weight: 0
a__length(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #3 #4
Number of SCCs: 1, DPs: 3, edges: 3
	SCC { #1 #5 #6 }
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...  found.
  #a__U11❆1_tt(zeros())	-#1->
  #a__U12❆1_tt(zeros())	--->*
  #a__U12❆1_tt(zeros())	-#6->
  #a__length(mark(zeros()))	--->*
  #a__length(cons(0(),zeros()))	-#5->
  #a__U11❆1_tt(zeros())	--->*
  #a__U11❆1_tt(zeros())
  Looping with: [ ]
NO