MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict 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(plus(), dummy, x, y) ->
    function(if(), function(iszero(), x, x, x), x, y)
  , function(if(), true(), x, y) -> y
  , function(if(), false(), x, y) ->
    function(plus(),
             function(third(), x, y, y),
             function(p(), x, x, y),
             s(y))
  , function(third(), x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { function^#(iszero(), 0(), dummy, dummy2) -> c_1()
  , function^#(iszero(), s(x), dummy, dummy2) -> c_2()
  , function^#(p(), 0(), dummy, dummy2) -> c_3()
  , function^#(p(), s(0()), dummy, dummy2) -> c_4()
  , function^#(p(), s(s(x)), dummy, dummy2) ->
    c_5(function^#(p(), s(x), x, x))
  , function^#(plus(), dummy, x, y) ->
    c_6(function^#(if(), function(iszero(), x, x, x), x, y),
        function^#(iszero(), x, x, x))
  , function^#(if(), true(), x, y) -> c_7()
  , function^#(if(), false(), x, y) ->
    c_8(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^#(third(), x, y, z) -> c_9() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { function^#(iszero(), 0(), dummy, dummy2) -> c_1()
  , function^#(iszero(), s(x), dummy, dummy2) -> c_2()
  , function^#(p(), 0(), dummy, dummy2) -> c_3()
  , function^#(p(), s(0()), dummy, dummy2) -> c_4()
  , function^#(p(), s(s(x)), dummy, dummy2) ->
    c_5(function^#(p(), s(x), x, x))
  , function^#(plus(), dummy, x, y) ->
    c_6(function^#(if(), function(iszero(), x, x, x), x, y),
        function^#(iszero(), x, x, x))
  , function^#(if(), true(), x, y) -> c_7()
  , function^#(if(), false(), x, y) ->
    c_8(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^#(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(plus(), dummy, x, y) ->
    function(if(), function(iszero(), x, x, x), x, y)
  , function(if(), true(), x, y) -> y
  , function(if(), false(), x, y) ->
    function(plus(),
             function(third(), x, y, y),
             function(p(), x, x, y),
             s(y))
  , function(third(), x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,2,3,4,7,9} by
applications of Pre({1,2,3,4,7,9}) = {5,6,8}. Here rules are
labeled as follows:

  DPs:
    { 1: function^#(iszero(), 0(), dummy, dummy2) -> c_1()
    , 2: function^#(iszero(), s(x), dummy, dummy2) -> c_2()
    , 3: function^#(p(), 0(), dummy, dummy2) -> c_3()
    , 4: function^#(p(), s(0()), dummy, dummy2) -> c_4()
    , 5: function^#(p(), s(s(x)), dummy, dummy2) ->
         c_5(function^#(p(), s(x), x, x))
    , 6: function^#(plus(), dummy, x, y) ->
         c_6(function^#(if(), function(iszero(), x, x, x), x, y),
             function^#(iszero(), x, x, x))
    , 7: function^#(if(), true(), x, y) -> c_7()
    , 8: function^#(if(), false(), x, y) ->
         c_8(function^#(plus(),
                        function(third(), x, y, y),
                        function(p(), x, x, y),
                        s(y)),
             function^#(third(), x, y, y),
             function^#(p(), x, x, y))
    , 9: function^#(third(), x, y, z) -> c_9() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { function^#(p(), s(s(x)), dummy, dummy2) ->
    c_5(function^#(p(), s(x), x, x))
  , function^#(plus(), dummy, x, y) ->
    c_6(function^#(if(), function(iszero(), x, x, x), x, y),
        function^#(iszero(), x, x, x))
  , function^#(if(), false(), x, y) ->
    c_8(function^#(plus(),
                   function(third(), x, y, y),
                   function(p(), x, x, y),
                   s(y)),
        function^#(third(), x, y, y),
        function^#(p(), x, x, y)) }
Weak DPs:
  { function^#(iszero(), 0(), dummy, dummy2) -> c_1()
  , function^#(iszero(), s(x), dummy, dummy2) -> c_2()
  , function^#(p(), 0(), dummy, dummy2) -> c_3()
  , function^#(p(), s(0()), dummy, dummy2) -> c_4()
  , function^#(if(), true(), x, y) -> c_7()
  , 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(plus(), dummy, x, y) ->
    function(if(), function(iszero(), x, x, x), x, y)
  , function(if(), true(), x, y) -> y
  , function(if(), false(), x, y) ->
    function(plus(),
             function(third(), x, y, y),
             function(p(), x, x, y),
             s(y))
  , function(third(), x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ function^#(iszero(), 0(), dummy, dummy2) -> c_1()
, function^#(iszero(), s(x), dummy, dummy2) -> c_2()
, function^#(p(), 0(), dummy, dummy2) -> c_3()
, function^#(p(), s(0()), dummy, dummy2) -> c_4()
, function^#(if(), true(), x, y) -> c_7()
, function^#(third(), x, y, z) -> c_9() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { function^#(p(), s(s(x)), dummy, dummy2) ->
    c_5(function^#(p(), s(x), x, x))
  , function^#(plus(), dummy, x, y) ->
    c_6(function^#(if(), function(iszero(), x, x, x), x, y),
        function^#(iszero(), x, x, x))
  , function^#(if(), false(), x, y) ->
    c_8(function^#(plus(),
                   function(third(), x, y, y),
                   function(p(), x, x, y),
                   s(y)),
        function^#(third(), x, y, y),
        function^#(p(), 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(plus(), dummy, x, y) ->
    function(if(), function(iszero(), x, x, x), x, y)
  , function(if(), true(), x, y) -> y
  , function(if(), false(), x, y) ->
    function(plus(),
             function(third(), x, y, y),
             function(p(), x, x, y),
             s(y))
  , function(third(), x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { function^#(plus(), dummy, x, y) ->
    c_6(function^#(if(), function(iszero(), x, x, x), x, y),
        function^#(iszero(), x, x, x))
  , function^#(if(), false(), x, y) ->
    c_8(function^#(plus(),
                   function(third(), x, y, y),
                   function(p(), x, x, y),
                   s(y)),
        function^#(third(), x, y, y),
        function^#(p(), x, x, y)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { function^#(p(), s(s(x)), dummy, dummy2) ->
    c_1(function^#(p(), s(x), x, x))
  , function^#(plus(), dummy, x, y) ->
    c_2(function^#(if(), function(iszero(), x, x, x), x, y))
  , function^#(if(), false(), x, y) ->
    c_3(function^#(plus(),
                   function(third(), x, y, y),
                   function(p(), x, x, y),
                   s(y)),
        function^#(p(), 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(plus(), dummy, x, y) ->
    function(if(), function(iszero(), x, x, x), x, y)
  , function(if(), true(), x, y) -> y
  , function(if(), false(), x, y) ->
    function(plus(),
             function(third(), x, y, y),
             function(p(), x, x, y),
             s(y))
  , function(third(), x, y, z) -> z }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..