MAYBE
1113.62/297.09	MAYBE
1113.62/297.09	
1113.62/297.09	We are left with following problem, upon which TcT provides the
1113.62/297.09	certificate MAYBE.
1113.62/297.09	
1113.62/297.09	Strict Trs:
1113.62/297.09	  { a__zeros() -> cons(0(), zeros())
1113.62/297.09	  , a__zeros() -> zeros()
1113.62/297.09	  , a__U11(X1, X2) -> U11(X1, X2)
1113.62/297.09	  , a__U11(tt(), L) -> s(a__length(mark(L)))
1113.62/297.09	  , a__length(X) -> length(X)
1113.62/297.09	  , a__length(cons(N, L)) ->
1113.62/297.09	    a__U11(a__and(a__isNatList(L), isNat(N)), L)
1113.62/297.09	  , a__length(nil()) -> 0()
1113.62/297.09	  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
1113.62/297.09	  , mark(0()) -> 0()
1113.62/297.09	  , mark(zeros()) -> a__zeros()
1113.62/297.09	  , mark(tt()) -> tt()
1113.62/297.09	  , mark(s(X)) -> s(mark(X))
1113.62/297.09	  , mark(length(X)) -> a__length(mark(X))
1113.62/297.09	  , mark(isNatIList(X)) -> a__isNatIList(X)
1113.62/297.09	  , mark(nil()) -> nil()
1113.62/297.09	  , mark(isNatList(X)) -> a__isNatList(X)
1113.62/297.09	  , mark(isNat(X)) -> a__isNat(X)
1113.62/297.09	  , mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
1113.62/297.09	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
1113.62/297.09	  , a__and(X1, X2) -> and(X1, X2)
1113.62/297.09	  , a__and(tt(), X) -> mark(X)
1113.62/297.09	  , a__isNat(X) -> isNat(X)
1113.62/297.09	  , a__isNat(0()) -> tt()
1113.62/297.09	  , a__isNat(s(V1)) -> a__isNat(V1)
1113.62/297.09	  , a__isNat(length(V1)) -> a__isNatList(V1)
1113.62/297.09	  , a__isNatList(X) -> isNatList(X)
1113.62/297.09	  , a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
1113.62/297.09	  , a__isNatList(nil()) -> tt()
1113.62/297.09	  , a__isNatIList(V) -> a__isNatList(V)
1113.62/297.09	  , a__isNatIList(X) -> isNatIList(X)
1113.62/297.09	  , a__isNatIList(cons(V1, V2)) ->
1113.62/297.09	    a__and(a__isNat(V1), isNatIList(V2))
1113.62/297.09	  , a__isNatIList(zeros()) -> tt() }
1113.62/297.09	Obligation:
1113.62/297.09	  innermost runtime complexity
1113.62/297.09	Answer:
1113.62/297.09	  MAYBE
1113.62/297.09	
1113.62/297.09	None of the processors succeeded.
1113.62/297.09	
1113.62/297.09	Details of failed attempt(s):
1113.62/297.09	-----------------------------
1113.62/297.09	1) 'empty' failed due to the following reason:
1113.62/297.09	   
1113.62/297.09	   Empty strict component of the problem is NOT empty.
1113.62/297.09	
1113.62/297.09	2) 'Best' failed due to the following reason:
1113.62/297.09	   
1113.62/297.09	   None of the processors succeeded.
1113.62/297.09	   
1113.62/297.09	   Details of failed attempt(s):
1113.62/297.09	   -----------------------------
1113.62/297.09	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1113.62/297.09	      following reason:
1113.62/297.09	      
1113.62/297.09	      Computation stopped due to timeout after 297.0 seconds.
1113.62/297.09	   
1113.62/297.09	   2) 'Best' failed due to the following reason:
1113.62/297.09	      
1113.62/297.09	      None of the processors succeeded.
1113.62/297.09	      
1113.62/297.09	      Details of failed attempt(s):
1113.62/297.09	      -----------------------------
1113.62/297.09	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1113.62/297.09	         seconds)' failed due to the following reason:
1113.62/297.09	         
1113.62/297.09	         Computation stopped due to timeout after 148.0 seconds.
1113.62/297.09	      
1113.62/297.09	      2) 'Best' failed due to the following reason:
1113.62/297.09	         
1113.62/297.09	         None of the processors succeeded.
1113.62/297.09	         
1113.62/297.09	         Details of failed attempt(s):
1113.62/297.09	         -----------------------------
1113.62/297.09	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1113.62/297.09	            following reason:
1113.62/297.09	            
1113.62/297.09	            The input cannot be shown compatible
1113.62/297.09	         
1113.62/297.09	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1113.62/297.09	            to the following reason:
1113.62/297.09	            
1113.62/297.09	            The input cannot be shown compatible
1113.62/297.09	         
1113.62/297.09	      
1113.62/297.09	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1113.62/297.09	         failed due to the following reason:
1113.62/297.09	         
1113.62/297.09	         None of the processors succeeded.
1113.62/297.09	         
1113.62/297.09	         Details of failed attempt(s):
1113.62/297.09	         -----------------------------
1113.62/297.09	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
1113.62/297.09	            failed due to the following reason:
1113.62/297.09	            
1113.62/297.09	            match-boundness of the problem could not be verified.
1113.62/297.09	         
1113.62/297.09	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1113.62/297.09	            failed due to the following reason:
1113.62/297.09	            
1113.62/297.09	            match-boundness of the problem could not be verified.
1113.62/297.09	         
1113.62/297.09	      
1113.62/297.09	   
1113.62/297.09	
1113.62/297.09	
1113.62/297.09	Arrrr..
1113.98/297.17	EOF