MAYBE

Problem:
 app(app(le(),0()),y) -> true()
 app(app(le(),app(s(),x)),0()) -> false()
 app(app(le(),app(s(),x)),app(s(),y)) -> app(app(le(),x),y)
 app(app(eq(),0()),0()) -> true()
 app(app(eq(),0()),app(s(),y)) -> false()
 app(app(eq(),app(s(),x)),0()) -> false()
 app(app(eq(),app(s(),x)),app(s(),y)) -> app(app(eq(),x),y)
 app(app(app(if(),true()),x),y) -> x
 app(app(app(if(),false()),x),y) -> y
 app(minsort(),nil()) -> nil()
 app(minsort(),app(app(cons(),x),y)) ->
 app(app(cons(),app(app(min(),x),y)),app(minsort(),app(app(del(),app(app(min(),x),y)),
                                                       app(app(cons(),x),y))))
 app(app(min(),x),nil()) -> x
 app(app(min(),x),app(app(cons(),y),z)) ->
 app(app(app(if(),app(app(le(),x),y)),app(app(min(),x),z)),app(app(min(),y),z))
 app(app(del(),x),nil()) -> nil()
 app(app(del(),x),app(app(cons(),y),z)) ->
 app(app(app(if(),app(app(eq(),x),y)),z),app(app(cons(),y),app(app(del(),x),z)))
 app(app(map(),f),nil()) -> nil()
 app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
 app(app(filter(),f),nil()) -> nil()
 app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
 app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
 app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)

Proof:
 Uncurry Processor:
  le2(0(),y) -> true()
  le2(s1(x),0()) -> false()
  le2(s1(x),s1(y)) -> le2(x,y)
  eq2(0(),0()) -> true()
  eq2(0(),s1(y)) -> false()
  eq2(s1(x),0()) -> false()
  eq2(s1(x),s1(y)) -> eq2(x,y)
  if3(true(),x,y) -> x
  if3(false(),x,y) -> y
  minsort1(nil()) -> nil()
  minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
  min2(x,nil()) -> x
  min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
  del2(x,nil()) -> nil()
  del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
  map2(f,nil()) -> nil()
  map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
  filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
  filter24(false(),f,x,xs) -> filter2(f,xs)
  app(le1(x7),x8) -> le2(x7,x8)
  app(le(),x8) -> le1(x8)
  app(s(),x8) -> s1(x8)
  app(eq1(x7),x8) -> eq2(x7,x8)
  app(eq(),x8) -> eq1(x8)
  app(if2(x7,x6),x8) -> if3(x7,x6,x8)
  app(if1(x7),x8) -> if2(x7,x8)
  app(if(),x8) -> if1(x8)
  app(minsort(),x8) -> minsort1(x8)
  app(cons1(x7),x8) -> cons2(x7,x8)
  app(cons(),x8) -> cons1(x8)
  app(min1(x7),x8) -> min2(x7,x8)
  app(min(),x8) -> min1(x8)
  app(del1(x7),x8) -> del2(x7,x8)
  app(del(),x8) -> del1(x8)
  app(map1(x7),x8) -> map2(x7,x8)
  app(map(),x8) -> map1(x8)
  app(filter1(x7),x8) -> filter2(x7,x8)
  app(filter(),x8) -> filter1(x8)
  app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
  app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
  app(filter21(x7),x8) -> filter22(x7,x8)
  app(filter2(),x8) -> filter21(x8)
  DP Processor:
   DPs:
    le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
    eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
    minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y))
    minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y)))
    minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y)
    min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
    min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
    min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y)
    min{2,#}(x,cons2(y,z)) -> if{3,#}(le2(x,y),min2(x,z),min2(y,z))
    del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z)
    del{2,#}(x,cons2(y,z)) -> eq{2,#}(x,y)
    del{2,#}(x,cons2(y,z)) -> if{3,#}(eq2(x,y),z,cons2(y,del2(x,z)))
    map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
    map{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
    filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
    filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
    app#(le1(x7),x8) -> le{2,#}(x7,x8)
    app#(eq1(x7),x8) -> eq{2,#}(x7,x8)
    app#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
    app#(minsort(),x8) -> minsort{1,#}(x8)
    app#(min1(x7),x8) -> min{2,#}(x7,x8)
    app#(del1(x7),x8) -> del{2,#}(x7,x8)
    app#(map1(x7),x8) -> map{2,#}(x7,x8)
    app#(filter1(x7),x8) -> filter{2,#}(x7,x8)
    app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8)
   TRS:
    le2(0(),y) -> true()
    le2(s1(x),0()) -> false()
    le2(s1(x),s1(y)) -> le2(x,y)
    eq2(0(),0()) -> true()
    eq2(0(),s1(y)) -> false()
    eq2(s1(x),0()) -> false()
    eq2(s1(x),s1(y)) -> eq2(x,y)
    if3(true(),x,y) -> x
    if3(false(),x,y) -> y
    minsort1(nil()) -> nil()
    minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
    min2(x,nil()) -> x
    min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
    del2(x,nil()) -> nil()
    del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
    map2(f,nil()) -> nil()
    map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
    filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
    filter24(false(),f,x,xs) -> filter2(f,xs)
    app(le1(x7),x8) -> le2(x7,x8)
    app(le(),x8) -> le1(x8)
    app(s(),x8) -> s1(x8)
    app(eq1(x7),x8) -> eq2(x7,x8)
    app(eq(),x8) -> eq1(x8)
    app(if2(x7,x6),x8) -> if3(x7,x6,x8)
    app(if1(x7),x8) -> if2(x7,x8)
    app(if(),x8) -> if1(x8)
    app(minsort(),x8) -> minsort1(x8)
    app(cons1(x7),x8) -> cons2(x7,x8)
    app(cons(),x8) -> cons1(x8)
    app(min1(x7),x8) -> min2(x7,x8)
    app(min(),x8) -> min1(x8)
    app(del1(x7),x8) -> del2(x7,x8)
    app(del(),x8) -> del1(x8)
    app(map1(x7),x8) -> map2(x7,x8)
    app(map(),x8) -> map1(x8)
    app(filter1(x7),x8) -> filter2(x7,x8)
    app(filter(),x8) -> filter1(x8)
    app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
    app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
    app(filter21(x7),x8) -> filter22(x7,x8)
    app(filter2(),x8) -> filter21(x8)
   TDG Processor:
    DPs:
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y))
     minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y)))
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
     min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y)
     min{2,#}(x,cons2(y,z)) -> if{3,#}(le2(x,y),min2(x,z),min2(y,z))
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z)
     del{2,#}(x,cons2(y,z)) -> eq{2,#}(x,y)
     del{2,#}(x,cons2(y,z)) -> if{3,#}(eq2(x,y),z,cons2(y,del2(x,z)))
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app#(le1(x7),x8) -> le{2,#}(x7,x8)
     app#(eq1(x7),x8) -> eq{2,#}(x7,x8)
     app#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
     app#(minsort(),x8) -> minsort{1,#}(x8)
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     app#(del1(x7),x8) -> del{2,#}(x7,x8)
     app#(map1(x7),x8) -> map{2,#}(x7,x8)
     app#(filter1(x7),x8) -> filter{2,#}(x7,x8)
     app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8)
    TRS:
     le2(0(),y) -> true()
     le2(s1(x),0()) -> false()
     le2(s1(x),s1(y)) -> le2(x,y)
     eq2(0(),0()) -> true()
     eq2(0(),s1(y)) -> false()
     eq2(s1(x),0()) -> false()
     eq2(s1(x),s1(y)) -> eq2(x,y)
     if3(true(),x,y) -> x
     if3(false(),x,y) -> y
     minsort1(nil()) -> nil()
     minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
     min2(x,nil()) -> x
     min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
     del2(x,nil()) -> nil()
     del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
     map2(f,nil()) -> nil()
     map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app(le1(x7),x8) -> le2(x7,x8)
     app(le(),x8) -> le1(x8)
     app(s(),x8) -> s1(x8)
     app(eq1(x7),x8) -> eq2(x7,x8)
     app(eq(),x8) -> eq1(x8)
     app(if2(x7,x6),x8) -> if3(x7,x6,x8)
     app(if1(x7),x8) -> if2(x7,x8)
     app(if(),x8) -> if1(x8)
     app(minsort(),x8) -> minsort1(x8)
     app(cons1(x7),x8) -> cons2(x7,x8)
     app(cons(),x8) -> cons1(x8)
     app(min1(x7),x8) -> min2(x7,x8)
     app(min(),x8) -> min1(x8)
     app(del1(x7),x8) -> del2(x7,x8)
     app(del(),x8) -> del1(x8)
     app(map1(x7),x8) -> map2(x7,x8)
     app(map(),x8) -> map1(x8)
     app(filter1(x7),x8) -> filter2(x7,x8)
     app(filter(),x8) -> filter1(x8)
     app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
     app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
     app(filter21(x7),x8) -> filter22(x7,x8)
     app(filter2(),x8) -> filter21(x8)
    graph:
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x7),x8) -> filter{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(map1(x7),x8) -> map{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(del1(x7),x8) -> del{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(minsort(),x8) -> minsort{1,#}(x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(eq1(x7),x8) -> eq{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(le1(x7),x8) -> le{2,#}(x7,x8)
     app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     app#(filter1(x7),x8) -> filter{2,#}(x7,x8) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     app#(filter1(x7),x8) -> filter{2,#}(x7,x8) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(map1(x7),x8) -> map{2,#}(x7,x8) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     app#(del1(x7),x8) -> del{2,#}(x7,x8) ->
     del{2,#}(x,cons2(y,z)) -> if{3,#}(eq2(x,y),z,cons2(y,del2(x,z)))
     app#(del1(x7),x8) -> del{2,#}(x7,x8) ->
     del{2,#}(x,cons2(y,z)) -> eq{2,#}(x,y)
     app#(del1(x7),x8) -> del{2,#}(x7,x8) ->
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z)
     app#(min1(x7),x8) -> min{2,#}(x7,x8) ->
     min{2,#}(x,cons2(y,z)) -> if{3,#}(le2(x,y),min2(x,z),min2(y,z))
     app#(min1(x7),x8) -> min{2,#}(x7,x8) ->
     min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y)
     app#(min1(x7),x8) -> min{2,#}(x7,x8) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
     app#(min1(x7),x8) -> min{2,#}(x7,x8) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
     app#(eq1(x7),x8) -> eq{2,#}(x7,x8) ->
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     app#(le1(x7),x8) -> le{2,#}(x7,x8) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     app#(minsort(),x8) -> minsort{1,#}(x8) ->
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y)
     app#(minsort(),x8) -> minsort{1,#}(x8) ->
     minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y)))
     app#(minsort(),x8) -> minsort{1,#}(x8) ->
     minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y))
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x7),x8) -> filter{2,#}(x7,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(map1(x7),x8) -> map{2,#}(x7,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(del1(x7),x8) -> del{2,#}(x7,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(min1(x7),x8) -> min{2,#}(x7,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(minsort(),x8) -> minsort{1,#}(x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(eq1(x7),x8) -> eq{2,#}(x7,x8)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(le1(x7),x8) -> le{2,#}(x7,x8)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z) ->
     min{2,#}(x,cons2(y,z)) -> if{3,#}(le2(x,y),min2(x,z),min2(y,z))
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z) ->
     min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z) ->
     min{2,#}(x,cons2(y,z)) -> if{3,#}(le2(x,y),min2(x,z),min2(y,z))
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z) ->
     min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
     min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z) ->
     del{2,#}(x,cons2(y,z)) -> if{3,#}(eq2(x,y),z,cons2(y,del2(x,z)))
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z) ->
     del{2,#}(x,cons2(y,z)) -> eq{2,#}(x,y)
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z) ->
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z)
     del{2,#}(x,cons2(y,z)) -> eq{2,#}(x,y) ->
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y) ->
     min{2,#}(x,cons2(y,z)) -> if{3,#}(le2(x,y),min2(x,z),min2(y,z))
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y) ->
     min{2,#}(x,cons2(y,z)) -> le{2,#}(x,y)
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y) ->
     min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
     minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y)) ->
     del{2,#}(x,cons2(y,z)) -> if{3,#}(eq2(x,y),z,cons2(y,del2(x,z)))
     minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y)) ->
     del{2,#}(x,cons2(y,z)) -> eq{2,#}(x,y)
     minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y)) ->
     del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z)
     minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y))) ->
     minsort{1,#}(cons2(x,y)) -> min{2,#}(x,y)
     minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y))) ->
     minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y)))
     minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y))) ->
     minsort{1,#}(cons2(x,y)) -> del{2,#}(min2(x,y),cons2(x,y))
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) ->
     eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) -> le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
    SCC Processor:
     #sccs: 6
     #rules: 15
     #arcs: 69/729
     DPs:
      filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
      app#(map1(x7),x8) -> map{2,#}(x7,x8)
      map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
      map{2,#}(f,cons2(x,xs)) -> app#(f,x)
      app#(filter1(x7),x8) -> filter{2,#}(x7,x8)
      filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
      filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
      app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8)
     TRS:
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      eq2(0(),0()) -> true()
      eq2(0(),s1(y)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      minsort1(nil()) -> nil()
      minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
      min2(x,nil()) -> x
      min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
      del2(x,nil()) -> nil()
      del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(le1(x7),x8) -> le2(x7,x8)
      app(le(),x8) -> le1(x8)
      app(s(),x8) -> s1(x8)
      app(eq1(x7),x8) -> eq2(x7,x8)
      app(eq(),x8) -> eq1(x8)
      app(if2(x7,x6),x8) -> if3(x7,x6,x8)
      app(if1(x7),x8) -> if2(x7,x8)
      app(if(),x8) -> if1(x8)
      app(minsort(),x8) -> minsort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(del1(x7),x8) -> del2(x7,x8)
      app(del(),x8) -> del1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
      app(filter1(x7),x8) -> filter2(x7,x8)
      app(filter(),x8) -> filter1(x8)
      app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
      app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
      app(filter21(x7),x8) -> filter22(x7,x8)
      app(filter2(),x8) -> filter21(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 1
       pi(app#) = 1
       pi(filter{2,#}) = 1
       pi(filter2{4,#}) = 3
      problem:
       DPs:
        filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
        app#(map1(x7),x8) -> map{2,#}(x7,x8)
        app#(filter1(x7),x8) -> filter{2,#}(x7,x8)
        filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
        app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8)
       TRS:
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        eq2(0(),0()) -> true()
        eq2(0(),s1(y)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        if3(true(),x,y) -> x
        if3(false(),x,y) -> y
        minsort1(nil()) -> nil()
        minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
        min2(x,nil()) -> x
        min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
        del2(x,nil()) -> nil()
        del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(le1(x7),x8) -> le2(x7,x8)
        app(le(),x8) -> le1(x8)
        app(s(),x8) -> s1(x8)
        app(eq1(x7),x8) -> eq2(x7,x8)
        app(eq(),x8) -> eq1(x8)
        app(if2(x7,x6),x8) -> if3(x7,x6,x8)
        app(if1(x7),x8) -> if2(x7,x8)
        app(if(),x8) -> if1(x8)
        app(minsort(),x8) -> minsort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(del1(x7),x8) -> del2(x7,x8)
        app(del(),x8) -> del1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
        app(filter1(x7),x8) -> filter2(x7,x8)
        app(filter(),x8) -> filter1(x8)
        app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
        app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
        app(filter21(x7),x8) -> filter22(x7,x8)
        app(filter2(),x8) -> filter21(x8)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 20/25
       
     
     DPs:
      minsort{1,#}(cons2(x,y)) -> minsort{1,#}(del2(min2(x,y),cons2(x,y)))
     TRS:
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      eq2(0(),0()) -> true()
      eq2(0(),s1(y)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      minsort1(nil()) -> nil()
      minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
      min2(x,nil()) -> x
      min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
      del2(x,nil()) -> nil()
      del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(le1(x7),x8) -> le2(x7,x8)
      app(le(),x8) -> le1(x8)
      app(s(),x8) -> s1(x8)
      app(eq1(x7),x8) -> eq2(x7,x8)
      app(eq(),x8) -> eq1(x8)
      app(if2(x7,x6),x8) -> if3(x7,x6,x8)
      app(if1(x7),x8) -> if2(x7,x8)
      app(if(),x8) -> if1(x8)
      app(minsort(),x8) -> minsort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(del1(x7),x8) -> del2(x7,x8)
      app(del(),x8) -> del1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
      app(filter1(x7),x8) -> filter2(x7,x8)
      app(filter(),x8) -> filter1(x8)
      app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
      app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
      app(filter21(x7),x8) -> filter22(x7,x8)
      app(filter2(),x8) -> filter21(x8)
     Open
     
     DPs:
      min{2,#}(x,cons2(y,z)) -> min{2,#}(y,z)
      min{2,#}(x,cons2(y,z)) -> min{2,#}(x,z)
     TRS:
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      eq2(0(),0()) -> true()
      eq2(0(),s1(y)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      minsort1(nil()) -> nil()
      minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
      min2(x,nil()) -> x
      min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
      del2(x,nil()) -> nil()
      del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(le1(x7),x8) -> le2(x7,x8)
      app(le(),x8) -> le1(x8)
      app(s(),x8) -> s1(x8)
      app(eq1(x7),x8) -> eq2(x7,x8)
      app(eq(),x8) -> eq1(x8)
      app(if2(x7,x6),x8) -> if3(x7,x6,x8)
      app(if1(x7),x8) -> if2(x7,x8)
      app(if(),x8) -> if1(x8)
      app(minsort(),x8) -> minsort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(del1(x7),x8) -> del2(x7,x8)
      app(del(),x8) -> del1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
      app(filter1(x7),x8) -> filter2(x7,x8)
      app(filter(),x8) -> filter1(x8)
      app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
      app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
      app(filter21(x7),x8) -> filter22(x7,x8)
      app(filter2(),x8) -> filter21(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(min{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        eq2(0(),0()) -> true()
        eq2(0(),s1(y)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        if3(true(),x,y) -> x
        if3(false(),x,y) -> y
        minsort1(nil()) -> nil()
        minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
        min2(x,nil()) -> x
        min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
        del2(x,nil()) -> nil()
        del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(le1(x7),x8) -> le2(x7,x8)
        app(le(),x8) -> le1(x8)
        app(s(),x8) -> s1(x8)
        app(eq1(x7),x8) -> eq2(x7,x8)
        app(eq(),x8) -> eq1(x8)
        app(if2(x7,x6),x8) -> if3(x7,x6,x8)
        app(if1(x7),x8) -> if2(x7,x8)
        app(if(),x8) -> if1(x8)
        app(minsort(),x8) -> minsort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(del1(x7),x8) -> del2(x7,x8)
        app(del(),x8) -> del1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
        app(filter1(x7),x8) -> filter2(x7,x8)
        app(filter(),x8) -> filter1(x8)
        app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
        app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
        app(filter21(x7),x8) -> filter22(x7,x8)
        app(filter2(),x8) -> filter21(x8)
      Qed
     
     DPs:
      del{2,#}(x,cons2(y,z)) -> del{2,#}(x,z)
     TRS:
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      eq2(0(),0()) -> true()
      eq2(0(),s1(y)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      minsort1(nil()) -> nil()
      minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
      min2(x,nil()) -> x
      min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
      del2(x,nil()) -> nil()
      del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(le1(x7),x8) -> le2(x7,x8)
      app(le(),x8) -> le1(x8)
      app(s(),x8) -> s1(x8)
      app(eq1(x7),x8) -> eq2(x7,x8)
      app(eq(),x8) -> eq1(x8)
      app(if2(x7,x6),x8) -> if3(x7,x6,x8)
      app(if1(x7),x8) -> if2(x7,x8)
      app(if(),x8) -> if1(x8)
      app(minsort(),x8) -> minsort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(del1(x7),x8) -> del2(x7,x8)
      app(del(),x8) -> del1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
      app(filter1(x7),x8) -> filter2(x7,x8)
      app(filter(),x8) -> filter1(x8)
      app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
      app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
      app(filter21(x7),x8) -> filter22(x7,x8)
      app(filter2(),x8) -> filter21(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(del{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        eq2(0(),0()) -> true()
        eq2(0(),s1(y)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        if3(true(),x,y) -> x
        if3(false(),x,y) -> y
        minsort1(nil()) -> nil()
        minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
        min2(x,nil()) -> x
        min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
        del2(x,nil()) -> nil()
        del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(le1(x7),x8) -> le2(x7,x8)
        app(le(),x8) -> le1(x8)
        app(s(),x8) -> s1(x8)
        app(eq1(x7),x8) -> eq2(x7,x8)
        app(eq(),x8) -> eq1(x8)
        app(if2(x7,x6),x8) -> if3(x7,x6,x8)
        app(if1(x7),x8) -> if2(x7,x8)
        app(if(),x8) -> if1(x8)
        app(minsort(),x8) -> minsort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(del1(x7),x8) -> del2(x7,x8)
        app(del(),x8) -> del1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
        app(filter1(x7),x8) -> filter2(x7,x8)
        app(filter(),x8) -> filter1(x8)
        app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
        app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
        app(filter21(x7),x8) -> filter22(x7,x8)
        app(filter2(),x8) -> filter21(x8)
      Qed
     
     DPs:
      eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y)
     TRS:
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      eq2(0(),0()) -> true()
      eq2(0(),s1(y)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      minsort1(nil()) -> nil()
      minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
      min2(x,nil()) -> x
      min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
      del2(x,nil()) -> nil()
      del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(le1(x7),x8) -> le2(x7,x8)
      app(le(),x8) -> le1(x8)
      app(s(),x8) -> s1(x8)
      app(eq1(x7),x8) -> eq2(x7,x8)
      app(eq(),x8) -> eq1(x8)
      app(if2(x7,x6),x8) -> if3(x7,x6,x8)
      app(if1(x7),x8) -> if2(x7,x8)
      app(if(),x8) -> if1(x8)
      app(minsort(),x8) -> minsort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(del1(x7),x8) -> del2(x7,x8)
      app(del(),x8) -> del1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
      app(filter1(x7),x8) -> filter2(x7,x8)
      app(filter(),x8) -> filter1(x8)
      app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
      app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
      app(filter21(x7),x8) -> filter22(x7,x8)
      app(filter2(),x8) -> filter21(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(eq{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        eq2(0(),0()) -> true()
        eq2(0(),s1(y)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        if3(true(),x,y) -> x
        if3(false(),x,y) -> y
        minsort1(nil()) -> nil()
        minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
        min2(x,nil()) -> x
        min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
        del2(x,nil()) -> nil()
        del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(le1(x7),x8) -> le2(x7,x8)
        app(le(),x8) -> le1(x8)
        app(s(),x8) -> s1(x8)
        app(eq1(x7),x8) -> eq2(x7,x8)
        app(eq(),x8) -> eq1(x8)
        app(if2(x7,x6),x8) -> if3(x7,x6,x8)
        app(if1(x7),x8) -> if2(x7,x8)
        app(if(),x8) -> if1(x8)
        app(minsort(),x8) -> minsort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(del1(x7),x8) -> del2(x7,x8)
        app(del(),x8) -> del1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
        app(filter1(x7),x8) -> filter2(x7,x8)
        app(filter(),x8) -> filter1(x8)
        app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
        app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
        app(filter21(x7),x8) -> filter22(x7,x8)
        app(filter2(),x8) -> filter21(x8)
      Qed
     
     DPs:
      le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     TRS:
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      eq2(0(),0()) -> true()
      eq2(0(),s1(y)) -> false()
      eq2(s1(x),0()) -> false()
      eq2(s1(x),s1(y)) -> eq2(x,y)
      if3(true(),x,y) -> x
      if3(false(),x,y) -> y
      minsort1(nil()) -> nil()
      minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
      min2(x,nil()) -> x
      min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
      del2(x,nil()) -> nil()
      del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(le1(x7),x8) -> le2(x7,x8)
      app(le(),x8) -> le1(x8)
      app(s(),x8) -> s1(x8)
      app(eq1(x7),x8) -> eq2(x7,x8)
      app(eq(),x8) -> eq1(x8)
      app(if2(x7,x6),x8) -> if3(x7,x6,x8)
      app(if1(x7),x8) -> if2(x7,x8)
      app(if(),x8) -> if1(x8)
      app(minsort(),x8) -> minsort1(x8)
      app(cons1(x7),x8) -> cons2(x7,x8)
      app(cons(),x8) -> cons1(x8)
      app(min1(x7),x8) -> min2(x7,x8)
      app(min(),x8) -> min1(x8)
      app(del1(x7),x8) -> del2(x7,x8)
      app(del(),x8) -> del1(x8)
      app(map1(x7),x8) -> map2(x7,x8)
      app(map(),x8) -> map1(x8)
      app(filter1(x7),x8) -> filter2(x7,x8)
      app(filter(),x8) -> filter1(x8)
      app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
      app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
      app(filter21(x7),x8) -> filter22(x7,x8)
      app(filter2(),x8) -> filter21(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(le{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        eq2(0(),0()) -> true()
        eq2(0(),s1(y)) -> false()
        eq2(s1(x),0()) -> false()
        eq2(s1(x),s1(y)) -> eq2(x,y)
        if3(true(),x,y) -> x
        if3(false(),x,y) -> y
        minsort1(nil()) -> nil()
        minsort1(cons2(x,y)) -> cons2(min2(x,y),minsort1(del2(min2(x,y),cons2(x,y))))
        min2(x,nil()) -> x
        min2(x,cons2(y,z)) -> if3(le2(x,y),min2(x,z),min2(y,z))
        del2(x,nil()) -> nil()
        del2(x,cons2(y,z)) -> if3(eq2(x,y),z,cons2(y,del2(x,z)))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(le1(x7),x8) -> le2(x7,x8)
        app(le(),x8) -> le1(x8)
        app(s(),x8) -> s1(x8)
        app(eq1(x7),x8) -> eq2(x7,x8)
        app(eq(),x8) -> eq1(x8)
        app(if2(x7,x6),x8) -> if3(x7,x6,x8)
        app(if1(x7),x8) -> if2(x7,x8)
        app(if(),x8) -> if1(x8)
        app(minsort(),x8) -> minsort1(x8)
        app(cons1(x7),x8) -> cons2(x7,x8)
        app(cons(),x8) -> cons1(x8)
        app(min1(x7),x8) -> min2(x7,x8)
        app(min(),x8) -> min1(x8)
        app(del1(x7),x8) -> del2(x7,x8)
        app(del(),x8) -> del1(x8)
        app(map1(x7),x8) -> map2(x7,x8)
        app(map(),x8) -> map1(x8)
        app(filter1(x7),x8) -> filter2(x7,x8)
        app(filter(),x8) -> filter1(x8)
        app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8)
        app(filter22(x7,x6),x8) -> filter23(x7,x6,x8)
        app(filter21(x7),x8) -> filter22(x7,x8)
        app(filter2(),x8) -> filter21(x8)
      Qed