Input TRS:
    1: active(zeros()) -> mark(cons(0(),zeros()))
    2: active(U11(tt(),L)) -> mark(s(length(L)))
    3: active(and(tt(),X)) -> mark(X)
    4: active(isNat(0())) -> mark(tt())
    5: active(isNat(length(V1))) -> mark(isNatList(V1))
    6: active(isNat(s(V1))) -> mark(isNat(V1))
    7: active(isNatIList(V)) -> mark(isNatList(V))
    8: active(isNatIList(zeros())) -> mark(tt())
    9: active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
    10: active(isNatList(nil())) -> mark(tt())
    11: active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
    12: active(length(nil())) -> mark(0())
    13: active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
    14: mark(zeros()) -> active(zeros())
    15: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    16: mark(0()) -> active(0())
    17: mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
    18: mark(tt()) -> active(tt())
    19: mark(s(X)) -> active(s(mark(X)))
    20: mark(length(X)) -> active(length(mark(X)))
    21: mark(and(X1,X2)) -> active(and(mark(X1),X2))
    22: mark(isNat(X)) -> active(isNat(X))
    23: mark(isNatList(X)) -> active(isNatList(X))
    24: mark(isNatIList(X)) -> active(isNatIList(X))
    25: mark(nil()) -> active(nil())
    26: cons(mark(X1),X2) -> cons(X1,X2)
    27: cons(X1,mark(X2)) -> cons(X1,X2)
    28: cons(active(X1),X2) -> cons(X1,X2)
    29: cons(X1,active(X2)) -> cons(X1,X2)
    30: U11(mark(X1),X2) -> U11(X1,X2)
    31: U11(X1,mark(X2)) -> U11(X1,X2)
    32: U11(active(X1),X2) -> U11(X1,X2)
    33: U11(X1,active(X2)) -> U11(X1,X2)
    34: s(mark(X)) -> s(X)
    35: s(active(X)) -> s(X)
    36: length(mark(X)) -> length(X)
    37: length(active(X)) -> length(X)
    38: and(mark(X1),X2) -> and(X1,X2)
    39: and(X1,mark(X2)) -> and(X1,X2)
    40: and(active(X1),X2) -> and(X1,X2)
    41: and(X1,active(X2)) -> and(X1,X2)
    42: isNat(mark(X)) -> isNat(X)
    43: isNat(active(X)) -> isNat(X)
    44: isNatList(mark(X)) -> isNatList(X)
    45: isNatList(active(X)) -> isNatList(X)
    46: isNatIList(mark(X)) -> isNatIList(X)
    47: isNatIList(active(X)) -> isNatIList(X)
Number of strict rules: 47
Direct Order(PosReal,>,Poly) ... removes: 8 5 7 12
isNatList(x1)	weight: x1
   U11(x1,x2)	weight: (/ 1 8) + x1 + x2
     s(x1)	weight: x1
   and(x1,x2)	weight: x1 + x2
isNatIList(x1)	weight: (/ 1 8) + x1
 zeros()	weight: 0
     0()	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
 isNat(x1)	weight: x1
active(x1)	weight: x1
  cons(x1,x2)	weight: 2 * x1 + 2 * x2
    tt()	weight: 0
length(x1)	weight: (/ 1 8) + x1
Number of strict rules: 43
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(U11(tt(),L)) -> #mark(s(length(L)))
   #2: #active(U11(tt(),L)) -> #s(length(L))
   #3: #active(U11(tt(),L)) -> #length(L)
   #4: #isNat(active(X)) -> #isNat(X)
   #5: #cons(X1,active(X2)) -> #cons(X1,X2)
   #6: #s(active(X)) -> #s(X)
   #7: #isNatIList(mark(X)) -> #isNatIList(X)
   #8: #isNat(mark(X)) -> #isNat(X)
   #9: #and(X1,active(X2)) -> #and(X1,X2)
   #10: #length(active(X)) -> #length(X)
   #11: #isNatIList(active(X)) -> #isNatIList(X)
   #12: #and(mark(X1),X2) -> #and(X1,X2)
   #13: #active(isNat(s(V1))) -> #mark(isNat(V1))
   #14: #active(isNat(s(V1))) -> #isNat(V1)
   #15: #and(active(X1),X2) -> #and(X1,X2)
   #16: #active(length(cons(N,L))) -> #mark(U11(and(isNatList(L),isNat(N)),L))
   #17: #active(length(cons(N,L))) -> #U11(and(isNatList(L),isNat(N)),L)
   #18: #active(length(cons(N,L))) -> #and(isNatList(L),isNat(N))
   #19: #active(length(cons(N,L))) -> #isNatList(L)
   #20: #active(length(cons(N,L))) -> #isNat(N)
   #21: #active(isNatIList(cons(V1,V2))) -> #mark(and(isNat(V1),isNatIList(V2)))
   #22: #active(isNatIList(cons(V1,V2))) -> #and(isNat(V1),isNatIList(V2))
   #23: #active(isNatIList(cons(V1,V2))) -> #isNat(V1)
   #24: #active(isNatIList(cons(V1,V2))) -> #isNatIList(V2)
   #25: #active(isNatList(cons(V1,V2))) -> #mark(and(isNat(V1),isNatList(V2)))
   #26: #active(isNatList(cons(V1,V2))) -> #and(isNat(V1),isNatList(V2))
   #27: #active(isNatList(cons(V1,V2))) -> #isNat(V1)
   #28: #active(isNatList(cons(V1,V2))) -> #isNatList(V2)
   #29: #mark(isNatIList(X)) -> #active(isNatIList(X))
   #30: #mark(isNatList(X)) -> #active(isNatList(X))
   #31: #isNatList(active(X)) -> #isNatList(X)
   #32: #U11(X1,mark(X2)) -> #U11(X1,X2)
   #33: #mark(zeros()) -> #active(zeros())
   #34: #U11(mark(X1),X2) -> #U11(X1,X2)
   #35: #mark(nil()) -> #active(nil())
   #36: #mark(length(X)) -> #active(length(mark(X)))
   #37: #mark(length(X)) -> #length(mark(X))
   #38: #mark(length(X)) -> #mark(X)
   #39: #and(X1,mark(X2)) -> #and(X1,X2)
   #40: #active(isNatList(nil())) -> #mark(tt())
   #41: #U11(X1,active(X2)) -> #U11(X1,X2)
   #42: #isNatList(mark(X)) -> #isNatList(X)
   #43: #cons(active(X1),X2) -> #cons(X1,X2)
   #44: #mark(isNat(X)) -> #active(isNat(X))
   #45: #s(mark(X)) -> #s(X)
   #46: #cons(X1,mark(X2)) -> #cons(X1,X2)
   #47: #mark(U11(X1,X2)) -> #active(U11(mark(X1),X2))
   #48: #mark(U11(X1,X2)) -> #U11(mark(X1),X2)
   #49: #mark(U11(X1,X2)) -> #mark(X1)
   #50: #U11(active(X1),X2) -> #U11(X1,X2)
   #51: #mark(s(X)) -> #active(s(mark(X)))
   #52: #mark(s(X)) -> #s(mark(X))
   #53: #mark(s(X)) -> #mark(X)
   #54: #cons(mark(X1),X2) -> #cons(X1,X2)
   #55: #length(mark(X)) -> #length(X)
   #56: #mark(and(X1,X2)) -> #active(and(mark(X1),X2))
   #57: #mark(and(X1,X2)) -> #and(mark(X1),X2)
   #58: #mark(and(X1,X2)) -> #mark(X1)
   #59: #mark(0()) -> #active(0())
   #60: #active(and(tt(),X)) -> #mark(X)
   #61: #active(zeros()) -> #mark(cons(0(),zeros()))
   #62: #active(zeros()) -> #cons(0(),zeros())
   #63: #mark(cons(X1,X2)) -> #active(cons(mark(X1),X2))
   #64: #mark(cons(X1,X2)) -> #cons(mark(X1),X2)
   #65: #mark(cons(X1,X2)) -> #mark(X1)
   #66: #active(isNat(0())) -> #mark(tt())
   #67: #mark(tt()) -> #active(tt())
Number of SCCs: 10, DPs: 41, edges: 150
	SCC { #4 #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: x1
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 isNat(x1)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #4 #8
Number of SCCs: 9, DPs: 39, edges: 146
	SCC { #7 #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 isNat(x1)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#isNatIList(x1)	weight: x1
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #11
Number of SCCs: 8, DPs: 37, edges: 142
	SCC { #6 #45 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 isNat(x1)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #6 #45
Number of SCCs: 7, DPs: 35, edges: 138
	SCC { #10 #55 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 isNat(x1)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: x1
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #55
Number of SCCs: 6, DPs: 33, edges: 134
	SCC { #31 #42 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
#isNatList(x1)	weight: x1
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 isNat(x1)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: 0
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #31 #42
Number of SCCs: 5, DPs: 31, edges: 130
	SCC { #13 #44 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 1 4) + x1
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: x1
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 42 43 }
    Removed DPs: #13 #44
Number of SCCs: 4, DPs: 29, edges: 128
	SCC { #5 #43 #46 #54 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: x1 + x2
     s(x1)	weight: (/ 1 2)
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 1 4) + x1
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: x1
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #5 #43 #46 #54
Number of SCCs: 3, DPs: 25, edges: 112
	SCC { #9 #12 #15 #39 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 1 4) + x1
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: x1
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: x1 + x2
    Usable rules: { }
    Removed DPs: #9 #12 #15 #39
Number of SCCs: 2, DPs: 21, edges: 96
	SCC { #32 #34 #41 #50 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: 0
#cons(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2)
#isNat(x1)	weight: 0
   and(x1,x2)	weight: 0
isNatIList(x1)	weight: 0
 zeros()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 1 4) + x1
 #U11(x1,x2)	weight: x1 + x2
active(x1)	weight: (/ 1 4) + x1
  cons(x1,x2)	weight: 0
#active(x1)	weight: x1
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: 0
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #32 #34 #41 #50
Number of SCCs: 1, DPs: 17, edges: 80
	SCC { #1 #16 #21 #25 #29 #30 #33 #36 #38 #47 #49 #53 #56 #58 #60 #61 #65 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: 0
   U11(x1,x2)	weight: (/ 1 2) + x1 + x2
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   and(x1,x2)	weight: x1 + x2
isNatIList(x1)	weight: (/ 1 2)
 zeros()	weight: 0
#mark(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: x1
 isNat(x1)	weight: 0
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: x1 + x2
#active(x1)	weight: (/ 1 2) + x1
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: (/ 1 2) + x1
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 1..4 6 9..11 13..47 }
    Removed DPs: #38 #49
Number of SCCs: 1, DPs: 15, edges: 49
	SCC { #1 #16 #21 #25 #29 #30 #33 #36 #47 #53 #56 #58 #60 #61 #65 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
isNatList(x1)	weight: (/ 1 4)
   U11(x1,x2)	weight: max{0, (/ 1 4) + x1}
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   and(x1,x2)	weight: max{x2, x1}
isNatIList(x1)	weight: (/ 1 2) + x1
 zeros()	weight: (/ 3 4)
#mark(x1)	weight: x1
     0()	weight: (/ 1 4)
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: (/ 1 4)
  mark(x1)	weight: x1
 isNat(x1)	weight: (/ 1 4)
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
#active(x1)	weight: x1
#isNatIList(x1)	weight: 0
    tt()	weight: (/ 1 4)
length(x1)	weight: (/ 1 2)
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 1..4 6 9..11 13..47 }
    Removed DPs: #65
Number of SCCs: 1, DPs: 12, edges: 32
	SCC { #1 #16 #21 #25 #29 #30 #36 #47 #53 #56 #58 #60 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
isNatList(x1)	weight: (/ 94447 4)
   U11(x1,x2)	weight: max{0, (/ 1 4) + x2}
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   and(x1,x2)	weight: max{x2, (/ 1 4) + x1}
isNatIList(x1)	weight: (/ 94447 4) + x1
 zeros()	weight: (/ 3 4)
#mark(x1)	weight: x1
     0()	weight: (/ 1 4)
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: (/ 1 4)
  mark(x1)	weight: x1
 isNat(x1)	weight: (/ 94445 4)
 #U11(x1,x2)	weight: 0
active(x1)	weight: x1
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
#active(x1)	weight: x1
#isNatIList(x1)	weight: 0
    tt()	weight: (/ 1 4)
length(x1)	weight: (/ 1 4) + x1
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 1..4 6 9..11 13..47 }
    Removed DPs: #58
Number of SCCs: 1, DPs: 11, edges: 21
	SCC { #1 #16 #21 #25 #29 #30 #36 #47 #53 #56 #60 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
isNatList(x1)	weight: (/ 173941 4) + x1
   U11(x1,x2)	weight: (/ 1 4)
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#isNat(x1)	weight: 0
   and(x1,x2)	weight: (/ 1 4) + x2
isNatIList(x1)	weight: (/ 1 4) + x1
 zeros()	weight: 0
#mark(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
#isNatList(x1)	weight: 0
   #s(x1)	weight: 0
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
 isNat(x1)	weight: (/ 1 4)
 #U11(x1,x2)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  cons(x1,x2)	weight: (/ 1 2) + x2
#active(x1)	weight: (/ 1 4) + x1
#isNatIList(x1)	weight: 0
    tt()	weight: 0
length(x1)	weight: (/ 1 4)
#length(x1)	weight: 0
 #and(x1,x2)	weight: 0
    Usable rules: { 26..33 36..47 }
    Removed DPs: #21 #25 #60
Number of SCCs: 1, DPs: 5, edges: 7
	SCC { #1 #16 #36 #47 #53 }
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)... succeeded.
isNatList(x1)	weight: (max (- (/ 1 16)) 0); x1_2
   U11(x1,x2)	weight: max{0, (/ 5 16) + x2_1 + x1_2}; (- (/ 1 16))
#cons(x1,x2)	weight: 0; 0
     s(x1)	weight: max{0, (/ 1 16) + x1_1}; (- (/ 1 16))
#isNat(x1)	weight: 0; 0
   and(x1,x2)	weight: max{0, x2_1}; x2_2 + x1_2
isNatIList(x1)	weight: (max (- (/ 1 16)) 0); (- (/ 1 16))
 zeros()	weight: (/ 1 16); (- (/ 5 16))
#mark(x1)	weight: max{0, (/ 1 8) + x1_1}; (- (/ 1 16))
     0()	weight: (/ 1 16); (- (/ 1 16))
#isNatList(x1)	weight: 0; 0
   #s(x1)	weight: 0; 0
   nil()	weight: (/ 1 16); 0
  mark(x1)	weight: max{0, x1_1}; x1_2
 isNat(x1)	weight: max{0, (/ 1 16) + x1_1}; 0
 #U11(x1,x2)	weight: 0; 0
active(x1)	weight: max{0, x1_1}; x1_2
  cons(x1,x2)	weight: max{0, (/ 5 16) + x2_1 + x2_2}; x2_2
#active(x1)	weight: max{0, (/ 1 16) + x1_1}; x1_2
#isNatIList(x1)	weight: 0; 0
    tt()	weight: 0; 0
length(x1)	weight: max{0, (/ 1 8) + x1_1}; (- (/ 1 16))
#length(x1)	weight: 0; 0
 #and(x1,x2)	weight: 0; 0
    Usable rules: { 1..4 6 9..11 13..47 }
    Removed DPs: #1 #16 #36 #47 #53
Number of SCCs: 0, DPs: 0, edges: 0
YES