YES

Problem:
 app(app(app(compose(),f),g),x) -> app(g,app(f,x))
 app(reverse(),l) -> app(app(reverse2(),l),nil())
 app(app(reverse2(),nil()),l) -> l
 app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
 app(hd(),app(app(cons(),x),xs)) -> x
 app(tl(),app(app(cons(),x),xs)) -> xs
 last() -> app(app(compose(),hd()),reverse())
 init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))

Proof:
 DP Processor:
  DPs:
   app#(app(app(compose(),f),g),x) -> app#(f,x)
   app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
   app#(reverse(),l) -> app#(reverse2(),l)
   app#(reverse(),l) -> app#(app(reverse2(),l),nil())
   app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
   app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
   app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
   last#() -> app#(compose(),hd())
   last#() -> app#(app(compose(),hd()),reverse())
   init#() -> app#(compose(),tl())
   init#() -> app#(app(compose(),tl()),reverse())
   init#() -> app#(compose(),reverse())
   init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
  TRS:
   app(app(app(compose(),f),g),x) -> app(g,app(f,x))
   app(reverse(),l) -> app(app(reverse2(),l),nil())
   app(app(reverse2(),nil()),l) -> l
   app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
   app(hd(),app(app(cons(),x),xs)) -> x
   app(tl(),app(app(cons(),x),xs)) -> xs
   last() -> app(app(compose(),hd()),reverse())
   init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
  TDG Processor:
   DPs:
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    last#() -> app#(compose(),hd())
    last#() -> app#(app(compose(),hd()),reverse())
    init#() -> app#(compose(),tl())
    init#() -> app#(app(compose(),tl()),reverse())
    init#() -> app#(compose(),reverse())
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
   TRS:
    app(app(app(compose(),f),g),x) -> app(g,app(f,x))
    app(reverse(),l) -> app(app(reverse2(),l),nil())
    app(app(reverse2(),nil()),l) -> l
    app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
    app(hd(),app(app(cons(),x),xs)) -> x
    app(tl(),app(app(cons(),x),xs)) -> xs
    last() -> app(app(compose(),hd()),reverse())
    init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
   graph:
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    init#() -> app#(app(compose(),tl()),reverse()) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    init#() -> app#(app(compose(),reverse()),app(app(compose(),tl()),reverse())) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    init#() -> app#(compose(),tl()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    init#() -> app#(compose(),tl()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    init#() -> app#(compose(),tl()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    init#() -> app#(compose(),tl()) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    init#() -> app#(compose(),tl()) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    init#() -> app#(compose(),tl()) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    init#() -> app#(compose(),tl()) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    init#() -> app#(compose(),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    init#() -> app#(compose(),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    init#() -> app#(compose(),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    init#() -> app#(compose(),reverse()) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    init#() -> app#(compose(),reverse()) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    init#() -> app#(compose(),reverse()) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    init#() -> app#(compose(),reverse()) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    last#() -> app#(app(compose(),hd()),reverse()) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    last#() -> app#(compose(),hd()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    last#() -> app#(compose(),hd()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    last#() -> app#(compose(),hd()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    last#() -> app#(compose(),hd()) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    last#() -> app#(compose(),hd()) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    last#() -> app#(compose(),hd()) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    last#() -> app#(compose(),hd()) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(reverse(),l) -> app#(reverse2(),l) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
    app#(app(app(compose(),f),g),x) -> app#(f,x)
    app#(app(app(compose(),f),g),x) -> app#(f,x) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    app#(app(app(compose(),f),g),x) -> app#(f,x) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
    app#(app(app(compose(),f),g),x) -> app#(f,x) ->
    app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
    app#(app(app(compose(),f),g),x) -> app#(f,x) ->
    app#(reverse(),l) -> app#(app(reverse2(),l),nil())
    app#(app(app(compose(),f),g),x) -> app#(f,x) ->
    app#(reverse(),l) -> app#(reverse2(),l)
    app#(app(app(compose(),f),g),x) -> app#(f,x) ->
    app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
    app#(app(app(compose(),f),g),x) -> app#(f,x) -> app#(app(app(compose(),f),g),x) -> app#(f,x)
   SCC Processor:
    #sccs: 1
    #rules: 7
    #arcs: 91/169
    DPs:
     app#(app(app(compose(),f),g),x) -> app#(f,x)
     app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
     app#(reverse(),l) -> app#(reverse2(),l)
     app#(reverse(),l) -> app#(app(reverse2(),l),nil())
     app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
     app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
     app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(reverse2(),xs),app(app(cons(),x),l))
    TRS:
     app(app(app(compose(),f),g),x) -> app(g,app(f,x))
     app(reverse(),l) -> app(app(reverse2(),l),nil())
     app(app(reverse2(),nil()),l) -> l
     app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
     app(hd(),app(app(cons(),x),xs)) -> x
     app(tl(),app(app(cons(),x),xs)) -> xs
     last() -> app(app(compose(),hd()),reverse())
     init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
    EDG Processor:
     DPs:
      app#(app(app(compose(),f),g),x) -> app#(f,x)
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
      app#(reverse(),l) -> app#(reverse2(),l)
      app#(reverse(),l) -> app#(app(reverse2(),l),nil())
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l))
     TRS:
      app(app(app(compose(),f),g),x) -> app(g,app(f,x))
      app(reverse(),l) -> app(app(reverse2(),l),nil())
      app(app(reverse2(),nil()),l) -> l
      app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
      app(hd(),app(app(cons(),x),xs)) -> x
      app(tl(),app(app(cons(),x),xs)) -> xs
      last() -> app(app(compose(),hd()),reverse())
      init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
     graph:
      app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
      app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
      app#(reverse(),l) -> app#(app(reverse2(),l),nil()) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l))
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l)) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l)) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l)) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l))
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(app(app(compose(),f),g),x) -> app#(f,x)
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(reverse(),l) -> app#(reverse2(),l)
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(reverse(),l) -> app#(app(reverse2(),l),nil())
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l))
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(app(app(compose(),f),g),x) -> app#(f,x)
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(reverse(),l) -> app#(reverse2(),l)
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(reverse(),l) -> app#(app(reverse2(),l),nil())
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
      app#(app(app(compose(),f),g),x) -> app#(f,x) ->
      app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
      app#(app(reverse2(),xs),app(app(cons(),x),l))
     CDG Processor:
      DPs:
       app#(app(app(compose(),f),g),x) -> app#(f,x)
       app#(app(app(compose(),f),g),x) -> app#(g,app(f,x))
       app#(reverse(),l) -> app#(reverse2(),l)
       app#(reverse(),l) -> app#(app(reverse2(),l),nil())
       app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
       app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
       app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
       app#(app(reverse2(),xs),app(app(cons(),x),l))
      TRS:
       app(app(app(compose(),f),g),x) -> app(g,app(f,x))
       app(reverse(),l) -> app(app(reverse2(),l),nil())
       app(app(reverse2(),nil()),l) -> l
       app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
       app(hd(),app(app(cons(),x),xs)) -> x
       app(tl(),app(app(cons(),x),xs)) -> xs
       last() -> app(app(compose(),hd()),reverse())
       init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
      graph:
       app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
       app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
       app#(app(reverse2(),xs),app(app(cons(),x),l))
       app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
       app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
       app#(app(app(compose(),f),g),x) -> app#(g,app(f,x)) ->
       app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
       app#(app(app(compose(),f),g),x) -> app#(f,x) ->
       app#(app(reverse2(),app(app(cons(),x),xs)),l) ->
       app#(app(reverse2(),xs),app(app(cons(),x),l))
       app#(app(app(compose(),f),g),x) -> app#(f,x) ->
       app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(reverse2(),xs)
       app#(app(app(compose(),f),g),x) -> app#(f,x) ->
       app#(app(reverse2(),app(app(cons(),x),xs)),l) -> app#(app(cons(),x),l)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 6/49