MAYBE MAYBE TRS: { cond(true(), n, l) -> l, cond(false(), n, l) -> tail(nthtail(s(n), l)), ge(u, 0()) -> true(), ge(s(u), s(v)) -> ge(u, v), ge(0(), s(v)) -> false(), length(nil()) -> 0(), length(cons(x, l)) -> s(length(l)), nthtail(n, l) -> cond(ge(n, length(l)), n, l), tail(nil()) -> nil(), tail(cons(x, l)) -> l } DUP: We consider a duplicating system. Trs: { cond(true(), n, l) -> l, cond(false(), n, l) -> tail(nthtail(s(n), l)), ge(u, 0()) -> true(), ge(s(u), s(v)) -> ge(u, v), ge(0(), s(v)) -> false(), length(nil()) -> 0(), length(cons(x, l)) -> s(length(l)), nthtail(n, l) -> cond(ge(n, length(l)), n, l), tail(nil()) -> nil(), tail(cons(x, l)) -> l } Fail