MAYBE

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

Strict Trs:
  { din(der(der(X))) -> u41(din(der(X)), X)
  , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
  , din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
  , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
  , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
  , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
  , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
  , u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
  , u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X), din^#(der(X)))
  , din^#(der(plus(X, Y))) ->
    c_2(u21^#(din(der(X)), X, Y), din^#(der(X)))
  , din^#(der(times(X, Y))) ->
    c_3(u31^#(din(der(X)), X, Y), din^#(der(X)))
  , u41^#(dout(DX), X) ->
    c_8(u42^#(din(der(DX)), X, DX), din^#(der(DX)))
  , u21^#(dout(DX), X, Y) ->
    c_4(u22^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u31^#(dout(DX), X, Y) ->
    c_6(u32^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u22^#(dout(DY), X, Y, DX) -> c_5()
  , u32^#(dout(DY), X, Y, DX) -> c_7()
  , u42^#(dout(DDX), X, DX) -> c_9() }

and mark the set of starting terms.

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

Strict DPs:
  { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X), din^#(der(X)))
  , din^#(der(plus(X, Y))) ->
    c_2(u21^#(din(der(X)), X, Y), din^#(der(X)))
  , din^#(der(times(X, Y))) ->
    c_3(u31^#(din(der(X)), X, Y), din^#(der(X)))
  , u41^#(dout(DX), X) ->
    c_8(u42^#(din(der(DX)), X, DX), din^#(der(DX)))
  , u21^#(dout(DX), X, Y) ->
    c_4(u22^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u31^#(dout(DX), X, Y) ->
    c_6(u32^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u22^#(dout(DY), X, Y, DX) -> c_5()
  , u32^#(dout(DY), X, Y, DX) -> c_7()
  , u42^#(dout(DDX), X, DX) -> c_9() }
Weak Trs:
  { din(der(der(X))) -> u41(din(der(X)), X)
  , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
  , din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
  , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
  , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
  , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
  , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
  , u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
  , u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: din^#(der(der(X))) ->
         c_1(u41^#(din(der(X)), X), din^#(der(X)))
    , 2: din^#(der(plus(X, Y))) ->
         c_2(u21^#(din(der(X)), X, Y), din^#(der(X)))
    , 3: din^#(der(times(X, Y))) ->
         c_3(u31^#(din(der(X)), X, Y), din^#(der(X)))
    , 4: u41^#(dout(DX), X) ->
         c_8(u42^#(din(der(DX)), X, DX), din^#(der(DX)))
    , 5: u21^#(dout(DX), X, Y) ->
         c_4(u22^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
    , 6: u31^#(dout(DX), X, Y) ->
         c_6(u32^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
    , 7: u22^#(dout(DY), X, Y, DX) -> c_5()
    , 8: u32^#(dout(DY), X, Y, DX) -> c_7()
    , 9: u42^#(dout(DDX), X, DX) -> c_9() }

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

Strict DPs:
  { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X), din^#(der(X)))
  , din^#(der(plus(X, Y))) ->
    c_2(u21^#(din(der(X)), X, Y), din^#(der(X)))
  , din^#(der(times(X, Y))) ->
    c_3(u31^#(din(der(X)), X, Y), din^#(der(X)))
  , u41^#(dout(DX), X) ->
    c_8(u42^#(din(der(DX)), X, DX), din^#(der(DX)))
  , u21^#(dout(DX), X, Y) ->
    c_4(u22^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u31^#(dout(DX), X, Y) ->
    c_6(u32^#(din(der(Y)), X, Y, DX), din^#(der(Y))) }
Weak DPs:
  { u22^#(dout(DY), X, Y, DX) -> c_5()
  , u32^#(dout(DY), X, Y, DX) -> c_7()
  , u42^#(dout(DDX), X, DX) -> c_9() }
Weak Trs:
  { din(der(der(X))) -> u41(din(der(X)), X)
  , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
  , din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
  , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
  , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
  , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
  , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
  , u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
  , u42(dout(DDX), X, DX) -> dout(DDX) }
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.

{ u22^#(dout(DY), X, Y, DX) -> c_5()
, u32^#(dout(DY), X, Y, DX) -> c_7()
, u42^#(dout(DDX), X, DX) -> c_9() }

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

Strict DPs:
  { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X), din^#(der(X)))
  , din^#(der(plus(X, Y))) ->
    c_2(u21^#(din(der(X)), X, Y), din^#(der(X)))
  , din^#(der(times(X, Y))) ->
    c_3(u31^#(din(der(X)), X, Y), din^#(der(X)))
  , u41^#(dout(DX), X) ->
    c_8(u42^#(din(der(DX)), X, DX), din^#(der(DX)))
  , u21^#(dout(DX), X, Y) ->
    c_4(u22^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u31^#(dout(DX), X, Y) ->
    c_6(u32^#(din(der(Y)), X, Y, DX), din^#(der(Y))) }
Weak Trs:
  { din(der(der(X))) -> u41(din(der(X)), X)
  , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
  , din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
  , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
  , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
  , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
  , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
  , u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
  , u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { u41^#(dout(DX), X) ->
    c_8(u42^#(din(der(DX)), X, DX), din^#(der(DX)))
  , u21^#(dout(DX), X, Y) ->
    c_4(u22^#(din(der(Y)), X, Y, DX), din^#(der(Y)))
  , u31^#(dout(DX), X, Y) ->
    c_6(u32^#(din(der(Y)), X, Y, DX), din^#(der(Y))) }

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

Strict DPs:
  { din^#(der(der(X))) -> c_1(u41^#(din(der(X)), X), din^#(der(X)))
  , din^#(der(plus(X, Y))) ->
    c_2(u21^#(din(der(X)), X, Y), din^#(der(X)))
  , din^#(der(times(X, Y))) ->
    c_3(u31^#(din(der(X)), X, Y), din^#(der(X)))
  , u41^#(dout(DX), X) -> c_4(din^#(der(DX)))
  , u21^#(dout(DX), X, Y) -> c_5(din^#(der(Y)))
  , u31^#(dout(DX), X, Y) -> c_6(din^#(der(Y))) }
Weak Trs:
  { din(der(der(X))) -> u41(din(der(X)), X)
  , din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
  , din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
  , u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
  , u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
  , u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
  , u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
  , u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
  , u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..