MAYBE
Time: 0.006319
TRS:
 {               last nil() -> 0(),
        last cons(x, nil()) -> x,
  last cons(x, cons(y, xs)) -> last cons(y, xs),
              del(x, nil()) -> nil(),
        del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs),
       if(true(), x, y, xs) -> xs,
      if(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),
              reverse nil() -> nil(),
        reverse cons(x, xs) -> cons(last cons(x, xs), reverse del(last cons(x, xs), cons(x, xs)))}
 DP:
  DP:
   {last# cons(x, cons(y, xs)) -> last# cons(y, xs),
          del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs),
          del#(x, cons(y, xs)) -> eq#(x, y),
        if#(false(), x, y, xs) -> del#(x, xs),
                 eq#(s x, s y) -> eq#(x, y),
          reverse# cons(x, xs) -> last# cons(x, xs),
          reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)),
          reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs))}
  TRS:
  {               last nil() -> 0(),
         last cons(x, nil()) -> x,
   last cons(x, cons(y, xs)) -> last cons(y, xs),
               del(x, nil()) -> nil(),
         del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs),
        if(true(), x, y, xs) -> xs,
       if(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),
               reverse nil() -> nil(),
         reverse cons(x, xs) -> cons(last cons(x, xs), reverse del(last cons(x, xs), cons(x, xs)))}
  EDG:
   {(reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> eq#(x, y))
    (reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (reverse# cons(x, xs) -> last# cons(x, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
    (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)))
    (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)))
    (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> last# cons(x, xs))
    (if#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs))
    (if#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> eq#(x, y))
    (last# cons(x, cons(y, xs)) -> last# cons(y, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
    (del#(x, cons(y, xs)) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs), if#(false(), x, y, xs) -> del#(x, xs))}
   EDG:
    {(reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> eq#(x, y))
     (reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs))
     (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (reverse# cons(x, xs) -> last# cons(x, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
     (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)))
     (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)))
     (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> last# cons(x, xs))
     (if#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs))
     (if#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> eq#(x, y))
     (last# cons(x, cons(y, xs)) -> last# cons(y, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
     (del#(x, cons(y, xs)) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
     (del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs), if#(false(), x, y, xs) -> del#(x, xs))}
    EDG:
     {(reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> eq#(x, y))
      (reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)), del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs))
      (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
      (reverse# cons(x, xs) -> last# cons(x, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
      (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)))
      (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> del#(last cons(x, xs), cons(x, xs)))
      (reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs)), reverse# cons(x, xs) -> last# cons(x, xs))
      (if#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs))
      (if#(false(), x, y, xs) -> del#(x, xs), del#(x, cons(y, xs)) -> eq#(x, y))
      (last# cons(x, cons(y, xs)) -> last# cons(y, xs), last# cons(x, cons(y, xs)) -> last# cons(y, xs))
      (del#(x, cons(y, xs)) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
      (del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs), if#(false(), x, y, xs) -> del#(x, xs))}
     STATUS:
      arrows: 0.812500
      SCCS (4):
       Scc:
        {reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs))}
       Scc:
        {last# cons(x, cons(y, xs)) -> last# cons(y, xs)}
       Scc:
        {  del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs),
         if#(false(), x, y, xs) -> del#(x, xs)}
       Scc:
        {eq#(s x, s y) -> eq#(x, y)}
       
       SCC (1):
        Strict:
         {reverse# cons(x, xs) -> reverse# del(last cons(x, xs), cons(x, xs))}
        Weak:
        {               last nil() -> 0(),
               last cons(x, nil()) -> x,
         last cons(x, cons(y, xs)) -> last cons(y, xs),
                     del(x, nil()) -> nil(),
               del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs),
              if(true(), x, y, xs) -> xs,
             if(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),
                     reverse nil() -> nil(),
               reverse cons(x, xs) -> cons(last cons(x, xs), reverse del(last cons(x, xs), cons(x, xs)))}
        Open
       
       SCC (1):
        Strict:
         {last# cons(x, cons(y, xs)) -> last# cons(y, xs)}
        Weak:
        {               last nil() -> 0(),
               last cons(x, nil()) -> x,
         last cons(x, cons(y, xs)) -> last cons(y, xs),
                     del(x, nil()) -> nil(),
               del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs),
              if(true(), x, y, xs) -> xs,
             if(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),
                     reverse nil() -> nil(),
               reverse cons(x, xs) -> cons(last cons(x, xs), reverse del(last cons(x, xs), cons(x, xs)))}
        Open
       
       SCC (2):
        Strict:
         {  del#(x, cons(y, xs)) -> if#(eq(x, y), x, y, xs),
          if#(false(), x, y, xs) -> del#(x, xs)}
        Weak:
        {               last nil() -> 0(),
               last cons(x, nil()) -> x,
         last cons(x, cons(y, xs)) -> last cons(y, xs),
                     del(x, nil()) -> nil(),
               del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs),
              if(true(), x, y, xs) -> xs,
             if(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),
                     reverse nil() -> nil(),
               reverse cons(x, xs) -> cons(last cons(x, xs), reverse del(last cons(x, xs), cons(x, xs)))}
        Open
       
       SCC (1):
        Strict:
         {eq#(s x, s y) -> eq#(x, y)}
        Weak:
        {               last nil() -> 0(),
               last cons(x, nil()) -> x,
         last cons(x, cons(y, xs)) -> last cons(y, xs),
                     del(x, nil()) -> nil(),
               del(x, cons(y, xs)) -> if(eq(x, y), x, y, xs),
              if(true(), x, y, xs) -> xs,
             if(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),
                     reverse nil() -> nil(),
               reverse cons(x, xs) -> cons(last cons(x, xs), reverse del(last cons(x, xs), cons(x, xs)))}
        Open