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:
 Uncurry Processor:
  apply2(f_1,x) -> app(f_1,x)
  id1(x) -> x
  uncurry3(f_2,x,y) -> app(app(f_2,x),y)
  swap3(f_2,y,x) -> app(app(f_2,x),y)
  compose3(g_1,f_1,x) -> app(g_1,app(f_1,x))
  const2(x,y) -> x
  listify1(x) -> cons2(x,nil())
  fold4(f_3,g_2,x,nil()) -> x
  fold4(f_3,g_2,x,cons2(z,t)) -> app(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
  sum1(l) -> fold4(add(),id(),0(),l)
  uncurry3(fold2(cons(),id()),nil(),x14) -> id1(x14)
  uncurry2(fold2(cons(),id()),nil()) -> id()
  append() -> compose2(swap2(fold(),cons()),id())
  reverse() -> uncurry2(fold2(swap1(append()),listify()),nil())
  length() -> uncurry2(fold2(add(),cons1(1())),0())
  app(apply1(x12),x13) -> apply2(x12,x13)
  app(apply(),x13) -> apply1(x13)
  app(id(),x13) -> id1(x13)
  app(uncurry2(x12,x11),x13) -> uncurry3(x12,x11,x13)
  app(uncurry1(x12),x13) -> uncurry2(x12,x13)
  app(uncurry(),x13) -> uncurry1(x13)
  app(swap2(x12,x11),x13) -> swap3(x12,x11,x13)
  app(swap1(x12),x13) -> swap2(x12,x13)
  app(swap(),x13) -> swap1(x13)
  app(compose2(x12,x11),x13) -> compose3(x12,x11,x13)
  app(compose1(x12),x13) -> compose2(x12,x13)
  app(compose(),x13) -> compose1(x13)
  app(const1(x12),x13) -> const2(x12,x13)
  app(const(),x13) -> const1(x13)
  app(listify(),x13) -> listify1(x13)
  app(cons1(x12),x13) -> cons2(x12,x13)
  app(cons(),x13) -> cons1(x13)
  app(fold3(x12,x11,x10),x13) -> fold4(x12,x11,x10,x13)
  app(fold2(x12,x11),x13) -> fold3(x12,x11,x13)
  app(fold1(x12),x13) -> fold2(x12,x13)
  app(fold(),x13) -> fold1(x13)
  app(sum(),x13) -> sum1(x13)
  DP Processor:
   DPs:
    apply{2,#}(f_1,x) -> app#(f_1,x)
    uncurry{3,#}(f_2,x,y) -> app#(f_2,x)
    uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y)
    swap{3,#}(f_2,y,x) -> app#(f_2,x)
    swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y)
    compose{3,#}(g_1,f_1,x) -> app#(f_1,x)
    compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x))
    fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t)
    fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z)
    fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z))
    fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
    sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l)
    uncurry{3,#}(fold2(cons(),id()),nil(),x14) -> id{1,#}(x14)
    reverse#() -> append#()
    reverse#() -> uncurry{2,#}(fold2(swap1(append()),listify()),nil())
    length#() -> uncurry{2,#}(fold2(add(),cons1(1())),0())
    app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
    app#(id(),x13) -> id{1,#}(x13)
    app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
    app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
    app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
    app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
    app#(const1(x12),x13) -> const{2,#}(x12,x13)
    app#(listify(),x13) -> listify{1,#}(x13)
    app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
    app#(sum(),x13) -> sum{1,#}(x13)
   TRS:
    apply2(f_1,x) -> app(f_1,x)
    id1(x) -> x
    uncurry3(f_2,x,y) -> app(app(f_2,x),y)
    swap3(f_2,y,x) -> app(app(f_2,x),y)
    compose3(g_1,f_1,x) -> app(g_1,app(f_1,x))
    const2(x,y) -> x
    listify1(x) -> cons2(x,nil())
    fold4(f_3,g_2,x,nil()) -> x
    fold4(f_3,g_2,x,cons2(z,t)) -> app(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
    sum1(l) -> fold4(add(),id(),0(),l)
    uncurry3(fold2(cons(),id()),nil(),x14) -> id1(x14)
    uncurry2(fold2(cons(),id()),nil()) -> id()
    append() -> compose2(swap2(fold(),cons()),id())
    reverse() -> uncurry2(fold2(swap1(append()),listify()),nil())
    length() -> uncurry2(fold2(add(),cons1(1())),0())
    app(apply1(x12),x13) -> apply2(x12,x13)
    app(apply(),x13) -> apply1(x13)
    app(id(),x13) -> id1(x13)
    app(uncurry2(x12,x11),x13) -> uncurry3(x12,x11,x13)
    app(uncurry1(x12),x13) -> uncurry2(x12,x13)
    app(uncurry(),x13) -> uncurry1(x13)
    app(swap2(x12,x11),x13) -> swap3(x12,x11,x13)
    app(swap1(x12),x13) -> swap2(x12,x13)
    app(swap(),x13) -> swap1(x13)
    app(compose2(x12,x11),x13) -> compose3(x12,x11,x13)
    app(compose1(x12),x13) -> compose2(x12,x13)
    app(compose(),x13) -> compose1(x13)
    app(const1(x12),x13) -> const2(x12,x13)
    app(const(),x13) -> const1(x13)
    app(listify(),x13) -> listify1(x13)
    app(cons1(x12),x13) -> cons2(x12,x13)
    app(cons(),x13) -> cons1(x13)
    app(fold3(x12,x11,x10),x13) -> fold4(x12,x11,x10,x13)
    app(fold2(x12,x11),x13) -> fold3(x12,x11,x13)
    app(fold1(x12),x13) -> fold2(x12,x13)
    app(fold(),x13) -> fold1(x13)
    app(sum(),x13) -> sum1(x13)
   TDG Processor:
    DPs:
     apply{2,#}(f_1,x) -> app#(f_1,x)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y)
     swap{3,#}(f_2,y,x) -> app#(f_2,x)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x))
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z))
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
     sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l)
     uncurry{3,#}(fold2(cons(),id()),nil(),x14) -> id{1,#}(x14)
     reverse#() -> append#()
     reverse#() -> uncurry{2,#}(fold2(swap1(append()),listify()),nil())
     length#() -> uncurry{2,#}(fold2(add(),cons1(1())),0())
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     app#(id(),x13) -> id{1,#}(x13)
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     app#(listify(),x13) -> listify{1,#}(x13)
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     app#(sum(),x13) -> sum{1,#}(x13)
    TRS:
     apply2(f_1,x) -> app(f_1,x)
     id1(x) -> x
     uncurry3(f_2,x,y) -> app(app(f_2,x),y)
     swap3(f_2,y,x) -> app(app(f_2,x),y)
     compose3(g_1,f_1,x) -> app(g_1,app(f_1,x))
     const2(x,y) -> x
     listify1(x) -> cons2(x,nil())
     fold4(f_3,g_2,x,nil()) -> x
     fold4(f_3,g_2,x,cons2(z,t)) -> app(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
     sum1(l) -> fold4(add(),id(),0(),l)
     uncurry3(fold2(cons(),id()),nil(),x14) -> id1(x14)
     uncurry2(fold2(cons(),id()),nil()) -> id()
     append() -> compose2(swap2(fold(),cons()),id())
     reverse() -> uncurry2(fold2(swap1(append()),listify()),nil())
     length() -> uncurry2(fold2(add(),cons1(1())),0())
     app(apply1(x12),x13) -> apply2(x12,x13)
     app(apply(),x13) -> apply1(x13)
     app(id(),x13) -> id1(x13)
     app(uncurry2(x12,x11),x13) -> uncurry3(x12,x11,x13)
     app(uncurry1(x12),x13) -> uncurry2(x12,x13)
     app(uncurry(),x13) -> uncurry1(x13)
     app(swap2(x12,x11),x13) -> swap3(x12,x11,x13)
     app(swap1(x12),x13) -> swap2(x12,x13)
     app(swap(),x13) -> swap1(x13)
     app(compose2(x12,x11),x13) -> compose3(x12,x11,x13)
     app(compose1(x12),x13) -> compose2(x12,x13)
     app(compose(),x13) -> compose1(x13)
     app(const1(x12),x13) -> const2(x12,x13)
     app(const(),x13) -> const1(x13)
     app(listify(),x13) -> listify1(x13)
     app(cons1(x12),x13) -> cons2(x12,x13)
     app(cons(),x13) -> cons1(x13)
     app(fold3(x12,x11,x10),x13) -> fold4(x12,x11,x10,x13)
     app(fold2(x12,x11),x13) -> fold3(x12,x11,x13)
     app(fold1(x12),x13) -> fold2(x12,x13)
     app(fold(),x13) -> fold1(x13)
     app(sum(),x13) -> sum1(x13)
    graph:
     sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
     sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z))
     sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z)
     sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z))
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(id(),x13) -> id{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t)) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(id(),x13) -> id{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(id(),x13) -> id{1,#}(x13)
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z)) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(id(),x13) -> id{1,#}(x13)
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x)) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(id(),x13) -> id{1,#}(x13)
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(id(),x13) -> id{1,#}(x13)
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(id(),x13) -> id{1,#}(x13)
     swap{3,#}(f_2,y,x) -> app#(f_2,x) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(id(),x13) -> id{1,#}(x13)
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(id(),x13) -> id{1,#}(x13)
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x) ->
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z))
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z)
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13) ->
     fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t)
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13) ->
     compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x))
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13) ->
     compose{3,#}(g_1,f_1,x) -> app#(f_1,x)
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13) ->
     swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y)
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13) ->
     swap{3,#}(f_2,y,x) -> app#(f_2,x)
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13) ->
     uncurry{3,#}(fold2(cons(),id()),nil(),x14) -> id{1,#}(x14)
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13) ->
     uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y)
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13) ->
     uncurry{3,#}(f_2,x,y) -> app#(f_2,x)
     app#(apply1(x12),x13) -> apply{2,#}(x12,x13) ->
     apply{2,#}(f_1,x) -> app#(f_1,x)
     app#(sum(),x13) -> sum{1,#}(x13) ->
     sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(sum(),x13) -> sum{1,#}(x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(listify(),x13) -> listify{1,#}(x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(const1(x12),x13) -> const{2,#}(x12,x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(uncurry1(x12),x13) -> uncurry{2,#}(x12,x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) ->
     app#(id(),x13) -> id{1,#}(x13)
     apply{2,#}(f_1,x) -> app#(f_1,x) -> app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
    SCC Processor:
     #sccs: 1
     #rules: 18
     #arcs: 121/676
     DPs:
      sum{1,#}(l) -> fold{4,#}(add(),id(),0(),l)
      fold{4,#}(f_3,g_2,x,cons2(z,t)) -> fold{4,#}(f_3,g_2,x,t)
      fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(g_2,z)
      app#(apply1(x12),x13) -> apply{2,#}(x12,x13)
      apply{2,#}(f_1,x) -> app#(f_1,x)
      app#(uncurry2(x12,x11),x13) -> uncurry{3,#}(x12,x11,x13)
      uncurry{3,#}(f_2,x,y) -> app#(f_2,x)
      app#(swap2(x12,x11),x13) -> swap{3,#}(x12,x11,x13)
      swap{3,#}(f_2,y,x) -> app#(f_2,x)
      app#(compose2(x12,x11),x13) -> compose{3,#}(x12,x11,x13)
      compose{3,#}(g_1,f_1,x) -> app#(f_1,x)
      app#(fold3(x12,x11,x10),x13) -> fold{4,#}(x12,x11,x10,x13)
      fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(f_3,app(g_2,z))
      app#(sum(),x13) -> sum{1,#}(x13)
      fold{4,#}(f_3,g_2,x,cons2(z,t)) -> app#(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
      compose{3,#}(g_1,f_1,x) -> app#(g_1,app(f_1,x))
      swap{3,#}(f_2,y,x) -> app#(app(f_2,x),y)
      uncurry{3,#}(f_2,x,y) -> app#(app(f_2,x),y)
     TRS:
      apply2(f_1,x) -> app(f_1,x)
      id1(x) -> x
      uncurry3(f_2,x,y) -> app(app(f_2,x),y)
      swap3(f_2,y,x) -> app(app(f_2,x),y)
      compose3(g_1,f_1,x) -> app(g_1,app(f_1,x))
      const2(x,y) -> x
      listify1(x) -> cons2(x,nil())
      fold4(f_3,g_2,x,nil()) -> x
      fold4(f_3,g_2,x,cons2(z,t)) -> app(app(f_3,app(g_2,z)),fold4(f_3,g_2,x,t))
      sum1(l) -> fold4(add(),id(),0(),l)
      uncurry3(fold2(cons(),id()),nil(),x14) -> id1(x14)
      uncurry2(fold2(cons(),id()),nil()) -> id()
      append() -> compose2(swap2(fold(),cons()),id())
      reverse() -> uncurry2(fold2(swap1(append()),listify()),nil())
      length() -> uncurry2(fold2(add(),cons1(1())),0())
      app(apply1(x12),x13) -> apply2(x12,x13)
      app(apply(),x13) -> apply1(x13)
      app(id(),x13) -> id1(x13)
      app(uncurry2(x12,x11),x13) -> uncurry3(x12,x11,x13)
      app(uncurry1(x12),x13) -> uncurry2(x12,x13)
      app(uncurry(),x13) -> uncurry1(x13)
      app(swap2(x12,x11),x13) -> swap3(x12,x11,x13)
      app(swap1(x12),x13) -> swap2(x12,x13)
      app(swap(),x13) -> swap1(x13)
      app(compose2(x12,x11),x13) -> compose3(x12,x11,x13)
      app(compose1(x12),x13) -> compose2(x12,x13)
      app(compose(),x13) -> compose1(x13)
      app(const1(x12),x13) -> const2(x12,x13)
      app(const(),x13) -> const1(x13)
      app(listify(),x13) -> listify1(x13)
      app(cons1(x12),x13) -> cons2(x12,x13)
      app(cons(),x13) -> cons1(x13)
      app(fold3(x12,x11,x10),x13) -> fold4(x12,x11,x10,x13)
      app(fold2(x12,x11),x13) -> fold3(x12,x11,x13)
      app(fold1(x12),x13) -> fold2(x12,x13)
      app(fold(),x13) -> fold1(x13)
      app(sum(),x13) -> sum1(x13)
     Open