MAYBE

Problem:
 concat(leaf(),Y) -> Y
 concat(cons(U,V),Y) -> cons(U,concat(V,Y))
 lessleaves(X,leaf()) -> false()
 lessleaves(leaf(),cons(W,Z)) -> true()
 lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))

Proof:
 DP Processor:
  DPs:
   concat#(cons(U,V),Y) -> concat#(V,Y)
   lessleaves#(cons(U,V),cons(W,Z)) -> concat#(W,Z)
   lessleaves#(cons(U,V),cons(W,Z)) -> concat#(U,V)
   lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z))
  TRS:
   concat(leaf(),Y) -> Y
   concat(cons(U,V),Y) -> cons(U,concat(V,Y))
   lessleaves(X,leaf()) -> false()
   lessleaves(leaf(),cons(W,Z)) -> true()
   lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
  TDG Processor:
   DPs:
    concat#(cons(U,V),Y) -> concat#(V,Y)
    lessleaves#(cons(U,V),cons(W,Z)) -> concat#(W,Z)
    lessleaves#(cons(U,V),cons(W,Z)) -> concat#(U,V)
    lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z))
   TRS:
    concat(leaf(),Y) -> Y
    concat(cons(U,V),Y) -> cons(U,concat(V,Y))
    lessleaves(X,leaf()) -> false()
    lessleaves(leaf(),cons(W,Z)) -> true()
    lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
   graph:
    lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z)) ->
    lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z))
    lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z)) ->
    lessleaves#(cons(U,V),cons(W,Z)) -> concat#(U,V)
    lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z)) ->
    lessleaves#(cons(U,V),cons(W,Z)) -> concat#(W,Z)
    lessleaves#(cons(U,V),cons(W,Z)) -> concat#(W,Z) ->
    concat#(cons(U,V),Y) -> concat#(V,Y)
    lessleaves#(cons(U,V),cons(W,Z)) -> concat#(U,V) ->
    concat#(cons(U,V),Y) -> concat#(V,Y)
    concat#(cons(U,V),Y) -> concat#(V,Y) -> concat#(cons(U,V),Y) -> concat#(V,Y)
   CDG Processor:
    DPs:
     concat#(cons(U,V),Y) -> concat#(V,Y)
     lessleaves#(cons(U,V),cons(W,Z)) -> concat#(W,Z)
     lessleaves#(cons(U,V),cons(W,Z)) -> concat#(U,V)
     lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z))
    TRS:
     concat(leaf(),Y) -> Y
     concat(cons(U,V),Y) -> cons(U,concat(V,Y))
     lessleaves(X,leaf()) -> false()
     lessleaves(leaf(),cons(W,Z)) -> true()
     lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
    graph:
     lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z)) ->
     lessleaves#(cons(U,V),cons(W,Z)) -> concat#(W,Z)
     lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z)) ->
     lessleaves#(cons(U,V),cons(W,Z)) -> concat#(U,V)
     lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z)) ->
     lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z))
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 3/16
     DPs:
      lessleaves#(cons(U,V),cons(W,Z)) -> lessleaves#(concat(U,V),concat(W,Z))
     TRS:
      concat(leaf(),Y) -> Y
      concat(cons(U,V),Y) -> cons(U,concat(V,Y))
      lessleaves(X,leaf()) -> false()
      lessleaves(leaf(),cons(W,Z)) -> true()
      lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z))
     Open