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