MAYBE
777.39/297.04	MAYBE
777.39/297.04	
777.39/297.04	We are left with following problem, upon which TcT provides the
777.39/297.04	certificate MAYBE.
777.39/297.04	
777.39/297.04	Strict Trs:
777.39/297.04	  { -(x, 0()) -> x
777.39/297.04	  , -(s(x), s(y)) -> -(x, y)
777.39/297.04	  , *(x, 0()) -> 0()
777.39/297.04	  , *(x, s(y)) -> +(*(x, y), x)
777.39/297.04	  , if(true(), x, y) -> x
777.39/297.04	  , if(true(), x, y) -> true()
777.39/297.04	  , if(false(), x, y) -> y
777.39/297.04	  , if(false(), x, y) -> false()
777.39/297.04	  , odd(0()) -> false()
777.39/297.04	  , odd(s(0())) -> true()
777.39/297.04	  , odd(s(s(x))) -> odd(x)
777.39/297.04	  , half(0()) -> 0()
777.39/297.04	  , half(s(0())) -> 0()
777.39/297.04	  , half(s(s(x))) -> s(half(x))
777.39/297.04	  , pow(x, y) -> f(x, y, s(0()))
777.39/297.04	  , f(x, 0(), z) -> z
777.39/297.04	  , f(x, s(y), z) ->
777.39/297.04	    if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) }
777.39/297.04	Obligation:
777.39/297.04	  runtime complexity
777.39/297.04	Answer:
777.39/297.04	  MAYBE
777.39/297.04	
777.39/297.04	None of the processors succeeded.
777.39/297.04	
777.39/297.04	Details of failed attempt(s):
777.39/297.04	-----------------------------
777.39/297.04	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
777.39/297.04	   following reason:
777.39/297.04	   
777.39/297.04	   Computation stopped due to timeout after 297.0 seconds.
777.39/297.04	
777.39/297.04	2) 'Best' failed due to the following reason:
777.39/297.04	   
777.39/297.04	   None of the processors succeeded.
777.39/297.04	   
777.39/297.04	   Details of failed attempt(s):
777.39/297.04	   -----------------------------
777.39/297.04	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
777.39/297.04	      seconds)' failed due to the following reason:
777.39/297.04	      
777.39/297.04	      Computation stopped due to timeout after 148.0 seconds.
777.39/297.04	   
777.39/297.04	   2) 'Best' failed due to the following reason:
777.39/297.04	      
777.39/297.04	      None of the processors succeeded.
777.39/297.04	      
777.39/297.04	      Details of failed attempt(s):
777.39/297.04	      -----------------------------
777.39/297.04	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
777.39/297.04	         following reason:
777.39/297.04	         
777.39/297.04	         The processor is inapplicable, reason:
777.39/297.04	           Processor only applicable for innermost runtime complexity analysis
777.39/297.04	      
777.39/297.04	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
777.39/297.04	         to the following reason:
777.39/297.04	         
777.39/297.04	         The processor is inapplicable, reason:
777.39/297.04	           Processor only applicable for innermost runtime complexity analysis
777.39/297.04	      
777.39/297.04	   
777.39/297.04	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
777.39/297.04	      failed due to the following reason:
777.39/297.04	      
777.39/297.04	      None of the processors succeeded.
777.39/297.04	      
777.39/297.04	      Details of failed attempt(s):
777.39/297.04	      -----------------------------
777.39/297.04	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
777.39/297.04	         failed due to the following reason:
777.39/297.04	         
777.39/297.04	         match-boundness of the problem could not be verified.
777.39/297.04	      
777.39/297.04	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
777.39/297.04	         failed due to the following reason:
777.39/297.04	         
777.39/297.04	         match-boundness of the problem could not be verified.
777.39/297.04	      
777.39/297.04	   
777.39/297.04	
777.39/297.04	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
777.39/297.04	   the following reason:
777.39/297.04	   
777.39/297.04	   We add the following weak dependency pairs:
777.39/297.04	   
777.39/297.04	   Strict DPs:
777.39/297.04	     { -^#(x, 0()) -> c_1(x)
777.39/297.04	     , -^#(s(x), s(y)) -> c_2(-^#(x, y))
777.39/297.04	     , *^#(x, 0()) -> c_3()
777.39/297.04	     , *^#(x, s(y)) -> c_4(*^#(x, y), x)
777.39/297.04	     , if^#(true(), x, y) -> c_5(x)
777.39/297.04	     , if^#(true(), x, y) -> c_6()
777.39/297.04	     , if^#(false(), x, y) -> c_7(y)
777.39/297.04	     , if^#(false(), x, y) -> c_8()
777.39/297.04	     , odd^#(0()) -> c_9()
777.39/297.04	     , odd^#(s(0())) -> c_10()
777.39/297.04	     , odd^#(s(s(x))) -> c_11(odd^#(x))
777.39/297.04	     , half^#(0()) -> c_12()
777.39/297.04	     , half^#(s(0())) -> c_13()
777.39/297.04	     , half^#(s(s(x))) -> c_14(half^#(x))
777.39/297.04	     , pow^#(x, y) -> c_15(f^#(x, y, s(0())))
777.39/297.04	     , f^#(x, 0(), z) -> c_16(z)
777.39/297.04	     , f^#(x, s(y), z) ->
777.39/297.04	       c_17(if^#(odd(s(y)),
777.39/297.04	                 f(x, y, *(x, z)),
777.39/297.04	                 f(*(x, x), half(s(y)), z))) }
777.39/297.04	   
777.39/297.04	   and mark the set of starting terms.
777.39/297.04	   
777.39/297.04	   We are left with following problem, upon which TcT provides the
777.39/297.04	   certificate MAYBE.
777.39/297.04	   
777.39/297.04	   Strict DPs:
777.39/297.04	     { -^#(x, 0()) -> c_1(x)
777.39/297.04	     , -^#(s(x), s(y)) -> c_2(-^#(x, y))
777.39/297.04	     , *^#(x, 0()) -> c_3()
777.39/297.04	     , *^#(x, s(y)) -> c_4(*^#(x, y), x)
777.39/297.04	     , if^#(true(), x, y) -> c_5(x)
777.39/297.04	     , if^#(true(), x, y) -> c_6()
777.39/297.04	     , if^#(false(), x, y) -> c_7(y)
777.39/297.04	     , if^#(false(), x, y) -> c_8()
777.39/297.04	     , odd^#(0()) -> c_9()
777.39/297.04	     , odd^#(s(0())) -> c_10()
777.39/297.04	     , odd^#(s(s(x))) -> c_11(odd^#(x))
777.39/297.04	     , half^#(0()) -> c_12()
777.39/297.04	     , half^#(s(0())) -> c_13()
777.39/297.04	     , half^#(s(s(x))) -> c_14(half^#(x))
777.39/297.04	     , pow^#(x, y) -> c_15(f^#(x, y, s(0())))
777.39/297.04	     , f^#(x, 0(), z) -> c_16(z)
777.39/297.04	     , f^#(x, s(y), z) ->
777.39/297.04	       c_17(if^#(odd(s(y)),
777.39/297.04	                 f(x, y, *(x, z)),
777.39/297.04	                 f(*(x, x), half(s(y)), z))) }
777.39/297.04	   Strict Trs:
777.39/297.04	     { -(x, 0()) -> x
777.39/297.04	     , -(s(x), s(y)) -> -(x, y)
777.39/297.04	     , *(x, 0()) -> 0()
777.39/297.04	     , *(x, s(y)) -> +(*(x, y), x)
777.39/297.04	     , if(true(), x, y) -> x
777.39/297.04	     , if(true(), x, y) -> true()
777.39/297.04	     , if(false(), x, y) -> y
777.39/297.04	     , if(false(), x, y) -> false()
777.39/297.04	     , odd(0()) -> false()
777.39/297.04	     , odd(s(0())) -> true()
777.39/297.04	     , odd(s(s(x))) -> odd(x)
777.39/297.04	     , half(0()) -> 0()
777.39/297.04	     , half(s(0())) -> 0()
777.39/297.04	     , half(s(s(x))) -> s(half(x))
777.39/297.04	     , pow(x, y) -> f(x, y, s(0()))
777.39/297.04	     , f(x, 0(), z) -> z
777.39/297.04	     , f(x, s(y), z) ->
777.39/297.04	       if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) }
777.39/297.04	   Obligation:
777.39/297.04	     runtime complexity
777.39/297.04	   Answer:
777.39/297.04	     MAYBE
777.39/297.04	   
777.39/297.04	   We estimate the number of application of {3,6,8,9,10,12,13} by
777.39/297.04	   applications of Pre({3,6,8,9,10,12,13}) = {1,4,5,7,11,14,16,17}.
777.39/297.04	   Here rules are labeled as follows:
777.39/297.04	   
777.39/297.04	     DPs:
777.39/297.04	       { 1: -^#(x, 0()) -> c_1(x)
777.39/297.04	       , 2: -^#(s(x), s(y)) -> c_2(-^#(x, y))
777.39/297.04	       , 3: *^#(x, 0()) -> c_3()
777.39/297.04	       , 4: *^#(x, s(y)) -> c_4(*^#(x, y), x)
777.39/297.04	       , 5: if^#(true(), x, y) -> c_5(x)
777.39/297.04	       , 6: if^#(true(), x, y) -> c_6()
777.39/297.04	       , 7: if^#(false(), x, y) -> c_7(y)
777.39/297.04	       , 8: if^#(false(), x, y) -> c_8()
777.39/297.04	       , 9: odd^#(0()) -> c_9()
777.39/297.04	       , 10: odd^#(s(0())) -> c_10()
777.39/297.04	       , 11: odd^#(s(s(x))) -> c_11(odd^#(x))
777.39/297.04	       , 12: half^#(0()) -> c_12()
777.39/297.04	       , 13: half^#(s(0())) -> c_13()
777.39/297.04	       , 14: half^#(s(s(x))) -> c_14(half^#(x))
777.39/297.04	       , 15: pow^#(x, y) -> c_15(f^#(x, y, s(0())))
777.39/297.04	       , 16: f^#(x, 0(), z) -> c_16(z)
777.39/297.04	       , 17: f^#(x, s(y), z) ->
777.39/297.04	             c_17(if^#(odd(s(y)),
777.39/297.04	                       f(x, y, *(x, z)),
777.39/297.04	                       f(*(x, x), half(s(y)), z))) }
777.39/297.04	   
777.39/297.04	   We are left with following problem, upon which TcT provides the
777.39/297.04	   certificate MAYBE.
777.39/297.04	   
777.39/297.04	   Strict DPs:
777.39/297.04	     { -^#(x, 0()) -> c_1(x)
777.39/297.04	     , -^#(s(x), s(y)) -> c_2(-^#(x, y))
777.39/297.04	     , *^#(x, s(y)) -> c_4(*^#(x, y), x)
777.39/297.04	     , if^#(true(), x, y) -> c_5(x)
777.39/297.04	     , if^#(false(), x, y) -> c_7(y)
777.39/297.04	     , odd^#(s(s(x))) -> c_11(odd^#(x))
777.39/297.04	     , half^#(s(s(x))) -> c_14(half^#(x))
777.39/297.04	     , pow^#(x, y) -> c_15(f^#(x, y, s(0())))
777.39/297.04	     , f^#(x, 0(), z) -> c_16(z)
777.39/297.04	     , f^#(x, s(y), z) ->
777.39/297.04	       c_17(if^#(odd(s(y)),
777.39/297.04	                 f(x, y, *(x, z)),
777.39/297.04	                 f(*(x, x), half(s(y)), z))) }
777.39/297.04	   Strict Trs:
777.39/297.04	     { -(x, 0()) -> x
777.39/297.04	     , -(s(x), s(y)) -> -(x, y)
777.39/297.04	     , *(x, 0()) -> 0()
777.39/297.04	     , *(x, s(y)) -> +(*(x, y), x)
777.39/297.04	     , if(true(), x, y) -> x
777.39/297.04	     , if(true(), x, y) -> true()
777.39/297.04	     , if(false(), x, y) -> y
777.39/297.04	     , if(false(), x, y) -> false()
777.39/297.04	     , odd(0()) -> false()
777.39/297.04	     , odd(s(0())) -> true()
777.39/297.04	     , odd(s(s(x))) -> odd(x)
777.39/297.04	     , half(0()) -> 0()
777.39/297.04	     , half(s(0())) -> 0()
777.39/297.04	     , half(s(s(x))) -> s(half(x))
777.39/297.04	     , pow(x, y) -> f(x, y, s(0()))
777.39/297.04	     , f(x, 0(), z) -> z
777.39/297.04	     , f(x, s(y), z) ->
777.39/297.04	       if(odd(s(y)), f(x, y, *(x, z)), f(*(x, x), half(s(y)), z)) }
777.39/297.04	   Weak DPs:
777.39/297.04	     { *^#(x, 0()) -> c_3()
777.39/297.04	     , if^#(true(), x, y) -> c_6()
777.39/297.05	     , if^#(false(), x, y) -> c_8()
777.39/297.05	     , odd^#(0()) -> c_9()
777.39/297.05	     , odd^#(s(0())) -> c_10()
777.39/297.05	     , half^#(0()) -> c_12()
777.39/297.05	     , half^#(s(0())) -> c_13() }
777.39/297.05	   Obligation:
777.39/297.05	     runtime complexity
777.39/297.05	   Answer:
777.39/297.05	     MAYBE
777.39/297.05	   
777.39/297.05	   Empty strict component of the problem is NOT empty.
777.39/297.05	
777.39/297.05	
777.39/297.05	Arrrr..
777.61/297.29	EOF