MAYBE
MAYBE
TRS:
 {
               st(n, l) -> cond1(member(n, l), n, l),
                sort(l) -> st(0(), l),
    cond1(true(), n, l) -> cons(n, st(s(n), l)),
   cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l),
  member(n, cons(m, l)) -> or(equal(n, m), member(n, l)),
       member(n, nil()) -> false(),
    cond2(true(), n, l) -> nil(),
   cond2(false(), n, l) -> st(s(n), l),
             gt(0(), v) -> false(),
          gt(s(u), 0()) -> true(),
         gt(s(u), s(v)) -> gt(u, v),
        max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)),
             max(nil()) -> 0(),
          or(x, true()) -> true(),
         or(x, false()) -> x,
        equal(0(), 0()) -> true(),
       equal(0(), s(y)) -> false(),
       equal(s(x), 0()) -> false(),
      equal(s(x), s(y)) -> equal(x, y),
       if(true(), u, v) -> u,
      if(false(), u, v) -> v
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                 st(n, l) -> cond1(member(n, l), n, l),
                  sort(l) -> st(0(), l),
      cond1(true(), n, l) -> cons(n, st(s(n), l)),
     cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l),
    member(n, cons(m, l)) -> or(equal(n, m), member(n, l)),
         member(n, nil()) -> false(),
      cond2(true(), n, l) -> nil(),
     cond2(false(), n, l) -> st(s(n), l),
               gt(0(), v) -> false(),
            gt(s(u), 0()) -> true(),
           gt(s(u), s(v)) -> gt(u, v),
          max(cons(u, l)) -> if(gt(u, max(l)), u, max(l)),
               max(nil()) -> 0(),
            or(x, true()) -> true(),
           or(x, false()) -> x,
          equal(0(), 0()) -> true(),
         equal(0(), s(y)) -> false(),
         equal(s(x), 0()) -> false(),
        equal(s(x), s(y)) -> equal(x, y),
         if(true(), u, v) -> u,
        if(false(), u, v) -> v
   }
  Fail