TRS:
 {   f(0()) -> cons(0()),
  f(s(0())) -> f(p(s(0()))),
    p(s(X)) -> X}
 Fail