MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            concat(cons(u,v),y) -> cons(u,concat(v,y))
            concat(leaf(),y) -> y
            if1(b,false(),u,v) -> if2(b,u,v)
            if1(b,true(),u,v) -> false()
            if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
            if2(true(),u,v) -> true()
            isLeaf(cons(u,v)) -> false()
            isLeaf(leaf()) -> true()
            left(cons(u,v)) -> u
            less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
            right(cons(u,v)) -> v
        - Signature:
            {concat/2,if1/4,if2/3,isLeaf/1,left/1,less_leaves/2,right/1} / {cons/2,false/0,leaf/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {concat,if1,if2,isLeaf,left,less_leaves
            ,right} and constructors {cons,false,leaf,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          concat#(cons(u,v),y) -> c_1(concat#(v,y))
          concat#(leaf(),y) -> c_2()
          if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
          if1#(b,true(),u,v) -> c_4()
          if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                  ,concat#(left(u),right(u))
                                  ,left#(u)
                                  ,right#(u)
                                  ,concat#(left(v),right(v))
                                  ,left#(v)
                                  ,right#(v))
          if2#(true(),u,v) -> c_6()
          isLeaf#(cons(u,v)) -> c_7()
          isLeaf#(leaf()) -> c_8()
          left#(cons(u,v)) -> c_9()
          less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
          right#(cons(u,v)) -> c_11()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            concat#(cons(u,v),y) -> c_1(concat#(v,y))
            concat#(leaf(),y) -> c_2()
            if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
            if1#(b,true(),u,v) -> c_4()
            if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                    ,concat#(left(u),right(u))
                                    ,left#(u)
                                    ,right#(u)
                                    ,concat#(left(v),right(v))
                                    ,left#(v)
                                    ,right#(v))
            if2#(true(),u,v) -> c_6()
            isLeaf#(cons(u,v)) -> c_7()
            isLeaf#(leaf()) -> c_8()
            left#(cons(u,v)) -> c_9()
            less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
            right#(cons(u,v)) -> c_11()
        - Weak TRS:
            concat(cons(u,v),y) -> cons(u,concat(v,y))
            concat(leaf(),y) -> y
            if1(b,false(),u,v) -> if2(b,u,v)
            if1(b,true(),u,v) -> false()
            if2(false(),u,v) -> less_leaves(concat(left(u),right(u)),concat(left(v),right(v)))
            if2(true(),u,v) -> true()
            isLeaf(cons(u,v)) -> false()
            isLeaf(leaf()) -> true()
            left(cons(u,v)) -> u
            less_leaves(u,v) -> if1(isLeaf(u),isLeaf(v),u,v)
            right(cons(u,v)) -> v
        - Signature:
            {concat/2,if1/4,if2/3,isLeaf/1,left/1,less_leaves/2,right/1,concat#/2,if1#/4,if2#/3,isLeaf#/1,left#/1
            ,less_leaves#/2,right#/1} / {cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/7,c_6/0,c_7/0,c_8/0
            ,c_9/0,c_10/3,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {concat#,if1#,if2#,isLeaf#,left#,less_leaves#
            ,right#} and constructors {cons,false,leaf,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          concat(cons(u,v),y) -> cons(u,concat(v,y))
          concat(leaf(),y) -> y
          isLeaf(cons(u,v)) -> false()
          isLeaf(leaf()) -> true()
          left(cons(u,v)) -> u
          right(cons(u,v)) -> v
          concat#(cons(u,v),y) -> c_1(concat#(v,y))
          concat#(leaf(),y) -> c_2()
          if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
          if1#(b,true(),u,v) -> c_4()
          if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                  ,concat#(left(u),right(u))
                                  ,left#(u)
                                  ,right#(u)
                                  ,concat#(left(v),right(v))
                                  ,left#(v)
                                  ,right#(v))
          if2#(true(),u,v) -> c_6()
          isLeaf#(cons(u,v)) -> c_7()
          isLeaf#(leaf()) -> c_8()
          left#(cons(u,v)) -> c_9()
          less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
          right#(cons(u,v)) -> c_11()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            concat#(cons(u,v),y) -> c_1(concat#(v,y))
            concat#(leaf(),y) -> c_2()
            if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
            if1#(b,true(),u,v) -> c_4()
            if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                    ,concat#(left(u),right(u))
                                    ,left#(u)
                                    ,right#(u)
                                    ,concat#(left(v),right(v))
                                    ,left#(v)
                                    ,right#(v))
            if2#(true(),u,v) -> c_6()
            isLeaf#(cons(u,v)) -> c_7()
            isLeaf#(leaf()) -> c_8()
            left#(cons(u,v)) -> c_9()
            less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
            right#(cons(u,v)) -> c_11()
        - Weak TRS:
            concat(cons(u,v),y) -> cons(u,concat(v,y))
            concat(leaf(),y) -> y
            isLeaf(cons(u,v)) -> false()
            isLeaf(leaf()) -> true()
            left(cons(u,v)) -> u
            right(cons(u,v)) -> v
        - Signature:
            {concat/2,if1/4,if2/3,isLeaf/1,left/1,less_leaves/2,right/1,concat#/2,if1#/4,if2#/3,isLeaf#/1,left#/1
            ,less_leaves#/2,right#/1} / {cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/7,c_6/0,c_7/0,c_8/0
            ,c_9/0,c_10/3,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {concat#,if1#,if2#,isLeaf#,left#,less_leaves#
            ,right#} and constructors {cons,false,leaf,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,6,7,8,9,11}
        by application of
          Pre({2,4,6,7,8,9,11}) = {1,3,5,10}.
        Here rules are labelled as follows:
          1: concat#(cons(u,v),y) -> c_1(concat#(v,y))
          2: concat#(leaf(),y) -> c_2()
          3: if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
          4: if1#(b,true(),u,v) -> c_4()
          5: if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                     ,concat#(left(u),right(u))
                                     ,left#(u)
                                     ,right#(u)
                                     ,concat#(left(v),right(v))
                                     ,left#(v)
                                     ,right#(v))
          6: if2#(true(),u,v) -> c_6()
          7: isLeaf#(cons(u,v)) -> c_7()
          8: isLeaf#(leaf()) -> c_8()
          9: left#(cons(u,v)) -> c_9()
          10: less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
          11: right#(cons(u,v)) -> c_11()
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            concat#(cons(u,v),y) -> c_1(concat#(v,y))
            if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
            if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                    ,concat#(left(u),right(u))
                                    ,left#(u)
                                    ,right#(u)
                                    ,concat#(left(v),right(v))
                                    ,left#(v)
                                    ,right#(v))
            less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
        - Weak DPs:
            concat#(leaf(),y) -> c_2()
            if1#(b,true(),u,v) -> c_4()
            if2#(true(),u,v) -> c_6()
            isLeaf#(cons(u,v)) -> c_7()
            isLeaf#(leaf()) -> c_8()
            left#(cons(u,v)) -> c_9()
            right#(cons(u,v)) -> c_11()
        - Weak TRS:
            concat(cons(u,v),y) -> cons(u,concat(v,y))
            concat(leaf(),y) -> y
            isLeaf(cons(u,v)) -> false()
            isLeaf(leaf()) -> true()
            left(cons(u,v)) -> u
            right(cons(u,v)) -> v
        - Signature:
            {concat/2,if1/4,if2/3,isLeaf/1,left/1,less_leaves/2,right/1,concat#/2,if1#/4,if2#/3,isLeaf#/1,left#/1
            ,less_leaves#/2,right#/1} / {cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/7,c_6/0,c_7/0,c_8/0
            ,c_9/0,c_10/3,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {concat#,if1#,if2#,isLeaf#,left#,less_leaves#
            ,right#} and constructors {cons,false,leaf,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:concat#(cons(u,v),y) -> c_1(concat#(v,y))
             -->_1 concat#(leaf(),y) -> c_2():5
             -->_1 concat#(cons(u,v),y) -> c_1(concat#(v,y)):1
          
          2:S:if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
             -->_1 if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                           ,concat#(left(u),right(u))
                                           ,left#(u)
                                           ,right#(u)
                                           ,concat#(left(v),right(v))
                                           ,left#(v)
                                           ,right#(v)):3
             -->_1 if2#(true(),u,v) -> c_6():7
          
          3:S:if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                      ,concat#(left(u),right(u))
                                      ,left#(u)
                                      ,right#(u)
                                      ,concat#(left(v),right(v))
                                      ,left#(v)
                                      ,right#(v))
             -->_1 less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v)):4
             -->_7 right#(cons(u,v)) -> c_11():11
             -->_4 right#(cons(u,v)) -> c_11():11
             -->_6 left#(cons(u,v)) -> c_9():10
             -->_3 left#(cons(u,v)) -> c_9():10
             -->_5 concat#(leaf(),y) -> c_2():5
             -->_2 concat#(leaf(),y) -> c_2():5
             -->_5 concat#(cons(u,v),y) -> c_1(concat#(v,y)):1
             -->_2 concat#(cons(u,v),y) -> c_1(concat#(v,y)):1
          
          4:S:less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
             -->_3 isLeaf#(leaf()) -> c_8():9
             -->_2 isLeaf#(leaf()) -> c_8():9
             -->_3 isLeaf#(cons(u,v)) -> c_7():8
             -->_2 isLeaf#(cons(u,v)) -> c_7():8
             -->_1 if1#(b,true(),u,v) -> c_4():6
             -->_1 if1#(b,false(),u,v) -> c_3(if2#(b,u,v)):2
          
          5:W:concat#(leaf(),y) -> c_2()
             
          
          6:W:if1#(b,true(),u,v) -> c_4()
             
          
          7:W:if2#(true(),u,v) -> c_6()
             
          
          8:W:isLeaf#(cons(u,v)) -> c_7()
             
          
          9:W:isLeaf#(leaf()) -> c_8()
             
          
          10:W:left#(cons(u,v)) -> c_9()
             
          
          11:W:right#(cons(u,v)) -> c_11()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: if2#(true(),u,v) -> c_6()
          10: left#(cons(u,v)) -> c_9()
          11: right#(cons(u,v)) -> c_11()
          6: if1#(b,true(),u,v) -> c_4()
          8: isLeaf#(cons(u,v)) -> c_7()
          9: isLeaf#(leaf()) -> c_8()
          5: concat#(leaf(),y) -> c_2()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            concat#(cons(u,v),y) -> c_1(concat#(v,y))
            if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
            if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                    ,concat#(left(u),right(u))
                                    ,left#(u)
                                    ,right#(u)
                                    ,concat#(left(v),right(v))
                                    ,left#(v)
                                    ,right#(v))
            less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
        - Weak TRS:
            concat(cons(u,v),y) -> cons(u,concat(v,y))
            concat(leaf(),y) -> y
            isLeaf(cons(u,v)) -> false()
            isLeaf(leaf()) -> true()
            left(cons(u,v)) -> u
            right(cons(u,v)) -> v
        - Signature:
            {concat/2,if1/4,if2/3,isLeaf/1,left/1,less_leaves/2,right/1,concat#/2,if1#/4,if2#/3,isLeaf#/1,left#/1
            ,less_leaves#/2,right#/1} / {cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/7,c_6/0,c_7/0,c_8/0
            ,c_9/0,c_10/3,c_11/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {concat#,if1#,if2#,isLeaf#,left#,less_leaves#
            ,right#} and constructors {cons,false,leaf,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:concat#(cons(u,v),y) -> c_1(concat#(v,y))
             -->_1 concat#(cons(u,v),y) -> c_1(concat#(v,y)):1
          
          2:S:if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
             -->_1 if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                           ,concat#(left(u),right(u))
                                           ,left#(u)
                                           ,right#(u)
                                           ,concat#(left(v),right(v))
                                           ,left#(v)
                                           ,right#(v)):3
          
          3:S:if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                      ,concat#(left(u),right(u))
                                      ,left#(u)
                                      ,right#(u)
                                      ,concat#(left(v),right(v))
                                      ,left#(v)
                                      ,right#(v))
             -->_1 less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v)):4
             -->_5 concat#(cons(u,v),y) -> c_1(concat#(v,y)):1
             -->_2 concat#(cons(u,v),y) -> c_1(concat#(v,y)):1
          
          4:S:less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v),isLeaf#(u),isLeaf#(v))
             -->_1 if1#(b,false(),u,v) -> c_3(if2#(b,u,v)):2
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                  ,concat#(left(u),right(u))
                                  ,concat#(left(v),right(v)))
          less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v))
* Step 6: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          concat#(cons(u,v),y) -> c_1(concat#(v,y))
          if1#(b,false(),u,v) -> c_3(if2#(b,u,v))
          if2#(false(),u,v) -> c_5(less_leaves#(concat(left(u),right(u)),concat(left(v),right(v)))
                                  ,concat#(left(u),right(u))
                                  ,concat#(left(v),right(v)))
          less_leaves#(u,v) -> c_10(if1#(isLeaf(u),isLeaf(v),u,v))
      - Weak TRS:
          concat(cons(u,v),y) -> cons(u,concat(v,y))
          concat(leaf(),y) -> y
          isLeaf(cons(u,v)) -> false()
          isLeaf(leaf()) -> true()
          left(cons(u,v)) -> u
          right(cons(u,v)) -> v
      - Signature:
          {concat/2,if1/4,if2/3,isLeaf/1,left/1,less_leaves/2,right/1,concat#/2,if1#/4,if2#/3,isLeaf#/1,left#/1
          ,less_leaves#/2,right#/1} / {cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/3,c_6/0,c_7/0,c_8/0
          ,c_9/0,c_10/1,c_11/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {concat#,if1#,if2#,isLeaf#,left#,less_leaves#
          ,right#} and constructors {cons,false,leaf,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE