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