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