MAYBE

Problem:
 double(0()) -> 0()
 double(s(x)) -> s(s(double(x)))
 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)
 first(nil()) -> 0()
 first(cons(x,xs)) -> x
 doublelist(nil()) -> nil()
 doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))

Proof:
 DP Processor:
  DPs:
   double#(s(x)) -> double#(x)
   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)
   doublelist#(cons(x,xs)) -> first#(cons(x,xs))
   doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs))
   doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs)))
   doublelist#(cons(x,xs)) -> double#(x)
  TRS:
   double(0()) -> 0()
   double(s(x)) -> s(s(double(x)))
   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)
   first(nil()) -> 0()
   first(cons(x,xs)) -> x
   doublelist(nil()) -> nil()
   doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))
  Usable Rule Processor:
   DPs:
    double#(s(x)) -> double#(x)
    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)
    doublelist#(cons(x,xs)) -> first#(cons(x,xs))
    doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs))
    doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs)))
    doublelist#(cons(x,xs)) -> double#(x)
   TRS:
    f18(x,y) -> x
    f18(x,y) -> y
    eq(0(),0()) -> true()
    eq(0(),s(y)) -> false()
    eq(s(x),0()) -> false()
    eq(s(x),s(y)) -> eq(x,y)
    first(cons(x,xs)) -> x
    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))
    del(x,nil()) -> nil()
   ADG Processor:
    DPs:
     double#(s(x)) -> double#(x)
     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)
     doublelist#(cons(x,xs)) -> first#(cons(x,xs))
     doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs))
     doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs)))
     doublelist#(cons(x,xs)) -> double#(x)
    TRS:
     f18(x,y) -> x
     f18(x,y) -> y
     eq(0(),0()) -> true()
     eq(0(),s(y)) -> false()
     eq(s(x),0()) -> false()
     eq(s(x),s(y)) -> eq(x,y)
     first(cons(x,xs)) -> x
     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))
     del(x,nil()) -> nil()
    graph:
     doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs))) ->
     doublelist#(cons(x,xs)) -> first#(cons(x,xs))
     doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs))) ->
     doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs))
     doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs))) ->
     doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs)))
     doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs))) ->
     doublelist#(cons(x,xs)) -> double#(x)
     doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs)) ->
     del#(x,cons(y,xs)) -> eq#(x,y)
     doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs)) ->
     del#(x,cons(y,xs)) -> if#(eq(x,y),x,y,xs)
     doublelist#(cons(x,xs)) -> double#(x) ->
     double#(s(x)) -> double#(x)
     if#(false(),x,y,xs) -> del#(x,xs) ->
     del#(x,cons(y,xs)) -> eq#(x,y)
     if#(false(),x,y,xs) -> del#(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)
     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)
     double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x)
    Restore Modifier:
     DPs:
      double#(s(x)) -> double#(x)
      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)
      doublelist#(cons(x,xs)) -> first#(cons(x,xs))
      doublelist#(cons(x,xs)) -> del#(first(cons(x,xs)),cons(x,xs))
      doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs)))
      doublelist#(cons(x,xs)) -> double#(x)
     TRS:
      double(0()) -> 0()
      double(s(x)) -> s(s(double(x)))
      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)
      first(nil()) -> 0()
      first(cons(x,xs)) -> x
      doublelist(nil()) -> nil()
      doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))
     SCC Processor:
      #sccs: 4
      #rules: 5
      #arcs: 13/81
      DPs:
       doublelist#(cons(x,xs)) -> doublelist#(del(first(cons(x,xs)),cons(x,xs)))
      TRS:
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       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)
       first(nil()) -> 0()
       first(cons(x,xs)) -> x
       doublelist(nil()) -> nil()
       doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))
      Open
      
      DPs:
       del#(x,cons(y,xs)) -> if#(eq(x,y),x,y,xs)
       if#(false(),x,y,xs) -> del#(x,xs)
      TRS:
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       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)
       first(nil()) -> 0()
       first(cons(x,xs)) -> x
       doublelist(nil()) -> nil()
       doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))
      Open
      
      DPs:
       eq#(s(x),s(y)) -> eq#(x,y)
      TRS:
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       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)
       first(nil()) -> 0()
       first(cons(x,xs)) -> x
       doublelist(nil()) -> nil()
       doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))
      Open
      
      DPs:
       double#(s(x)) -> double#(x)
      TRS:
       double(0()) -> 0()
       double(s(x)) -> s(s(double(x)))
       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)
       first(nil()) -> 0()
       first(cons(x,xs)) -> x
       doublelist(nil()) -> nil()
       doublelist(cons(x,xs)) -> cons(double(x),doublelist(del(first(cons(x,xs)),cons(x,xs))))
      Open