MAYBE

Problem:
 app(app(app(sort(),f),g),nil()) -> nil()
 app(app(app(sort(),f),g),app(app(cons(),x),y)) ->
 app(app(app(app(insert(),f),g),app(app(app(sort(),f),g),y)),x)
 app(app(app(app(insert(),f),g),nil()),y) -> app(app(cons(),y),nil())
 app(app(app(app(insert(),f),g),app(app(cons(),x),z)),y) ->
 app(app(cons(),app(app(f,x),y)),app(app(app(app(insert(),f),g),z),app(app(g,x),y)))
 app(app(max(),0()),y) -> y
 app(app(max(),x),0()) -> x
 app(app(max(),app(s(),x)),app(s(),y)) -> app(app(max(),x),y)
 app(app(min(),0()),y) -> 0()
 app(app(min(),x),0()) -> 0()
 app(app(min(),app(s(),x)),app(s(),y)) -> app(app(min(),x),y)
 app(asort(),z) -> app(app(app(sort(),min()),max()),z)
 app(dsort(),z) -> app(app(app(sort(),max()),min()),z)

Proof:
 Uncurry Processor:
  sort3(f,g,nil()) -> nil()
  sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
  insert4(f,g,nil(),y) -> cons2(y,nil())
  insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
  max2(0(),y) -> y
  max2(x,0()) -> x
  max2(s1(x),s1(y)) -> max2(x,y)
  min2(0(),y) -> 0()
  min2(x,0()) -> 0()
  min2(s1(x),s1(y)) -> min2(x,y)
  asort1(z) -> sort3(min(),max(),z)
  dsort1(z) -> sort3(max(),min(),z)
  app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
  app(sort1(x7),x8) -> sort2(x7,x8)
  app(sort(),x8) -> sort1(x8)
  app(cons1(x7),x8) -> cons2(x7,x8)
  app(cons(),x8) -> cons1(x8)
  app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
  app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
  app(insert1(x7),x8) -> insert2(x7,x8)
  app(insert(),x8) -> insert1(x8)
  app(max1(x7),x8) -> max2(x7,x8)
  app(max(),x8) -> max1(x8)
  app(s(),x8) -> s1(x8)
  app(min1(x7),x8) -> min2(x7,x8)
  app(min(),x8) -> min1(x8)
  app(asort(),x8) -> asort1(x8)
  app(dsort(),x8) -> dsort1(x8)
  DP Processor:
   DPs:
    sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
    sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
    insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x)
    insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y)
    insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y))
    insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x)
    insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y)
    max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
    min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
    asort{1,#}(z) -> sort{3,#}(min(),max(),z)
    dsort{1,#}(z) -> sort{3,#}(max(),min(),z)
    app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
    app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
    app#(max1(x7),x8) -> max{2,#}(x7,x8)
    app#(min1(x7),x8) -> min{2,#}(x7,x8)
    app#(asort(),x8) -> asort{1,#}(x8)
    app#(dsort(),x8) -> dsort{1,#}(x8)
   TRS:
    sort3(f,g,nil()) -> nil()
    sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
    insert4(f,g,nil(),y) -> cons2(y,nil())
    insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
    max2(0(),y) -> y
    max2(x,0()) -> x
    max2(s1(x),s1(y)) -> max2(x,y)
    min2(0(),y) -> 0()
    min2(x,0()) -> 0()
    min2(s1(x),s1(y)) -> min2(x,y)
    asort1(z) -> sort3(min(),max(),z)
    dsort1(z) -> sort3(max(),min(),z)
    app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
    app(sort1(x7),x8) -> sort2(x7,x8)
    app(sort(),x8) -> sort1(x8)
    app(cons1(x7),x8) -> cons2(x7,x8)
    app(cons(),x8) -> cons1(x8)
    app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
    app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
    app(insert1(x7),x8) -> insert2(x7,x8)
    app(insert(),x8) -> insert1(x8)
    app(max1(x7),x8) -> max2(x7,x8)
    app(max(),x8) -> max1(x8)
    app(s(),x8) -> s1(x8)
    app(min1(x7),x8) -> min2(x7,x8)
    app(min(),x8) -> min1(x8)
    app(asort(),x8) -> asort1(x8)
    app(dsort(),x8) -> dsort1(x8)
   TDG Processor:
    DPs:
     sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y)
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y))
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y)
     max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
     min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     asort{1,#}(z) -> sort{3,#}(min(),max(),z)
     dsort{1,#}(z) -> sort{3,#}(max(),min(),z)
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
     app#(max1(x7),x8) -> max{2,#}(x7,x8)
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     app#(asort(),x8) -> asort{1,#}(x8)
     app#(dsort(),x8) -> dsort{1,#}(x8)
    TRS:
     sort3(f,g,nil()) -> nil()
     sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
     insert4(f,g,nil(),y) -> cons2(y,nil())
     insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
     max2(0(),y) -> y
     max2(x,0()) -> x
     max2(s1(x),s1(y)) -> max2(x,y)
     min2(0(),y) -> 0()
     min2(x,0()) -> 0()
     min2(s1(x),s1(y)) -> min2(x,y)
     asort1(z) -> sort3(min(),max(),z)
     dsort1(z) -> sort3(max(),min(),z)
     app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
     app(sort1(x7),x8) -> sort2(x7,x8)
     app(sort(),x8) -> sort1(x8)
     app(cons1(x7),x8) -> cons2(x7,x8)
     app(cons(),x8) -> cons1(x8)
     app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
     app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
     app(insert1(x7),x8) -> insert2(x7,x8)
     app(insert(),x8) -> insert1(x8)
     app(max1(x7),x8) -> max2(x7,x8)
     app(max(),x8) -> max1(x8)
     app(s(),x8) -> s1(x8)
     app(min1(x7),x8) -> min2(x7,x8)
     app(min(),x8) -> min1(x8)
     app(asort(),x8) -> asort1(x8)
     app(dsort(),x8) -> dsort1(x8)
    graph:
     dsort{1,#}(z) -> sort{3,#}(max(),min(),z) ->
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
     dsort{1,#}(z) -> sort{3,#}(max(),min(),z) ->
     sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
     asort{1,#}(z) -> sort{3,#}(min(),max(),z) ->
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
     asort{1,#}(z) -> sort{3,#}(min(),max(),z) ->
     sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
     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)
     app#(min1(x7),x8) -> min{2,#}(x7,x8) ->
     min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     app#(max1(x7),x8) -> max{2,#}(x7,x8) ->
     max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y)
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x)
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8) ->
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y))
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y)
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x)
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8) ->
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8) ->
     sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
     app#(dsort(),x8) -> dsort{1,#}(x8) ->
     dsort{1,#}(z) -> sort{3,#}(max(),min(),z)
     app#(asort(),x8) -> asort{1,#}(x8) ->
     asort{1,#}(z) -> sort{3,#}(min(),max(),z)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y) ->
     app#(dsort(),x8) -> dsort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y) ->
     app#(asort(),x8) -> asort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y) ->
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y) ->
     app#(max1(x7),x8) -> max{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y) ->
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y) ->
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y) ->
     app#(dsort(),x8) -> dsort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y) ->
     app#(asort(),x8) -> asort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y) ->
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y) ->
     app#(max1(x7),x8) -> max{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y) ->
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y) ->
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x) ->
     app#(dsort(),x8) -> dsort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x) ->
     app#(asort(),x8) -> asort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x) ->
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x) ->
     app#(max1(x7),x8) -> max{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x) ->
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x) ->
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x) ->
     app#(dsort(),x8) -> dsort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x) ->
     app#(asort(),x8) -> asort{1,#}(x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x) ->
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x) ->
     app#(max1(x7),x8) -> max{2,#}(x7,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x) ->
     app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x) ->
     app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y)) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y)
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y)) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x)
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y)) ->
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y))
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y)) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y)
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y)) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x)
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y)
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x)
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x) ->
     insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y))
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y)
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x) ->
     insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x)
     sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y) ->
     sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
     sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y) -> sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
    SCC Processor:
     #sccs: 3
     #rules: 15
     #arcs: 53/289
     DPs:
      dsort{1,#}(z) -> sort{3,#}(max(),min(),z)
      sort{3,#}(f,g,cons2(x,y)) -> sort{3,#}(f,g,y)
      sort{3,#}(f,g,cons2(x,y)) -> insert{4,#}(f,g,sort3(f,g,y),x)
      insert{4,#}(f,g,cons2(x,z),y) -> app#(g,x)
      app#(sort2(x7,x6),x8) -> sort{3,#}(x7,x6,x8)
      app#(insert3(x7,x6,x5),x8) -> insert{4,#}(x7,x6,x5,x8)
      insert{4,#}(f,g,cons2(x,z),y) -> app#(app(g,x),y)
      app#(asort(),x8) -> asort{1,#}(x8)
      asort{1,#}(z) -> sort{3,#}(min(),max(),z)
      app#(dsort(),x8) -> dsort{1,#}(x8)
      insert{4,#}(f,g,cons2(x,z),y) -> insert{4,#}(f,g,z,app(app(g,x),y))
      insert{4,#}(f,g,cons2(x,z),y) -> app#(f,x)
      insert{4,#}(f,g,cons2(x,z),y) -> app#(app(f,x),y)
     TRS:
      sort3(f,g,nil()) -> nil()
      sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
      insert4(f,g,nil(),y) -> cons2(y,nil())
      insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
      max2(0(),y) -> y
      max2(x,0()) -> x
      max2(s1(x),s1(y)) -> max2(x,y)
      min2(0(),y) -> 0()
      min2(x,0()) -> 0()
      min2(s1(x),s1(y)) -> min2(x,y)
      asort1(z) -> sort3(min(),max(),z)
      dsort1(z) -> sort3(max(),min(),z)
      app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
      app(sort1(x7),x8) -> sort2(x7,x8)
      app(sort(),x8) -> sort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
      app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
      app(insert1(x7),x8) -> insert2(x7,x8)
      app(insert(),x8) -> insert1(x8)
      app(max1(x7),x8) -> max2(x7,x8)
      app(max(),x8) -> max1(x8)
      app(s(),x8) -> s1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(asort(),x8) -> asort1(x8)
      app(dsort(),x8) -> dsort1(x8)
     Open
     
     DPs:
      min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
     TRS:
      sort3(f,g,nil()) -> nil()
      sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
      insert4(f,g,nil(),y) -> cons2(y,nil())
      insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
      max2(0(),y) -> y
      max2(x,0()) -> x
      max2(s1(x),s1(y)) -> max2(x,y)
      min2(0(),y) -> 0()
      min2(x,0()) -> 0()
      min2(s1(x),s1(y)) -> min2(x,y)
      asort1(z) -> sort3(min(),max(),z)
      dsort1(z) -> sort3(max(),min(),z)
      app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
      app(sort1(x7),x8) -> sort2(x7,x8)
      app(sort(),x8) -> sort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
      app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
      app(insert1(x7),x8) -> insert2(x7,x8)
      app(insert(),x8) -> insert1(x8)
      app(max1(x7),x8) -> max2(x7,x8)
      app(max(),x8) -> max1(x8)
      app(s(),x8) -> s1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(asort(),x8) -> asort1(x8)
      app(dsort(),x8) -> dsort1(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(min{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        sort3(f,g,nil()) -> nil()
        sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
        insert4(f,g,nil(),y) -> cons2(y,nil())
        insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
        max2(0(),y) -> y
        max2(x,0()) -> x
        max2(s1(x),s1(y)) -> max2(x,y)
        min2(0(),y) -> 0()
        min2(x,0()) -> 0()
        min2(s1(x),s1(y)) -> min2(x,y)
        asort1(z) -> sort3(min(),max(),z)
        dsort1(z) -> sort3(max(),min(),z)
        app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
        app(sort1(x7),x8) -> sort2(x7,x8)
        app(sort(),x8) -> sort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
        app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
        app(insert1(x7),x8) -> insert2(x7,x8)
        app(insert(),x8) -> insert1(x8)
        app(max1(x7),x8) -> max2(x7,x8)
        app(max(),x8) -> max1(x8)
        app(s(),x8) -> s1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(asort(),x8) -> asort1(x8)
        app(dsort(),x8) -> dsort1(x8)
      Qed
     
     DPs:
      max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
     TRS:
      sort3(f,g,nil()) -> nil()
      sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
      insert4(f,g,nil(),y) -> cons2(y,nil())
      insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
      max2(0(),y) -> y
      max2(x,0()) -> x
      max2(s1(x),s1(y)) -> max2(x,y)
      min2(0(),y) -> 0()
      min2(x,0()) -> 0()
      min2(s1(x),s1(y)) -> min2(x,y)
      asort1(z) -> sort3(min(),max(),z)
      dsort1(z) -> sort3(max(),min(),z)
      app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
      app(sort1(x7),x8) -> sort2(x7,x8)
      app(sort(),x8) -> sort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
      app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
      app(insert1(x7),x8) -> insert2(x7,x8)
      app(insert(),x8) -> insert1(x8)
      app(max1(x7),x8) -> max2(x7,x8)
      app(max(),x8) -> max1(x8)
      app(s(),x8) -> s1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(asort(),x8) -> asort1(x8)
      app(dsort(),x8) -> dsort1(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(max{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        sort3(f,g,nil()) -> nil()
        sort3(f,g,cons2(x,y)) -> insert4(f,g,sort3(f,g,y),x)
        insert4(f,g,nil(),y) -> cons2(y,nil())
        insert4(f,g,cons2(x,z),y) -> cons2(app(app(f,x),y),insert4(f,g,z,app(app(g,x),y)))
        max2(0(),y) -> y
        max2(x,0()) -> x
        max2(s1(x),s1(y)) -> max2(x,y)
        min2(0(),y) -> 0()
        min2(x,0()) -> 0()
        min2(s1(x),s1(y)) -> min2(x,y)
        asort1(z) -> sort3(min(),max(),z)
        dsort1(z) -> sort3(max(),min(),z)
        app(sort2(x7,x6),x8) -> sort3(x7,x6,x8)
        app(sort1(x7),x8) -> sort2(x7,x8)
        app(sort(),x8) -> sort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(insert3(x7,x6,x5),x8) -> insert4(x7,x6,x5,x8)
        app(insert2(x7,x6),x8) -> insert3(x7,x6,x8)
        app(insert1(x7),x8) -> insert2(x7,x8)
        app(insert(),x8) -> insert1(x8)
        app(max1(x7),x8) -> max2(x7,x8)
        app(max(),x8) -> max1(x8)
        app(s(),x8) -> s1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(asort(),x8) -> asort1(x8)
        app(dsort(),x8) -> dsort1(x8)
      Qed