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