MAYBE
905.13/297.02	MAYBE
905.13/297.02	
905.13/297.02	We are left with following problem, upon which TcT provides the
905.13/297.02	certificate MAYBE.
905.13/297.02	
905.13/297.02	Strict Trs:
905.13/297.02	  { eq(0(), 0()) -> true()
905.13/297.02	  , eq(0(), s(x)) -> false()
905.13/297.02	  , eq(s(x), 0()) -> false()
905.13/297.02	  , eq(s(x), s(y)) -> eq(x, y)
905.13/297.02	  , or(true(), y) -> true()
905.13/297.02	  , or(false(), y) -> y
905.13/297.02	  , union(empty(), h) -> h
905.13/297.02	  , union(edge(x, y, i), h) -> edge(x, y, union(i, h))
905.13/297.02	  , reach(x, y, empty(), h) -> false()
905.13/297.02	  , reach(x, y, edge(u, v, i), h) ->
905.13/297.02	    if_reach_1(eq(x, u), x, y, edge(u, v, i), h)
905.13/297.02	  , if_reach_1(true(), x, y, edge(u, v, i), h) ->
905.13/297.02	    if_reach_2(eq(y, v), x, y, edge(u, v, i), h)
905.13/297.02	  , if_reach_1(false(), x, y, edge(u, v, i), h) ->
905.13/297.02	    reach(x, y, i, edge(u, v, h))
905.13/297.02	  , if_reach_2(true(), x, y, edge(u, v, i), h) -> true()
905.13/297.02	  , if_reach_2(false(), x, y, edge(u, v, i), h) ->
905.13/297.02	    or(reach(x, y, i, h), reach(v, y, union(i, h), empty())) }
905.13/297.02	Obligation:
905.13/297.02	  innermost runtime complexity
905.13/297.02	Answer:
905.13/297.02	  MAYBE
905.13/297.02	
905.13/297.02	None of the processors succeeded.
905.13/297.02	
905.13/297.02	Details of failed attempt(s):
905.13/297.02	-----------------------------
905.13/297.02	1) 'empty' failed due to the following reason:
905.13/297.02	   
905.13/297.02	   Empty strict component of the problem is NOT empty.
905.13/297.02	
905.13/297.02	2) 'Best' failed due to the following reason:
905.13/297.02	   
905.13/297.02	   None of the processors succeeded.
905.13/297.02	   
905.13/297.02	   Details of failed attempt(s):
905.13/297.02	   -----------------------------
905.13/297.02	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
905.13/297.02	      following reason:
905.13/297.02	      
905.13/297.02	      Computation stopped due to timeout after 297.0 seconds.
905.13/297.02	   
905.13/297.02	   2) 'Best' failed due to the following reason:
905.13/297.02	      
905.13/297.02	      None of the processors succeeded.
905.13/297.02	      
905.13/297.02	      Details of failed attempt(s):
905.13/297.02	      -----------------------------
905.13/297.02	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
905.13/297.02	         seconds)' failed due to the following reason:
905.13/297.02	         
905.13/297.02	         Computation stopped due to timeout after 148.0 seconds.
905.13/297.02	      
905.13/297.02	      2) 'Best' failed due to the following reason:
905.13/297.02	         
905.13/297.02	         None of the processors succeeded.
905.13/297.02	         
905.13/297.02	         Details of failed attempt(s):
905.13/297.02	         -----------------------------
905.13/297.02	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
905.13/297.02	            following reason:
905.13/297.02	            
905.13/297.02	            The input cannot be shown compatible
905.13/297.02	         
905.13/297.02	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
905.13/297.02	            to the following reason:
905.13/297.02	            
905.13/297.02	            The input cannot be shown compatible
905.13/297.02	         
905.13/297.02	      
905.13/297.02	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
905.13/297.02	         failed due to the following reason:
905.13/297.02	         
905.13/297.02	         None of the processors succeeded.
905.13/297.02	         
905.13/297.02	         Details of failed attempt(s):
905.13/297.02	         -----------------------------
905.13/297.02	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
905.13/297.02	            failed due to the following reason:
905.13/297.02	            
905.13/297.02	            match-boundness of the problem could not be verified.
905.13/297.02	         
905.13/297.02	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
905.13/297.02	            failed due to the following reason:
905.13/297.02	            
905.13/297.02	            match-boundness of the problem could not be verified.
905.13/297.02	         
905.13/297.02	      
905.13/297.02	   
905.13/297.02	
905.13/297.02	
905.13/297.02	Arrrr..
905.34/297.21	EOF