MAYBE
1119.67/297.15	MAYBE
1119.67/297.15	
1119.67/297.15	We are left with following problem, upon which TcT provides the
1119.67/297.15	certificate MAYBE.
1119.67/297.15	
1119.67/297.15	Strict Trs:
1119.67/297.15	  { app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y)
1119.67/297.15	  , helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs)
1119.67/297.15	  , plus(x, 0()) -> x
1119.67/297.15	  , plus(x, s(y)) -> s(plus(x, y))
1119.67/297.15	  , length(nil()) -> 0()
1119.67/297.15	  , length(cons(x, y)) -> s(length(y))
1119.67/297.15	  , if(true(), c, l, ys, zs) -> nil()
1119.67/297.15	  , if(false(), c, l, ys, zs) ->
1119.67/297.15	    helpb(c, l, greater(ys, zs), smaller(ys, zs))
1119.67/297.15	  , ge(x, 0()) -> true()
1119.67/297.15	  , ge(0(), s(x)) -> false()
1119.67/297.15	  , ge(s(x), s(y)) -> ge(x, y)
1119.67/297.15	  , helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs))
1119.67/297.15	  , greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs)
1119.67/297.15	  , smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys)
1119.67/297.15	  , helpc(true(), ys, zs) -> ys
1119.67/297.15	  , helpc(false(), ys, zs) -> zs }
1119.67/297.15	Obligation:
1119.67/297.15	  innermost runtime complexity
1119.67/297.15	Answer:
1119.67/297.15	  MAYBE
1119.67/297.15	
1119.67/297.15	None of the processors succeeded.
1119.67/297.15	
1119.67/297.15	Details of failed attempt(s):
1119.67/297.15	-----------------------------
1119.67/297.15	1) 'empty' failed due to the following reason:
1119.67/297.15	   
1119.67/297.15	   Empty strict component of the problem is NOT empty.
1119.67/297.15	
1119.67/297.15	2) 'Best' failed due to the following reason:
1119.67/297.15	   
1119.67/297.15	   None of the processors succeeded.
1119.67/297.15	   
1119.67/297.15	   Details of failed attempt(s):
1119.67/297.15	   -----------------------------
1119.67/297.15	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1119.67/297.15	      following reason:
1119.67/297.15	      
1119.67/297.15	      Computation stopped due to timeout after 297.0 seconds.
1119.67/297.15	   
1119.67/297.15	   2) 'Best' failed due to the following reason:
1119.67/297.15	      
1119.67/297.15	      None of the processors succeeded.
1119.67/297.15	      
1119.67/297.15	      Details of failed attempt(s):
1119.67/297.15	      -----------------------------
1119.67/297.15	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1119.67/297.15	         seconds)' failed due to the following reason:
1119.67/297.15	         
1119.67/297.15	         Computation stopped due to timeout after 148.0 seconds.
1119.67/297.15	      
1119.67/297.15	      2) 'Best' failed due to the following reason:
1119.67/297.15	         
1119.67/297.15	         None of the processors succeeded.
1119.67/297.15	         
1119.67/297.15	         Details of failed attempt(s):
1119.67/297.15	         -----------------------------
1119.67/297.15	         1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1119.67/297.15	            to the following reason:
1119.67/297.15	            
1119.67/297.15	            The input cannot be shown compatible
1119.67/297.15	         
1119.67/297.15	         2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1119.67/297.15	            following reason:
1119.67/297.15	            
1119.67/297.15	            The input cannot be shown compatible
1119.67/297.15	         
1119.67/297.15	      
1119.67/297.15	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1119.67/297.15	         failed due to the following reason:
1119.67/297.15	         
1119.67/297.15	         None of the processors succeeded.
1119.67/297.15	         
1119.67/297.15	         Details of failed attempt(s):
1119.67/297.15	         -----------------------------
1119.67/297.15	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
1119.67/297.15	            failed due to the following reason:
1119.67/297.15	            
1119.67/297.15	            match-boundness of the problem could not be verified.
1119.67/297.15	         
1119.67/297.15	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1119.67/297.15	            failed due to the following reason:
1119.67/297.15	            
1119.67/297.15	            match-boundness of the problem could not be verified.
1119.67/297.15	         
1119.67/297.15	      
1119.67/297.15	   
1119.67/297.15	
1119.67/297.15	
1119.67/297.15	Arrrr..
1120.14/297.45	EOF