MAYBE
967.69/297.04	MAYBE
967.69/297.04	
967.69/297.04	We are left with following problem, upon which TcT provides the
967.69/297.04	certificate MAYBE.
967.69/297.04	
967.69/297.04	Strict Trs:
967.69/297.04	  { isEmpty(cons(x, xs)) -> false()
967.69/297.04	  , isEmpty(nil()) -> true()
967.69/297.04	  , isZero(0()) -> true()
967.69/297.04	  , isZero(s(x)) -> false()
967.69/297.04	  , head(cons(x, xs)) -> x
967.69/297.04	  , tail(cons(x, xs)) -> xs
967.69/297.04	  , tail(nil()) -> nil()
967.69/297.04	  , append(cons(y, ys), x) -> cons(y, append(ys, x))
967.69/297.04	  , append(nil(), x) -> cons(x, nil())
967.69/297.04	  , p(0()) -> 0()
967.69/297.04	  , p(s(0())) -> 0()
967.69/297.04	  , p(s(s(x))) -> s(p(s(x)))
967.69/297.04	  , inc(0()) -> s(0())
967.69/297.04	  , inc(s(x)) -> s(inc(x))
967.69/297.04	  , addLists(xs, ys, zs) ->
967.69/297.04	    if(isEmpty(xs),
967.69/297.04	       isEmpty(ys),
967.69/297.04	       isZero(head(xs)),
967.69/297.04	       tail(xs),
967.69/297.04	       tail(ys),
967.69/297.04	       cons(p(head(xs)), tail(xs)),
967.69/297.04	       cons(inc(head(ys)), tail(ys)),
967.69/297.04	       zs,
967.69/297.04	       append(zs, head(ys)))
967.69/297.04	  , if(false(), false(), false(), xs, ys, xs2, ys2, zs, zs2) ->
967.69/297.04	    addLists(xs2, ys2, zs)
967.69/297.04	  , if(false(), false(), true(), xs, ys, xs2, ys2, zs, zs2) ->
967.69/297.04	    addLists(xs, ys, zs2)
967.69/297.04	  , if(false(), true(), b, xs, ys, xs2, ys2, zs, zs2) ->
967.69/297.04	    differentLengthError()
967.69/297.04	  , if(true(), false(), b, xs, ys, xs2, ys2, zs, zs2) ->
967.69/297.04	    differentLengthError()
967.69/297.04	  , if(true(), true(), b, xs, ys, xs2, ys2, zs, zs2) -> zs
967.69/297.04	  , addList(xs, ys) -> addLists(xs, ys, nil()) }
967.69/297.04	Obligation:
967.69/297.04	  innermost runtime complexity
967.69/297.04	Answer:
967.69/297.04	  MAYBE
967.69/297.04	
967.69/297.04	None of the processors succeeded.
967.69/297.04	
967.69/297.04	Details of failed attempt(s):
967.69/297.04	-----------------------------
967.69/297.04	1) 'empty' failed due to the following reason:
967.69/297.04	   
967.69/297.04	   Empty strict component of the problem is NOT empty.
967.69/297.04	
967.69/297.04	2) 'Best' failed due to the following reason:
967.69/297.04	   
967.69/297.04	   None of the processors succeeded.
967.69/297.04	   
967.69/297.04	   Details of failed attempt(s):
967.69/297.04	   -----------------------------
967.69/297.04	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
967.69/297.04	      following reason:
967.69/297.04	      
967.69/297.04	      Computation stopped due to timeout after 297.0 seconds.
967.69/297.04	   
967.69/297.04	   2) 'Best' failed due to the following reason:
967.69/297.04	      
967.69/297.04	      None of the processors succeeded.
967.69/297.04	      
967.69/297.04	      Details of failed attempt(s):
967.69/297.04	      -----------------------------
967.69/297.04	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
967.69/297.04	         seconds)' failed due to the following reason:
967.69/297.04	         
967.69/297.04	         Computation stopped due to timeout after 148.0 seconds.
967.69/297.04	      
967.69/297.04	      2) 'Best' failed due to the following reason:
967.69/297.04	         
967.69/297.04	         None of the processors succeeded.
967.69/297.04	         
967.69/297.04	         Details of failed attempt(s):
967.69/297.04	         -----------------------------
967.69/297.04	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
967.69/297.04	            following reason:
967.69/297.04	            
967.69/297.04	            The input cannot be shown compatible
967.69/297.04	         
967.69/297.04	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
967.69/297.04	            to the following reason:
967.69/297.04	            
967.69/297.04	            The input cannot be shown compatible
967.69/297.04	         
967.69/297.04	      
967.69/297.04	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
967.69/297.04	         failed due to the following reason:
967.69/297.04	         
967.69/297.04	         None of the processors succeeded.
967.69/297.04	         
967.69/297.04	         Details of failed attempt(s):
967.69/297.04	         -----------------------------
967.69/297.04	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
967.69/297.04	            failed due to the following reason:
967.69/297.04	            
967.69/297.04	            match-boundness of the problem could not be verified.
967.69/297.04	         
967.69/297.04	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
967.69/297.04	            failed due to the following reason:
967.69/297.04	            
967.69/297.04	            match-boundness of the problem could not be verified.
967.69/297.04	         
967.69/297.04	      
967.69/297.04	   
967.69/297.04	
967.69/297.04	
967.69/297.04	Arrrr..
968.27/297.60	EOF