MAYBE

Problem:
 null(nil()) -> true()
 null(add(n,x)) -> false()
 tail(add(n,x)) -> x
 tail(nil()) -> nil()
 head(add(n,x)) -> n
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 reverse(nil()) -> nil()
 reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
 shuffle(x) -> shuff(x,nil())
 shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
 if(true(),x,y,z) -> y
 if(false(),x,y,z) -> shuff(reverse(tail(x)),z)

Proof:
 DP Processor:
  DPs:
   app#(add(n,x),y) -> app#(x,y)
   reverse#(add(n,x)) -> reverse#(x)
   reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
   shuffle#(x) -> shuff#(x,nil())
   shuff#(x,y) -> head#(x)
   shuff#(x,y) -> app#(y,add(head(x),nil()))
   shuff#(x,y) -> null#(x)
   shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
   if#(false(),x,y,z) -> tail#(x)
   if#(false(),x,y,z) -> reverse#(tail(x))
   if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
  TRS:
   null(nil()) -> true()
   null(add(n,x)) -> false()
   tail(add(n,x)) -> x
   tail(nil()) -> nil()
   head(add(n,x)) -> n
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   reverse(nil()) -> nil()
   reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
   shuffle(x) -> shuff(x,nil())
   shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
   if(true(),x,y,z) -> y
   if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
  Usable Rule Processor:
   DPs:
    app#(add(n,x),y) -> app#(x,y)
    reverse#(add(n,x)) -> reverse#(x)
    reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
    shuffle#(x) -> shuff#(x,nil())
    shuff#(x,y) -> head#(x)
    shuff#(x,y) -> app#(y,add(head(x),nil()))
    shuff#(x,y) -> null#(x)
    shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
    if#(false(),x,y,z) -> tail#(x)
    if#(false(),x,y,z) -> reverse#(tail(x))
    if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
   TRS:
    f20(x,y) -> x
    f20(x,y) -> y
    reverse(nil()) -> nil()
    reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
    app(nil(),y) -> y
    app(add(n,x),y) -> add(n,app(x,y))
    head(add(n,x)) -> n
    null(nil()) -> true()
    null(add(n,x)) -> false()
    tail(add(n,x)) -> x
    tail(nil()) -> nil()
   CDG Processor:
    DPs:
     app#(add(n,x),y) -> app#(x,y)
     reverse#(add(n,x)) -> reverse#(x)
     reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
     shuffle#(x) -> shuff#(x,nil())
     shuff#(x,y) -> head#(x)
     shuff#(x,y) -> app#(y,add(head(x),nil()))
     shuff#(x,y) -> null#(x)
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
     if#(false(),x,y,z) -> tail#(x)
     if#(false(),x,y,z) -> reverse#(tail(x))
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
    TRS:
     f20(x,y) -> x
     f20(x,y) -> y
     reverse(nil()) -> nil()
     reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
     app(nil(),y) -> y
     app(add(n,x),y) -> add(n,app(x,y))
     head(add(n,x)) -> n
     null(nil()) -> true()
     null(add(n,x)) -> false()
     tail(add(n,x)) -> x
     tail(nil()) -> nil()
    graph:
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
     shuff#(x,y) -> head#(x)
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
     shuff#(x,y) -> app#(y,add(head(x),nil()))
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
     shuff#(x,y) -> null#(x)
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z) ->
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
     if#(false(),x,y,z) -> reverse#(tail(x)) ->
     reverse#(add(n,x)) -> reverse#(x)
     if#(false(),x,y,z) -> reverse#(tail(x)) ->
     reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil()))) ->
     if#(false(),x,y,z) -> tail#(x)
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil()))) ->
     if#(false(),x,y,z) -> reverse#(tail(x))
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil()))) ->
     if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
     shuff#(x,y) -> app#(y,add(head(x),nil())) ->
     app#(add(n,x),y) -> app#(x,y)
     shuffle#(x) -> shuff#(x,nil()) -> shuff#(x,y) -> head#(x)
     shuffle#(x) -> shuff#(x,nil()) ->
     shuff#(x,y) -> app#(y,add(head(x),nil()))
     shuffle#(x) -> shuff#(x,nil()) -> shuff#(x,y) -> null#(x)
     shuffle#(x) -> shuff#(x,nil()) ->
     shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
     reverse#(add(n,x)) -> reverse#(x) ->
     reverse#(add(n,x)) -> reverse#(x)
     reverse#(add(n,x)) -> reverse#(x) ->
     reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
     reverse#(add(n,x)) -> app#(reverse(x),add(n,nil())) ->
     app#(add(n,x),y) -> app#(x,y)
     app#(add(n,x),y) -> app#(x,y) -> app#(add(n,x),y) -> app#(x,y)
    Restore Modifier:
     DPs:
      app#(add(n,x),y) -> app#(x,y)
      reverse#(add(n,x)) -> reverse#(x)
      reverse#(add(n,x)) -> app#(reverse(x),add(n,nil()))
      shuffle#(x) -> shuff#(x,nil())
      shuff#(x,y) -> head#(x)
      shuff#(x,y) -> app#(y,add(head(x),nil()))
      shuff#(x,y) -> null#(x)
      shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
      if#(false(),x,y,z) -> tail#(x)
      if#(false(),x,y,z) -> reverse#(tail(x))
      if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
     TRS:
      null(nil()) -> true()
      null(add(n,x)) -> false()
      tail(add(n,x)) -> x
      tail(nil()) -> nil()
      head(add(n,x)) -> n
      app(nil(),y) -> y
      app(add(n,x),y) -> add(n,app(x,y))
      reverse(nil()) -> nil()
      reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
      shuffle(x) -> shuff(x,nil())
      shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
      if(true(),x,y,z) -> y
      if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 18/121
      DPs:
       if#(false(),x,y,z) -> shuff#(reverse(tail(x)),z)
       shuff#(x,y) -> if#(null(x),x,y,app(y,add(head(x),nil())))
      TRS:
       null(nil()) -> true()
       null(add(n,x)) -> false()
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       head(add(n,x)) -> n
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(x) -> shuff(x,nil())
       shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
       if(true(),x,y,z) -> y
       if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
      Open
      
      DPs:
       reverse#(add(n,x)) -> reverse#(x)
      TRS:
       null(nil()) -> true()
       null(add(n,x)) -> false()
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       head(add(n,x)) -> n
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(x) -> shuff(x,nil())
       shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
       if(true(),x,y,z) -> y
       if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
      Open
      
      DPs:
       app#(add(n,x),y) -> app#(x,y)
      TRS:
       null(nil()) -> true()
       null(add(n,x)) -> false()
       tail(add(n,x)) -> x
       tail(nil()) -> nil()
       head(add(n,x)) -> n
       app(nil(),y) -> y
       app(add(n,x),y) -> add(n,app(x,y))
       reverse(nil()) -> nil()
       reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
       shuffle(x) -> shuff(x,nil())
       shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
       if(true(),x,y,z) -> y
       if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
      Open