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))
  Usable Rule 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))
   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))
    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))
    Restore Modifier:
     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))
     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