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