MAYBE
Time: 0.009566
TRS:
 {               max nil() -> 0(),
        max cons(x, nil()) -> x,
  max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
     if1(true(), x, y, xs) -> max cons(x, xs),
    if1(false(), x, y, xs) -> max cons(y, xs),
              ge(0(), 0()) -> true(),
              ge(0(), s x) -> false(),
              ge(s x, 0()) -> true(),
              ge(s x, s y) -> ge(x, y),
             del(x, nil()) -> nil(),
       del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
     if2(true(), x, y, xs) -> xs,
    if2(false(), x, y, xs) -> cons(y, del(x, xs)),
              eq(0(), 0()) -> true(),
              eq(0(), s y) -> false(),
              eq(s x, 0()) -> false(),
              eq(s x, s y) -> eq(x, y),
                sort nil() -> nil(),
          sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                   h nil() -> nil(),
             h cons(x, xs) -> cons(x, h xs)}
 DP:
  DP:
   {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs),
    max# cons(x, cons(y, xs)) -> ge#(x, y),
       if1#(true(), x, y, xs) -> max# cons(x, xs),
      if1#(false(), x, y, xs) -> max# cons(y, xs),
                ge#(s x, s y) -> ge#(x, y),
         del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs),
         del#(x, cons(y, xs)) -> eq#(x, y),
      if2#(false(), x, y, xs) -> del#(x, xs),
                eq#(s x, s y) -> eq#(x, y),
            sort# cons(x, xs) -> max# cons(x, xs),
            sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)),
            sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)),
            sort# cons(x, xs) -> h# del(max cons(x, xs), cons(x, xs)),
               h# cons(x, xs) -> h# xs}
  TRS:
  {               max nil() -> 0(),
         max cons(x, nil()) -> x,
   max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
      if1(true(), x, y, xs) -> max cons(x, xs),
     if1(false(), x, y, xs) -> max cons(y, xs),
               ge(0(), 0()) -> true(),
               ge(0(), s x) -> false(),
               ge(s x, 0()) -> true(),
               ge(s x, s y) -> ge(x, y),
              del(x, nil()) -> nil(),
        del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
      if2(true(), x, y, xs) -> xs,
     if2(false(), x, y, xs) -> cons(y, del(x, xs)),
               eq(0(), 0()) -> true(),
               eq(0(), s y) -> false(),
               eq(s x, 0()) -> false(),
               eq(s x, s y) -> eq(x, y),
                 sort nil() -> nil(),
           sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                    h nil() -> nil(),
              h cons(x, xs) -> cons(x, h xs)}
  EDG:
   {(sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> eq#(x, y))
    (sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs))
    (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (if2#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> eq#(x, y))
    (if2#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs))
    (if1#(false(), x, y, xs) -> max# cons(y, xs), max# cons(x, cons(y, xs)) -> ge#(x, y))
    (if1#(false(), x, y, xs) -> max# cons(y, xs), max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs))
    (h# cons(x, xs) -> h# xs, h# cons(x, xs) -> h# xs)
    (del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs), if2#(false(), x, y, xs) -> del#(x, xs))
    (max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(true(), x, y, xs) -> max# cons(x, xs))
    (max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs), if1#(false(), x, y, xs) -> max# cons(y, xs))
    (sort# cons(x, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs))
    (sort# cons(x, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> ge#(x, y))
    (if1#(true(), x, y, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs))
    (if1#(true(), x, y, xs) -> max# cons(x, xs), max# cons(x, cons(y, xs)) -> ge#(x, y))
    (sort# cons(x, xs) -> h# del(max cons(x, xs), cons(x, xs)), h# cons(x, xs) -> h# xs)
    (del#(x, cons(y, xs)) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (max# cons(x, cons(y, xs)) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
    (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> max# cons(x, xs))
    (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> del#(max cons(x, xs), cons(x, xs)))
    (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)))
    (sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs)), sort# cons(x, xs) -> h# del(max cons(x, xs), cons(x, xs)))}
   STATUS:
    arrows: 0.882653
    SCCS (6):
     Scc:
      {sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs))}
     Scc:
      {h# cons(x, xs) -> h# xs}
     Scc:
      {   del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs),
       if2#(false(), x, y, xs) -> del#(x, xs)}
     Scc:
      {eq#(s x, s y) -> eq#(x, y)}
     Scc:
      {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs),
          if1#(true(), x, y, xs) -> max# cons(x, xs),
         if1#(false(), x, y, xs) -> max# cons(y, xs)}
     Scc:
      {ge#(s x, s y) -> ge#(x, y)}
     
     SCC (1):
      Strict:
       {sort# cons(x, xs) -> sort# h del(max cons(x, xs), cons(x, xs))}
      Weak:
      {               max nil() -> 0(),
             max cons(x, nil()) -> x,
       max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
          if1(true(), x, y, xs) -> max cons(x, xs),
         if1(false(), x, y, xs) -> max cons(y, xs),
                   ge(0(), 0()) -> true(),
                   ge(0(), s x) -> false(),
                   ge(s x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                  del(x, nil()) -> nil(),
            del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
          if2(true(), x, y, xs) -> xs,
         if2(false(), x, y, xs) -> cons(y, del(x, xs)),
                   eq(0(), 0()) -> true(),
                   eq(0(), s y) -> false(),
                   eq(s x, 0()) -> false(),
                   eq(s x, s y) -> eq(x, y),
                     sort nil() -> nil(),
               sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                        h nil() -> nil(),
                  h cons(x, xs) -> cons(x, h xs)}
      Open
     
     SCC (1):
      Strict:
       {h# cons(x, xs) -> h# xs}
      Weak:
      {               max nil() -> 0(),
             max cons(x, nil()) -> x,
       max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
          if1(true(), x, y, xs) -> max cons(x, xs),
         if1(false(), x, y, xs) -> max cons(y, xs),
                   ge(0(), 0()) -> true(),
                   ge(0(), s x) -> false(),
                   ge(s x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                  del(x, nil()) -> nil(),
            del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
          if2(true(), x, y, xs) -> xs,
         if2(false(), x, y, xs) -> cons(y, del(x, xs)),
                   eq(0(), 0()) -> true(),
                   eq(0(), s y) -> false(),
                   eq(s x, 0()) -> false(),
                   eq(s x, s y) -> eq(x, y),
                     sort nil() -> nil(),
               sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                        h nil() -> nil(),
                  h cons(x, xs) -> cons(x, h xs)}
      Open
     
     SCC (2):
      Strict:
       {   del#(x, cons(y, xs)) -> if2#(eq(x, y), x, y, xs),
        if2#(false(), x, y, xs) -> del#(x, xs)}
      Weak:
      {               max nil() -> 0(),
             max cons(x, nil()) -> x,
       max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
          if1(true(), x, y, xs) -> max cons(x, xs),
         if1(false(), x, y, xs) -> max cons(y, xs),
                   ge(0(), 0()) -> true(),
                   ge(0(), s x) -> false(),
                   ge(s x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                  del(x, nil()) -> nil(),
            del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
          if2(true(), x, y, xs) -> xs,
         if2(false(), x, y, xs) -> cons(y, del(x, xs)),
                   eq(0(), 0()) -> true(),
                   eq(0(), s y) -> false(),
                   eq(s x, 0()) -> false(),
                   eq(s x, s y) -> eq(x, y),
                     sort nil() -> nil(),
               sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                        h nil() -> nil(),
                  h cons(x, xs) -> cons(x, h xs)}
      Open
     
     SCC (1):
      Strict:
       {eq#(s x, s y) -> eq#(x, y)}
      Weak:
      {               max nil() -> 0(),
             max cons(x, nil()) -> x,
       max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
          if1(true(), x, y, xs) -> max cons(x, xs),
         if1(false(), x, y, xs) -> max cons(y, xs),
                   ge(0(), 0()) -> true(),
                   ge(0(), s x) -> false(),
                   ge(s x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                  del(x, nil()) -> nil(),
            del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
          if2(true(), x, y, xs) -> xs,
         if2(false(), x, y, xs) -> cons(y, del(x, xs)),
                   eq(0(), 0()) -> true(),
                   eq(0(), s y) -> false(),
                   eq(s x, 0()) -> false(),
                   eq(s x, s y) -> eq(x, y),
                     sort nil() -> nil(),
               sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                        h nil() -> nil(),
                  h cons(x, xs) -> cons(x, h xs)}
      Open
     
     SCC (3):
      Strict:
       {max# cons(x, cons(y, xs)) -> if1#(ge(x, y), x, y, xs),
           if1#(true(), x, y, xs) -> max# cons(x, xs),
          if1#(false(), x, y, xs) -> max# cons(y, xs)}
      Weak:
      {               max nil() -> 0(),
             max cons(x, nil()) -> x,
       max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
          if1(true(), x, y, xs) -> max cons(x, xs),
         if1(false(), x, y, xs) -> max cons(y, xs),
                   ge(0(), 0()) -> true(),
                   ge(0(), s x) -> false(),
                   ge(s x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                  del(x, nil()) -> nil(),
            del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
          if2(true(), x, y, xs) -> xs,
         if2(false(), x, y, xs) -> cons(y, del(x, xs)),
                   eq(0(), 0()) -> true(),
                   eq(0(), s y) -> false(),
                   eq(s x, 0()) -> false(),
                   eq(s x, s y) -> eq(x, y),
                     sort nil() -> nil(),
               sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                        h nil() -> nil(),
                  h cons(x, xs) -> cons(x, h xs)}
      Open
     
     SCC (1):
      Strict:
       {ge#(s x, s y) -> ge#(x, y)}
      Weak:
      {               max nil() -> 0(),
             max cons(x, nil()) -> x,
       max cons(x, cons(y, xs)) -> if1(ge(x, y), x, y, xs),
          if1(true(), x, y, xs) -> max cons(x, xs),
         if1(false(), x, y, xs) -> max cons(y, xs),
                   ge(0(), 0()) -> true(),
                   ge(0(), s x) -> false(),
                   ge(s x, 0()) -> true(),
                   ge(s x, s y) -> ge(x, y),
                  del(x, nil()) -> nil(),
            del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs),
          if2(true(), x, y, xs) -> xs,
         if2(false(), x, y, xs) -> cons(y, del(x, xs)),
                   eq(0(), 0()) -> true(),
                   eq(0(), s y) -> false(),
                   eq(s x, 0()) -> false(),
                   eq(s x, s y) -> eq(x, y),
                     sort nil() -> nil(),
               sort cons(x, xs) -> cons(max cons(x, xs), sort h del(max cons(x, xs), cons(x, xs))),
                        h nil() -> nil(),
                  h cons(x, xs) -> cons(x, h xs)}
      Open