MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            app(add(n,x),y) -> add(n,app(x,y))
            app(nil(),y) -> y
            head(add(n,x)) -> n
            if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
            if(true(),x,y,z) -> y
            null(add(n,x)) -> false()
            null(nil()) -> true()
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
            reverse(nil()) -> nil()
            shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
            shuffle(x) -> shuff(x,nil())
            tail(add(n,x)) -> x
            tail(nil()) -> nil()
        - Signature:
            {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1} / {add/2,false/0,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {app,head,if,null,reverse,shuff,shuffle
            ,tail} and constructors {add,false,nil,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          app#(add(n,x),y) -> c_1(app#(x,y))
          app#(nil(),y) -> c_2()
          head#(add(n,x)) -> c_3()
          if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
          if#(true(),x,y,z) -> c_5()
          null#(add(n,x)) -> c_6()
          null#(nil()) -> c_7()
          reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
          reverse#(nil()) -> c_9()
          shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),null#(x),app#(y,add(head(x),nil())),head#(x))
          shuffle#(x) -> c_11(shuff#(x,nil()))
          tail#(add(n,x)) -> c_12()
          tail#(nil()) -> c_13()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(add(n,x),y) -> c_1(app#(x,y))
            app#(nil(),y) -> c_2()
            head#(add(n,x)) -> c_3()
            if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
            if#(true(),x,y,z) -> c_5()
            null#(add(n,x)) -> c_6()
            null#(nil()) -> c_7()
            reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
            reverse#(nil()) -> c_9()
            shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),null#(x),app#(y,add(head(x),nil())),head#(x))
            shuffle#(x) -> c_11(shuff#(x,nil()))
            tail#(add(n,x)) -> c_12()
            tail#(nil()) -> c_13()
        - Weak TRS:
            app(add(n,x),y) -> add(n,app(x,y))
            app(nil(),y) -> y
            head(add(n,x)) -> n
            if(false(),x,y,z) -> shuff(reverse(tail(x)),z)
            if(true(),x,y,z) -> y
            null(add(n,x)) -> false()
            null(nil()) -> true()
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
            reverse(nil()) -> nil()
            shuff(x,y) -> if(null(x),x,y,app(y,add(head(x),nil())))
            shuffle(x) -> shuff(x,nil())
            tail(add(n,x)) -> x
            tail(nil()) -> nil()
        - Signature:
            {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1,app#/2,head#/1,if#/4,null#/1,reverse#/1
            ,shuff#/2,shuffle#/1,tail#/1} / {add/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0,c_8/2
            ,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {app#,head#,if#,null#,reverse#,shuff#,shuffle#
            ,tail#} and constructors {add,false,nil,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          app(add(n,x),y) -> add(n,app(x,y))
          app(nil(),y) -> y
          head(add(n,x)) -> n
          null(add(n,x)) -> false()
          null(nil()) -> true()
          reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
          reverse(nil()) -> nil()
          tail(add(n,x)) -> x
          tail(nil()) -> nil()
          app#(add(n,x),y) -> c_1(app#(x,y))
          app#(nil(),y) -> c_2()
          head#(add(n,x)) -> c_3()
          if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
          if#(true(),x,y,z) -> c_5()
          null#(add(n,x)) -> c_6()
          null#(nil()) -> c_7()
          reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
          reverse#(nil()) -> c_9()
          shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),null#(x),app#(y,add(head(x),nil())),head#(x))
          shuffle#(x) -> c_11(shuff#(x,nil()))
          tail#(add(n,x)) -> c_12()
          tail#(nil()) -> c_13()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(add(n,x),y) -> c_1(app#(x,y))
            app#(nil(),y) -> c_2()
            head#(add(n,x)) -> c_3()
            if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
            if#(true(),x,y,z) -> c_5()
            null#(add(n,x)) -> c_6()
            null#(nil()) -> c_7()
            reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
            reverse#(nil()) -> c_9()
            shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),null#(x),app#(y,add(head(x),nil())),head#(x))
            shuffle#(x) -> c_11(shuff#(x,nil()))
            tail#(add(n,x)) -> c_12()
            tail#(nil()) -> c_13()
        - Weak TRS:
            app(add(n,x),y) -> add(n,app(x,y))
            app(nil(),y) -> y
            head(add(n,x)) -> n
            null(add(n,x)) -> false()
            null(nil()) -> true()
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
            reverse(nil()) -> nil()
            tail(add(n,x)) -> x
            tail(nil()) -> nil()
        - Signature:
            {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1,app#/2,head#/1,if#/4,null#/1,reverse#/1
            ,shuff#/2,shuffle#/1,tail#/1} / {add/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0,c_8/2
            ,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {app#,head#,if#,null#,reverse#,shuff#,shuffle#
            ,tail#} and constructors {add,false,nil,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,3,5,6,7,9,12,13}
        by application of
          Pre({2,3,5,6,7,9,12,13}) = {1,4,8,10}.
        Here rules are labelled as follows:
          1: app#(add(n,x),y) -> c_1(app#(x,y))
          2: app#(nil(),y) -> c_2()
          3: head#(add(n,x)) -> c_3()
          4: if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
          5: if#(true(),x,y,z) -> c_5()
          6: null#(add(n,x)) -> c_6()
          7: null#(nil()) -> c_7()
          8: reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
          9: reverse#(nil()) -> c_9()
          10: shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                 ,null#(x)
                                 ,app#(y,add(head(x),nil()))
                                 ,head#(x))
          11: shuffle#(x) -> c_11(shuff#(x,nil()))
          12: tail#(add(n,x)) -> c_12()
          13: tail#(nil()) -> c_13()
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(add(n,x),y) -> c_1(app#(x,y))
            if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
            reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
            shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),null#(x),app#(y,add(head(x),nil())),head#(x))
            shuffle#(x) -> c_11(shuff#(x,nil()))
        - Weak DPs:
            app#(nil(),y) -> c_2()
            head#(add(n,x)) -> c_3()
            if#(true(),x,y,z) -> c_5()
            null#(add(n,x)) -> c_6()
            null#(nil()) -> c_7()
            reverse#(nil()) -> c_9()
            tail#(add(n,x)) -> c_12()
            tail#(nil()) -> c_13()
        - Weak TRS:
            app(add(n,x),y) -> add(n,app(x,y))
            app(nil(),y) -> y
            head(add(n,x)) -> n
            null(add(n,x)) -> false()
            null(nil()) -> true()
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
            reverse(nil()) -> nil()
            tail(add(n,x)) -> x
            tail(nil()) -> nil()
        - Signature:
            {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1,app#/2,head#/1,if#/4,null#/1,reverse#/1
            ,shuff#/2,shuffle#/1,tail#/1} / {add/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0,c_8/2
            ,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {app#,head#,if#,null#,reverse#,shuff#,shuffle#
            ,tail#} and constructors {add,false,nil,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:app#(add(n,x),y) -> c_1(app#(x,y))
             -->_1 app#(nil(),y) -> c_2():6
             -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
          
          2:S:if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
             -->_1 shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                      ,null#(x)
                                      ,app#(y,add(head(x),nil()))
                                      ,head#(x)):4
             -->_2 reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x)):3
             -->_3 tail#(nil()) -> c_13():13
             -->_3 tail#(add(n,x)) -> c_12():12
             -->_2 reverse#(nil()) -> c_9():11
          
          3:S:reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
             -->_2 reverse#(nil()) -> c_9():11
             -->_1 app#(nil(),y) -> c_2():6
             -->_2 reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x)):3
             -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
          
          4:S:shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                 ,null#(x)
                                 ,app#(y,add(head(x),nil()))
                                 ,head#(x))
             -->_2 null#(nil()) -> c_7():10
             -->_2 null#(add(n,x)) -> c_6():9
             -->_1 if#(true(),x,y,z) -> c_5():8
             -->_4 head#(add(n,x)) -> c_3():7
             -->_3 app#(nil(),y) -> c_2():6
             -->_1 if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x)):2
             -->_3 app#(add(n,x),y) -> c_1(app#(x,y)):1
          
          5:S:shuffle#(x) -> c_11(shuff#(x,nil()))
             -->_1 shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                      ,null#(x)
                                      ,app#(y,add(head(x),nil()))
                                      ,head#(x)):4
          
          6:W:app#(nil(),y) -> c_2()
             
          
          7:W:head#(add(n,x)) -> c_3()
             
          
          8:W:if#(true(),x,y,z) -> c_5()
             
          
          9:W:null#(add(n,x)) -> c_6()
             
          
          10:W:null#(nil()) -> c_7()
             
          
          11:W:reverse#(nil()) -> c_9()
             
          
          12:W:tail#(add(n,x)) -> c_12()
             
          
          13:W:tail#(nil()) -> c_13()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          12: tail#(add(n,x)) -> c_12()
          13: tail#(nil()) -> c_13()
          11: reverse#(nil()) -> c_9()
          7: head#(add(n,x)) -> c_3()
          8: if#(true(),x,y,z) -> c_5()
          9: null#(add(n,x)) -> c_6()
          10: null#(nil()) -> c_7()
          6: app#(nil(),y) -> c_2()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(add(n,x),y) -> c_1(app#(x,y))
            if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
            reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
            shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),null#(x),app#(y,add(head(x),nil())),head#(x))
            shuffle#(x) -> c_11(shuff#(x,nil()))
        - Weak TRS:
            app(add(n,x),y) -> add(n,app(x,y))
            app(nil(),y) -> y
            head(add(n,x)) -> n
            null(add(n,x)) -> false()
            null(nil()) -> true()
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
            reverse(nil()) -> nil()
            tail(add(n,x)) -> x
            tail(nil()) -> nil()
        - Signature:
            {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1,app#/2,head#/1,if#/4,null#/1,reverse#/1
            ,shuff#/2,shuffle#/1,tail#/1} / {add/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/3,c_5/0,c_6/0,c_7/0,c_8/2
            ,c_9/0,c_10/4,c_11/1,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {app#,head#,if#,null#,reverse#,shuff#,shuffle#
            ,tail#} and constructors {add,false,nil,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:app#(add(n,x),y) -> c_1(app#(x,y))
             -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
          
          2:S:if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x))
             -->_1 shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                      ,null#(x)
                                      ,app#(y,add(head(x),nil()))
                                      ,head#(x)):4
             -->_2 reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x)):3
          
          3:S:reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
             -->_2 reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x)):3
             -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
          
          4:S:shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                 ,null#(x)
                                 ,app#(y,add(head(x),nil()))
                                 ,head#(x))
             -->_1 if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)),tail#(x)):2
             -->_3 app#(add(n,x),y) -> c_1(app#(x,y)):1
          
          5:S:shuffle#(x) -> c_11(shuff#(x,nil()))
             -->_1 shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil())))
                                      ,null#(x)
                                      ,app#(y,add(head(x),nil()))
                                      ,head#(x)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)))
          shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),app#(y,add(head(x),nil())))
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            app#(add(n,x),y) -> c_1(app#(x,y))
            if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)))
            reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
            shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),app#(y,add(head(x),nil())))
            shuffle#(x) -> c_11(shuff#(x,nil()))
        - Weak TRS:
            app(add(n,x),y) -> add(n,app(x,y))
            app(nil(),y) -> y
            head(add(n,x)) -> n
            null(add(n,x)) -> false()
            null(nil()) -> true()
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
            reverse(nil()) -> nil()
            tail(add(n,x)) -> x
            tail(nil()) -> nil()
        - Signature:
            {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1,app#/2,head#/1,if#/4,null#/1,reverse#/1
            ,shuff#/2,shuffle#/1,tail#/1} / {add/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/2
            ,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {app#,head#,if#,null#,reverse#,shuff#,shuffle#
            ,tail#} and constructors {add,false,nil,true}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:app#(add(n,x),y) -> c_1(app#(x,y))
           -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
        
        2:S:if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)))
           -->_1 shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),app#(y,add(head(x),nil()))):4
           -->_2 reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x)):3
        
        3:S:reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
           -->_2 reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x)):3
           -->_1 app#(add(n,x),y) -> c_1(app#(x,y)):1
        
        4:S:shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),app#(y,add(head(x),nil())))
           -->_1 if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x))):2
           -->_2 app#(add(n,x),y) -> c_1(app#(x,y)):1
        
        5:S:shuffle#(x) -> c_11(shuff#(x,nil()))
           -->_1 shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),app#(y,add(head(x),nil()))):4
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(5,shuffle#(x) -> c_11(shuff#(x,nil())))]
* Step 7: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          app#(add(n,x),y) -> c_1(app#(x,y))
          if#(false(),x,y,z) -> c_4(shuff#(reverse(tail(x)),z),reverse#(tail(x)))
          reverse#(add(n,x)) -> c_8(app#(reverse(x),add(n,nil())),reverse#(x))
          shuff#(x,y) -> c_10(if#(null(x),x,y,app(y,add(head(x),nil()))),app#(y,add(head(x),nil())))
      - Weak TRS:
          app(add(n,x),y) -> add(n,app(x,y))
          app(nil(),y) -> y
          head(add(n,x)) -> n
          null(add(n,x)) -> false()
          null(nil()) -> true()
          reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
          reverse(nil()) -> nil()
          tail(add(n,x)) -> x
          tail(nil()) -> nil()
      - Signature:
          {app/2,head/1,if/4,null/1,reverse/1,shuff/2,shuffle/1,tail/1,app#/2,head#/1,if#/4,null#/1,reverse#/1
          ,shuff#/2,shuffle#/1,tail#/1} / {add/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/0,c_6/0,c_7/0,c_8/2
          ,c_9/0,c_10/2,c_11/1,c_12/0,c_13/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {app#,head#,if#,null#,reverse#,shuff#,shuffle#
          ,tail#} and constructors {add,false,nil,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE