Input TRS:
    1: from(X) -> cons(X)
    2: length() -> 0()
    3: length() -> s(length1())
    4: length1() -> length()
Number of Rules: 4
Direct QWPOS(mPol) ... failed.