MAYBE

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

Strict Trs:
  { breadth(@breadth@1, @breadth@2) ->
    breadth#1(dequeue(@breadth@1, @breadth@2))
  , breadth#1(tuple#2(@queue', @elem)) -> breadth#2(@elem, @queue')
  , dequeue(@dequeue@1, @dequeue@2) ->
    dequeue#1(tuple#2(@dequeue@1, @dequeue@2))
  , breadth#2(::(@z, @_@9), @queue') ->
    breadth#3(breadth#4(@z), @queue')
  , breadth#2(nil(), @queue') -> nil()
  , breadth#3(tuple#2(@x, @ys), @queue') ->
    ::(@x, breadth#5(enqueues(@ys, @queue')))
  , breadth#4(tuple#4(@children@3,
                      @children@4,
                      @children@5,
                      @children@6))
    -> children(@children@3, @children@4, @children@5, @children@6)
  , breadth#5(tuple#2(@breadth@7, @breadth@8)) ->
    breadth(@breadth@7, @breadth@8)
  , enqueues(@l, @queue) -> enqueues#1(@l, @queue)
  , children(@a, @b, @l1, @l2) ->
    tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2))
  , children#1(::(@x, @xs), @b, @l2) -> children#3(@l2, @b, @x, @xs)
  , children#1(nil(), @b, @l2) -> children#2(@l2, @b)
  , children#3(::(@y, @ys), @b, @x, @xs) ->
    ::(tuple#4(@x, @b, nil(), @xs),
       ::(tuple#4(@x, @y, @xs, @ys), nil()))
  , children#3(nil(), @b, @x, @xs) -> nil()
  , children#2(::(@y, @ys), @b) ->
    ::(tuple#4(@y, @b, nil(), @ys), nil())
  , children#2(nil(), @b) -> nil()
  , copyover(@copyover@1, @copyover@2) ->
    copyover#1(tuple#2(@copyover@1, @copyover@2))
  , copyover#1(tuple#2(@inq, @outq)) -> copyover#2(@inq, @outq)
  , copyover#2(::(@x, @xs), @outq) -> copyover(@xs, ::(@x, @outq))
  , copyover#2(nil(), @outq) -> tuple#2(nil(), @outq)
  , dequeue#1(tuple#2(@inq, @outq)) -> dequeue#2(@outq, @inq)
  , dequeue#2(::(@y, @ys), @inq) ->
    tuple#2(tuple#2(@inq, @ys), ::(@y, nil()))
  , dequeue#2(nil(), @inq) -> dequeue#3(@inq)
  , dequeue#3(::(@x, @xs)) -> dequeue#4(copyover(::(@x, @xs), nil()))
  , dequeue#3(nil()) -> tuple#2(tuple#2(nil(), nil()), nil())
  , dequeue#4(tuple#2(@dequeue@3, @dequeue@4)) ->
    dequeue(@dequeue@3, @dequeue@4)
  , empty(@x) -> tuple#2(nil(), nil())
  , enqueue(@x, @queue) -> enqueue#1(@queue, @x)
  , enqueue#1(tuple#2(@inq, @outq), @x) ->
    tuple#2(::(@x, @inq), @outq)
  , enqueues#1(::(@x, @xs), @queue) ->
    enqueues(@xs, enqueue(@x, @queue))
  , enqueues#1(nil(), @queue) -> @queue
  , startBreadth(@xs) -> startBreadth#1(@xs)
  , startBreadth#1(::(@x, @xs)) ->
    startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit())))
  , startBreadth#1(nil()) -> nil()
  , startBreadth#2(tuple#2(@breadth@1, @breadth@2)) ->
    breadth(@breadth@1, @breadth@2) }
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 perSymbol-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
         2) 'Bounds with minimal-enrichment and initial automaton 'match''
            failed due to the following reason:
            
            match-boundness of the problem could not be verified.
         
      
   


Arrrr..