MAYBE

Problem:
 app(app(apply(),f_1),x) -> app(f_1,x)
 app(id(),x) -> x
 app(app(app(uncurry(),f_2),x),y) -> app(app(f_2,x),y)
 app(app(app(swap(),f_2),y),x) -> app(app(f_2,x),y)
 app(app(app(compose(),g_1),f_1),x) -> app(g_1,app(f_1,x))
 app(app(const(),x),y) -> x
 app(listify(),x) -> app(app(cons(),x),nil())
 app(app(app(app(fold(),f_3),g_2),x),nil()) -> x
 app(app(app(app(fold(),f_3),g_2),x),app(app(cons(),z),t)) ->
 app(app(f_3,app(g_2,z)),app(app(app(app(fold(),f_3),g_2),x),t))
 app(sum(),l) -> app(app(app(app(fold(),add()),id()),0()),l)
 app(app(uncurry(),app(app(fold(),cons()),id())),nil()) -> id()
 append() -> app(app(compose(),app(app(swap(),fold()),cons())),id())
 reverse() -> app(app(uncurry(),app(app(fold(),app(swap(),append())),listify())),nil())
 length() -> app(app(uncurry(),app(app(fold(),add()),app(cons(),1()))),0())

Proof:
 DP Processor:
  DPs:
   app#(app(apply(),f_1),x) -> app#(f_1,x)
   app#(app(app(uncurry(),f_2),x),y) -> app#(f_2,x)
   app#(app(app(uncurry(),f_2),x),y) -> app#(app(f_2,x),y)
   app#(app(app(swap(),f_2),y),x) -> app#(f_2,x)
   app#(app(app(swap(),f_2),y),x) -> app#(app(f_2,x),y)
   app#(app(app(compose(),g_1),f_1),x) -> app#(f_1,x)
   app#(app(app(compose(),g_1),f_1),x) -> app#(g_1,app(f_1,x))
   app#(listify(),x) -> app#(cons(),x)
   app#(listify(),x) -> app#(app(cons(),x),nil())
   app#(app(app(app(fold(),f_3),g_2),x),app(app(cons(),z),t)) ->
   app#(app(app(app(fold(),f_3),g_2),x),t)
   app#(app(app(app(fold(),f_3),g_2),x),app(app(cons(),z),t)) -> app#(g_2,z)
   app#(app(app(app(fold(),f_3),g_2),x),app(app(cons(),z),t)) -> app#(f_3,app(g_2,z))
   app#(app(app(app(fold(),f_3),g_2),x),app(app(cons(),z),t)) ->
   app#(app(f_3,app(g_2,z)),app(app(app(app(fold(),f_3),g_2),x),t))
   app#(sum(),l) -> app#(fold(),add())
   app#(sum(),l) -> app#(app(fold(),add()),id())
   app#(sum(),l) -> app#(app(app(fold(),add()),id()),0())
   app#(sum(),l) -> app#(app(app(app(fold(),add()),id()),0()),l)
   append#() -> app#(swap(),fold())
   append#() -> app#(app(swap(),fold()),cons())
   append#() -> app#(compose(),app(app(swap(),fold()),cons()))
   append#() -> app#(app(compose(),app(app(swap(),fold()),cons())),id())
   reverse#() -> append#()
   reverse#() -> app#(swap(),append())
   reverse#() -> app#(fold(),app(swap(),append()))
   reverse#() -> app#(app(fold(),app(swap(),append())),listify())
   reverse#() -> app#(uncurry(),app(app(fold(),app(swap(),append())),listify()))
   reverse#() -> app#(app(uncurry(),app(app(fold(),app(swap(),append())),listify())),nil())
   length#() -> app#(cons(),1())
   length#() -> app#(fold(),add())
   length#() -> app#(app(fold(),add()),app(cons(),1()))
   length#() -> app#(uncurry(),app(app(fold(),add()),app(cons(),1())))
   length#() -> app#(app(uncurry(),app(app(fold(),add()),app(cons(),1()))),0())
  TRS:
   app(app(apply(),f_1),x) -> app(f_1,x)
   app(id(),x) -> x
   app(app(app(uncurry(),f_2),x),y) -> app(app(f_2,x),y)
   app(app(app(swap(),f_2),y),x) -> app(app(f_2,x),y)
   app(app(app(compose(),g_1),f_1),x) -> app(g_1,app(f_1,x))
   app(app(const(),x),y) -> x
   app(listify(),x) -> app(app(cons(),x),nil())
   app(app(app(app(fold(),f_3),g_2),x),nil()) -> x
   app(app(app(app(fold(),f_3),g_2),x),app(app(cons(),z),t)) ->
   app(app(f_3,app(g_2,z)),app(app(app(app(fold(),f_3),g_2),x),t))
   app(sum(),l) -> app(app(app(app(fold(),add()),id()),0()),l)
   app(app(uncurry(),app(app(fold(),cons()),id())),nil()) -> id()
   append() -> app(app(compose(),app(app(swap(),fold()),cons())),id())
   reverse() -> app(app(uncurry(),app(app(fold(),app(swap(),append())),listify())),nil())
   length() -> app(app(uncurry(),app(app(fold(),add()),app(cons(),1()))),0())
  Open