MAYBE

Problem:
 from(X) -> cons(X)
 length() -> 0()
 length() -> s(length1())
 length1() -> length()

Proof:
 DP Processor:
  DPs:
   length#() -> length1#()
   length1#() -> length#()
  TRS:
   from(X) -> cons(X)
   length() -> 0()
   length() -> s(length1())
   length1() -> length()
  EDG Processor:
   DPs:
    length#() -> length1#()
    length1#() -> length#()
   TRS:
    from(X) -> cons(X)
    length() -> 0()
    length() -> s(length1())
    length1() -> length()
   graph:
    length1#() -> length#() -> length#() -> length1#()
    length#() -> length1#() -> length1#() -> length#()
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 2/4
    DPs:
     length1#() -> length#()
     length#() -> length1#()
    TRS:
     from(X) -> cons(X)
     length() -> 0()
     length() -> s(length1())
     length1() -> length()
    Open