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