MAYBE

Problem:
 qsort(nil()) -> nil()
 qsort(cons(x,xs)) ->
 append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
 filterlow(n,nil()) -> nil()
 filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
 if1(true(),n,x,xs) -> filterlow(n,xs)
 if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
 filterhigh(n,nil()) -> nil()
 filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
 if2(true(),n,x,xs) -> filterhigh(n,xs)
 if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
 ge(x,0()) -> true()
 ge(0(),s(x)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 append(nil(),ys()) -> ys()
 append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))

Proof:
 DP Processor:
  DPs:
   qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
   qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
   qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
   qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
   qsort#(cons(x,xs)) ->
   append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
   filterlow#(n,cons(x,xs)) -> ge#(n,x)
   filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
   if1#(true(),n,x,xs) -> filterlow#(n,xs)
   if1#(false(),n,x,xs) -> filterlow#(n,xs)
   filterhigh#(n,cons(x,xs)) -> ge#(x,n)
   filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
   if2#(true(),n,x,xs) -> filterhigh#(n,xs)
   if2#(false(),n,x,xs) -> filterhigh#(n,xs)
   ge#(s(x),s(y)) -> ge#(x,y)
   append#(cons(x,xs),ys()) -> append#(xs,ys())
  TRS:
   qsort(nil()) -> nil()
   qsort(cons(x,xs)) ->
   append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
   filterlow(n,nil()) -> nil()
   filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
   if1(true(),n,x,xs) -> filterlow(n,xs)
   if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
   filterhigh(n,nil()) -> nil()
   filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
   if2(true(),n,x,xs) -> filterhigh(n,xs)
   if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
   ge(x,0()) -> true()
   ge(0(),s(x)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   append(nil(),ys()) -> ys()
   append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
  Usable Rule Processor:
   DPs:
    qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
    qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
    qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
    qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
    qsort#(cons(x,xs)) ->
    append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
    filterlow#(n,cons(x,xs)) -> ge#(n,x)
    filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
    if1#(true(),n,x,xs) -> filterlow#(n,xs)
    if1#(false(),n,x,xs) -> filterlow#(n,xs)
    filterhigh#(n,cons(x,xs)) -> ge#(x,n)
    filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
    if2#(true(),n,x,xs) -> filterhigh#(n,xs)
    if2#(false(),n,x,xs) -> filterhigh#(n,xs)
    ge#(s(x),s(y)) -> ge#(x,y)
    append#(cons(x,xs),ys()) -> append#(xs,ys())
   TRS:
    f21(x,y) -> x
    f21(x,y) -> y
    filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
    if2(true(),n,x,xs) -> filterhigh(n,xs)
    if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
    ge(x,0()) -> true()
    ge(0(),s(x)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    filterhigh(n,nil()) -> nil()
    filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
    if1(true(),n,x,xs) -> filterlow(n,xs)
    if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
    filterlow(n,nil()) -> nil()
    qsort(nil()) -> nil()
    qsort(cons(x,xs)) ->
    append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
   TDG Processor:
    DPs:
     qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
     qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
     qsort#(cons(x,xs)) ->
     append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
     filterlow#(n,cons(x,xs)) -> ge#(n,x)
     filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
     if1#(true(),n,x,xs) -> filterlow#(n,xs)
     if1#(false(),n,x,xs) -> filterlow#(n,xs)
     filterhigh#(n,cons(x,xs)) -> ge#(x,n)
     filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
     if2#(true(),n,x,xs) -> filterhigh#(n,xs)
     if2#(false(),n,x,xs) -> filterhigh#(n,xs)
     ge#(s(x),s(y)) -> ge#(x,y)
     append#(cons(x,xs),ys()) -> append#(xs,ys())
    TRS:
     f21(x,y) -> x
     f21(x,y) -> y
     filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
     if2(true(),n,x,xs) -> filterhigh(n,xs)
     if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
     ge(x,0()) -> true()
     ge(0(),s(x)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     filterhigh(n,nil()) -> nil()
     filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
     if1(true(),n,x,xs) -> filterlow(n,xs)
     if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
     filterlow(n,nil()) -> nil()
     qsort(nil()) -> nil()
     qsort(cons(x,xs)) ->
     append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
    graph:
     if2#(false(),n,x,xs) -> filterhigh#(n,xs) ->
     filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
     if2#(false(),n,x,xs) -> filterhigh#(n,xs) ->
     filterhigh#(n,cons(x,xs)) -> ge#(x,n)
     if2#(true(),n,x,xs) -> filterhigh#(n,xs) ->
     filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
     if2#(true(),n,x,xs) -> filterhigh#(n,xs) ->
     filterhigh#(n,cons(x,xs)) -> ge#(x,n)
     if1#(false(),n,x,xs) -> filterlow#(n,xs) ->
     filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
     if1#(false(),n,x,xs) -> filterlow#(n,xs) ->
     filterlow#(n,cons(x,xs)) -> ge#(n,x)
     if1#(true(),n,x,xs) -> filterlow#(n,xs) ->
     filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
     if1#(true(),n,x,xs) -> filterlow#(n,xs) ->
     filterlow#(n,cons(x,xs)) -> ge#(n,x)
     ge#(s(x),s(y)) -> ge#(x,y) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     append#(cons(x,xs),ys()) -> append#(xs,ys()) ->
     append#(cons(x,xs),ys()) -> append#(xs,ys())
     filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) ->
     if1#(false(),n,x,xs) -> filterlow#(n,xs)
     filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) ->
     if1#(true(),n,x,xs) -> filterlow#(n,xs)
     filterlow#(n,cons(x,xs)) -> ge#(n,x) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) ->
     if2#(false(),n,x,xs) -> filterhigh#(n,xs)
     filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) ->
     if2#(true(),n,x,xs) -> filterhigh#(n,xs)
     filterhigh#(n,cons(x,xs)) -> ge#(x,n) ->
     ge#(s(x),s(y)) -> ge#(x,y)
     qsort#(cons(x,xs)) ->
     append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs))))) ->
     append#(cons(x,xs),ys()) -> append#(xs,ys())
     qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs)) ->
     filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
     qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs)) ->
     filterlow#(n,cons(x,xs)) -> ge#(n,x)
     qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs)) ->
     filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
     qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs)) ->
     filterhigh#(n,cons(x,xs)) -> ge#(x,n)
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) ->
     append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) ->
     append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
     qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
     qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
    EDG Processor:
     DPs:
      qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
      qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
      qsort#(cons(x,xs)) ->
      append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
      filterlow#(n,cons(x,xs)) -> ge#(n,x)
      filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
      if1#(true(),n,x,xs) -> filterlow#(n,xs)
      if1#(false(),n,x,xs) -> filterlow#(n,xs)
      filterhigh#(n,cons(x,xs)) -> ge#(x,n)
      filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
      if2#(true(),n,x,xs) -> filterhigh#(n,xs)
      if2#(false(),n,x,xs) -> filterhigh#(n,xs)
      ge#(s(x),s(y)) -> ge#(x,y)
      append#(cons(x,xs),ys()) -> append#(xs,ys())
     TRS:
      f21(x,y) -> x
      f21(x,y) -> y
      filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
      if2(true(),n,x,xs) -> filterhigh(n,xs)
      if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
      ge(x,0()) -> true()
      ge(0(),s(x)) -> false()
      ge(s(x),s(y)) -> ge(x,y)
      filterhigh(n,nil()) -> nil()
      filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
      if1(true(),n,x,xs) -> filterlow(n,xs)
      if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
      filterlow(n,nil()) -> nil()
      qsort(nil()) -> nil()
      qsort(cons(x,xs)) ->
      append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
     graph:
      if2#(false(),n,x,xs) -> filterhigh#(n,xs) ->
      filterhigh#(n,cons(x,xs)) -> ge#(x,n)
      if2#(false(),n,x,xs) -> filterhigh#(n,xs) ->
      filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
      if2#(true(),n,x,xs) -> filterhigh#(n,xs) ->
      filterhigh#(n,cons(x,xs)) -> ge#(x,n)
      if2#(true(),n,x,xs) -> filterhigh#(n,xs) ->
      filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
      if1#(false(),n,x,xs) -> filterlow#(n,xs) ->
      filterlow#(n,cons(x,xs)) -> ge#(n,x)
      if1#(false(),n,x,xs) -> filterlow#(n,xs) ->
      filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
      if1#(true(),n,x,xs) -> filterlow#(n,xs) ->
      filterlow#(n,cons(x,xs)) -> ge#(n,x)
      if1#(true(),n,x,xs) -> filterlow#(n,xs) ->
      filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
      ge#(s(x),s(y)) -> ge#(x,y) ->
      ge#(s(x),s(y)) -> ge#(x,y)
      append#(cons(x,xs),ys()) -> append#(xs,ys()) ->
      append#(cons(x,xs),ys()) -> append#(xs,ys())
      filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) ->
      if1#(true(),n,x,xs) -> filterlow#(n,xs)
      filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) ->
      if1#(false(),n,x,xs) -> filterlow#(n,xs)
      filterlow#(n,cons(x,xs)) -> ge#(n,x) ->
      ge#(s(x),s(y)) -> ge#(x,y)
      filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) ->
      if2#(true(),n,x,xs) -> filterhigh#(n,xs)
      filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) ->
      if2#(false(),n,x,xs) -> filterhigh#(n,xs)
      filterhigh#(n,cons(x,xs)) -> ge#(x,n) ->
      ge#(s(x),s(y)) -> ge#(x,y)
      qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs)) ->
      filterlow#(n,cons(x,xs)) -> ge#(n,x)
      qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs)) ->
      filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
      qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs)) ->
      filterhigh#(n,cons(x,xs)) -> ge#(x,n)
      qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs)) ->
      filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) ->
      append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
      qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs))) ->
      qsort#(cons(x,xs)) ->
      append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
     Restore Modifier:
      DPs:
       qsort#(cons(x,xs)) -> filterhigh#(x,cons(x,xs))
       qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
       qsort#(cons(x,xs)) -> filterlow#(x,cons(x,xs))
       qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
       qsort#(cons(x,xs)) ->
       append#(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
       filterlow#(n,cons(x,xs)) -> ge#(n,x)
       filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
       if1#(true(),n,x,xs) -> filterlow#(n,xs)
       if1#(false(),n,x,xs) -> filterlow#(n,xs)
       filterhigh#(n,cons(x,xs)) -> ge#(x,n)
       filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
       if2#(true(),n,x,xs) -> filterhigh#(n,xs)
       if2#(false(),n,x,xs) -> filterhigh#(n,xs)
       ge#(s(x),s(y)) -> ge#(x,y)
       append#(cons(x,xs),ys()) -> append#(xs,ys())
      TRS:
       qsort(nil()) -> nil()
       qsort(cons(x,xs)) ->
       append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
       filterlow(n,nil()) -> nil()
       filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
       if1(true(),n,x,xs) -> filterlow(n,xs)
       if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
       filterhigh(n,nil()) -> nil()
       filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
       if2(true(),n,x,xs) -> filterhigh(n,xs)
       if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
       ge(x,0()) -> true()
       ge(0(),s(x)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       append(nil(),ys()) -> ys()
       append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
      SCC Processor:
       #sccs: 5
       #rules: 10
       #arcs: 30/225
       DPs:
        qsort#(cons(x,xs)) -> qsort#(filterhigh(x,cons(x,xs)))
        qsort#(cons(x,xs)) -> qsort#(filterlow(x,cons(x,xs)))
       TRS:
        qsort(nil()) -> nil()
        qsort(cons(x,xs)) ->
        append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
        filterlow(n,nil()) -> nil()
        filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
        if1(true(),n,x,xs) -> filterlow(n,xs)
        if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
        filterhigh(n,nil()) -> nil()
        filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
        if2(true(),n,x,xs) -> filterhigh(n,xs)
        if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
        ge(x,0()) -> true()
        ge(0(),s(x)) -> false()
        ge(s(x),s(y)) -> ge(x,y)
        append(nil(),ys()) -> ys()
        append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
       Open
       
       DPs:
        append#(cons(x,xs),ys()) -> append#(xs,ys())
       TRS:
        qsort(nil()) -> nil()
        qsort(cons(x,xs)) ->
        append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
        filterlow(n,nil()) -> nil()
        filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
        if1(true(),n,x,xs) -> filterlow(n,xs)
        if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
        filterhigh(n,nil()) -> nil()
        filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
        if2(true(),n,x,xs) -> filterhigh(n,xs)
        if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
        ge(x,0()) -> true()
        ge(0(),s(x)) -> false()
        ge(s(x),s(y)) -> ge(x,y)
        append(nil(),ys()) -> ys()
        append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
       Open
       
       DPs:
        if1#(false(),n,x,xs) -> filterlow#(n,xs)
        filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
        if1#(true(),n,x,xs) -> filterlow#(n,xs)
       TRS:
        qsort(nil()) -> nil()
        qsort(cons(x,xs)) ->
        append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
        filterlow(n,nil()) -> nil()
        filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
        if1(true(),n,x,xs) -> filterlow(n,xs)
        if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
        filterhigh(n,nil()) -> nil()
        filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
        if2(true(),n,x,xs) -> filterhigh(n,xs)
        if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
        ge(x,0()) -> true()
        ge(0(),s(x)) -> false()
        ge(s(x),s(y)) -> ge(x,y)
        append(nil(),ys()) -> ys()
        append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
       Open
       
       DPs:
        if2#(false(),n,x,xs) -> filterhigh#(n,xs)
        filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
        if2#(true(),n,x,xs) -> filterhigh#(n,xs)
       TRS:
        qsort(nil()) -> nil()
        qsort(cons(x,xs)) ->
        append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
        filterlow(n,nil()) -> nil()
        filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
        if1(true(),n,x,xs) -> filterlow(n,xs)
        if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
        filterhigh(n,nil()) -> nil()
        filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
        if2(true(),n,x,xs) -> filterhigh(n,xs)
        if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
        ge(x,0()) -> true()
        ge(0(),s(x)) -> false()
        ge(s(x),s(y)) -> ge(x,y)
        append(nil(),ys()) -> ys()
        append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
       Open
       
       DPs:
        ge#(s(x),s(y)) -> ge#(x,y)
       TRS:
        qsort(nil()) -> nil()
        qsort(cons(x,xs)) ->
        append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
        filterlow(n,nil()) -> nil()
        filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
        if1(true(),n,x,xs) -> filterlow(n,xs)
        if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
        filterhigh(n,nil()) -> nil()
        filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
        if2(true(),n,x,xs) -> filterhigh(n,xs)
        if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
        ge(x,0()) -> true()
        ge(0(),s(x)) -> false()
        ge(s(x),s(y)) -> ge(x,y)
        append(nil(),ys()) -> ys()
        append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
       Open