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