TRS:
 {  from(X) -> cons(X),
   length() -> 0(),
   length() -> s(length1()),
  length1() -> length()}
 Fail