MAYBE

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

Strict Trs:
  { empty(nil()) -> true()
  , empty(cons(x, y)) -> false()
  , tail(nil()) -> nil()
  , tail(cons(x, y)) -> y
  , head(cons(x, y)) -> x
  , zero(0()) -> true()
  , zero(s(x)) -> false()
  , p(0()) -> 0()
  , p(s(0())) -> 0()
  , p(s(s(x))) -> s(p(s(x)))
  , intlist(x) -> if_intlist(empty(x), x)
  , if_intlist(true(), x) -> nil()
  , if_intlist(false(), x) -> cons(s(head(x)), intlist(tail(x)))
  , int(x, y) -> if_int(zero(x), zero(y), x, y)
  , if_int(true(), b, x, y) -> if1(b, x, y)
  , if_int(false(), b, x, y) -> if2(b, x, y)
  , if1(true(), x, y) -> cons(0(), nil())
  , if1(false(), x, y) -> cons(0(), int(s(0()), y))
  , if2(true(), x, y) -> nil()
  , if2(false(), x, y) -> intlist(int(p(x), p(y))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { empty^#(nil()) -> c_1()
  , empty^#(cons(x, y)) -> c_2()
  , tail^#(nil()) -> c_3()
  , tail^#(cons(x, y)) -> c_4()
  , head^#(cons(x, y)) -> c_5()
  , zero^#(0()) -> c_6()
  , zero^#(s(x)) -> c_7()
  , p^#(0()) -> c_8()
  , p^#(s(0())) -> c_9()
  , p^#(s(s(x))) -> c_10(p^#(s(x)))
  , intlist^#(x) -> c_11(if_intlist^#(empty(x), x), empty^#(x))
  , if_intlist^#(true(), x) -> c_12()
  , if_intlist^#(false(), x) ->
    c_13(head^#(x), intlist^#(tail(x)), tail^#(x))
  , int^#(x, y) ->
    c_14(if_int^#(zero(x), zero(y), x, y), zero^#(x), zero^#(y))
  , if_int^#(true(), b, x, y) -> c_15(if1^#(b, x, y))
  , if_int^#(false(), b, x, y) -> c_16(if2^#(b, x, y))
  , if1^#(true(), x, y) -> c_17()
  , if1^#(false(), x, y) -> c_18(int^#(s(0()), y))
  , if2^#(true(), x, y) -> c_19()
  , if2^#(false(), x, y) ->
    c_20(intlist^#(int(p(x), p(y))),
         int^#(p(x), p(y)),
         p^#(x),
         p^#(y)) }

and mark the set of starting terms.

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

Strict DPs:
  { empty^#(nil()) -> c_1()
  , empty^#(cons(x, y)) -> c_2()
  , tail^#(nil()) -> c_3()
  , tail^#(cons(x, y)) -> c_4()
  , head^#(cons(x, y)) -> c_5()
  , zero^#(0()) -> c_6()
  , zero^#(s(x)) -> c_7()
  , p^#(0()) -> c_8()
  , p^#(s(0())) -> c_9()
  , p^#(s(s(x))) -> c_10(p^#(s(x)))
  , intlist^#(x) -> c_11(if_intlist^#(empty(x), x), empty^#(x))
  , if_intlist^#(true(), x) -> c_12()
  , if_intlist^#(false(), x) ->
    c_13(head^#(x), intlist^#(tail(x)), tail^#(x))
  , int^#(x, y) ->
    c_14(if_int^#(zero(x), zero(y), x, y), zero^#(x), zero^#(y))
  , if_int^#(true(), b, x, y) -> c_15(if1^#(b, x, y))
  , if_int^#(false(), b, x, y) -> c_16(if2^#(b, x, y))
  , if1^#(true(), x, y) -> c_17()
  , if1^#(false(), x, y) -> c_18(int^#(s(0()), y))
  , if2^#(true(), x, y) -> c_19()
  , if2^#(false(), x, y) ->
    c_20(intlist^#(int(p(x), p(y))),
         int^#(p(x), p(y)),
         p^#(x),
         p^#(y)) }
Weak Trs:
  { empty(nil()) -> true()
  , empty(cons(x, y)) -> false()
  , tail(nil()) -> nil()
  , tail(cons(x, y)) -> y
  , head(cons(x, y)) -> x
  , zero(0()) -> true()
  , zero(s(x)) -> false()
  , p(0()) -> 0()
  , p(s(0())) -> 0()
  , p(s(s(x))) -> s(p(s(x)))
  , intlist(x) -> if_intlist(empty(x), x)
  , if_intlist(true(), x) -> nil()
  , if_intlist(false(), x) -> cons(s(head(x)), intlist(tail(x)))
  , int(x, y) -> if_int(zero(x), zero(y), x, y)
  , if_int(true(), b, x, y) -> if1(b, x, y)
  , if_int(false(), b, x, y) -> if2(b, x, y)
  , if1(true(), x, y) -> cons(0(), nil())
  , if1(false(), x, y) -> cons(0(), int(s(0()), y))
  , if2(true(), x, y) -> nil()
  , if2(false(), x, y) -> intlist(int(p(x), p(y))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of
{1,2,3,4,5,6,7,8,9,12,17,19} by applications of
Pre({1,2,3,4,5,6,7,8,9,12,17,19}) = {10,11,13,14,15,16,20}. Here
rules are labeled as follows:

  DPs:
    { 1: empty^#(nil()) -> c_1()
    , 2: empty^#(cons(x, y)) -> c_2()
    , 3: tail^#(nil()) -> c_3()
    , 4: tail^#(cons(x, y)) -> c_4()
    , 5: head^#(cons(x, y)) -> c_5()
    , 6: zero^#(0()) -> c_6()
    , 7: zero^#(s(x)) -> c_7()
    , 8: p^#(0()) -> c_8()
    , 9: p^#(s(0())) -> c_9()
    , 10: p^#(s(s(x))) -> c_10(p^#(s(x)))
    , 11: intlist^#(x) -> c_11(if_intlist^#(empty(x), x), empty^#(x))
    , 12: if_intlist^#(true(), x) -> c_12()
    , 13: if_intlist^#(false(), x) ->
          c_13(head^#(x), intlist^#(tail(x)), tail^#(x))
    , 14: int^#(x, y) ->
          c_14(if_int^#(zero(x), zero(y), x, y), zero^#(x), zero^#(y))
    , 15: if_int^#(true(), b, x, y) -> c_15(if1^#(b, x, y))
    , 16: if_int^#(false(), b, x, y) -> c_16(if2^#(b, x, y))
    , 17: if1^#(true(), x, y) -> c_17()
    , 18: if1^#(false(), x, y) -> c_18(int^#(s(0()), y))
    , 19: if2^#(true(), x, y) -> c_19()
    , 20: if2^#(false(), x, y) ->
          c_20(intlist^#(int(p(x), p(y))),
               int^#(p(x), p(y)),
               p^#(x),
               p^#(y)) }

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

Strict DPs:
  { p^#(s(s(x))) -> c_10(p^#(s(x)))
  , intlist^#(x) -> c_11(if_intlist^#(empty(x), x), empty^#(x))
  , if_intlist^#(false(), x) ->
    c_13(head^#(x), intlist^#(tail(x)), tail^#(x))
  , int^#(x, y) ->
    c_14(if_int^#(zero(x), zero(y), x, y), zero^#(x), zero^#(y))
  , if_int^#(true(), b, x, y) -> c_15(if1^#(b, x, y))
  , if_int^#(false(), b, x, y) -> c_16(if2^#(b, x, y))
  , if1^#(false(), x, y) -> c_18(int^#(s(0()), y))
  , if2^#(false(), x, y) ->
    c_20(intlist^#(int(p(x), p(y))),
         int^#(p(x), p(y)),
         p^#(x),
         p^#(y)) }
Weak DPs:
  { empty^#(nil()) -> c_1()
  , empty^#(cons(x, y)) -> c_2()
  , tail^#(nil()) -> c_3()
  , tail^#(cons(x, y)) -> c_4()
  , head^#(cons(x, y)) -> c_5()
  , zero^#(0()) -> c_6()
  , zero^#(s(x)) -> c_7()
  , p^#(0()) -> c_8()
  , p^#(s(0())) -> c_9()
  , if_intlist^#(true(), x) -> c_12()
  , if1^#(true(), x, y) -> c_17()
  , if2^#(true(), x, y) -> c_19() }
Weak Trs:
  { empty(nil()) -> true()
  , empty(cons(x, y)) -> false()
  , tail(nil()) -> nil()
  , tail(cons(x, y)) -> y
  , head(cons(x, y)) -> x
  , zero(0()) -> true()
  , zero(s(x)) -> false()
  , p(0()) -> 0()
  , p(s(0())) -> 0()
  , p(s(s(x))) -> s(p(s(x)))
  , intlist(x) -> if_intlist(empty(x), x)
  , if_intlist(true(), x) -> nil()
  , if_intlist(false(), x) -> cons(s(head(x)), intlist(tail(x)))
  , int(x, y) -> if_int(zero(x), zero(y), x, y)
  , if_int(true(), b, x, y) -> if1(b, x, y)
  , if_int(false(), b, x, y) -> if2(b, x, y)
  , if1(true(), x, y) -> cons(0(), nil())
  , if1(false(), x, y) -> cons(0(), int(s(0()), y))
  , if2(true(), x, y) -> nil()
  , if2(false(), x, y) -> intlist(int(p(x), p(y))) }
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.

{ empty^#(nil()) -> c_1()
, empty^#(cons(x, y)) -> c_2()
, tail^#(nil()) -> c_3()
, tail^#(cons(x, y)) -> c_4()
, head^#(cons(x, y)) -> c_5()
, zero^#(0()) -> c_6()
, zero^#(s(x)) -> c_7()
, p^#(0()) -> c_8()
, p^#(s(0())) -> c_9()
, if_intlist^#(true(), x) -> c_12()
, if1^#(true(), x, y) -> c_17()
, if2^#(true(), x, y) -> c_19() }

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

Strict DPs:
  { p^#(s(s(x))) -> c_10(p^#(s(x)))
  , intlist^#(x) -> c_11(if_intlist^#(empty(x), x), empty^#(x))
  , if_intlist^#(false(), x) ->
    c_13(head^#(x), intlist^#(tail(x)), tail^#(x))
  , int^#(x, y) ->
    c_14(if_int^#(zero(x), zero(y), x, y), zero^#(x), zero^#(y))
  , if_int^#(true(), b, x, y) -> c_15(if1^#(b, x, y))
  , if_int^#(false(), b, x, y) -> c_16(if2^#(b, x, y))
  , if1^#(false(), x, y) -> c_18(int^#(s(0()), y))
  , if2^#(false(), x, y) ->
    c_20(intlist^#(int(p(x), p(y))),
         int^#(p(x), p(y)),
         p^#(x),
         p^#(y)) }
Weak Trs:
  { empty(nil()) -> true()
  , empty(cons(x, y)) -> false()
  , tail(nil()) -> nil()
  , tail(cons(x, y)) -> y
  , head(cons(x, y)) -> x
  , zero(0()) -> true()
  , zero(s(x)) -> false()
  , p(0()) -> 0()
  , p(s(0())) -> 0()
  , p(s(s(x))) -> s(p(s(x)))
  , intlist(x) -> if_intlist(empty(x), x)
  , if_intlist(true(), x) -> nil()
  , if_intlist(false(), x) -> cons(s(head(x)), intlist(tail(x)))
  , int(x, y) -> if_int(zero(x), zero(y), x, y)
  , if_int(true(), b, x, y) -> if1(b, x, y)
  , if_int(false(), b, x, y) -> if2(b, x, y)
  , if1(true(), x, y) -> cons(0(), nil())
  , if1(false(), x, y) -> cons(0(), int(s(0()), y))
  , if2(true(), x, y) -> nil()
  , if2(false(), x, y) -> intlist(int(p(x), p(y))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { intlist^#(x) -> c_11(if_intlist^#(empty(x), x), empty^#(x))
  , if_intlist^#(false(), x) ->
    c_13(head^#(x), intlist^#(tail(x)), tail^#(x))
  , int^#(x, y) ->
    c_14(if_int^#(zero(x), zero(y), x, y), zero^#(x), zero^#(y)) }

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

Strict DPs:
  { p^#(s(s(x))) -> c_1(p^#(s(x)))
  , intlist^#(x) -> c_2(if_intlist^#(empty(x), x))
  , if_intlist^#(false(), x) -> c_3(intlist^#(tail(x)))
  , int^#(x, y) -> c_4(if_int^#(zero(x), zero(y), x, y))
  , if_int^#(true(), b, x, y) -> c_5(if1^#(b, x, y))
  , if_int^#(false(), b, x, y) -> c_6(if2^#(b, x, y))
  , if1^#(false(), x, y) -> c_7(int^#(s(0()), y))
  , if2^#(false(), x, y) ->
    c_8(intlist^#(int(p(x), p(y))),
        int^#(p(x), p(y)),
        p^#(x),
        p^#(y)) }
Weak Trs:
  { empty(nil()) -> true()
  , empty(cons(x, y)) -> false()
  , tail(nil()) -> nil()
  , tail(cons(x, y)) -> y
  , head(cons(x, y)) -> x
  , zero(0()) -> true()
  , zero(s(x)) -> false()
  , p(0()) -> 0()
  , p(s(0())) -> 0()
  , p(s(s(x))) -> s(p(s(x)))
  , intlist(x) -> if_intlist(empty(x), x)
  , if_intlist(true(), x) -> nil()
  , if_intlist(false(), x) -> cons(s(head(x)), intlist(tail(x)))
  , int(x, y) -> if_int(zero(x), zero(y), x, y)
  , if_int(true(), b, x, y) -> if1(b, x, y)
  , if_int(false(), b, x, y) -> if2(b, x, y)
  , if1(true(), x, y) -> cons(0(), nil())
  , if1(false(), x, y) -> cons(0(), int(s(0()), y))
  , if2(true(), x, y) -> nil()
  , if2(false(), x, y) -> intlist(int(p(x), p(y))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..