MAYBE

Problem:
 app(app(max(),0()),x) -> x
 app(app(max(),x),0()) -> x
 app(app(max(),app(s(),x)),app(s(),y)) -> app(app(max(),x),y)
 app(app(min(),0()),x) -> 0()
 app(app(min(),x),0()) -> 0()
 app(app(min(),app(s(),x)),app(s(),y)) -> app(app(min(),x),y)
 app(app(app(app(insert(),f),g),nil()),x) -> app(app(cons(),x),nil())
 app(app(app(app(insert(),f),g),app(app(cons(),h),t)),x) ->
 app(app(cons(),app(app(f,x),h)),app(app(app(app(insert(),f),g),t),app(app(g,x),h)))
 app(app(app(sort(),f),g),nil()) -> nil()
 app(app(app(sort(),f),g),app(app(cons(),h),t)) ->
 app(app(app(app(insert(),f),g),app(app(app(sort(),f),g),t)),h)
 app(ascending_sort(),l) -> app(app(app(sort(),min()),max()),l)
 app(descending_sort(),l) -> app(app(app(sort(),max()),min()),l)

Proof:
 Uncurry Processor:
  max2(0(),x) -> x
  max2(x,0()) -> x
  max2(s1(x),s1(y)) -> max2(x,y)
  min2(0(),x) -> 0()
  min2(x,0()) -> 0()
  min2(s1(x),s1(y)) -> min2(x,y)
  insert4(f,g,nil(),x) -> cons2(x,nil())
  insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
  sort3(f,g,nil()) -> nil()
  sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
  ascending_sort1(l) -> sort3(min(),max(),l)
  descending_sort1(l) -> sort3(max(),min(),l)
  app(max1(x9),x10) -> max2(x9,x10)
  app(max(),x10) -> max1(x10)
  app(s(),x10) -> s1(x10)
  app(min1(x9),x10) -> min2(x9,x10)
  app(min(),x10) -> min1(x10)
  app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
  app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
  app(insert1(x9),x10) -> insert2(x9,x10)
  app(insert(),x10) -> insert1(x10)
  app(cons1(x9),x10) -> cons2(x9,x10)
  app(cons(),x10) -> cons1(x10)
  app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
  app(sort1(x9),x10) -> sort2(x9,x10)
  app(sort(),x10) -> sort1(x10)
  app(ascending_sort(),x10) -> ascending_sort1(x10)
  app(descending_sort(),x10) -> descending_sort1(x10)
  DP Processor:
   DPs:
    max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
    min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
    insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
    insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
    insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
    insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
    insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
    sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
    sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
    ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
    descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
    app#(max1(x9),x10) -> max{2,#}(x9,x10)
    app#(min1(x9),x10) -> min{2,#}(x9,x10)
    app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
    app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
    app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
    app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
   TRS:
    max2(0(),x) -> x
    max2(x,0()) -> x
    max2(s1(x),s1(y)) -> max2(x,y)
    min2(0(),x) -> 0()
    min2(x,0()) -> 0()
    min2(s1(x),s1(y)) -> min2(x,y)
    insert4(f,g,nil(),x) -> cons2(x,nil())
    insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
    sort3(f,g,nil()) -> nil()
    sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
    ascending_sort1(l) -> sort3(min(),max(),l)
    descending_sort1(l) -> sort3(max(),min(),l)
    app(max1(x9),x10) -> max2(x9,x10)
    app(max(),x10) -> max1(x10)
    app(s(),x10) -> s1(x10)
    app(min1(x9),x10) -> min2(x9,x10)
    app(min(),x10) -> min1(x10)
    app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
    app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
    app(insert1(x9),x10) -> insert2(x9,x10)
    app(insert(),x10) -> insert1(x10)
    app(cons1(x9),x10) -> cons2(x9,x10)
    app(cons(),x10) -> cons1(x10)
    app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
    app(sort1(x9),x10) -> sort2(x9,x10)
    app(sort(),x10) -> sort1(x10)
    app(ascending_sort(),x10) -> ascending_sort1(x10)
    app(descending_sort(),x10) -> descending_sort1(x10)
   TDG Processor:
    DPs:
     max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
     min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
     ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
     descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
     app#(max1(x9),x10) -> max{2,#}(x9,x10)
     app#(min1(x9),x10) -> min{2,#}(x9,x10)
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
     app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
     app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
    TRS:
     max2(0(),x) -> x
     max2(x,0()) -> x
     max2(s1(x),s1(y)) -> max2(x,y)
     min2(0(),x) -> 0()
     min2(x,0()) -> 0()
     min2(s1(x),s1(y)) -> min2(x,y)
     insert4(f,g,nil(),x) -> cons2(x,nil())
     insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
     sort3(f,g,nil()) -> nil()
     sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
     ascending_sort1(l) -> sort3(min(),max(),l)
     descending_sort1(l) -> sort3(max(),min(),l)
     app(max1(x9),x10) -> max2(x9,x10)
     app(max(),x10) -> max1(x10)
     app(s(),x10) -> s1(x10)
     app(min1(x9),x10) -> min2(x9,x10)
     app(min(),x10) -> min1(x10)
     app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
     app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
     app(insert1(x9),x10) -> insert2(x9,x10)
     app(insert(),x10) -> insert1(x10)
     app(cons1(x9),x10) -> cons2(x9,x10)
     app(cons(),x10) -> cons1(x10)
     app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
     app(sort1(x9),x10) -> sort2(x9,x10)
     app(sort(),x10) -> sort1(x10)
     app(ascending_sort(),x10) -> ascending_sort1(x10)
     app(descending_sort(),x10) -> descending_sort1(x10)
    graph:
     descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l) ->
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
     descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l) ->
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
     ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l) ->
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
     ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l) ->
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t) ->
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t) ->
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10) ->
     sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10) ->
     sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
     app#(min1(x9),x10) -> min{2,#}(x9,x10) ->
     min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     app#(max1(x9),x10) -> max{2,#}(x9,x10) ->
     max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
     app#(descending_sort(),x10) -> descending_sort{1,#}(x10) ->
     descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
     app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10) ->
     ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
     app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
     app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
     app#(min1(x9),x10) -> min{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
     app#(max1(x9),x10) -> max{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(min1(x9),x10) -> min{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
     app#(max1(x9),x10) -> max{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
     app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
     app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
     app#(min1(x9),x10) -> min{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
     app#(max1(x9),x10) -> max{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
     app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
     app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
     app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
     app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
     app#(min1(x9),x10) -> min{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
     app#(max1(x9),x10) -> max{2,#}(x9,x10)
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
     insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
     insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
     min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y) ->
     min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y) -> max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
    SCC Processor:
     #sccs: 3
     #rules: 15
     #arcs: 53/289
     DPs:
      descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
      sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
      sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
      insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
      app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
      insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
      app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
      app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
      ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
      app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
      insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
      insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
      insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
     TRS:
      max2(0(),x) -> x
      max2(x,0()) -> x
      max2(s1(x),s1(y)) -> max2(x,y)
      min2(0(),x) -> 0()
      min2(x,0()) -> 0()
      min2(s1(x),s1(y)) -> min2(x,y)
      insert4(f,g,nil(),x) -> cons2(x,nil())
      insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
      sort3(f,g,nil()) -> nil()
      sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
      ascending_sort1(l) -> sort3(min(),max(),l)
      descending_sort1(l) -> sort3(max(),min(),l)
      app(max1(x9),x10) -> max2(x9,x10)
      app(max(),x10) -> max1(x10)
      app(s(),x10) -> s1(x10)
      app(min1(x9),x10) -> min2(x9,x10)
      app(min(),x10) -> min1(x10)
      app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
      app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
      app(insert1(x9),x10) -> insert2(x9,x10)
      app(insert(),x10) -> insert1(x10)
      app(cons1(x9),x10) -> cons2(x9,x10)
      app(cons(),x10) -> cons1(x10)
      app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
      app(sort1(x9),x10) -> sort2(x9,x10)
      app(sort(),x10) -> sort1(x10)
      app(ascending_sort(),x10) -> ascending_sort1(x10)
      app(descending_sort(),x10) -> descending_sort1(x10)
     Open
     
     DPs:
      min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     TRS:
      max2(0(),x) -> x
      max2(x,0()) -> x
      max2(s1(x),s1(y)) -> max2(x,y)
      min2(0(),x) -> 0()
      min2(x,0()) -> 0()
      min2(s1(x),s1(y)) -> min2(x,y)
      insert4(f,g,nil(),x) -> cons2(x,nil())
      insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
      sort3(f,g,nil()) -> nil()
      sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
      ascending_sort1(l) -> sort3(min(),max(),l)
      descending_sort1(l) -> sort3(max(),min(),l)
      app(max1(x9),x10) -> max2(x9,x10)
      app(max(),x10) -> max1(x10)
      app(s(),x10) -> s1(x10)
      app(min1(x9),x10) -> min2(x9,x10)
      app(min(),x10) -> min1(x10)
      app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
      app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
      app(insert1(x9),x10) -> insert2(x9,x10)
      app(insert(),x10) -> insert1(x10)
      app(cons1(x9),x10) -> cons2(x9,x10)
      app(cons(),x10) -> cons1(x10)
      app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
      app(sort1(x9),x10) -> sort2(x9,x10)
      app(sort(),x10) -> sort1(x10)
      app(ascending_sort(),x10) -> ascending_sort1(x10)
      app(descending_sort(),x10) -> descending_sort1(x10)
     Subterm Criterion Processor:
      simple projection:
       pi(min{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        max2(0(),x) -> x
        max2(x,0()) -> x
        max2(s1(x),s1(y)) -> max2(x,y)
        min2(0(),x) -> 0()
        min2(x,0()) -> 0()
        min2(s1(x),s1(y)) -> min2(x,y)
        insert4(f,g,nil(),x) -> cons2(x,nil())
        insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
        sort3(f,g,nil()) -> nil()
        sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
        ascending_sort1(l) -> sort3(min(),max(),l)
        descending_sort1(l) -> sort3(max(),min(),l)
        app(max1(x9),x10) -> max2(x9,x10)
        app(max(),x10) -> max1(x10)
        app(s(),x10) -> s1(x10)
        app(min1(x9),x10) -> min2(x9,x10)
        app(min(),x10) -> min1(x10)
        app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
        app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
        app(insert1(x9),x10) -> insert2(x9,x10)
        app(insert(),x10) -> insert1(x10)
        app(cons1(x9),x10) -> cons2(x9,x10)
        app(cons(),x10) -> cons1(x10)
        app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
        app(sort1(x9),x10) -> sort2(x9,x10)
        app(sort(),x10) -> sort1(x10)
        app(ascending_sort(),x10) -> ascending_sort1(x10)
        app(descending_sort(),x10) -> descending_sort1(x10)
      Qed
     
     DPs:
      max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
     TRS:
      max2(0(),x) -> x
      max2(x,0()) -> x
      max2(s1(x),s1(y)) -> max2(x,y)
      min2(0(),x) -> 0()
      min2(x,0()) -> 0()
      min2(s1(x),s1(y)) -> min2(x,y)
      insert4(f,g,nil(),x) -> cons2(x,nil())
      insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
      sort3(f,g,nil()) -> nil()
      sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
      ascending_sort1(l) -> sort3(min(),max(),l)
      descending_sort1(l) -> sort3(max(),min(),l)
      app(max1(x9),x10) -> max2(x9,x10)
      app(max(),x10) -> max1(x10)
      app(s(),x10) -> s1(x10)
      app(min1(x9),x10) -> min2(x9,x10)
      app(min(),x10) -> min1(x10)
      app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
      app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
      app(insert1(x9),x10) -> insert2(x9,x10)
      app(insert(),x10) -> insert1(x10)
      app(cons1(x9),x10) -> cons2(x9,x10)
      app(cons(),x10) -> cons1(x10)
      app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
      app(sort1(x9),x10) -> sort2(x9,x10)
      app(sort(),x10) -> sort1(x10)
      app(ascending_sort(),x10) -> ascending_sort1(x10)
      app(descending_sort(),x10) -> descending_sort1(x10)
     Subterm Criterion Processor:
      simple projection:
       pi(max{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        max2(0(),x) -> x
        max2(x,0()) -> x
        max2(s1(x),s1(y)) -> max2(x,y)
        min2(0(),x) -> 0()
        min2(x,0()) -> 0()
        min2(s1(x),s1(y)) -> min2(x,y)
        insert4(f,g,nil(),x) -> cons2(x,nil())
        insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
        sort3(f,g,nil()) -> nil()
        sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
        ascending_sort1(l) -> sort3(min(),max(),l)
        descending_sort1(l) -> sort3(max(),min(),l)
        app(max1(x9),x10) -> max2(x9,x10)
        app(max(),x10) -> max1(x10)
        app(s(),x10) -> s1(x10)
        app(min1(x9),x10) -> min2(x9,x10)
        app(min(),x10) -> min1(x10)
        app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
        app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
        app(insert1(x9),x10) -> insert2(x9,x10)
        app(insert(),x10) -> insert1(x10)
        app(cons1(x9),x10) -> cons2(x9,x10)
        app(cons(),x10) -> cons1(x10)
        app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
        app(sort1(x9),x10) -> sort2(x9,x10)
        app(sort(),x10) -> sort1(x10)
        app(ascending_sort(),x10) -> ascending_sort1(x10)
        app(descending_sort(),x10) -> descending_sort1(x10)
      Qed