MAYBE
584.55/156.07	MAYBE
584.55/156.07	
584.55/156.07	We are left with following problem, upon which TcT provides the
584.55/156.07	certificate MAYBE.
584.55/156.07	
584.55/156.07	Strict Trs:
584.55/156.07	  { top1(free(x), y) -> top2(x, check(new(y)))
584.55/156.07	  , top1(free(x), y) -> top2(check(x), new(y))
584.55/156.07	  , top1(free(x), y) -> top2(check(new(x)), y)
584.55/156.07	  , top1(free(x), y) -> top2(new(x), check(y))
584.55/156.07	  , top2(x, free(y)) -> top1(x, check(new(y)))
584.55/156.07	  , top2(x, free(y)) -> top1(check(x), new(y))
584.55/156.07	  , top2(x, free(y)) -> top1(check(new(x)), y)
584.55/156.07	  , top2(x, free(y)) -> top1(new(x), check(y))
584.55/156.07	  , check(free(x)) -> free(check(x))
584.55/156.07	  , check(new(x)) -> new(check(x))
584.55/156.07	  , check(old(x)) -> old(x)
584.55/156.07	  , check(old(x)) -> old(check(x))
584.55/156.07	  , new(free(x)) -> free(new(x))
584.55/156.07	  , new(serve()) -> free(serve())
584.55/156.07	  , old(free(x)) -> free(old(x))
584.55/156.07	  , old(serve()) -> free(serve()) }
584.55/156.07	Obligation:
584.55/156.07	  runtime complexity
584.55/156.07	Answer:
584.55/156.07	  MAYBE
584.55/156.07	
584.55/156.07	None of the processors succeeded.
584.55/156.07	
584.55/156.07	Details of failed attempt(s):
584.55/156.07	-----------------------------
584.55/156.07	1) 'Best' failed due to the following reason:
584.55/156.07	   
584.55/156.07	   None of the processors succeeded.
584.55/156.07	   
584.55/156.07	   Details of failed attempt(s):
584.55/156.07	   -----------------------------
584.55/156.07	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
584.55/156.07	      seconds)' failed due to the following reason:
584.55/156.07	      
584.55/156.07	      Computation stopped due to timeout after 148.0 seconds.
584.55/156.07	   
584.55/156.07	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
584.55/156.07	      failed due to the following reason:
584.55/156.07	      
584.55/156.07	      Computation stopped due to timeout after 24.0 seconds.
584.55/156.07	   
584.55/156.07	   3) 'Best' failed due to the following reason:
584.55/156.07	      
584.55/156.07	      None of the processors succeeded.
584.55/156.07	      
584.55/156.07	      Details of failed attempt(s):
584.55/156.07	      -----------------------------
584.55/156.07	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
584.55/156.07	         following reason:
584.55/156.07	         
584.55/156.07	         The processor is inapplicable, reason:
584.55/156.07	           Processor only applicable for innermost runtime complexity analysis
584.55/156.07	      
584.55/156.07	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
584.55/156.07	         to the following reason:
584.55/156.07	         
584.55/156.07	         The processor is inapplicable, reason:
584.55/156.07	           Processor only applicable for innermost runtime complexity analysis
584.55/156.07	      
584.55/156.07	   
584.55/156.07	
584.55/156.07	2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
584.55/156.07	   the following reason:
584.55/156.07	   
584.55/156.07	   We add the following weak dependency pairs:
584.55/156.07	   
584.55/156.07	   Strict DPs:
584.55/156.07	     { top1^#(free(x), y) -> c_1(top2^#(x, check(new(y))))
584.55/156.07	     , top1^#(free(x), y) -> c_2(top2^#(check(x), new(y)))
584.55/156.07	     , top1^#(free(x), y) -> c_3(top2^#(check(new(x)), y))
584.55/156.07	     , top1^#(free(x), y) -> c_4(top2^#(new(x), check(y)))
584.55/156.07	     , top2^#(x, free(y)) -> c_5(top1^#(x, check(new(y))))
584.55/156.07	     , top2^#(x, free(y)) -> c_6(top1^#(check(x), new(y)))
584.55/156.07	     , top2^#(x, free(y)) -> c_7(top1^#(check(new(x)), y))
584.55/156.07	     , top2^#(x, free(y)) -> c_8(top1^#(new(x), check(y)))
584.55/156.07	     , check^#(free(x)) -> c_9(check^#(x))
584.55/156.07	     , check^#(new(x)) -> c_10(new^#(check(x)))
584.55/156.07	     , check^#(old(x)) -> c_11(old^#(x))
584.55/156.07	     , check^#(old(x)) -> c_12(old^#(check(x)))
584.55/156.07	     , new^#(free(x)) -> c_13(new^#(x))
584.55/156.07	     , new^#(serve()) -> c_14()
584.55/156.07	     , old^#(free(x)) -> c_15(old^#(x))
584.55/156.07	     , old^#(serve()) -> c_16() }
584.55/156.07	   
584.55/156.07	   and mark the set of starting terms.
584.55/156.07	   
584.55/156.07	   We are left with following problem, upon which TcT provides the
584.55/156.07	   certificate MAYBE.
584.55/156.07	   
584.55/156.07	   Strict DPs:
584.55/156.07	     { top1^#(free(x), y) -> c_1(top2^#(x, check(new(y))))
584.55/156.07	     , top1^#(free(x), y) -> c_2(top2^#(check(x), new(y)))
584.55/156.07	     , top1^#(free(x), y) -> c_3(top2^#(check(new(x)), y))
584.55/156.07	     , top1^#(free(x), y) -> c_4(top2^#(new(x), check(y)))
584.55/156.07	     , top2^#(x, free(y)) -> c_5(top1^#(x, check(new(y))))
584.55/156.07	     , top2^#(x, free(y)) -> c_6(top1^#(check(x), new(y)))
584.55/156.07	     , top2^#(x, free(y)) -> c_7(top1^#(check(new(x)), y))
584.55/156.07	     , top2^#(x, free(y)) -> c_8(top1^#(new(x), check(y)))
584.55/156.07	     , check^#(free(x)) -> c_9(check^#(x))
584.55/156.07	     , check^#(new(x)) -> c_10(new^#(check(x)))
584.55/156.07	     , check^#(old(x)) -> c_11(old^#(x))
584.55/156.07	     , check^#(old(x)) -> c_12(old^#(check(x)))
584.55/156.07	     , new^#(free(x)) -> c_13(new^#(x))
584.55/156.07	     , new^#(serve()) -> c_14()
584.55/156.07	     , old^#(free(x)) -> c_15(old^#(x))
584.55/156.07	     , old^#(serve()) -> c_16() }
584.55/156.07	   Strict Trs:
584.55/156.07	     { top1(free(x), y) -> top2(x, check(new(y)))
584.55/156.07	     , top1(free(x), y) -> top2(check(x), new(y))
584.55/156.07	     , top1(free(x), y) -> top2(check(new(x)), y)
584.55/156.07	     , top1(free(x), y) -> top2(new(x), check(y))
584.55/156.07	     , top2(x, free(y)) -> top1(x, check(new(y)))
584.55/156.07	     , top2(x, free(y)) -> top1(check(x), new(y))
584.55/156.07	     , top2(x, free(y)) -> top1(check(new(x)), y)
584.55/156.07	     , top2(x, free(y)) -> top1(new(x), check(y))
584.55/156.07	     , check(free(x)) -> free(check(x))
584.55/156.07	     , check(new(x)) -> new(check(x))
584.55/156.07	     , check(old(x)) -> old(x)
584.55/156.07	     , check(old(x)) -> old(check(x))
584.55/156.07	     , new(free(x)) -> free(new(x))
584.55/156.07	     , new(serve()) -> free(serve())
584.55/156.07	     , old(free(x)) -> free(old(x))
584.55/156.07	     , old(serve()) -> free(serve()) }
584.55/156.07	   Obligation:
584.55/156.07	     runtime complexity
584.55/156.07	   Answer:
584.55/156.07	     MAYBE
584.55/156.07	   
584.55/156.07	   We estimate the number of application of {14,16} by applications of
584.55/156.07	   Pre({14,16}) = {11,13,15}. Here rules are labeled as follows:
584.55/156.07	   
584.55/156.07	     DPs:
584.55/156.07	       { 1: top1^#(free(x), y) -> c_1(top2^#(x, check(new(y))))
584.55/156.07	       , 2: top1^#(free(x), y) -> c_2(top2^#(check(x), new(y)))
584.55/156.07	       , 3: top1^#(free(x), y) -> c_3(top2^#(check(new(x)), y))
584.55/156.07	       , 4: top1^#(free(x), y) -> c_4(top2^#(new(x), check(y)))
584.55/156.07	       , 5: top2^#(x, free(y)) -> c_5(top1^#(x, check(new(y))))
584.55/156.07	       , 6: top2^#(x, free(y)) -> c_6(top1^#(check(x), new(y)))
584.55/156.07	       , 7: top2^#(x, free(y)) -> c_7(top1^#(check(new(x)), y))
584.55/156.07	       , 8: top2^#(x, free(y)) -> c_8(top1^#(new(x), check(y)))
584.55/156.07	       , 9: check^#(free(x)) -> c_9(check^#(x))
584.55/156.07	       , 10: check^#(new(x)) -> c_10(new^#(check(x)))
584.55/156.07	       , 11: check^#(old(x)) -> c_11(old^#(x))
584.55/156.07	       , 12: check^#(old(x)) -> c_12(old^#(check(x)))
584.55/156.07	       , 13: new^#(free(x)) -> c_13(new^#(x))
584.55/156.07	       , 14: new^#(serve()) -> c_14()
584.55/156.07	       , 15: old^#(free(x)) -> c_15(old^#(x))
584.55/156.07	       , 16: old^#(serve()) -> c_16() }
584.55/156.07	   
584.55/156.07	   We are left with following problem, upon which TcT provides the
584.55/156.07	   certificate MAYBE.
584.55/156.07	   
584.55/156.07	   Strict DPs:
584.55/156.07	     { top1^#(free(x), y) -> c_1(top2^#(x, check(new(y))))
584.55/156.07	     , top1^#(free(x), y) -> c_2(top2^#(check(x), new(y)))
584.55/156.07	     , top1^#(free(x), y) -> c_3(top2^#(check(new(x)), y))
584.55/156.07	     , top1^#(free(x), y) -> c_4(top2^#(new(x), check(y)))
584.55/156.07	     , top2^#(x, free(y)) -> c_5(top1^#(x, check(new(y))))
584.55/156.07	     , top2^#(x, free(y)) -> c_6(top1^#(check(x), new(y)))
584.55/156.07	     , top2^#(x, free(y)) -> c_7(top1^#(check(new(x)), y))
584.55/156.07	     , top2^#(x, free(y)) -> c_8(top1^#(new(x), check(y)))
584.55/156.07	     , check^#(free(x)) -> c_9(check^#(x))
584.55/156.07	     , check^#(new(x)) -> c_10(new^#(check(x)))
584.55/156.07	     , check^#(old(x)) -> c_11(old^#(x))
584.55/156.07	     , check^#(old(x)) -> c_12(old^#(check(x)))
584.55/156.07	     , new^#(free(x)) -> c_13(new^#(x))
584.55/156.07	     , old^#(free(x)) -> c_15(old^#(x)) }
584.55/156.07	   Strict Trs:
584.55/156.07	     { top1(free(x), y) -> top2(x, check(new(y)))
584.55/156.07	     , top1(free(x), y) -> top2(check(x), new(y))
584.55/156.07	     , top1(free(x), y) -> top2(check(new(x)), y)
584.55/156.07	     , top1(free(x), y) -> top2(new(x), check(y))
584.55/156.07	     , top2(x, free(y)) -> top1(x, check(new(y)))
584.55/156.07	     , top2(x, free(y)) -> top1(check(x), new(y))
584.55/156.07	     , top2(x, free(y)) -> top1(check(new(x)), y)
584.55/156.07	     , top2(x, free(y)) -> top1(new(x), check(y))
584.55/156.07	     , check(free(x)) -> free(check(x))
584.55/156.07	     , check(new(x)) -> new(check(x))
584.55/156.07	     , check(old(x)) -> old(x)
584.55/156.07	     , check(old(x)) -> old(check(x))
584.55/156.07	     , new(free(x)) -> free(new(x))
584.55/156.07	     , new(serve()) -> free(serve())
584.55/156.07	     , old(free(x)) -> free(old(x))
584.55/156.07	     , old(serve()) -> free(serve()) }
584.55/156.07	   Weak DPs:
584.55/156.07	     { new^#(serve()) -> c_14()
584.55/156.07	     , old^#(serve()) -> c_16() }
584.55/156.07	   Obligation:
584.55/156.07	     runtime complexity
584.55/156.07	   Answer:
584.55/156.07	     MAYBE
584.55/156.07	   
584.55/156.07	   Empty strict component of the problem is NOT empty.
584.55/156.07	
584.55/156.07	
584.55/156.07	Arrrr..
584.92/156.39	EOF