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