MAYBE

Problem:
 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))))

Proof:
 DP Processor:
  DPs:
   last#(cons(x,cons(y,xs))) -> last#(cons(y,xs))
   del#(x,cons(y,xs)) -> eq#(x,y)
   del#(x,cons(y,xs)) -> if#(eq(x,y),x,y,xs)
   if#(false(),x,y,xs) -> del#(x,xs)
   eq#(s(x),s(y)) -> eq#(x,y)
   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))
  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))))
  TDG Processor:
   DPs:
    last#(cons(x,cons(y,xs))) -> last#(cons(y,xs))
    del#(x,cons(y,xs)) -> eq#(x,y)
    del#(x,cons(y,xs)) -> if#(eq(x,y),x,y,xs)
    if#(false(),x,y,xs) -> del#(x,xs)
    eq#(s(x),s(y)) -> eq#(x,y)
    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))
   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))))
   graph:
    reverse#(cons(x,xs)) -> reverse#(del(last(cons(x,xs)),cons(x,xs))) ->
    reverse#(cons(x,xs)) -> last#(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)) -> 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)) -> del#(last(cons(x,xs)),cons(x,xs)) ->
    del#(x,cons(y,xs)) -> if#(eq(x,y),x,y,xs)
    reverse#(cons(x,xs)) -> del#(last(cons(x,xs)),cons(x,xs)) ->
    del#(x,cons(y,xs)) -> eq#(x,y)
    reverse#(cons(x,xs)) -> last#(cons(x,xs)) ->
    last#(cons(x,cons(y,xs))) -> last#(cons(y,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)
    eq#(s(x),s(y)) -> 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)
    del#(x,cons(y,xs)) -> eq#(x,y) ->
    eq#(s(x),s(y)) -> eq#(x,y)
    last#(cons(x,cons(y,xs))) -> last#(cons(y,xs)) ->
    last#(cons(x,cons(y,xs))) -> last#(cons(y,xs))
   SCC Processor:
    #sccs: 4
    #rules: 5
    #arcs: 12/64
    DPs:
     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))))
    Open
    
    DPs:
     last#(cons(x,cons(y,xs))) -> last#(cons(y,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))))
    Subterm Criterion Processor:
     simple projection:
      pi(last#) = 0
     problem:
      DPs:
       
      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))))
     Qed
    
    DPs:
     del#(x,cons(y,xs)) -> if#(eq(x,y),x,y,xs)
     if#(false(),x,y,xs) -> del#(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))))
    Subterm Criterion Processor:
     simple projection:
      pi(del#) = 1
      pi(if#) = 3
     problem:
      DPs:
       if#(false(),x,y,xs) -> del#(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))))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    DPs:
     eq#(s(x),s(y)) -> eq#(x,y)
    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))))
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      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))))
     Qed