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