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