MAYBE
1116.93/297.04	MAYBE
1116.93/297.04	
1116.93/297.04	We are left with following problem, upon which TcT provides the
1116.93/297.04	certificate MAYBE.
1116.93/297.04	
1116.93/297.04	Strict Trs:
1116.93/297.04	  { O(0()) -> 0()
1116.93/297.04	  , +(x, 0()) -> x
1116.93/297.04	  , +(x, +(y, z)) -> +(+(x, y), z)
1116.93/297.04	  , +(O(x), O(y)) -> O(+(x, y))
1116.93/297.04	  , +(O(x), I(y)) -> I(+(x, y))
1116.93/297.04	  , +(0(), x) -> x
1116.93/297.04	  , +(I(x), O(y)) -> I(+(x, y))
1116.93/297.04	  , +(I(x), I(y)) -> O(+(+(x, y), I(0())))
1116.93/297.04	  , -(x, 0()) -> x
1116.93/297.04	  , -(O(x), O(y)) -> O(-(x, y))
1116.93/297.04	  , -(O(x), I(y)) -> I(-(-(x, y), I(1())))
1116.93/297.04	  , -(0(), x) -> 0()
1116.93/297.04	  , -(I(x), O(y)) -> I(-(x, y))
1116.93/297.04	  , -(I(x), I(y)) -> O(-(x, y))
1116.93/297.04	  , not(true()) -> false()
1116.93/297.04	  , not(false()) -> true()
1116.93/297.04	  , and(x, true()) -> x
1116.93/297.04	  , and(x, false()) -> false()
1116.93/297.04	  , if(true(), x, y) -> x
1116.93/297.04	  , if(false(), x, y) -> y
1116.93/297.04	  , ge(x, 0()) -> true()
1116.93/297.04	  , ge(O(x), O(y)) -> ge(x, y)
1116.93/297.04	  , ge(O(x), I(y)) -> not(ge(y, x))
1116.93/297.04	  , ge(0(), O(x)) -> ge(0(), x)
1116.93/297.04	  , ge(0(), I(x)) -> false()
1116.93/297.04	  , ge(I(x), O(y)) -> ge(x, y)
1116.93/297.04	  , ge(I(x), I(y)) -> ge(x, y)
1116.93/297.04	  , Log'(O(x)) -> if(ge(x, I(0())), +(Log'(x), I(0())), 0())
1116.93/297.04	  , Log'(0()) -> 0()
1116.93/297.04	  , Log'(I(x)) -> +(Log'(x), I(0()))
1116.93/297.04	  , Log(x) -> -(Log'(x), I(0()))
1116.93/297.04	  , Val(L(x)) -> x
1116.93/297.04	  , Val(N(x, l(), r())) -> x
1116.93/297.04	  , Min(L(x)) -> x
1116.93/297.04	  , Min(N(x, l(), r())) -> Min(l())
1116.93/297.04	  , Max(L(x)) -> x
1116.93/297.04	  , Max(N(x, l(), r())) -> Max(r())
1116.93/297.04	  , BS(L(x)) -> true()
1116.93/297.04	  , BS(N(x, l(), r())) ->
1116.93/297.04	    and(and(ge(x, Max(l())), ge(Min(r()), x)), and(BS(l()), BS(r())))
1116.93/297.04	  , Size(L(x)) -> I(0())
1116.93/297.04	  , Size(N(x, l(), r())) -> +(+(Size(l()), Size(r())), I(1()))
1116.93/297.04	  , WB(L(x)) -> true()
1116.93/297.04	  , WB(N(x, l(), r())) ->
1116.93/297.04	    and(if(ge(Size(l()), Size(r())),
1116.93/297.04	           ge(I(0()), -(Size(l()), Size(r()))),
1116.93/297.04	           ge(I(0()), -(Size(r()), Size(l())))),
1116.93/297.04	        and(WB(l()), WB(r()))) }
1116.93/297.04	Obligation:
1116.93/297.04	  innermost runtime complexity
1116.93/297.04	Answer:
1116.93/297.04	  MAYBE
1116.93/297.04	
1116.93/297.04	None of the processors succeeded.
1116.93/297.04	
1116.93/297.04	Details of failed attempt(s):
1116.93/297.04	-----------------------------
1116.93/297.04	1) 'empty' failed due to the following reason:
1116.93/297.04	   
1116.93/297.04	   Empty strict component of the problem is NOT empty.
1116.93/297.04	
1116.93/297.04	2) 'Best' failed due to the following reason:
1116.93/297.04	   
1116.93/297.04	   None of the processors succeeded.
1116.93/297.04	   
1116.93/297.04	   Details of failed attempt(s):
1116.93/297.04	   -----------------------------
1116.93/297.04	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1116.93/297.04	      following reason:
1116.93/297.04	      
1116.93/297.04	      Computation stopped due to timeout after 297.0 seconds.
1116.93/297.04	   
1116.93/297.04	   2) 'Best' failed due to the following reason:
1116.93/297.04	      
1116.93/297.04	      None of the processors succeeded.
1116.93/297.04	      
1116.93/297.04	      Details of failed attempt(s):
1116.93/297.04	      -----------------------------
1116.93/297.04	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1116.93/297.04	         seconds)' failed due to the following reason:
1116.93/297.04	         
1116.93/297.04	         Computation stopped due to timeout after 148.0 seconds.
1116.93/297.04	      
1116.93/297.04	      2) 'Best' failed due to the following reason:
1116.93/297.04	         
1116.93/297.04	         None of the processors succeeded.
1116.93/297.04	         
1116.93/297.04	         Details of failed attempt(s):
1116.93/297.04	         -----------------------------
1116.93/297.04	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1116.93/297.04	            following reason:
1116.93/297.04	            
1116.93/297.04	            The input cannot be shown compatible
1116.93/297.04	         
1116.93/297.04	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1116.93/297.04	            to the following reason:
1116.93/297.04	            
1116.93/297.04	            The input cannot be shown compatible
1116.93/297.04	         
1116.93/297.04	      
1116.93/297.04	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1116.93/297.04	         failed due to the following reason:
1116.93/297.04	         
1116.93/297.04	         None of the processors succeeded.
1116.93/297.04	         
1116.93/297.04	         Details of failed attempt(s):
1116.93/297.04	         -----------------------------
1116.93/297.04	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
1116.93/297.04	            failed due to the following reason:
1116.93/297.04	            
1116.93/297.04	            match-boundness of the problem could not be verified.
1116.93/297.04	         
1116.93/297.04	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1116.93/297.04	            failed due to the following reason:
1116.93/297.04	            
1116.93/297.04	            match-boundness of the problem could not be verified.
1116.93/297.04	         
1116.93/297.04	      
1116.93/297.04	   
1116.93/297.04	
1116.93/297.04	
1116.93/297.04	Arrrr..
1117.58/297.63	EOF