MAYBE

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

Strict Trs:
  { #equal(@x, @y) -> #eq(@x, @y)
  , bfs#4(#true(), @futurequeue, @t1, @t2, @ts, @x, @y) ->
    node(@y, @t1, @t2)
  , bfs#4(#false(), @futurequeue, @t1, @t2, @ts, @x, @y) ->
    bfs(@ts, ::(@t2, ::(@t1, @futurequeue)), @x)
  , reverse(@xs) -> appendreverse(@xs, nil())
  , appendreverse#1(nil(), @sofar) -> @sofar
  , appendreverse#1(::(@a, @as), @sofar) ->
    appendreverse(@as, ::(@a, @sofar))
  , appendreverse(@toreverse, @sofar) ->
    appendreverse#1(@toreverse, @sofar)
  , dfs#1(nil(), @x) -> leaf()
  , dfs#1(::(@t, @ts), @x) -> dfs#2(@t, @t, @ts, @x)
  , dobfs(@t, @x) -> bfs(::(@t, nil()), nil(), @x)
  , dodfs(@t, @x) -> dfs(::(@t, nil()), @x)
  , bfs2#1(@t', @x) -> dobfs(@t', @x)
  , bfs2(@t, @x) -> bfs2#1(dobfs(@t, @x), @x)
  , bfs(@queue, @futurequeue, @x) -> bfs#1(@queue, @futurequeue, @x)
  , bfs#2(nil(), @x) -> leaf()
  , bfs#2(::(@t, @ts), @x) -> bfs(reverse(::(@t, @ts)), nil(), @x)
  , bfs#1(nil(), @futurequeue, @x) -> bfs#2(@futurequeue, @x)
  , bfs#1(::(@t, @ts), @futurequeue, @x) ->
    bfs#3(@t, @futurequeue, @ts, @x)
  , dfs#2(leaf(), @t, @ts, @x) -> dfs(@ts, @x)
  , dfs#2(node(@a, @t1, @t2), @t, @ts, @x) ->
    dfs#3(#equal(@a, @x), @t, @t1, @t2, @ts, @x)
  , bfs#3(leaf(), @futurequeue, @ts, @x) ->
    bfs(@ts, @futurequeue, @x)
  , bfs#3(node(@y, @t1, @t2), @futurequeue, @ts, @x) ->
    bfs#4(#equal(@x, @y), @futurequeue, @t1, @t2, @ts, @x, @y)
  , dfs(@queue, @x) -> dfs#1(@queue, @x)
  , dfs#3(#true(), @t, @t1, @t2, @ts, @x) -> @t
  , dfs#3(#false(), @t, @t1, @t2, @ts, @x) ->
    dfs(::(@t1, ::(@t2, @ts)), @x) }
Weak Trs:
  { #eq(leaf(), leaf()) -> #true()
  , #eq(leaf(), node(@y_1, @y_2, @y_3)) -> #false()
  , #eq(leaf(), nil()) -> #false()
  , #eq(leaf(), ::(@y_1, @y_2)) -> #false()
  , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y)
  , #eq(#pos(@x), #0()) -> #false()
  , #eq(#pos(@x), #neg(@y)) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), leaf()) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), node(@y_1, @y_2, @y_3)) ->
    #and(#eq(@x_1, @y_1), #and(#eq(@x_2, @y_2), #eq(@x_3, @y_3)))
  , #eq(node(@x_1, @x_2, @x_3), nil()) -> #false()
  , #eq(node(@x_1, @x_2, @x_3), ::(@y_1, @y_2)) -> #false()
  , #eq(nil(), leaf()) -> #false()
  , #eq(nil(), node(@y_1, @y_2, @y_3)) -> #false()
  , #eq(nil(), nil()) -> #true()
  , #eq(nil(), ::(@y_1, @y_2)) -> #false()
  , #eq(::(@x_1, @x_2), leaf()) -> #false()
  , #eq(::(@x_1, @x_2), node(@y_1, @y_2, @y_3)) -> #false()
  , #eq(::(@x_1, @x_2), nil()) -> #false()
  , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) ->
    #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
  , #eq(#0(), #pos(@y)) -> #false()
  , #eq(#0(), #0()) -> #true()
  , #eq(#0(), #neg(@y)) -> #false()
  , #eq(#0(), #s(@y)) -> #false()
  , #eq(#neg(@x), #pos(@y)) -> #false()
  , #eq(#neg(@x), #0()) -> #false()
  , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y)
  , #eq(#s(@x), #0()) -> #false()
  , #eq(#s(@x), #s(@y)) -> #eq(@x, @y)
  , #and(#true(), #true()) -> #true()
  , #and(#true(), #false()) -> #false()
  , #and(#false(), #true()) -> #false()
  , #and(#false(), #false()) -> #false() }
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) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
         2) 'bsearch-popstar (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..