MAYBE

Problem:
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 eq(0(),0()) -> true()
 eq(0(),s(y)) -> false()
 eq(s(x),0()) -> false()
 eq(s(x),s(y)) -> eq(x,y)
 minsort(nil()) -> nil()
 minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
 min(nil()) -> 0()
 min(cons(x,nil())) -> x
 min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
 if1(true(),x,y,xs) -> min(cons(x,xs))
 if1(false(),x,y,xs) -> min(cons(y,xs))
 rm(x,nil()) -> nil()
 rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
 if2(true(),x,y,xs) -> rm(x,xs)
 if2(false(),x,y,xs) -> cons(y,rm(x,xs))

Proof:
 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   eq#(s(x),s(y)) -> eq#(x,y)
   minsort#(cons(x,xs)) -> rm#(min(cons(x,xs)),cons(x,xs))
   minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs)))
   minsort#(cons(x,xs)) -> min#(cons(x,xs))
   min#(cons(x,cons(y,xs))) -> le#(x,y)
   min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs)
   if1#(true(),x,y,xs) -> min#(cons(x,xs))
   if1#(false(),x,y,xs) -> min#(cons(y,xs))
   rm#(x,cons(y,xs)) -> eq#(x,y)
   rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
   if2#(true(),x,y,xs) -> rm#(x,xs)
   if2#(false(),x,y,xs) -> rm#(x,xs)
  TRS:
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   eq(0(),0()) -> true()
   eq(0(),s(y)) -> false()
   eq(s(x),0()) -> false()
   eq(s(x),s(y)) -> eq(x,y)
   minsort(nil()) -> nil()
   minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
   min(nil()) -> 0()
   min(cons(x,nil())) -> x
   min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
   if1(true(),x,y,xs) -> min(cons(x,xs))
   if1(false(),x,y,xs) -> min(cons(y,xs))
   rm(x,nil()) -> nil()
   rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
   if2(true(),x,y,xs) -> rm(x,xs)
   if2(false(),x,y,xs) -> cons(y,rm(x,xs))
  CDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    eq#(s(x),s(y)) -> eq#(x,y)
    minsort#(cons(x,xs)) -> rm#(min(cons(x,xs)),cons(x,xs))
    minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs)))
    minsort#(cons(x,xs)) -> min#(cons(x,xs))
    min#(cons(x,cons(y,xs))) -> le#(x,y)
    min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs)
    if1#(true(),x,y,xs) -> min#(cons(x,xs))
    if1#(false(),x,y,xs) -> min#(cons(y,xs))
    rm#(x,cons(y,xs)) -> eq#(x,y)
    rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
    if2#(true(),x,y,xs) -> rm#(x,xs)
    if2#(false(),x,y,xs) -> rm#(x,xs)
   TRS:
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    eq(0(),0()) -> true()
    eq(0(),s(y)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    minsort(nil()) -> nil()
    minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
    min(nil()) -> 0()
    min(cons(x,nil())) -> x
    min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
    if1(true(),x,y,xs) -> min(cons(x,xs))
    if1(false(),x,y,xs) -> min(cons(y,xs))
    rm(x,nil()) -> nil()
    rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
    if2(true(),x,y,xs) -> rm(x,xs)
    if2(false(),x,y,xs) -> cons(y,rm(x,xs))
   graph:
    if2#(false(),x,y,xs) -> rm#(x,xs) ->
    rm#(x,cons(y,xs)) -> eq#(x,y)
    if2#(false(),x,y,xs) -> rm#(x,xs) ->
    rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
    if2#(true(),x,y,xs) -> rm#(x,xs) ->
    rm#(x,cons(y,xs)) -> eq#(x,y)
    if2#(true(),x,y,xs) -> rm#(x,xs) ->
    rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
    if1#(false(),x,y,xs) -> min#(cons(y,xs)) ->
    min#(cons(x,cons(y,xs))) -> le#(x,y)
    if1#(false(),x,y,xs) -> min#(cons(y,xs)) ->
    min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs)
    if1#(true(),x,y,xs) -> min#(cons(x,xs)) ->
    min#(cons(x,cons(y,xs))) -> le#(x,y)
    if1#(true(),x,y,xs) -> min#(cons(x,xs)) ->
    min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs)
    min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs) ->
    if1#(true(),x,y,xs) -> min#(cons(x,xs))
    min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs) ->
    if1#(false(),x,y,xs) -> min#(cons(y,xs))
    min#(cons(x,cons(y,xs))) -> le#(x,y) ->
    le#(s(x),s(y)) -> le#(x,y)
    rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs) ->
    if2#(true(),x,y,xs) -> rm#(x,xs)
    rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs) ->
    if2#(false(),x,y,xs) -> rm#(x,xs)
    rm#(x,cons(y,xs)) -> eq#(x,y) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    minsort#(cons(x,xs)) -> min#(cons(x,xs)) ->
    min#(cons(x,cons(y,xs))) -> le#(x,y)
    minsort#(cons(x,xs)) -> min#(cons(x,xs)) ->
    min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs)
    minsort#(cons(x,xs)) -> rm#(min(cons(x,xs)),cons(x,xs)) ->
    rm#(x,cons(y,xs)) -> eq#(x,y)
    minsort#(cons(x,xs)) -> rm#(min(cons(x,xs)),cons(x,xs)) ->
    rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
    minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs))) ->
    minsort#(cons(x,xs)) -> rm#(min(cons(x,xs)),cons(x,xs))
    minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs))) ->
    minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs)))
    minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs))) ->
    minsort#(cons(x,xs)) -> min#(cons(x,xs))
    eq#(s(x),s(y)) -> eq#(x,y) -> eq#(s(x),s(y)) -> eq#(x,y)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   SCC Processor:
    #sccs: 5
    #rules: 9
    #arcs: 23/169
    DPs:
     minsort#(cons(x,xs)) -> minsort#(rm(min(cons(x,xs)),cons(x,xs)))
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     minsort(nil()) -> nil()
     minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
     min(nil()) -> 0()
     min(cons(x,nil())) -> x
     min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
     if1(true(),x,y,xs) -> min(cons(x,xs))
     if1(false(),x,y,xs) -> min(cons(y,xs))
     rm(x,nil()) -> nil()
     rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
     if2(true(),x,y,xs) -> rm(x,xs)
     if2(false(),x,y,xs) -> cons(y,rm(x,xs))
    Open
    
    DPs:
     if1#(false(),x,y,xs) -> min#(cons(y,xs))
     min#(cons(x,cons(y,xs))) -> if1#(le(x,y),x,y,xs)
     if1#(true(),x,y,xs) -> min#(cons(x,xs))
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     minsort(nil()) -> nil()
     minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
     min(nil()) -> 0()
     min(cons(x,nil())) -> x
     min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
     if1(true(),x,y,xs) -> min(cons(x,xs))
     if1(false(),x,y,xs) -> min(cons(y,xs))
     rm(x,nil()) -> nil()
     rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
     if2(true(),x,y,xs) -> rm(x,xs)
     if2(false(),x,y,xs) -> cons(y,rm(x,xs))
    Open
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     minsort(nil()) -> nil()
     minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
     min(nil()) -> 0()
     min(cons(x,nil())) -> x
     min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
     if1(true(),x,y,xs) -> min(cons(x,xs))
     if1(false(),x,y,xs) -> min(cons(y,xs))
     rm(x,nil()) -> nil()
     rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
     if2(true(),x,y,xs) -> rm(x,xs)
     if2(false(),x,y,xs) -> cons(y,rm(x,xs))
    Open
    
    DPs:
     if2#(false(),x,y,xs) -> rm#(x,xs)
     rm#(x,cons(y,xs)) -> if2#(eq(x,y),x,y,xs)
     if2#(true(),x,y,xs) -> rm#(x,xs)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     minsort(nil()) -> nil()
     minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
     min(nil()) -> 0()
     min(cons(x,nil())) -> x
     min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
     if1(true(),x,y,xs) -> min(cons(x,xs))
     if1(false(),x,y,xs) -> min(cons(y,xs))
     rm(x,nil()) -> nil()
     rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
     if2(true(),x,y,xs) -> rm(x,xs)
     if2(false(),x,y,xs) -> cons(y,rm(x,xs))
    Open
    
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     minsort(nil()) -> nil()
     minsort(cons(x,xs)) -> cons(min(cons(x,xs)),minsort(rm(min(cons(x,xs)),cons(x,xs))))
     min(nil()) -> 0()
     min(cons(x,nil())) -> x
     min(cons(x,cons(y,xs))) -> if1(le(x,y),x,y,xs)
     if1(true(),x,y,xs) -> min(cons(x,xs))
     if1(false(),x,y,xs) -> min(cons(y,xs))
     rm(x,nil()) -> nil()
     rm(x,cons(y,xs)) -> if2(eq(x,y),x,y,xs)
     if2(true(),x,y,xs) -> rm(x,xs)
     if2(false(),x,y,xs) -> cons(y,rm(x,xs))
    Open