MAYBE

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

Strict Trs:
  { a__f(X) -> a__if(mark(X), c(), f(true()))
  , a__f(X) -> f(X)
  , a__if(X1, X2, X3) -> if(X1, X2, X3)
  , a__if(true(), X, Y) -> mark(X)
  , a__if(false(), X, Y) -> mark(Y)
  , mark(c()) -> c()
  , mark(f(X)) -> a__f(mark(X))
  , mark(true()) -> true()
  , mark(false()) -> false()
  , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { a__f^#(X) -> c_1(a__if^#(mark(X), c(), f(true())), mark^#(X))
  , a__f^#(X) -> c_2()
  , a__if^#(X1, X2, X3) -> c_3()
  , a__if^#(true(), X, Y) -> c_4(mark^#(X))
  , a__if^#(false(), X, Y) -> c_5(mark^#(Y))
  , mark^#(c()) -> c_6()
  , mark^#(f(X)) -> c_7(a__f^#(mark(X)), mark^#(X))
  , mark^#(true()) -> c_8()
  , mark^#(false()) -> c_9()
  , mark^#(if(X1, X2, X3)) ->
    c_10(a__if^#(mark(X1), mark(X2), X3), mark^#(X1), mark^#(X2)) }

and mark the set of starting terms.

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

Strict DPs:
  { a__f^#(X) -> c_1(a__if^#(mark(X), c(), f(true())), mark^#(X))
  , a__f^#(X) -> c_2()
  , a__if^#(X1, X2, X3) -> c_3()
  , a__if^#(true(), X, Y) -> c_4(mark^#(X))
  , a__if^#(false(), X, Y) -> c_5(mark^#(Y))
  , mark^#(c()) -> c_6()
  , mark^#(f(X)) -> c_7(a__f^#(mark(X)), mark^#(X))
  , mark^#(true()) -> c_8()
  , mark^#(false()) -> c_9()
  , mark^#(if(X1, X2, X3)) ->
    c_10(a__if^#(mark(X1), mark(X2), X3), mark^#(X1), mark^#(X2)) }
Weak Trs:
  { a__f(X) -> a__if(mark(X), c(), f(true()))
  , a__f(X) -> f(X)
  , a__if(X1, X2, X3) -> if(X1, X2, X3)
  , a__if(true(), X, Y) -> mark(X)
  , a__if(false(), X, Y) -> mark(Y)
  , mark(c()) -> c()
  , mark(f(X)) -> a__f(mark(X))
  , mark(true()) -> true()
  , mark(false()) -> false()
  , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: a__f^#(X) -> c_1(a__if^#(mark(X), c(), f(true())), mark^#(X))
    , 2: a__f^#(X) -> c_2()
    , 3: a__if^#(X1, X2, X3) -> c_3()
    , 4: a__if^#(true(), X, Y) -> c_4(mark^#(X))
    , 5: a__if^#(false(), X, Y) -> c_5(mark^#(Y))
    , 6: mark^#(c()) -> c_6()
    , 7: mark^#(f(X)) -> c_7(a__f^#(mark(X)), mark^#(X))
    , 8: mark^#(true()) -> c_8()
    , 9: mark^#(false()) -> c_9()
    , 10: mark^#(if(X1, X2, X3)) ->
          c_10(a__if^#(mark(X1), mark(X2), X3), mark^#(X1), mark^#(X2)) }

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

Strict DPs:
  { a__f^#(X) -> c_1(a__if^#(mark(X), c(), f(true())), mark^#(X))
  , a__if^#(true(), X, Y) -> c_4(mark^#(X))
  , a__if^#(false(), X, Y) -> c_5(mark^#(Y))
  , mark^#(f(X)) -> c_7(a__f^#(mark(X)), mark^#(X))
  , mark^#(if(X1, X2, X3)) ->
    c_10(a__if^#(mark(X1), mark(X2), X3), mark^#(X1), mark^#(X2)) }
Weak DPs:
  { a__f^#(X) -> c_2()
  , a__if^#(X1, X2, X3) -> c_3()
  , mark^#(c()) -> c_6()
  , mark^#(true()) -> c_8()
  , mark^#(false()) -> c_9() }
Weak Trs:
  { a__f(X) -> a__if(mark(X), c(), f(true()))
  , a__f(X) -> f(X)
  , a__if(X1, X2, X3) -> if(X1, X2, X3)
  , a__if(true(), X, Y) -> mark(X)
  , a__if(false(), X, Y) -> mark(Y)
  , mark(c()) -> c()
  , mark(f(X)) -> a__f(mark(X))
  , mark(true()) -> true()
  , mark(false()) -> false()
  , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) }
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.

{ a__f^#(X) -> c_2()
, a__if^#(X1, X2, X3) -> c_3()
, mark^#(c()) -> c_6()
, mark^#(true()) -> c_8()
, mark^#(false()) -> c_9() }

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

Strict DPs:
  { a__f^#(X) -> c_1(a__if^#(mark(X), c(), f(true())), mark^#(X))
  , a__if^#(true(), X, Y) -> c_4(mark^#(X))
  , a__if^#(false(), X, Y) -> c_5(mark^#(Y))
  , mark^#(f(X)) -> c_7(a__f^#(mark(X)), mark^#(X))
  , mark^#(if(X1, X2, X3)) ->
    c_10(a__if^#(mark(X1), mark(X2), X3), mark^#(X1), mark^#(X2)) }
Weak Trs:
  { a__f(X) -> a__if(mark(X), c(), f(true()))
  , a__f(X) -> f(X)
  , a__if(X1, X2, X3) -> if(X1, X2, X3)
  , a__if(true(), X, Y) -> mark(X)
  , a__if(false(), X, Y) -> mark(Y)
  , mark(c()) -> c()
  , mark(f(X)) -> a__f(mark(X))
  , mark(true()) -> true()
  , mark(false()) -> false()
  , mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..