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