MAYBE

Problem:
 sort(l) -> st(0(),l)
 st(n,l) -> cond1(member(n,l),n,l)
 cond1(true(),n,l) -> cons(n,st(s(n),l))
 cond1(false(),n,l) -> cond2(gt(n,max(l)),n,l)
 cond2(true(),n,l) -> nil()
 cond2(false(),n,l) -> st(s(n),l)
 member(n,nil()) -> false()
 member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
 or(x,true()) -> true()
 or(x,false()) -> x
 equal(0(),0()) -> true()
 equal(s(x),0()) -> false()
 equal(0(),s(y)) -> false()
 equal(s(x),s(y)) -> equal(x,y)
 gt(0(),v) -> false()
 gt(s(u),0()) -> true()
 gt(s(u),s(v)) -> gt(u,v)
 max(nil()) -> 0()
 max(cons(u,l)) -> if(gt(u,max(l)),u,max(l))
 if(true(),u,v) -> u
 if(false(),u,v) -> v

Proof:
 DP Processor:
  DPs:
   sort#(l) -> st#(0(),l)
   st#(n,l) -> member#(n,l)
   st#(n,l) -> cond1#(member(n,l),n,l)
   cond1#(true(),n,l) -> st#(s(n),l)
   cond1#(false(),n,l) -> max#(l)
   cond1#(false(),n,l) -> gt#(n,max(l))
   cond1#(false(),n,l) -> cond2#(gt(n,max(l)),n,l)
   cond2#(false(),n,l) -> st#(s(n),l)
   member#(n,cons(m,l)) -> member#(n,l)
   member#(n,cons(m,l)) -> equal#(n,m)
   member#(n,cons(m,l)) -> or#(equal(n,m),member(n,l))
   equal#(s(x),s(y)) -> equal#(x,y)
   gt#(s(u),s(v)) -> gt#(u,v)
   max#(cons(u,l)) -> max#(l)
   max#(cons(u,l)) -> gt#(u,max(l))
   max#(cons(u,l)) -> if#(gt(u,max(l)),u,max(l))
  TRS:
   sort(l) -> st(0(),l)
   st(n,l) -> cond1(member(n,l),n,l)
   cond1(true(),n,l) -> cons(n,st(s(n),l))
   cond1(false(),n,l) -> cond2(gt(n,max(l)),n,l)
   cond2(true(),n,l) -> nil()
   cond2(false(),n,l) -> st(s(n),l)
   member(n,nil()) -> false()
   member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
   or(x,true()) -> true()
   or(x,false()) -> x
   equal(0(),0()) -> true()
   equal(s(x),0()) -> false()
   equal(0(),s(y)) -> false()
   equal(s(x),s(y)) -> equal(x,y)
   gt(0(),v) -> false()
   gt(s(u),0()) -> true()
   gt(s(u),s(v)) -> gt(u,v)
   max(nil()) -> 0()
   max(cons(u,l)) -> if(gt(u,max(l)),u,max(l))
   if(true(),u,v) -> u
   if(false(),u,v) -> v
  Usable Rule Processor:
   DPs:
    sort#(l) -> st#(0(),l)
    st#(n,l) -> member#(n,l)
    st#(n,l) -> cond1#(member(n,l),n,l)
    cond1#(true(),n,l) -> st#(s(n),l)
    cond1#(false(),n,l) -> max#(l)
    cond1#(false(),n,l) -> gt#(n,max(l))
    cond1#(false(),n,l) -> cond2#(gt(n,max(l)),n,l)
    cond2#(false(),n,l) -> st#(s(n),l)
    member#(n,cons(m,l)) -> member#(n,l)
    member#(n,cons(m,l)) -> equal#(n,m)
    member#(n,cons(m,l)) -> or#(equal(n,m),member(n,l))
    equal#(s(x),s(y)) -> equal#(x,y)
    gt#(s(u),s(v)) -> gt#(u,v)
    max#(cons(u,l)) -> max#(l)
    max#(cons(u,l)) -> gt#(u,max(l))
    max#(cons(u,l)) -> if#(gt(u,max(l)),u,max(l))
   TRS:
    member(n,nil()) -> false()
    member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
    or(x,true()) -> true()
    or(x,false()) -> x
    equal(0(),0()) -> true()
    equal(s(x),0()) -> false()
    equal(0(),s(y)) -> false()
    equal(s(x),s(y)) -> equal(x,y)
    max(nil()) -> 0()
    max(cons(u,l)) -> if(gt(u,max(l)),u,max(l))
    if(true(),u,v) -> u
    if(false(),u,v) -> v
    gt(0(),v) -> false()
    gt(s(u),0()) -> true()
    gt(s(u),s(v)) -> gt(u,v)
   Open