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()))
  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:
    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()))
   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))
   SCC Processor:
    #sccs: 5
    #rules: 10
    #arcs: 31/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()))
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
     problem:
      DPs:
       
      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()))
     Qed
    
    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()))
    Subterm Criterion Processor:
     simple projection:
      pi(filterlow#) = 1
      pi(if1#) = 3
     problem:
      DPs:
       if1#(false(),n,x,xs) -> filterlow#(n,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()))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/4
      
    
    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()))
    Subterm Criterion Processor:
     simple projection:
      pi(filterhigh#) = 1
      pi(if2#) = 3
     problem:
      DPs:
       if2#(false(),n,x,xs) -> filterhigh#(n,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()))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/4
      
    
    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()))
    Subterm Criterion Processor:
     simple projection:
      pi(ge#) = 1
     problem:
      DPs:
       
      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()))
     Qed