MAYBE

Problem:
 eq(0(),0()) -> true()
 eq(s(X),s(Y)) -> eq(X,Y)
 eq(X,Y) -> false()
 inf(X) -> cons(X,inf(s(X)))
 take(0(),X) -> nil()
 take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
 length(nil()) -> 0()
 length(cons(X,L)) -> s(length(L))

Proof:
 DP Processor:
  DPs:
   eq#(s(X),s(Y)) -> eq#(X,Y)
   inf#(X) -> inf#(s(X))
   take#(s(X),cons(Y,L)) -> take#(X,L)
   length#(cons(X,L)) -> length#(L)
  TRS:
   eq(0(),0()) -> true()
   eq(s(X),s(Y)) -> eq(X,Y)
   eq(X,Y) -> false()
   inf(X) -> cons(X,inf(s(X)))
   take(0(),X) -> nil()
   take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
   length(nil()) -> 0()
   length(cons(X,L)) -> s(length(L))
  Usable Rule Processor:
   DPs:
    eq#(s(X),s(Y)) -> eq#(X,Y)
    inf#(X) -> inf#(s(X))
    take#(s(X),cons(Y,L)) -> take#(X,L)
    length#(cons(X,L)) -> length#(L)
   TRS:
    
   TDG Processor:
    DPs:
     eq#(s(X),s(Y)) -> eq#(X,Y)
     inf#(X) -> inf#(s(X))
     take#(s(X),cons(Y,L)) -> take#(X,L)
     length#(cons(X,L)) -> length#(L)
    TRS:
     
    graph:
     length#(cons(X,L)) -> length#(L) ->
     length#(cons(X,L)) -> length#(L)
     take#(s(X),cons(Y,L)) -> take#(X,L) ->
     take#(s(X),cons(Y,L)) -> take#(X,L)
     inf#(X) -> inf#(s(X)) -> inf#(X) -> inf#(s(X))
     eq#(s(X),s(Y)) -> eq#(X,Y) -> eq#(s(X),s(Y)) -> eq#(X,Y)
    CDG Processor:
     DPs:
      eq#(s(X),s(Y)) -> eq#(X,Y)
      inf#(X) -> inf#(s(X))
      take#(s(X),cons(Y,L)) -> take#(X,L)
      length#(cons(X,L)) -> length#(L)
     TRS:
      
     graph:
      inf#(X) -> inf#(s(X)) -> inf#(X) -> inf#(s(X))
     Restore Modifier:
      DPs:
       eq#(s(X),s(Y)) -> eq#(X,Y)
       inf#(X) -> inf#(s(X))
       take#(s(X),cons(Y,L)) -> take#(X,L)
       length#(cons(X,L)) -> length#(L)
      TRS:
       eq(0(),0()) -> true()
       eq(s(X),s(Y)) -> eq(X,Y)
       eq(X,Y) -> false()
       inf(X) -> cons(X,inf(s(X)))
       take(0(),X) -> nil()
       take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
       length(nil()) -> 0()
       length(cons(X,L)) -> s(length(L))
      SCC Processor:
       #sccs: 1
       #rules: 1
       #arcs: 1/16
       DPs:
        inf#(X) -> inf#(s(X))
       TRS:
        eq(0(),0()) -> true()
        eq(s(X),s(Y)) -> eq(X,Y)
        eq(X,Y) -> false()
        inf(X) -> cons(X,inf(s(X)))
        take(0(),X) -> nil()
        take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
        length(nil()) -> 0()
        length(cons(X,L)) -> s(length(L))
       Open