MAYBE
Time: 0.009436
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:
  DP:
   {             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)}
  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}
  EDG:
   {(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))
    (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))
    (equal#(s x, s y) -> equal#(x, y), equal#(s x, s y) -> equal#(x, y))
    (max# cons(u, l) -> gt#(u, max l), gt#(s u, s v) -> gt#(u, v))
    (member#(n, cons(m, l)) -> member#(n, l), member#(n, cons(m, l)) -> equal#(n, m))
    (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)) -> member#(n, 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))
    (cond1#(true(), n, l) -> st#(s n, l), st#(n, l) -> member#(n, l))
    (cond1#(true(), n, l) -> st#(s n, l), st#(n, l) -> cond1#(member(n, l), n, l))
    (member#(n, cons(m, l)) -> equal#(n, m), equal#(s x, s y) -> equal#(x, y))
    (cond2#(false(), n, l) -> st#(s n, l), st#(n, l) -> cond1#(member(n, l), n, l))
    (cond2#(false(), n, l) -> st#(s n, l), st#(n, l) -> member#(n, l))
    (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))
    (cond1#(false(), n, l) -> cond2#(gt(n, max l), n, l), cond2#(false(), n, l) -> st#(s 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))
    (gt#(s u, s v) -> gt#(u, v), gt#(s u, s v) -> gt#(u, v))}
   STATUS:
    arrows: 0.890625
    SCCS (5):
     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:
      {member#(n, cons(m, l)) -> member#(n, l)}
     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 (4):
      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}
      Open
     
     
     SCC (1):
      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}
      Open
     
     SCC (1):
      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}
      Open
     
     
     SCC (1):
      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}
      Open
     
     
     SCC (1):
      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}
      Open