MAYBE
Time: 0.073933
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)))}
  UR:
   {        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,
         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))),
               a(w, v) -> w,
               a(w, v) -> v}
   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)))}
       Fail
      
      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)))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + 1,
         
         [le](x0, x1) = x0 + 1,
         
         [eq](x0, x1) = x0 + 1,
         
         [cons](x0, x1) = x0 + x1 + 1,
         
         [min](x0, x1) = 1,
         
         [del](x0, x1) = 0,
         
         [s](x0) = 1,
         
         [minsort](x0) = x0 + 1,
         
         [true] = 1,
         
         [0] = 1,
         
         [false] = 1,
         
         [nil] = 1,
         
         [del#](x0, x1) = x0 + 1
        Strict:
         del#(x, cons(y, z)) -> del#(x, z)
         2 + 1y + 0x + 1z >= 1 + 0x + 1z
        Weak:
         del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))
         0 + 0y + 0x + 0z >= 2 + 0y + 1x + 0z
         del(x, nil()) -> nil()
         0 + 0x >= 1
         min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z))
         1 + 0y + 0x + 0z >= 2 + 0y + 1x + 0z
         min(x, nil()) -> x
         1 + 0x >= 1x
         minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y)))
         2 + 1y + 1x >= 3 + 0y + 0x
         minsort nil() -> nil()
         2 >= 1
         if(false(), x, y) -> y
         2 + 0y + 0x >= 1y
         if(true(), x, y) -> x
         2 + 0y + 0x >= 1x
         eq(s x, s y) -> eq(x, y)
         2 + 0y + 0x >= 1 + 0y + 1x
         eq(s x, 0()) -> false()
         2 + 0x >= 1
         eq(0(), s y) -> false()
         2 + 0y >= 1
         eq(0(), 0()) -> true()
         2 >= 1
         le(s x, s y) -> le(x, y)
         2 + 0y + 0x >= 1 + 0y + 1x
         le(s x, 0()) -> false()
         2 + 0x >= 1
         le(0(), y) -> true()
         2 + 0y >= 1
       Qed
     
     
     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)))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = x0 + x1 + 1,
        
        [le](x0, x1) = x0 + 1,
        
        [eq](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = 1,
        
        [min](x0, x1) = x0 + 1,
        
        [del](x0, x1) = x0,
        
        [s](x0) = x0 + 1,
        
        [minsort](x0) = x0 + 1,
        
        [true] = 1,
        
        [0] = 1,
        
        [false] = 1,
        
        [nil] = 1,
        
        [eq#](x0, x1) = x0 + 1
       Strict:
        eq#(s x, s y) -> eq#(x, y)
        2 + 0y + 1x >= 1 + 0y + 1x
       Weak:
        del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))
        1 + 0y + 0x + 0z >= 3 + 0y + 1x + 0z
        del(x, nil()) -> nil()
        1 + 0x >= 1
        min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z))
        2 + 0y + 0x + 0z >= 3 + 0y + 1x + 1z
        min(x, nil()) -> x
        2 + 0x >= 1x
        minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y)))
        2 + 0y + 0x >= 1 + 0y + 0x
        minsort nil() -> nil()
        2 >= 1
        if(false(), x, y) -> y
        2 + 1y + 0x >= 1y
        if(true(), x, y) -> x
        2 + 1y + 0x >= 1x
        eq(s x, s y) -> eq(x, y)
        2 + 0y + 1x >= 1 + 0y + 1x
        eq(s x, 0()) -> false()
        2 + 1x >= 1
        eq(0(), s y) -> false()
        2 + 0y >= 1
        eq(0(), 0()) -> true()
        2 >= 1
        le(s x, s y) -> le(x, y)
        2 + 0y + 1x >= 1 + 0y + 1x
        le(s x, 0()) -> false()
        2 + 1x >= 1
        le(0(), y) -> true()
        2 + 0y >= 1
      Qed
     
     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)))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = x0 + x1 + 1,
        
        [le](x0, x1) = x0 + 1,
        
        [eq](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [min](x0, x1) = 1,
        
        [del](x0, x1) = 0,
        
        [s](x0) = 1,
        
        [minsort](x0) = x0 + 1,
        
        [true] = 1,
        
        [0] = 1,
        
        [false] = 1,
        
        [nil] = 1,
        
        [min#](x0, x1) = x0 + 1
       Strict:
        min#(x, cons(y, z)) -> min#(x, z)
        2 + 1y + 0x + 1z >= 1 + 0x + 1z
        min#(x, cons(y, z)) -> min#(y, z)
        2 + 1y + 0x + 1z >= 1 + 0y + 1z
       Weak:
        del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))
        0 + 0y + 0x + 0z >= 3 + 1y + 1x + 0z
        del(x, nil()) -> nil()
        0 + 0x >= 1
        min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z))
        1 + 0y + 0x + 0z >= 3 + 0y + 1x + 0z
        min(x, nil()) -> x
        1 + 0x >= 1x
        minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y)))
        2 + 1y + 1x >= 3 + 0y + 0x
        minsort nil() -> nil()
        2 >= 1
        if(false(), x, y) -> y
        2 + 1y + 0x >= 1y
        if(true(), x, y) -> x
        2 + 1y + 0x >= 1x
        eq(s x, s y) -> eq(x, y)
        2 + 0y + 0x >= 1 + 0y + 1x
        eq(s x, 0()) -> false()
        2 + 0x >= 1
        eq(0(), s y) -> false()
        2 + 0y >= 1
        eq(0(), 0()) -> true()
        2 >= 1
        le(s x, s y) -> le(x, y)
        2 + 0y + 0x >= 1 + 0y + 1x
        le(s x, 0()) -> false()
        2 + 0x >= 1
        le(0(), y) -> true()
        2 + 0y >= 1
      Qed
    
    
    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)))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + x1 + 1,
       
       [le](x0, x1) = x0 + 1,
       
       [eq](x0, x1) = x0 + 1,
       
       [cons](x0, x1) = 1,
       
       [min](x0, x1) = x0 + 1,
       
       [del](x0, x1) = x0,
       
       [s](x0) = x0 + 1,
       
       [minsort](x0) = x0 + 1,
       
       [true] = 1,
       
       [0] = 1,
       
       [false] = 1,
       
       [nil] = 1,
       
       [le#](x0, x1) = x0 + 1
      Strict:
       le#(s x, s y) -> le#(x, y)
       2 + 0y + 1x >= 1 + 0y + 1x
      Weak:
       del(x, cons(y, z)) -> if(eq(x, y), z, cons(y, del(x, z)))
       1 + 0y + 0x + 0z >= 3 + 0y + 1x + 0z
       del(x, nil()) -> nil()
       1 + 0x >= 1
       min(x, cons(y, z)) -> if(le(x, y), min(x, z), min(y, z))
       2 + 0y + 0x + 0z >= 3 + 0y + 1x + 1z
       min(x, nil()) -> x
       2 + 0x >= 1x
       minsort cons(x, y) -> cons(min(x, y), minsort del(min(x, y), cons(x, y)))
       2 + 0y + 0x >= 1 + 0y + 0x
       minsort nil() -> nil()
       2 >= 1
       if(false(), x, y) -> y
       2 + 1y + 0x >= 1y
       if(true(), x, y) -> x
       2 + 1y + 0x >= 1x
       eq(s x, s y) -> eq(x, y)
       2 + 0y + 1x >= 1 + 0y + 1x
       eq(s x, 0()) -> false()
       2 + 1x >= 1
       eq(0(), s y) -> false()
       2 + 0y >= 1
       eq(0(), 0()) -> true()
       2 >= 1
       le(s x, s y) -> le(x, y)
       2 + 0y + 1x >= 1 + 0y + 1x
       le(s x, 0()) -> false()
       2 + 1x >= 1
       le(0(), y) -> true()
       2 + 0y >= 1
     Qed