MAYBE
726.88/297.09	MAYBE
726.88/297.09	
726.88/297.09	We are left with following problem, upon which TcT provides the
726.88/297.09	certificate MAYBE.
726.88/297.09	
726.88/297.09	Strict Trs:
726.88/297.09	  { top(sent(x)) -> top(check(rest(x)))
726.88/297.09	  , check(sent(x)) -> sent(check(x))
726.88/297.09	  , check(rest(x)) -> rest(check(x))
726.88/297.09	  , check(cons(x, y)) -> cons(x, y)
726.88/297.09	  , check(cons(x, y)) -> cons(x, check(y))
726.88/297.09	  , check(cons(x, y)) -> cons(check(x), y)
726.88/297.09	  , rest(nil()) -> sent(nil())
726.88/297.09	  , rest(cons(x, y)) -> sent(y) }
726.88/297.09	Obligation:
726.88/297.09	  runtime complexity
726.88/297.09	Answer:
726.88/297.09	  MAYBE
726.88/297.09	
726.88/297.09	None of the processors succeeded.
726.88/297.09	
726.88/297.09	Details of failed attempt(s):
726.88/297.09	-----------------------------
726.88/297.09	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
726.88/297.09	   following reason:
726.88/297.09	   
726.88/297.09	   Computation stopped due to timeout after 297.0 seconds.
726.88/297.09	
726.88/297.09	2) 'Best' failed due to the following reason:
726.88/297.09	   
726.88/297.09	   None of the processors succeeded.
726.88/297.09	   
726.88/297.09	   Details of failed attempt(s):
726.88/297.09	   -----------------------------
726.88/297.09	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
726.88/297.09	      seconds)' failed due to the following reason:
726.88/297.09	      
726.88/297.09	      Computation stopped due to timeout after 148.0 seconds.
726.88/297.10	   
726.88/297.10	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
726.88/297.10	      failed due to the following reason:
726.88/297.10	      
726.88/297.10	      Computation stopped due to timeout after 24.0 seconds.
726.88/297.10	   
726.88/297.10	   3) 'Best' failed due to the following reason:
726.88/297.10	      
726.88/297.10	      None of the processors succeeded.
726.88/297.10	      
726.88/297.10	      Details of failed attempt(s):
726.88/297.10	      -----------------------------
726.88/297.10	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
726.88/297.10	         following reason:
726.88/297.10	         
726.88/297.10	         The processor is inapplicable, reason:
726.88/297.10	           Processor only applicable for innermost runtime complexity analysis
726.88/297.10	      
726.88/297.10	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
726.88/297.10	         to the following reason:
726.88/297.10	         
726.88/297.10	         The processor is inapplicable, reason:
726.88/297.10	           Processor only applicable for innermost runtime complexity analysis
726.88/297.10	      
726.88/297.10	   
726.88/297.10	
726.88/297.10	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
726.88/297.10	   the following reason:
726.88/297.10	   
726.88/297.10	   We add the following weak dependency pairs:
726.88/297.10	   
726.88/297.10	   Strict DPs:
726.88/297.10	     { top^#(sent(x)) -> c_1(top^#(check(rest(x))))
726.88/297.10	     , check^#(sent(x)) -> c_2(check^#(x))
726.88/297.10	     , check^#(rest(x)) -> c_3(rest^#(check(x)))
726.88/297.10	     , check^#(cons(x, y)) -> c_4(x, y)
726.88/297.10	     , check^#(cons(x, y)) -> c_5(x, check^#(y))
726.88/297.10	     , check^#(cons(x, y)) -> c_6(check^#(x), y)
726.88/297.10	     , rest^#(nil()) -> c_7()
726.88/297.10	     , rest^#(cons(x, y)) -> c_8(y) }
726.88/297.10	   
726.88/297.10	   and mark the set of starting terms.
726.88/297.10	   
726.88/297.10	   We are left with following problem, upon which TcT provides the
726.88/297.10	   certificate MAYBE.
726.88/297.10	   
726.88/297.10	   Strict DPs:
726.88/297.10	     { top^#(sent(x)) -> c_1(top^#(check(rest(x))))
726.88/297.10	     , check^#(sent(x)) -> c_2(check^#(x))
726.88/297.10	     , check^#(rest(x)) -> c_3(rest^#(check(x)))
726.88/297.10	     , check^#(cons(x, y)) -> c_4(x, y)
726.88/297.10	     , check^#(cons(x, y)) -> c_5(x, check^#(y))
726.88/297.10	     , check^#(cons(x, y)) -> c_6(check^#(x), y)
726.88/297.10	     , rest^#(nil()) -> c_7()
726.88/297.10	     , rest^#(cons(x, y)) -> c_8(y) }
726.88/297.10	   Strict Trs:
726.88/297.10	     { top(sent(x)) -> top(check(rest(x)))
726.88/297.10	     , check(sent(x)) -> sent(check(x))
726.88/297.10	     , check(rest(x)) -> rest(check(x))
726.88/297.10	     , check(cons(x, y)) -> cons(x, y)
726.88/297.10	     , check(cons(x, y)) -> cons(x, check(y))
726.88/297.10	     , check(cons(x, y)) -> cons(check(x), y)
726.88/297.10	     , rest(nil()) -> sent(nil())
726.88/297.10	     , rest(cons(x, y)) -> sent(y) }
726.88/297.10	   Obligation:
726.88/297.10	     runtime complexity
726.88/297.10	   Answer:
726.88/297.10	     MAYBE
726.88/297.10	   
726.88/297.10	   We estimate the number of application of {7} by applications of
726.88/297.10	   Pre({7}) = {4,5,6,8}. Here rules are labeled as follows:
726.88/297.10	   
726.88/297.10	     DPs:
726.88/297.10	       { 1: top^#(sent(x)) -> c_1(top^#(check(rest(x))))
726.88/297.10	       , 2: check^#(sent(x)) -> c_2(check^#(x))
726.88/297.10	       , 3: check^#(rest(x)) -> c_3(rest^#(check(x)))
726.88/297.10	       , 4: check^#(cons(x, y)) -> c_4(x, y)
726.88/297.10	       , 5: check^#(cons(x, y)) -> c_5(x, check^#(y))
726.88/297.10	       , 6: check^#(cons(x, y)) -> c_6(check^#(x), y)
726.88/297.10	       , 7: rest^#(nil()) -> c_7()
726.88/297.10	       , 8: rest^#(cons(x, y)) -> c_8(y) }
726.88/297.10	   
726.88/297.10	   We are left with following problem, upon which TcT provides the
726.88/297.10	   certificate MAYBE.
726.88/297.10	   
726.88/297.10	   Strict DPs:
726.88/297.10	     { top^#(sent(x)) -> c_1(top^#(check(rest(x))))
726.88/297.10	     , check^#(sent(x)) -> c_2(check^#(x))
726.88/297.10	     , check^#(rest(x)) -> c_3(rest^#(check(x)))
726.88/297.10	     , check^#(cons(x, y)) -> c_4(x, y)
726.88/297.10	     , check^#(cons(x, y)) -> c_5(x, check^#(y))
726.88/297.10	     , check^#(cons(x, y)) -> c_6(check^#(x), y)
726.88/297.10	     , rest^#(cons(x, y)) -> c_8(y) }
726.88/297.10	   Strict Trs:
726.88/297.10	     { top(sent(x)) -> top(check(rest(x)))
726.88/297.10	     , check(sent(x)) -> sent(check(x))
726.88/297.10	     , check(rest(x)) -> rest(check(x))
726.88/297.10	     , check(cons(x, y)) -> cons(x, y)
726.88/297.10	     , check(cons(x, y)) -> cons(x, check(y))
726.88/297.10	     , check(cons(x, y)) -> cons(check(x), y)
726.88/297.10	     , rest(nil()) -> sent(nil())
726.88/297.10	     , rest(cons(x, y)) -> sent(y) }
726.88/297.10	   Weak DPs: { rest^#(nil()) -> c_7() }
726.88/297.10	   Obligation:
726.88/297.10	     runtime complexity
726.88/297.10	   Answer:
726.88/297.10	     MAYBE
726.88/297.10	   
726.88/297.10	   Empty strict component of the problem is NOT empty.
726.88/297.10	
726.88/297.10	
726.88/297.10	Arrrr..
726.99/297.12	EOF