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())))

Proof:
 DP Processor:
  DPs:
   app#(cons(x,xs),ys) -> app#(xs,ys)
   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())))
  TDG Processor:
   DPs:
    app#(cons(x,xs),ys) -> app#(xs,ys)
    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())))
   graph:
    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)
   CDG Processor:
    DPs:
     app#(cons(x,xs),ys) -> app#(xs,ys)
     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())))
    graph:
     rev#(cons(x,xs)) -> rev#(cons(x,nil())) -> rev#(cons(x,xs)) -> rev#(cons(x,nil()))
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 1/4
     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())))
     Open