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)))
  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:
    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)))
   graph:
    shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) ->
    shuffle#(cons(x,xs)) -> rev#(xs)
    shuffle#(cons(x,xs)) -> shuffle#(rev(xs)) ->
    shuffle#(cons(x,xs)) -> shuffle#(rev(xs))
    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)
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 5/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)))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     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:
     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)))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [shuffle#](x0) = x0 + 1,
      
      [shuffle](x0) = x0,
      
      [append](x0, x1) = 0,
      
      [rev](x0) = 0,
      
      [cons](x0, x1) = 1,
      
      [app](x0, x1) = x0,
      
      [nil] = 0
     orientation:
      shuffle#(cons(x,xs)) = 2 >= 1 = shuffle#(rev(xs))
      
      app(nil(),xs) = 0 >= 0 = nil()
      
      app(cons(x,xs),ys) = 1 >= 1 = cons(x,app(xs,ys))
      
      rev(nil()) = 0 >= 0 = nil()
      
      rev(cons(x,xs)) = 0 >= 0 = append(xs,rev(cons(x,nil())))
      
      shuffle(nil()) = 0 >= 0 = nil()
      
      shuffle(cons(x,xs)) = 1 >= 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