MAYBE

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

Strict Trs:
  { reach(u, v, edges) ->
    reach[Ite](member(E(u, v), edges), u, v, edges)
  , via(u, v, Nil(), edges) -> Nil()
  , via(u, v, Cons(E(x, y), xs), edges) ->
    via[Ite][False][Ite](!EQ(u, x), u, v, Cons(E(x, y), xs), edges)
  , member(x, Nil()) -> False()
  , member(x', Cons(x, xs)) ->
    member[Ite][False][Ite](eqEdge(x', x), x', Cons(x, xs))
  , getNodeFromEdge(S(S(x')), E(x, y)) -> y
  , getNodeFromEdge(S(0()), E(x, y)) -> x
  , getNodeFromEdge(0(), E(x, y)) -> x
  , notEmpty(Nil()) -> False()
  , notEmpty(Cons(x, xs)) -> True()
  , goal(u, v, edges) -> reach(u, v, edges)
  , eqEdge(E(e11, e12), E(e21, e22)) ->
    eqEdge[Match][E][Match][E][Ite](and(!EQ(e11, e21), !EQ(e12, e22)),
                                    e21,
                                    e22,
                                    e11,
                                    e12) }
Weak Trs:
  { via[Ite][False][Ite](True(), u, v, Cons(E(x, y), xs), edges) ->
    via[Ite][False][Ite][True][Let](u,
                                    v,
                                    Cons(E(x, y), xs),
                                    edges,
                                    reach(y, v, edges))
  , via[Ite][False][Ite](False(), u, v, Cons(x, xs), edges) ->
    via(u, v, xs, edges)
  , and(True(), True()) -> True()
  , and(True(), False()) -> False()
  , and(False(), True()) -> False()
  , and(False(), False()) -> False()
  , !EQ(S(x), S(y)) -> !EQ(x, y)
  , !EQ(S(x), 0()) -> False()
  , !EQ(0(), S(y)) -> False()
  , !EQ(0(), 0()) -> True()
  , member[Ite][False][Ite](True(), x, xs) -> True()
  , member[Ite][False][Ite](False(), x', Cons(x, xs)) ->
    member(x', xs)
  , reach[Ite](True(), u, v, edges) -> Cons(E(u, v), Nil())
  , reach[Ite](False(), u, v, edges) -> via(u, v, edges, edges) }
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..