MAYBE

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

Strict Trs:
  { bftMult'#2(tuple#2(@dequeue@1, @dequeue@2)) ->
    dequeue(@dequeue@1, @dequeue@2)
  , reverse(@xs) -> appendreverse(@xs, nil())
  , bftMult'#5(@queue', @acc, @y) ->
    bftMult'(@queue', matrixMult(@acc, @y))
  , appendreverse#1(nil(), @sofar) -> @sofar
  , appendreverse#1(::(@a, @as), @sofar) ->
    appendreverse(@as, ::(@a, @sofar))
  , computeLine#1(nil(), @acc, @m) -> @acc
  , computeLine#1(::(@x, @xs), @acc, @m) ->
    computeLine#2(@m, @acc, @x, @xs)
  , bftMult'#3(nil(), @acc, @queue) -> @acc
  , bftMult'#3(::(@t, @_@3), @acc, @queue) ->
    bftMult'#4(@t, @acc, @queue)
  , appendreverse(@toreverse, @sofar) ->
    appendreverse#1(@toreverse, @sofar)
  , matrixMult#1(nil(), @m2) -> nil()
  , matrixMult#1(::(@l, @ls), @m2) ->
    ::(computeLine(@l, @m2, nil()), matrixMult(@ls, @m2))
  , bftMult(@t, @acc) ->
    bftMult'(tuple#2(::(@t, nil()), nil()), @acc)
  , lineMult(@n, @l1, @l2) -> lineMult#1(@l1, @l2, @n)
  , lineMult#2(nil(), @n, @x, @xs) ->
    ::(*(@x, @n), lineMult(@n, @xs, nil()))
  , lineMult#2(::(@y, @ys), @n, @x, @xs) ->
    ::(+(*(@x, @n), @y), lineMult(@n, @xs, @ys))
  , dequeue(@outq, @inq) -> dequeue#1(@outq, @inq)
  , bftMult'#1(tuple#2(@elem, @queue), @acc) ->
    bftMult'#3(@elem, @acc, @queue)
  , bftMult'(@queue, @acc) -> bftMult'#1(bftMult'#2(@queue), @acc)
  , computeLine(@line, @m, @acc) -> computeLine#1(@line, @acc, @m)
  , bftMult'#4(leaf(), @acc, @queue) -> bftMult'(@queue, @acc)
  , bftMult'#4(node(@y, @t1, @t2), @acc, @queue) ->
    bftMult'#5(enqueue(@t2, enqueue(@t1, @queue)), @acc, @y)
  , dequeue#1(nil(), @inq) -> dequeue#2(reverse(@inq))
  , dequeue#1(::(@t, @ts), @inq) ->
    tuple#2(::(@t, nil()), tuple#2(@ts, @inq))
  , +(@x, @y) -> #add(@x, @y)
  , enqueue#1(tuple#2(@outq, @inq), @t) ->
    tuple#2(@outq, ::(@t, @inq))
  , matrixMult(@m1, @m2) -> matrixMult#1(@m1, @m2)
  , *(@x, @y) -> #mult(@x, @y)
  , enqueue(@t, @queue) -> enqueue#1(@queue, @t)
  , dequeue#2(nil()) -> tuple#2(nil(), tuple#2(nil(), nil()))
  , dequeue#2(::(@t, @ts)) ->
    tuple#2(::(@t, nil()), tuple#2(@ts, nil()))
  , lineMult#1(nil(), @l2, @n) -> nil()
  , lineMult#1(::(@x, @xs), @l2, @n) -> lineMult#2(@l2, @n, @x, @xs)
  , computeLine#2(nil(), @acc, @x, @xs) -> nil()
  , computeLine#2(::(@l, @ls), @acc, @x, @xs) ->
    computeLine(@xs, @ls, lineMult(@x, @l, @acc)) }
Weak Trs:
  { #natmult(#0(), @y) -> #0()
  , #natmult(#s(@x), @y) -> #add(#pos(@y), #natmult(@x, @y))
  , #add(#pos(#s(#0())), @y) -> #succ(@y)
  , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
  , #add(#0(), @y) -> @y
  , #add(#neg(#s(#0())), @y) -> #pred(@y)
  , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
  , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y))
  , #mult(#pos(@x), #0()) -> #0()
  , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#0(), #pos(@y)) -> #0()
  , #mult(#0(), #0()) -> #0()
  , #mult(#0(), #neg(@y)) -> #0()
  , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y))
  , #mult(#neg(@x), #0()) -> #0()
  , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y))
  , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
  , #succ(#0()) -> #pos(#s(#0()))
  , #succ(#neg(#s(#0()))) -> #0()
  , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x))
  , #pred(#pos(#s(#0()))) -> #0()
  , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
  , #pred(#0()) -> #neg(#s(#0()))
  , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 60 seconds)' failed due to the
      following reason:
      
      Computation stopped due to timeout after 60.0 seconds.
   
   2) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
         failed due to the following reason:
         
         Computation stopped due to timeout after 30.0 seconds.
      
      2) 'Best' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
         2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
      
      3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
         due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'Bounds with minimal-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
      
   


Arrrr..