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