MAYBE
790.13/297.05	MAYBE
790.13/297.05	
790.13/297.05	We are left with following problem, upon which TcT provides the
790.13/297.05	certificate MAYBE.
790.13/297.05	
790.13/297.05	Strict Trs:
790.13/297.05	  { times(x, y) -> sum(generate(x, y))
790.13/297.05	  , sum(xs) -> sum2(xs, 0())
790.13/297.05	  , generate(x, y) -> gen(x, y, 0())
790.13/297.05	  , gen(x, y, z) -> if(ge(z, x), x, y, z)
790.13/297.05	  , if(true(), x, y, z) -> nil()
790.13/297.05	  , if(false(), x, y, z) -> cons(y, gen(x, y, s(z)))
790.13/297.05	  , ge(x, 0()) -> true()
790.13/297.05	  , ge(0(), s(y)) -> false()
790.13/297.05	  , ge(s(x), s(y)) -> ge(x, y)
790.13/297.05	  , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y)
790.13/297.05	  , ifsum(true(), b, xs, y) -> y
790.13/297.05	  , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y)
790.13/297.05	  , isNil(nil()) -> true()
790.13/297.05	  , isNil(cons(x, xs)) -> false()
790.13/297.05	  , isZero(0()) -> true()
790.13/297.05	  , isZero(s(0())) -> false()
790.13/297.05	  , isZero(s(s(x))) -> isZero(s(x))
790.13/297.05	  , head(nil()) -> error()
790.13/297.05	  , head(cons(x, xs)) -> x
790.13/297.05	  , ifsum2(true(), xs, y) -> sum2(tail(xs), y)
790.13/297.05	  , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y))
790.13/297.05	  , tail(nil()) -> nil()
790.13/297.05	  , tail(cons(x, xs)) -> xs
790.13/297.05	  , p(0()) -> s(s(0()))
790.13/297.05	  , p(s(0())) -> 0()
790.13/297.05	  , p(s(s(x))) -> s(p(s(x)))
790.13/297.05	  , a() -> c()
790.13/297.05	  , a() -> d() }
790.13/297.05	Obligation:
790.13/297.05	  runtime complexity
790.13/297.05	Answer:
790.13/297.05	  MAYBE
790.13/297.05	
790.13/297.05	None of the processors succeeded.
790.13/297.05	
790.13/297.05	Details of failed attempt(s):
790.13/297.05	-----------------------------
790.13/297.05	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
790.13/297.05	   following reason:
790.13/297.05	   
790.13/297.05	   Computation stopped due to timeout after 297.0 seconds.
790.13/297.05	
790.13/297.05	2) 'Best' failed due to the following reason:
790.13/297.05	   
790.13/297.05	   None of the processors succeeded.
790.13/297.05	   
790.13/297.05	   Details of failed attempt(s):
790.13/297.05	   -----------------------------
790.13/297.05	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
790.13/297.05	      seconds)' failed due to the following reason:
790.13/297.05	      
790.13/297.05	      Computation stopped due to timeout after 148.0 seconds.
790.13/297.05	   
790.13/297.05	   2) 'Best' failed due to the following reason:
790.13/297.05	      
790.13/297.05	      None of the processors succeeded.
790.13/297.05	      
790.13/297.05	      Details of failed attempt(s):
790.13/297.05	      -----------------------------
790.13/297.05	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
790.13/297.05	         following reason:
790.13/297.05	         
790.13/297.05	         The processor is inapplicable, reason:
790.13/297.05	           Processor only applicable for innermost runtime complexity analysis
790.13/297.05	      
790.13/297.05	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
790.13/297.05	         to the following reason:
790.13/297.05	         
790.13/297.05	         The processor is inapplicable, reason:
790.13/297.05	           Processor only applicable for innermost runtime complexity analysis
790.13/297.05	      
790.13/297.05	   
790.13/297.05	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
790.13/297.05	      failed due to the following reason:
790.13/297.05	      
790.13/297.05	      None of the processors succeeded.
790.13/297.05	      
790.13/297.05	      Details of failed attempt(s):
790.13/297.05	      -----------------------------
790.13/297.05	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
790.13/297.05	         failed due to the following reason:
790.13/297.05	         
790.13/297.05	         match-boundness of the problem could not be verified.
790.13/297.05	      
790.13/297.05	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
790.13/297.05	         failed due to the following reason:
790.13/297.05	         
790.13/297.05	         match-boundness of the problem could not be verified.
790.13/297.05	      
790.13/297.05	   
790.13/297.05	
790.13/297.05	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
790.13/297.05	   the following reason:
790.13/297.05	   
790.13/297.05	   We add the following weak dependency pairs:
790.13/297.05	   
790.13/297.05	   Strict DPs:
790.13/297.05	     { times^#(x, y) -> c_1(sum^#(generate(x, y)))
790.13/297.05	     , sum^#(xs) -> c_2(sum2^#(xs, 0()))
790.13/297.05	     , sum2^#(xs, y) ->
790.13/297.05	       c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y))
790.13/297.05	     , generate^#(x, y) -> c_3(gen^#(x, y, 0()))
790.13/297.05	     , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z))
790.13/297.05	     , if^#(true(), x, y, z) -> c_5()
790.13/297.05	     , if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z)))
790.13/297.05	     , ge^#(x, 0()) -> c_7()
790.13/297.05	     , ge^#(0(), s(y)) -> c_8()
790.13/297.05	     , ge^#(s(x), s(y)) -> c_9(ge^#(x, y))
790.13/297.05	     , ifsum^#(true(), b, xs, y) -> c_11(y)
790.13/297.05	     , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y))
790.13/297.05	     , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y))
790.13/297.05	     , ifsum2^#(false(), xs, y) ->
790.13/297.05	       c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)))
790.13/297.05	     , isNil^#(nil()) -> c_13()
790.13/297.05	     , isNil^#(cons(x, xs)) -> c_14()
790.13/297.05	     , isZero^#(0()) -> c_15()
790.13/297.05	     , isZero^#(s(0())) -> c_16()
790.13/297.05	     , isZero^#(s(s(x))) -> c_17(isZero^#(s(x)))
790.13/297.05	     , head^#(nil()) -> c_18()
790.13/297.05	     , head^#(cons(x, xs)) -> c_19(x)
790.13/297.05	     , tail^#(nil()) -> c_22()
790.13/297.05	     , tail^#(cons(x, xs)) -> c_23(xs)
790.13/297.05	     , p^#(0()) -> c_24()
790.13/297.05	     , p^#(s(0())) -> c_25()
790.13/297.05	     , p^#(s(s(x))) -> c_26(p^#(s(x)))
790.13/297.05	     , a^#() -> c_27()
790.13/297.05	     , a^#() -> c_28() }
790.13/297.05	   
790.13/297.05	   and mark the set of starting terms.
790.13/297.05	   
790.13/297.05	   We are left with following problem, upon which TcT provides the
790.13/297.05	   certificate MAYBE.
790.13/297.05	   
790.13/297.05	   Strict DPs:
790.13/297.05	     { times^#(x, y) -> c_1(sum^#(generate(x, y)))
790.13/297.05	     , sum^#(xs) -> c_2(sum2^#(xs, 0()))
790.13/297.05	     , sum2^#(xs, y) ->
790.13/297.05	       c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y))
790.13/297.05	     , generate^#(x, y) -> c_3(gen^#(x, y, 0()))
790.13/297.05	     , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z))
790.13/297.05	     , if^#(true(), x, y, z) -> c_5()
790.13/297.05	     , if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z)))
790.13/297.05	     , ge^#(x, 0()) -> c_7()
790.13/297.05	     , ge^#(0(), s(y)) -> c_8()
790.13/297.05	     , ge^#(s(x), s(y)) -> c_9(ge^#(x, y))
790.13/297.05	     , ifsum^#(true(), b, xs, y) -> c_11(y)
790.13/297.05	     , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y))
790.13/297.05	     , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y))
790.13/297.05	     , ifsum2^#(false(), xs, y) ->
790.13/297.05	       c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)))
790.13/297.05	     , isNil^#(nil()) -> c_13()
790.13/297.05	     , isNil^#(cons(x, xs)) -> c_14()
790.13/297.05	     , isZero^#(0()) -> c_15()
790.13/297.05	     , isZero^#(s(0())) -> c_16()
790.13/297.05	     , isZero^#(s(s(x))) -> c_17(isZero^#(s(x)))
790.13/297.05	     , head^#(nil()) -> c_18()
790.13/297.05	     , head^#(cons(x, xs)) -> c_19(x)
790.13/297.05	     , tail^#(nil()) -> c_22()
790.13/297.05	     , tail^#(cons(x, xs)) -> c_23(xs)
790.13/297.05	     , p^#(0()) -> c_24()
790.13/297.05	     , p^#(s(0())) -> c_25()
790.13/297.05	     , p^#(s(s(x))) -> c_26(p^#(s(x)))
790.13/297.05	     , a^#() -> c_27()
790.13/297.05	     , a^#() -> c_28() }
790.13/297.05	   Strict Trs:
790.13/297.05	     { times(x, y) -> sum(generate(x, y))
790.13/297.05	     , sum(xs) -> sum2(xs, 0())
790.13/297.05	     , generate(x, y) -> gen(x, y, 0())
790.13/297.05	     , gen(x, y, z) -> if(ge(z, x), x, y, z)
790.13/297.05	     , if(true(), x, y, z) -> nil()
790.13/297.05	     , if(false(), x, y, z) -> cons(y, gen(x, y, s(z)))
790.13/297.05	     , ge(x, 0()) -> true()
790.13/297.05	     , ge(0(), s(y)) -> false()
790.13/297.05	     , ge(s(x), s(y)) -> ge(x, y)
790.13/297.05	     , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y)
790.13/297.05	     , ifsum(true(), b, xs, y) -> y
790.13/297.05	     , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y)
790.13/297.05	     , isNil(nil()) -> true()
790.13/297.05	     , isNil(cons(x, xs)) -> false()
790.13/297.05	     , isZero(0()) -> true()
790.13/297.05	     , isZero(s(0())) -> false()
790.13/297.05	     , isZero(s(s(x))) -> isZero(s(x))
790.13/297.05	     , head(nil()) -> error()
790.13/297.05	     , head(cons(x, xs)) -> x
790.13/297.05	     , ifsum2(true(), xs, y) -> sum2(tail(xs), y)
790.13/297.05	     , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y))
790.13/297.05	     , tail(nil()) -> nil()
790.13/297.05	     , tail(cons(x, xs)) -> xs
790.13/297.05	     , p(0()) -> s(s(0()))
790.13/297.05	     , p(s(0())) -> 0()
790.13/297.05	     , p(s(s(x))) -> s(p(s(x)))
790.13/297.05	     , a() -> c()
790.13/297.05	     , a() -> d() }
790.13/297.05	   Obligation:
790.13/297.05	     runtime complexity
790.13/297.05	   Answer:
790.13/297.05	     MAYBE
790.13/297.05	   
790.13/297.05	   We estimate the number of application of
790.13/297.05	   {6,8,9,15,16,17,18,20,22,24,25,27,28} by applications of
790.13/297.05	   Pre({6,8,9,15,16,17,18,20,22,24,25,27,28}) =
790.13/297.05	   {5,7,10,11,19,21,23,26}. Here rules are labeled as follows:
790.13/297.05	   
790.13/297.05	     DPs:
790.13/297.05	       { 1: times^#(x, y) -> c_1(sum^#(generate(x, y)))
790.13/297.05	       , 2: sum^#(xs) -> c_2(sum2^#(xs, 0()))
790.13/297.05	       , 3: sum2^#(xs, y) ->
790.13/297.05	            c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y))
790.13/297.05	       , 4: generate^#(x, y) -> c_3(gen^#(x, y, 0()))
790.13/297.05	       , 5: gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z))
790.13/297.05	       , 6: if^#(true(), x, y, z) -> c_5()
790.13/297.05	       , 7: if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z)))
790.13/297.05	       , 8: ge^#(x, 0()) -> c_7()
790.13/297.05	       , 9: ge^#(0(), s(y)) -> c_8()
790.13/297.05	       , 10: ge^#(s(x), s(y)) -> c_9(ge^#(x, y))
790.13/297.05	       , 11: ifsum^#(true(), b, xs, y) -> c_11(y)
790.13/297.05	       , 12: ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y))
790.13/297.05	       , 13: ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y))
790.13/297.05	       , 14: ifsum2^#(false(), xs, y) ->
790.13/297.05	             c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)))
790.13/297.05	       , 15: isNil^#(nil()) -> c_13()
790.13/297.05	       , 16: isNil^#(cons(x, xs)) -> c_14()
790.13/297.05	       , 17: isZero^#(0()) -> c_15()
790.13/297.05	       , 18: isZero^#(s(0())) -> c_16()
790.13/297.05	       , 19: isZero^#(s(s(x))) -> c_17(isZero^#(s(x)))
790.13/297.05	       , 20: head^#(nil()) -> c_18()
790.13/297.05	       , 21: head^#(cons(x, xs)) -> c_19(x)
790.13/297.05	       , 22: tail^#(nil()) -> c_22()
790.13/297.05	       , 23: tail^#(cons(x, xs)) -> c_23(xs)
790.13/297.05	       , 24: p^#(0()) -> c_24()
790.13/297.05	       , 25: p^#(s(0())) -> c_25()
790.13/297.05	       , 26: p^#(s(s(x))) -> c_26(p^#(s(x)))
790.13/297.05	       , 27: a^#() -> c_27()
790.13/297.05	       , 28: a^#() -> c_28() }
790.13/297.05	   
790.13/297.05	   We are left with following problem, upon which TcT provides the
790.13/297.05	   certificate MAYBE.
790.13/297.05	   
790.13/297.05	   Strict DPs:
790.13/297.05	     { times^#(x, y) -> c_1(sum^#(generate(x, y)))
790.13/297.05	     , sum^#(xs) -> c_2(sum2^#(xs, 0()))
790.13/297.05	     , sum2^#(xs, y) ->
790.13/297.05	       c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y))
790.13/297.05	     , generate^#(x, y) -> c_3(gen^#(x, y, 0()))
790.13/297.05	     , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z))
790.13/297.05	     , if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z)))
790.13/297.05	     , ge^#(s(x), s(y)) -> c_9(ge^#(x, y))
790.13/297.05	     , ifsum^#(true(), b, xs, y) -> c_11(y)
790.13/297.05	     , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y))
790.13/297.05	     , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y))
790.13/297.05	     , ifsum2^#(false(), xs, y) ->
790.13/297.05	       c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)))
790.13/297.05	     , isZero^#(s(s(x))) -> c_17(isZero^#(s(x)))
790.13/297.05	     , head^#(cons(x, xs)) -> c_19(x)
790.13/297.05	     , tail^#(cons(x, xs)) -> c_23(xs)
790.13/297.05	     , p^#(s(s(x))) -> c_26(p^#(s(x))) }
790.13/297.05	   Strict Trs:
790.13/297.05	     { times(x, y) -> sum(generate(x, y))
790.13/297.05	     , sum(xs) -> sum2(xs, 0())
790.13/297.05	     , generate(x, y) -> gen(x, y, 0())
790.13/297.05	     , gen(x, y, z) -> if(ge(z, x), x, y, z)
790.13/297.05	     , if(true(), x, y, z) -> nil()
790.13/297.05	     , if(false(), x, y, z) -> cons(y, gen(x, y, s(z)))
790.13/297.05	     , ge(x, 0()) -> true()
790.13/297.05	     , ge(0(), s(y)) -> false()
790.13/297.05	     , ge(s(x), s(y)) -> ge(x, y)
790.13/297.05	     , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y)
790.13/297.05	     , ifsum(true(), b, xs, y) -> y
790.13/297.05	     , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y)
790.13/297.05	     , isNil(nil()) -> true()
790.13/297.05	     , isNil(cons(x, xs)) -> false()
790.13/297.05	     , isZero(0()) -> true()
790.13/297.05	     , isZero(s(0())) -> false()
790.13/297.05	     , isZero(s(s(x))) -> isZero(s(x))
790.13/297.05	     , head(nil()) -> error()
790.13/297.05	     , head(cons(x, xs)) -> x
790.13/297.05	     , ifsum2(true(), xs, y) -> sum2(tail(xs), y)
790.13/297.05	     , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y))
790.13/297.05	     , tail(nil()) -> nil()
790.13/297.05	     , tail(cons(x, xs)) -> xs
790.13/297.05	     , p(0()) -> s(s(0()))
790.13/297.05	     , p(s(0())) -> 0()
790.13/297.05	     , p(s(s(x))) -> s(p(s(x)))
790.13/297.05	     , a() -> c()
790.13/297.05	     , a() -> d() }
790.13/297.05	   Weak DPs:
790.13/297.05	     { if^#(true(), x, y, z) -> c_5()
790.13/297.05	     , ge^#(x, 0()) -> c_7()
790.13/297.05	     , ge^#(0(), s(y)) -> c_8()
790.13/297.05	     , isNil^#(nil()) -> c_13()
790.13/297.05	     , isNil^#(cons(x, xs)) -> c_14()
790.13/297.05	     , isZero^#(0()) -> c_15()
790.13/297.05	     , isZero^#(s(0())) -> c_16()
790.13/297.05	     , head^#(nil()) -> c_18()
790.13/297.05	     , tail^#(nil()) -> c_22()
790.13/297.05	     , p^#(0()) -> c_24()
790.13/297.05	     , p^#(s(0())) -> c_25()
790.13/297.05	     , a^#() -> c_27()
790.13/297.05	     , a^#() -> c_28() }
790.13/297.05	   Obligation:
790.13/297.05	     runtime complexity
790.13/297.05	   Answer:
790.13/297.05	     MAYBE
790.13/297.05	   
790.13/297.05	   Empty strict component of the problem is NOT empty.
790.13/297.05	
790.13/297.05	
790.13/297.05	Arrrr..
790.36/297.24	EOF