MAYBE

Problem:
 app(nil(),xs) -> nil()
 app(cons(x,xs),ys) -> cons(x,app(xs,ys))
 rev(nil()) -> nil()
 rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
 shuffle(nil()) -> nil()
 shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))

Proof:
 DP Processor:
  DPs:
   app#(cons(x,xs),ys) -> app#(xs,ys)
   rev#(cons(x,xs)) -> rev#(cons(x,nil()))
   shuffle#(cons(x,xs)) -> rev#(xs)
   shuffle#(cons(x,xs)) -> shuffle#(rev(xs))
  TRS:
   app(nil(),xs) -> nil()
   app(cons(x,xs),ys) -> cons(x,app(xs,ys))
   rev(nil()) -> nil()
   rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
   shuffle(nil()) -> nil()
   shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
  Usable Rule Processor:
   DPs:
    app#(cons(x,xs),ys) -> app#(xs,ys)
    rev#(cons(x,xs)) -> rev#(cons(x,nil()))
    shuffle#(cons(x,xs)) -> rev#(xs)
    shuffle#(cons(x,xs)) -> shuffle#(rev(xs))
   TRS:
    rev(nil()) -> nil()
    rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
   EDG Processor:
    DPs:
     app#(cons(x,xs),ys) -> app#(xs,ys)
     rev#(cons(x,xs)) -> rev#(cons(x,nil()))
     shuffle#(cons(x,xs)) -> rev#(xs)
     shuffle#(cons(x,xs)) -> shuffle#(rev(xs))
    TRS:
     rev(nil()) -> nil()
     rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
    graph:
     shuffle#(cons(x,xs)) -> rev#(xs) ->
     rev#(cons(x,xs)) -> rev#(cons(x,nil()))
     rev#(cons(x,xs)) -> rev#(cons(x,nil())) ->
     rev#(cons(x,xs)) -> rev#(cons(x,nil()))
     app#(cons(x,xs),ys) -> app#(xs,ys) -> app#(cons(x,xs),ys) -> app#(xs,ys)
    Restore Modifier:
     DPs:
      app#(cons(x,xs),ys) -> app#(xs,ys)
      rev#(cons(x,xs)) -> rev#(cons(x,nil()))
      shuffle#(cons(x,xs)) -> rev#(xs)
      shuffle#(cons(x,xs)) -> shuffle#(rev(xs))
     TRS:
      app(nil(),xs) -> nil()
      app(cons(x,xs),ys) -> cons(x,app(xs,ys))
      rev(nil()) -> nil()
      rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
      shuffle(nil()) -> nil()
      shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
     SCC Processor:
      #sccs: 2
      #rules: 2
      #arcs: 3/16
      DPs:
       app#(cons(x,xs),ys) -> app#(xs,ys)
      TRS:
       app(nil(),xs) -> nil()
       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
       rev(nil()) -> nil()
       rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
       shuffle(nil()) -> nil()
       shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [app#](x0, x1) = x0 + 1,
        
        [shuffle](x0) = x0,
        
        [append](x0, x1) = x0,
        
        [rev](x0) = x0,
        
        [cons](x0, x1) = x1 + 1,
        
        [app](x0, x1) = x0 + 1,
        
        [nil] = 1
       orientation:
        app#(cons(x,xs),ys) = xs + 2 >= xs + 1 = app#(xs,ys)
        
        app(nil(),xs) = 2 >= 1 = nil()
        
        app(cons(x,xs),ys) = xs + 2 >= xs + 2 = cons(x,app(xs,ys))
        
        rev(nil()) = 1 >= 1 = nil()
        
        rev(cons(x,xs)) = xs + 1 >= xs = append(xs,rev(cons(x,nil())))
        
        shuffle(nil()) = 1 >= 1 = nil()
        
        shuffle(cons(x,xs)) = xs + 1 >= xs + 1 = cons(x,shuffle(rev(xs)))
       problem:
        DPs:
         
        TRS:
         app(nil(),xs) -> nil()
         app(cons(x,xs),ys) -> cons(x,app(xs,ys))
         rev(nil()) -> nil()
         rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
         shuffle(nil()) -> nil()
         shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
       Qed
      
      DPs:
       rev#(cons(x,xs)) -> rev#(cons(x,nil()))
      TRS:
       app(nil(),xs) -> nil()
       app(cons(x,xs),ys) -> cons(x,app(xs,ys))
       rev(nil()) -> nil()
       rev(cons(x,xs)) -> append(xs,rev(cons(x,nil())))
       shuffle(nil()) -> nil()
       shuffle(cons(x,xs)) -> cons(x,shuffle(rev(xs)))
      Open