MAYBE

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

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