MAYBE
963.50/297.05	MAYBE
963.50/297.05	
963.50/297.05	We are left with following problem, upon which TcT provides the
963.50/297.05	certificate MAYBE.
963.50/297.05	
963.50/297.05	Strict Trs:
963.50/297.05	  { eq(0(), 0()) -> true()
963.50/297.05	  , eq(0(), s(x)) -> false()
963.50/297.05	  , eq(s(x), 0()) -> false()
963.50/297.05	  , eq(s(x), s(y)) -> eq(x, y)
963.50/297.05	  , or(true(), y) -> true()
963.50/297.05	  , or(false(), y) -> y
963.50/297.05	  , and(true(), y) -> y
963.50/297.05	  , and(false(), y) -> false()
963.50/297.05	  , size(empty()) -> 0()
963.50/297.05	  , size(edge(x, y, i)) -> s(size(i))
963.50/297.05	  , le(0(), y) -> true()
963.50/297.05	  , le(s(x), 0()) -> false()
963.50/297.05	  , le(s(x), s(y)) -> le(x, y)
963.50/297.05	  , reachable(x, y, i) -> reach(x, y, 0(), i, i)
963.50/297.05	  , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
963.50/297.05	  , if1(true(), x, y, c, i, j) -> true()
963.50/297.05	  , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
963.50/297.05	  , if2(true(), x, y, c, empty(), j) -> false()
963.50/297.05	  , if2(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.05	    or(if2(true(), x, y, c, i, j),
963.50/297.05	       and(eq(x, u), reach(v, y, s(c), j, j)))
963.50/297.05	  , if2(false(), x, y, c, i, j) -> false() }
963.50/297.05	Obligation:
963.50/297.05	  runtime complexity
963.50/297.05	Answer:
963.50/297.05	  MAYBE
963.50/297.05	
963.50/297.05	None of the processors succeeded.
963.50/297.05	
963.50/297.05	Details of failed attempt(s):
963.50/297.05	-----------------------------
963.50/297.05	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
963.50/297.05	   following reason:
963.50/297.05	   
963.50/297.05	   Computation stopped due to timeout after 297.0 seconds.
963.50/297.05	
963.50/297.05	2) 'Best' failed due to the following reason:
963.50/297.05	   
963.50/297.05	   None of the processors succeeded.
963.50/297.05	   
963.50/297.05	   Details of failed attempt(s):
963.50/297.05	   -----------------------------
963.50/297.05	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
963.50/297.05	      seconds)' failed due to the following reason:
963.50/297.05	      
963.50/297.05	      Computation stopped due to timeout after 148.0 seconds.
963.50/297.05	   
963.50/297.05	   2) 'Best' failed due to the following reason:
963.50/297.05	      
963.50/297.05	      None of the processors succeeded.
963.50/297.05	      
963.50/297.05	      Details of failed attempt(s):
963.50/297.05	      -----------------------------
963.50/297.05	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
963.50/297.05	         following reason:
963.50/297.05	         
963.50/297.05	         The processor is inapplicable, reason:
963.50/297.05	           Processor only applicable for innermost runtime complexity analysis
963.50/297.05	      
963.50/297.05	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
963.50/297.05	         to the following reason:
963.50/297.05	         
963.50/297.05	         The processor is inapplicable, reason:
963.50/297.05	           Processor only applicable for innermost runtime complexity analysis
963.50/297.05	      
963.50/297.05	   
963.50/297.05	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
963.50/297.05	      failed due to the following reason:
963.50/297.05	      
963.50/297.05	      None of the processors succeeded.
963.50/297.05	      
963.50/297.05	      Details of failed attempt(s):
963.50/297.05	      -----------------------------
963.50/297.05	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
963.50/297.05	         failed due to the following reason:
963.50/297.05	         
963.50/297.05	         match-boundness of the problem could not be verified.
963.50/297.05	      
963.50/297.05	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
963.50/297.05	         failed due to the following reason:
963.50/297.05	         
963.50/297.05	         match-boundness of the problem could not be verified.
963.50/297.05	      
963.50/297.05	   
963.50/297.05	
963.50/297.05	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
963.50/297.05	   the following reason:
963.50/297.05	   
963.50/297.05	   We add the following weak dependency pairs:
963.50/297.05	   
963.50/297.05	   Strict DPs:
963.50/297.05	     { eq^#(0(), 0()) -> c_1()
963.50/297.05	     , eq^#(0(), s(x)) -> c_2()
963.50/297.05	     , eq^#(s(x), 0()) -> c_3()
963.50/297.05	     , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
963.50/297.05	     , or^#(true(), y) -> c_5()
963.50/297.05	     , or^#(false(), y) -> c_6(y)
963.50/297.05	     , and^#(true(), y) -> c_7(y)
963.50/297.05	     , and^#(false(), y) -> c_8()
963.50/297.05	     , size^#(empty()) -> c_9()
963.50/297.05	     , size^#(edge(x, y, i)) -> c_10(size^#(i))
963.50/297.05	     , le^#(0(), y) -> c_11()
963.50/297.05	     , le^#(s(x), 0()) -> c_12()
963.50/297.05	     , le^#(s(x), s(y)) -> c_13(le^#(x, y))
963.50/297.05	     , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
963.50/297.05	     , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j))
963.50/297.05	     , if1^#(true(), x, y, c, i, j) -> c_16()
963.50/297.05	     , if1^#(false(), x, y, c, i, j) ->
963.50/297.05	       c_17(if2^#(le(c, size(j)), x, y, c, i, j))
963.50/297.05	     , if2^#(true(), x, y, c, empty(), j) -> c_18()
963.50/297.05	     , if2^#(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.05	       c_19(or^#(if2(true(), x, y, c, i, j),
963.50/297.05	                 and(eq(x, u), reach(v, y, s(c), j, j))))
963.50/297.05	     , if2^#(false(), x, y, c, i, j) -> c_20() }
963.50/297.05	   
963.50/297.05	   and mark the set of starting terms.
963.50/297.05	   
963.50/297.05	   We are left with following problem, upon which TcT provides the
963.50/297.05	   certificate MAYBE.
963.50/297.05	   
963.50/297.05	   Strict DPs:
963.50/297.05	     { eq^#(0(), 0()) -> c_1()
963.50/297.05	     , eq^#(0(), s(x)) -> c_2()
963.50/297.05	     , eq^#(s(x), 0()) -> c_3()
963.50/297.05	     , eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
963.50/297.05	     , or^#(true(), y) -> c_5()
963.50/297.05	     , or^#(false(), y) -> c_6(y)
963.50/297.05	     , and^#(true(), y) -> c_7(y)
963.50/297.05	     , and^#(false(), y) -> c_8()
963.50/297.05	     , size^#(empty()) -> c_9()
963.50/297.05	     , size^#(edge(x, y, i)) -> c_10(size^#(i))
963.50/297.05	     , le^#(0(), y) -> c_11()
963.50/297.05	     , le^#(s(x), 0()) -> c_12()
963.50/297.05	     , le^#(s(x), s(y)) -> c_13(le^#(x, y))
963.50/297.05	     , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
963.50/297.05	     , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j))
963.50/297.05	     , if1^#(true(), x, y, c, i, j) -> c_16()
963.50/297.05	     , if1^#(false(), x, y, c, i, j) ->
963.50/297.05	       c_17(if2^#(le(c, size(j)), x, y, c, i, j))
963.50/297.05	     , if2^#(true(), x, y, c, empty(), j) -> c_18()
963.50/297.05	     , if2^#(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.05	       c_19(or^#(if2(true(), x, y, c, i, j),
963.50/297.05	                 and(eq(x, u), reach(v, y, s(c), j, j))))
963.50/297.05	     , if2^#(false(), x, y, c, i, j) -> c_20() }
963.50/297.05	   Strict Trs:
963.50/297.05	     { eq(0(), 0()) -> true()
963.50/297.05	     , eq(0(), s(x)) -> false()
963.50/297.05	     , eq(s(x), 0()) -> false()
963.50/297.05	     , eq(s(x), s(y)) -> eq(x, y)
963.50/297.05	     , or(true(), y) -> true()
963.50/297.05	     , or(false(), y) -> y
963.50/297.05	     , and(true(), y) -> y
963.50/297.05	     , and(false(), y) -> false()
963.50/297.05	     , size(empty()) -> 0()
963.50/297.05	     , size(edge(x, y, i)) -> s(size(i))
963.50/297.05	     , le(0(), y) -> true()
963.50/297.05	     , le(s(x), 0()) -> false()
963.50/297.05	     , le(s(x), s(y)) -> le(x, y)
963.50/297.05	     , reachable(x, y, i) -> reach(x, y, 0(), i, i)
963.50/297.05	     , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
963.50/297.05	     , if1(true(), x, y, c, i, j) -> true()
963.50/297.05	     , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
963.50/297.05	     , if2(true(), x, y, c, empty(), j) -> false()
963.50/297.05	     , if2(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.05	       or(if2(true(), x, y, c, i, j),
963.50/297.05	          and(eq(x, u), reach(v, y, s(c), j, j)))
963.50/297.05	     , if2(false(), x, y, c, i, j) -> false() }
963.50/297.05	   Obligation:
963.50/297.05	     runtime complexity
963.50/297.05	   Answer:
963.50/297.05	     MAYBE
963.50/297.05	   
963.50/297.05	   We estimate the number of application of
963.50/297.05	   {1,2,3,5,8,9,11,12,16,18,20} by applications of
963.50/297.05	   Pre({1,2,3,5,8,9,11,12,16,18,20}) = {4,6,7,10,13,15,17,19}. Here
963.50/297.05	   rules are labeled as follows:
963.50/297.05	   
963.50/297.05	     DPs:
963.50/297.05	       { 1: eq^#(0(), 0()) -> c_1()
963.50/297.05	       , 2: eq^#(0(), s(x)) -> c_2()
963.50/297.05	       , 3: eq^#(s(x), 0()) -> c_3()
963.50/297.05	       , 4: eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
963.50/297.05	       , 5: or^#(true(), y) -> c_5()
963.50/297.05	       , 6: or^#(false(), y) -> c_6(y)
963.50/297.05	       , 7: and^#(true(), y) -> c_7(y)
963.50/297.05	       , 8: and^#(false(), y) -> c_8()
963.50/297.05	       , 9: size^#(empty()) -> c_9()
963.50/297.05	       , 10: size^#(edge(x, y, i)) -> c_10(size^#(i))
963.50/297.05	       , 11: le^#(0(), y) -> c_11()
963.50/297.05	       , 12: le^#(s(x), 0()) -> c_12()
963.50/297.05	       , 13: le^#(s(x), s(y)) -> c_13(le^#(x, y))
963.50/297.05	       , 14: reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
963.50/297.05	       , 15: reach^#(x, y, c, i, j) ->
963.50/297.05	             c_15(if1^#(eq(x, y), x, y, c, i, j))
963.50/297.05	       , 16: if1^#(true(), x, y, c, i, j) -> c_16()
963.50/297.05	       , 17: if1^#(false(), x, y, c, i, j) ->
963.50/297.05	             c_17(if2^#(le(c, size(j)), x, y, c, i, j))
963.50/297.05	       , 18: if2^#(true(), x, y, c, empty(), j) -> c_18()
963.50/297.06	       , 19: if2^#(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.06	             c_19(or^#(if2(true(), x, y, c, i, j),
963.50/297.06	                       and(eq(x, u), reach(v, y, s(c), j, j))))
963.50/297.06	       , 20: if2^#(false(), x, y, c, i, j) -> c_20() }
963.50/297.06	   
963.50/297.06	   We are left with following problem, upon which TcT provides the
963.50/297.06	   certificate MAYBE.
963.50/297.06	   
963.50/297.06	   Strict DPs:
963.50/297.06	     { eq^#(s(x), s(y)) -> c_4(eq^#(x, y))
963.50/297.06	     , or^#(false(), y) -> c_6(y)
963.50/297.06	     , and^#(true(), y) -> c_7(y)
963.50/297.06	     , size^#(edge(x, y, i)) -> c_10(size^#(i))
963.50/297.06	     , le^#(s(x), s(y)) -> c_13(le^#(x, y))
963.50/297.06	     , reachable^#(x, y, i) -> c_14(reach^#(x, y, 0(), i, i))
963.50/297.06	     , reach^#(x, y, c, i, j) -> c_15(if1^#(eq(x, y), x, y, c, i, j))
963.50/297.06	     , if1^#(false(), x, y, c, i, j) ->
963.50/297.06	       c_17(if2^#(le(c, size(j)), x, y, c, i, j))
963.50/297.06	     , if2^#(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.06	       c_19(or^#(if2(true(), x, y, c, i, j),
963.50/297.06	                 and(eq(x, u), reach(v, y, s(c), j, j)))) }
963.50/297.06	   Strict Trs:
963.50/297.06	     { eq(0(), 0()) -> true()
963.50/297.06	     , eq(0(), s(x)) -> false()
963.50/297.06	     , eq(s(x), 0()) -> false()
963.50/297.06	     , eq(s(x), s(y)) -> eq(x, y)
963.50/297.06	     , or(true(), y) -> true()
963.50/297.06	     , or(false(), y) -> y
963.50/297.06	     , and(true(), y) -> y
963.50/297.06	     , and(false(), y) -> false()
963.50/297.06	     , size(empty()) -> 0()
963.50/297.06	     , size(edge(x, y, i)) -> s(size(i))
963.50/297.06	     , le(0(), y) -> true()
963.50/297.06	     , le(s(x), 0()) -> false()
963.50/297.06	     , le(s(x), s(y)) -> le(x, y)
963.50/297.06	     , reachable(x, y, i) -> reach(x, y, 0(), i, i)
963.50/297.06	     , reach(x, y, c, i, j) -> if1(eq(x, y), x, y, c, i, j)
963.50/297.06	     , if1(true(), x, y, c, i, j) -> true()
963.50/297.06	     , if1(false(), x, y, c, i, j) -> if2(le(c, size(j)), x, y, c, i, j)
963.50/297.06	     , if2(true(), x, y, c, empty(), j) -> false()
963.50/297.06	     , if2(true(), x, y, c, edge(u, v, i), j) ->
963.50/297.06	       or(if2(true(), x, y, c, i, j),
963.50/297.06	          and(eq(x, u), reach(v, y, s(c), j, j)))
963.50/297.06	     , if2(false(), x, y, c, i, j) -> false() }
963.50/297.06	   Weak DPs:
963.50/297.06	     { eq^#(0(), 0()) -> c_1()
963.50/297.06	     , eq^#(0(), s(x)) -> c_2()
963.50/297.06	     , eq^#(s(x), 0()) -> c_3()
963.50/297.06	     , or^#(true(), y) -> c_5()
963.50/297.06	     , and^#(false(), y) -> c_8()
963.50/297.06	     , size^#(empty()) -> c_9()
963.50/297.06	     , le^#(0(), y) -> c_11()
963.50/297.06	     , le^#(s(x), 0()) -> c_12()
963.50/297.06	     , if1^#(true(), x, y, c, i, j) -> c_16()
963.50/297.06	     , if2^#(true(), x, y, c, empty(), j) -> c_18()
963.50/297.06	     , if2^#(false(), x, y, c, i, j) -> c_20() }
963.50/297.06	   Obligation:
963.50/297.06	     runtime complexity
963.50/297.06	   Answer:
963.50/297.06	     MAYBE
963.50/297.06	   
963.50/297.06	   Empty strict component of the problem is NOT empty.
963.50/297.06	
963.50/297.06	
963.50/297.06	Arrrr..
963.63/297.19	EOF