MAYBE
Time: 0.004354
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),
    if(true(), x, y) -> x,
   if(false(), x, y) -> y,
       minsort nil() -> nil(),
  minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
       min(x, nil()) -> x,
  min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
       del(x, nil()) -> nil(),
  del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
 DP:
  DP:
   {      le#(s x, s y) -> le#(x, y),
          eq#(s x, s y) -> eq#(x, y),
    minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y)),
    minsort# cons(x, y) -> min#(x, y),
    minsort# cons(x, y) -> del#(min(x, y), cons(x, y)),
    min#(x, cons(y, z)) -> le#(x, y),
    min#(x, cons(y, z)) -> if#(le(x, y), min(x, z), min(y, z)),
    min#(x, cons(y, z)) -> min#(y, z),
    min#(x, cons(y, z)) -> min#(x, z),
    del#(x, cons(y, z)) -> eq#(x, y),
    del#(x, cons(y, z)) -> if#(eq(x, y), z, cons(y, del(x, z))),
    del#(x, cons(y, z)) -> del#(x, z)}
  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),
     if(true(), x, y) -> x,
    if(false(), x, y) -> y,
        minsort nil() -> nil(),
   minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
        min(x, nil()) -> x,
   min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
        del(x, nil()) -> nil(),
   del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
  EDG:
   {(minsort# cons(x, y) -> del#(min(x, y), cons(x, y)), del#(x, cons(y, z)) -> del#(x, z))
    (minsort# cons(x, y) -> del#(min(x, y), cons(x, y)), del#(x, cons(y, z)) -> if#(eq(x, y), z, cons(y, del(x, z))))
    (minsort# cons(x, y) -> del#(min(x, y), cons(x, y)), del#(x, cons(y, z)) -> eq#(x, y))
    (min#(x, cons(y, z)) -> min#(x, z), min#(x, cons(y, z)) -> min#(x, z))
    (min#(x, cons(y, z)) -> min#(x, z), min#(x, cons(y, z)) -> min#(y, z))
    (min#(x, cons(y, z)) -> min#(x, z), min#(x, cons(y, z)) -> if#(le(x, y), min(x, z), min(y, z)))
    (min#(x, cons(y, z)) -> min#(x, z), min#(x, cons(y, z)) -> le#(x, y))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (min#(x, cons(y, z)) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (del#(x, cons(y, z)) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (minsort# cons(x, y) -> min#(x, y), min#(x, cons(y, z)) -> le#(x, y))
    (minsort# cons(x, y) -> min#(x, y), min#(x, cons(y, z)) -> if#(le(x, y), min(x, z), min(y, z)))
    (minsort# cons(x, y) -> min#(x, y), min#(x, cons(y, z)) -> min#(y, z))
    (minsort# cons(x, y) -> min#(x, y), min#(x, cons(y, z)) -> min#(x, z))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (del#(x, cons(y, z)) -> del#(x, z), del#(x, cons(y, z)) -> eq#(x, y))
    (del#(x, cons(y, z)) -> del#(x, z), del#(x, cons(y, z)) -> if#(eq(x, y), z, cons(y, del(x, z))))
    (del#(x, cons(y, z)) -> del#(x, z), del#(x, cons(y, z)) -> del#(x, z))
    (min#(x, cons(y, z)) -> min#(y, z), min#(x, cons(y, z)) -> le#(x, y))
    (min#(x, cons(y, z)) -> min#(y, z), min#(x, cons(y, z)) -> if#(le(x, y), min(x, z), min(y, z)))
    (min#(x, cons(y, z)) -> min#(y, z), min#(x, cons(y, z)) -> min#(y, z))
    (min#(x, cons(y, z)) -> min#(y, z), min#(x, cons(y, z)) -> min#(x, z))
    (minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y)), minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y)))
    (minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y)), minsort# cons(x, y) -> min#(x, y))
    (minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y)), minsort# cons(x, y) -> del#(min(x, y), cons(x, y)))}
   STATUS:
    arrows: 0.826389
    SCCS (5):
     Scc:
      {minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y))}
     Scc:
      {del#(x, cons(y, z)) -> del#(x, z)}
     Scc:
      {eq#(s x, s y) -> eq#(x, y)}
     Scc:
      {min#(x, cons(y, z)) -> min#(y, z),
       min#(x, cons(y, z)) -> min#(x, z)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     SCC (1):
      Strict:
       {minsort# cons(x, y) -> minsort# del(min(x, y), cons(x, y))}
      Weak:
      {        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),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            minsort nil() -> nil(),
       minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
            min(x, nil()) -> x,
       min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
            del(x, nil()) -> nil(),
       del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
      Open
     
     SCC (1):
      Strict:
       {del#(x, cons(y, z)) -> del#(x, z)}
      Weak:
      {        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),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            minsort nil() -> nil(),
       minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
            min(x, nil()) -> x,
       min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
            del(x, nil()) -> nil(),
       del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
      Open
     
     
     SCC (1):
      Strict:
       {eq#(s x, s y) -> eq#(x, y)}
      Weak:
      {        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),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            minsort nil() -> nil(),
       minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
            min(x, nil()) -> x,
       min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
            del(x, nil()) -> nil(),
       del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
      Open
     
     SCC (2):
      Strict:
       {min#(x, cons(y, z)) -> min#(y, z),
        min#(x, cons(y, z)) -> min#(x, z)}
      Weak:
      {        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),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            minsort nil() -> nil(),
       minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
            min(x, nil()) -> x,
       min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
            del(x, nil()) -> nil(),
       del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
      Open
     
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {        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),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
            minsort nil() -> nil(),
       minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y))),
            min(x, nil()) -> x,
       min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z)),
            del(x, nil()) -> nil(),
       del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))}
      Open