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}
 DP:
  Strict:
   {             st#(n, l) -> cond1#(member(n, l), n, l),
                 st#(n, l) -> member#(n, l),
                  sort#(l) -> st#(0(), l),
      cond1#(true(), n, l) -> st#(s(n), l),
     cond1#(false(), n, l) -> cond2#(gt(n, max(l)), n, l),
     cond1#(false(), n, l) -> gt#(n, max(l)),
     cond1#(false(), n, l) -> max#(l),
    member#(n, cons(m, l)) -> member#(n, l),
    member#(n, cons(m, l)) -> or#(equal(n, m), member(n, l)),
    member#(n, cons(m, l)) -> equal#(n, m),
     cond2#(false(), n, l) -> st#(s(n), l),
           gt#(s(u), s(v)) -> gt#(u, v),
          max#(cons(u, l)) -> gt#(u, max(l)),
          max#(cons(u, l)) -> max#(l),
          max#(cons(u, l)) -> if#(gt(u, max(l)), u, max(l)),
        equal#(s(x), s(y)) -> equal#(x, y)}
  Weak:
  {             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}
  EDG:
   {(cond2#(false(), n, l) -> st#(s(n), l), st#(n, l) -> member#(n, l))
    (cond2#(false(), n, l) -> st#(s(n), l), st#(n, l) -> cond1#(member(n, l), n, l))
    (gt#(s(u), s(v)) -> gt#(u, v), gt#(s(u), s(v)) -> gt#(u, v))
    (max#(cons(u, l)) -> gt#(u, max(l)), gt#(s(u), s(v)) -> gt#(u, v))
    (equal#(s(x), s(y)) -> equal#(x, y), equal#(s(x), s(y)) -> equal#(x, y))
    (st#(n, l) -> cond1#(member(n, l), n, l), cond1#(false(), n, l) -> max#(l))
    (st#(n, l) -> cond1#(member(n, l), n, l), cond1#(false(), n, l) -> gt#(n, max(l)))
    (st#(n, l) -> cond1#(member(n, l), n, l), cond1#(false(), n, l) -> cond2#(gt(n, max(l)), n, l))
    (st#(n, l) -> cond1#(member(n, l), n, l), cond1#(true(), n, l) -> st#(s(n), l))
    (cond1#(false(), n, l) -> cond2#(gt(n, max(l)), n, l), cond2#(false(), n, l) -> st#(s(n), l))
    (cond1#(false(), n, l) -> max#(l), max#(cons(u, l)) -> if#(gt(u, max(l)), u, max(l)))
    (cond1#(false(), n, l) -> max#(l), max#(cons(u, l)) -> max#(l))
    (cond1#(false(), n, l) -> max#(l), max#(cons(u, l)) -> gt#(u, max(l)))
    (sort#(l) -> st#(0(), l), st#(n, l) -> member#(n, l))
    (sort#(l) -> st#(0(), l), st#(n, l) -> cond1#(member(n, l), n, l))
    (max#(cons(u, l)) -> max#(l), max#(cons(u, l)) -> gt#(u, max(l)))
    (max#(cons(u, l)) -> max#(l), max#(cons(u, l)) -> max#(l))
    (max#(cons(u, l)) -> max#(l), max#(cons(u, l)) -> if#(gt(u, max(l)), u, max(l)))
    (member#(n, cons(m, l)) -> member#(n, l), member#(n, cons(m, l)) -> member#(n, l))
    (member#(n, cons(m, l)) -> member#(n, l), member#(n, cons(m, l)) -> or#(equal(n, m), member(n, l)))
    (member#(n, cons(m, l)) -> member#(n, l), member#(n, cons(m, l)) -> equal#(n, m))
    (st#(n, l) -> member#(n, l), member#(n, cons(m, l)) -> member#(n, l))
    (st#(n, l) -> member#(n, l), member#(n, cons(m, l)) -> or#(equal(n, m), member(n, l)))
    (st#(n, l) -> member#(n, l), member#(n, cons(m, l)) -> equal#(n, m))
    (cond1#(false(), n, l) -> gt#(n, max(l)), gt#(s(u), s(v)) -> gt#(u, v))
    (member#(n, cons(m, l)) -> equal#(n, m), equal#(s(x), s(y)) -> equal#(x, y))
    (cond1#(true(), n, l) -> st#(s(n), l), st#(n, l) -> cond1#(member(n, l), n, l))
    (cond1#(true(), n, l) -> st#(s(n), l), st#(n, l) -> member#(n, l))}
   SCCS:
    Scc:
     {equal#(s(x), s(y)) -> equal#(x, y)}
    Scc:
     {max#(cons(u, l)) -> max#(l)}
    Scc:
     {gt#(s(u), s(v)) -> gt#(u, v)}
    Scc:
     {member#(n, cons(m, l)) -> member#(n, l)}
    Scc:
     {            st#(n, l) -> cond1#(member(n, l), n, l),
       cond1#(true(), n, l) -> st#(s(n), l),
      cond1#(false(), n, l) -> cond2#(gt(n, max(l)), n, l),
      cond2#(false(), n, l) -> st#(s(n), l)}
    SCC:
     Strict:
      {equal#(s(x), s(y)) -> equal#(x, y)}
     Weak:
     {             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}
     SPSC:
      Simple Projection:
       pi(equal#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {max#(cons(u, l)) -> max#(l)}
     Weak:
     {             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}
     SPSC:
      Simple Projection:
       pi(max#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {gt#(s(u), s(v)) -> gt#(u, v)}
     Weak:
     {             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}
     SPSC:
      Simple Projection:
       pi(gt#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {member#(n, cons(m, l)) -> member#(n, l)}
     Weak:
     {             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}
     SPSC:
      Simple Projection:
       pi(member#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {            st#(n, l) -> cond1#(member(n, l), n, l),
        cond1#(true(), n, l) -> st#(s(n), l),
       cond1#(false(), n, l) -> cond2#(gt(n, max(l)), n, l),
       cond2#(false(), n, l) -> st#(s(n), l)}
     Weak:
     {             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