YES

Problem:
 a__eq(0(),0()) -> true()
 a__eq(s(X),s(Y)) -> a__eq(X,Y)
 a__eq(X,Y) -> false()
 a__inf(X) -> cons(X,inf(s(X)))
 a__take(0(),X) -> nil()
 a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
 a__length(nil()) -> 0()
 a__length(cons(X,L)) -> s(length(L))
 mark(eq(X1,X2)) -> a__eq(X1,X2)
 mark(inf(X)) -> a__inf(mark(X))
 mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
 mark(length(X)) -> a__length(mark(X))
 mark(0()) -> 0()
 mark(true()) -> true()
 mark(s(X)) -> s(X)
 mark(false()) -> false()
 mark(cons(X1,X2)) -> cons(X1,X2)
 mark(nil()) -> nil()
 a__eq(X1,X2) -> eq(X1,X2)
 a__inf(X) -> inf(X)
 a__take(X1,X2) -> take(X1,X2)
 a__length(X) -> length(X)

Proof:
 DP Processor:
  DPs:
   a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
   mark#(eq(X1,X2)) -> a__eq#(X1,X2)
   mark#(inf(X)) -> mark#(X)
   mark#(inf(X)) -> a__inf#(mark(X))
   mark#(take(X1,X2)) -> mark#(X2)
   mark#(take(X1,X2)) -> mark#(X1)
   mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
   mark#(length(X)) -> mark#(X)
   mark#(length(X)) -> a__length#(mark(X))
  TRS:
   a__eq(0(),0()) -> true()
   a__eq(s(X),s(Y)) -> a__eq(X,Y)
   a__eq(X,Y) -> false()
   a__inf(X) -> cons(X,inf(s(X)))
   a__take(0(),X) -> nil()
   a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
   a__length(nil()) -> 0()
   a__length(cons(X,L)) -> s(length(L))
   mark(eq(X1,X2)) -> a__eq(X1,X2)
   mark(inf(X)) -> a__inf(mark(X))
   mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
   mark(length(X)) -> a__length(mark(X))
   mark(0()) -> 0()
   mark(true()) -> true()
   mark(s(X)) -> s(X)
   mark(false()) -> false()
   mark(cons(X1,X2)) -> cons(X1,X2)
   mark(nil()) -> nil()
   a__eq(X1,X2) -> eq(X1,X2)
   a__inf(X) -> inf(X)
   a__take(X1,X2) -> take(X1,X2)
   a__length(X) -> length(X)
  TDG Processor:
   DPs:
    a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
    mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(inf(X)) -> mark#(X)
    mark#(inf(X)) -> a__inf#(mark(X))
    mark#(take(X1,X2)) -> mark#(X2)
    mark#(take(X1,X2)) -> mark#(X1)
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> a__length#(mark(X))
   TRS:
    a__eq(0(),0()) -> true()
    a__eq(s(X),s(Y)) -> a__eq(X,Y)
    a__eq(X,Y) -> false()
    a__inf(X) -> cons(X,inf(s(X)))
    a__take(0(),X) -> nil()
    a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
    a__length(nil()) -> 0()
    a__length(cons(X,L)) -> s(length(L))
    mark(eq(X1,X2)) -> a__eq(X1,X2)
    mark(inf(X)) -> a__inf(mark(X))
    mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
    mark(length(X)) -> a__length(mark(X))
    mark(0()) -> 0()
    mark(true()) -> true()
    mark(s(X)) -> s(X)
    mark(false()) -> false()
    mark(cons(X1,X2)) -> cons(X1,X2)
    mark(nil()) -> nil()
    a__eq(X1,X2) -> eq(X1,X2)
    a__inf(X) -> inf(X)
    a__take(X1,X2) -> take(X1,X2)
    a__length(X) -> length(X)
   graph:
    mark#(eq(X1,X2)) -> a__eq#(X1,X2) ->
    a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
    mark#(length(X)) -> mark#(X) ->
    mark#(length(X)) -> a__length#(mark(X))
    mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(length(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X2)
    mark#(length(X)) -> mark#(X) -> mark#(inf(X)) -> a__inf#(mark(X))
    mark#(length(X)) -> mark#(X) -> mark#(inf(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) ->
    mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(length(X)) -> a__length#(mark(X))
    mark#(take(X1,X2)) -> mark#(X2) -> mark#(length(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(take(X1,X2)) -> mark#(X1)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(take(X1,X2)) -> mark#(X2)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(inf(X)) -> a__inf#(mark(X))
    mark#(take(X1,X2)) -> mark#(X2) -> mark#(inf(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X2) ->
    mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> a__length#(mark(X))
    mark#(take(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(take(X1,X2)) -> mark#(X1)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(take(X1,X2)) -> mark#(X2)
    mark#(take(X1,X2)) -> mark#(X1) ->
    mark#(inf(X)) -> a__inf#(mark(X))
    mark#(take(X1,X2)) -> mark#(X1) -> mark#(inf(X)) -> mark#(X)
    mark#(take(X1,X2)) -> mark#(X1) -> mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    mark#(inf(X)) -> mark#(X) -> mark#(length(X)) -> a__length#(mark(X))
    mark#(inf(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(inf(X)) -> mark#(X) ->
    mark#(take(X1,X2)) -> a__take#(mark(X1),mark(X2))
    mark#(inf(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X1)
    mark#(inf(X)) -> mark#(X) -> mark#(take(X1,X2)) -> mark#(X2)
    mark#(inf(X)) -> mark#(X) -> mark#(inf(X)) -> a__inf#(mark(X))
    mark#(inf(X)) -> mark#(X) -> mark#(inf(X)) -> mark#(X)
    mark#(inf(X)) -> mark#(X) -> mark#(eq(X1,X2)) -> a__eq#(X1,X2)
    a__eq#(s(X),s(Y)) -> a__eq#(X,Y) -> a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 34/81
    DPs:
     mark#(length(X)) -> mark#(X)
     mark#(inf(X)) -> mark#(X)
     mark#(take(X1,X2)) -> mark#(X2)
     mark#(take(X1,X2)) -> mark#(X1)
    TRS:
     a__eq(0(),0()) -> true()
     a__eq(s(X),s(Y)) -> a__eq(X,Y)
     a__eq(X,Y) -> false()
     a__inf(X) -> cons(X,inf(s(X)))
     a__take(0(),X) -> nil()
     a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
     a__length(nil()) -> 0()
     a__length(cons(X,L)) -> s(length(L))
     mark(eq(X1,X2)) -> a__eq(X1,X2)
     mark(inf(X)) -> a__inf(mark(X))
     mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
     mark(length(X)) -> a__length(mark(X))
     mark(0()) -> 0()
     mark(true()) -> true()
     mark(s(X)) -> s(X)
     mark(false()) -> false()
     mark(cons(X1,X2)) -> cons(X1,X2)
     mark(nil()) -> nil()
     a__eq(X1,X2) -> eq(X1,X2)
     a__inf(X) -> inf(X)
     a__take(X1,X2) -> take(X1,X2)
     a__length(X) -> length(X)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [mark#](x0) = 6x0 + 4,
      
      [mark](x0) = 5x0,
      
      [eq](x0, x1) = 2,
      
      [length](x0) = 4x0 + 1,
      
      [a__length](x0) = 4x0 + 5,
      
      [take](x0, x1) = x0 + 4x1 + 1,
      
      [nil] = 2,
      
      [a__take](x0, x1) = x0 + 4x1 + 5,
      
      [cons](x0, x1) = x0 + 5,
      
      [inf](x0) = x0 + 4,
      
      [a__inf](x0) = x0 + 5,
      
      [false] = 2,
      
      [s](x0) = 3,
      
      [true] = 4,
      
      [a__eq](x0, x1) = 4,
      
      [0] = 0
     orientation:
      mark#(length(X)) = 24X + 10 >= 6X + 4 = mark#(X)
      
      mark#(inf(X)) = 6X + 28 >= 6X + 4 = mark#(X)
      
      mark#(take(X1,X2)) = 6X1 + 24X2 + 10 >= 6X2 + 4 = mark#(X2)
      
      mark#(take(X1,X2)) = 6X1 + 24X2 + 10 >= 6X1 + 4 = mark#(X1)
      
      a__eq(0(),0()) = 4 >= 4 = true()
      
      a__eq(s(X),s(Y)) = 4 >= 4 = a__eq(X,Y)
      
      a__eq(X,Y) = 4 >= 2 = false()
      
      a__inf(X) = X + 5 >= X + 5 = cons(X,inf(s(X)))
      
      a__take(0(),X) = 4X + 5 >= 2 = nil()
      
      a__take(s(X),cons(Y,L)) = 4Y + 28 >= Y + 5 = cons(Y,take(X,L))
      
      a__length(nil()) = 13 >= 0 = 0()
      
      a__length(cons(X,L)) = 4X + 25 >= 3 = s(length(L))
      
      mark(eq(X1,X2)) = 10 >= 4 = a__eq(X1,X2)
      
      mark(inf(X)) = 5X + 20 >= 5X + 5 = a__inf(mark(X))
      
      mark(take(X1,X2)) = 5X1 + 20X2 + 5 >= 5X1 + 20X2 + 5 = a__take(mark(X1),mark(X2))
      
      mark(length(X)) = 20X + 5 >= 20X + 5 = a__length(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(true()) = 20 >= 4 = true()
      
      mark(s(X)) = 15 >= 3 = s(X)
      
      mark(false()) = 10 >= 2 = false()
      
      mark(cons(X1,X2)) = 5X1 + 25 >= X1 + 5 = cons(X1,X2)
      
      mark(nil()) = 10 >= 2 = nil()
      
      a__eq(X1,X2) = 4 >= 2 = eq(X1,X2)
      
      a__inf(X) = X + 5 >= X + 4 = inf(X)
      
      a__take(X1,X2) = X1 + 4X2 + 5 >= X1 + 4X2 + 1 = take(X1,X2)
      
      a__length(X) = 4X + 5 >= 4X + 1 = length(X)
     problem:
      DPs:
       
      TRS:
       a__eq(0(),0()) -> true()
       a__eq(s(X),s(Y)) -> a__eq(X,Y)
       a__eq(X,Y) -> false()
       a__inf(X) -> cons(X,inf(s(X)))
       a__take(0(),X) -> nil()
       a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
       a__length(nil()) -> 0()
       a__length(cons(X,L)) -> s(length(L))
       mark(eq(X1,X2)) -> a__eq(X1,X2)
       mark(inf(X)) -> a__inf(mark(X))
       mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
       mark(length(X)) -> a__length(mark(X))
       mark(0()) -> 0()
       mark(true()) -> true()
       mark(s(X)) -> s(X)
       mark(false()) -> false()
       mark(cons(X1,X2)) -> cons(X1,X2)
       mark(nil()) -> nil()
       a__eq(X1,X2) -> eq(X1,X2)
       a__inf(X) -> inf(X)
       a__take(X1,X2) -> take(X1,X2)
       a__length(X) -> length(X)
     Qed
    
    DPs:
     a__eq#(s(X),s(Y)) -> a__eq#(X,Y)
    TRS:
     a__eq(0(),0()) -> true()
     a__eq(s(X),s(Y)) -> a__eq(X,Y)
     a__eq(X,Y) -> false()
     a__inf(X) -> cons(X,inf(s(X)))
     a__take(0(),X) -> nil()
     a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
     a__length(nil()) -> 0()
     a__length(cons(X,L)) -> s(length(L))
     mark(eq(X1,X2)) -> a__eq(X1,X2)
     mark(inf(X)) -> a__inf(mark(X))
     mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
     mark(length(X)) -> a__length(mark(X))
     mark(0()) -> 0()
     mark(true()) -> true()
     mark(s(X)) -> s(X)
     mark(false()) -> false()
     mark(cons(X1,X2)) -> cons(X1,X2)
     mark(nil()) -> nil()
     a__eq(X1,X2) -> eq(X1,X2)
     a__inf(X) -> inf(X)
     a__take(X1,X2) -> take(X1,X2)
     a__length(X) -> length(X)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [a__eq#](x0, x1) = 1x0 + 2x1,
      
      [mark](x0) = 4x0 + 3,
      
      [eq](x0, x1) = x0,
      
      [length](x0) = 3,
      
      [a__length](x0) = 6,
      
      [take](x0, x1) = 1,
      
      [nil] = 3,
      
      [a__take](x0, x1) = 4,
      
      [cons](x0, x1) = 0,
      
      [inf](x0) = 2,
      
      [a__inf](x0) = 3,
      
      [false] = 0,
      
      [s](x0) = 2x0 + 2,
      
      [true] = 0,
      
      [a__eq](x0, x1) = 1x0 + 1,
      
      [0] = 0
     orientation:
      a__eq#(s(X),s(Y)) = 3X + 4Y + 4 >= 1X + 2Y = a__eq#(X,Y)
      
      a__eq(0(),0()) = 1 >= 0 = true()
      
      a__eq(s(X),s(Y)) = 3X + 3 >= 1X + 1 = a__eq(X,Y)
      
      a__eq(X,Y) = 1X + 1 >= 0 = false()
      
      a__inf(X) = 3 >= 0 = cons(X,inf(s(X)))
      
      a__take(0(),X) = 4 >= 3 = nil()
      
      a__take(s(X),cons(Y,L)) = 4 >= 0 = cons(Y,take(X,L))
      
      a__length(nil()) = 6 >= 0 = 0()
      
      a__length(cons(X,L)) = 6 >= 5 = s(length(L))
      
      mark(eq(X1,X2)) = 4X1 + 3 >= 1X1 + 1 = a__eq(X1,X2)
      
      mark(inf(X)) = 6 >= 3 = a__inf(mark(X))
      
      mark(take(X1,X2)) = 5 >= 4 = a__take(mark(X1),mark(X2))
      
      mark(length(X)) = 7 >= 6 = a__length(mark(X))
      
      mark(0()) = 4 >= 0 = 0()
      
      mark(true()) = 4 >= 0 = true()
      
      mark(s(X)) = 6X + 6 >= 2X + 2 = s(X)
      
      mark(false()) = 4 >= 0 = false()
      
      mark(cons(X1,X2)) = 4 >= 0 = cons(X1,X2)
      
      mark(nil()) = 7 >= 3 = nil()
      
      a__eq(X1,X2) = 1X1 + 1 >= X1 = eq(X1,X2)
      
      a__inf(X) = 3 >= 2 = inf(X)
      
      a__take(X1,X2) = 4 >= 1 = take(X1,X2)
      
      a__length(X) = 6 >= 3 = length(X)
     problem:
      DPs:
       
      TRS:
       a__eq(0(),0()) -> true()
       a__eq(s(X),s(Y)) -> a__eq(X,Y)
       a__eq(X,Y) -> false()
       a__inf(X) -> cons(X,inf(s(X)))
       a__take(0(),X) -> nil()
       a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
       a__length(nil()) -> 0()
       a__length(cons(X,L)) -> s(length(L))
       mark(eq(X1,X2)) -> a__eq(X1,X2)
       mark(inf(X)) -> a__inf(mark(X))
       mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
       mark(length(X)) -> a__length(mark(X))
       mark(0()) -> 0()
       mark(true()) -> true()
       mark(s(X)) -> s(X)
       mark(false()) -> false()
       mark(cons(X1,X2)) -> cons(X1,X2)
       mark(nil()) -> nil()
       a__eq(X1,X2) -> eq(X1,X2)
       a__inf(X) -> inf(X)
       a__take(X1,X2) -> take(X1,X2)
       a__length(X) -> length(X)
     Qed