MAYBE
365.55/297.10	MAYBE
365.55/297.10	
365.55/297.10	We are left with following problem, upon which TcT provides the
365.55/297.10	certificate MAYBE.
365.55/297.10	
365.55/297.10	Strict Trs:
365.55/297.10	  { r(xs, ys, zs, nil()) -> xs
365.55/297.10	  , r(xs, nil(), zs, cons(w, ws)) ->
365.55/297.10	    r(xs, xs, cons(succ(zero()), zs), ws)
365.55/297.10	  , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
365.55/297.10	    r(xs, xs, cons(succ(zero()), nil()), ws)
365.55/297.10	  , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
365.55/297.10	    r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws))) }
365.55/297.10	Obligation:
365.55/297.10	  runtime complexity
365.55/297.10	Answer:
365.55/297.10	  MAYBE
365.55/297.10	
365.55/297.10	None of the processors succeeded.
365.55/297.10	
365.55/297.10	Details of failed attempt(s):
365.55/297.10	-----------------------------
365.55/297.10	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
365.55/297.10	   following reason:
365.55/297.10	   
365.55/297.10	   Computation stopped due to timeout after 297.0 seconds.
365.55/297.10	
365.55/297.10	2) 'Best' failed due to the following reason:
365.55/297.10	   
365.55/297.10	   None of the processors succeeded.
365.55/297.10	   
365.55/297.10	   Details of failed attempt(s):
365.55/297.10	   -----------------------------
365.55/297.10	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
365.55/297.10	      seconds)' failed due to the following reason:
365.55/297.10	      
365.55/297.10	      None of the processors succeeded.
365.55/297.10	      
365.55/297.10	      Details of failed attempt(s):
365.55/297.10	      -----------------------------
365.55/297.10	      1) 'empty' failed due to the following reason:
365.55/297.10	         
365.55/297.10	         Empty strict component of the problem is NOT empty.
365.55/297.10	      
365.55/297.10	      2) 'With Problem ...' failed due to the following reason:
365.55/297.10	         
365.55/297.10	         None of the processors succeeded.
365.55/297.10	         
365.55/297.10	         Details of failed attempt(s):
365.55/297.10	         -----------------------------
365.55/297.10	         1) 'empty' failed due to the following reason:
365.55/297.10	            
365.55/297.10	            Empty strict component of the problem is NOT empty.
365.55/297.10	         
365.55/297.10	         2) 'Fastest' failed due to the following reason:
365.55/297.10	            
365.55/297.10	            None of the processors succeeded.
365.55/297.10	            
365.55/297.10	            Details of failed attempt(s):
365.55/297.10	            -----------------------------
365.55/297.10	            1) 'With Problem ...' failed due to the following reason:
365.55/297.10	               
365.55/297.10	               None of the processors succeeded.
365.55/297.10	               
365.55/297.10	               Details of failed attempt(s):
365.55/297.10	               -----------------------------
365.55/297.10	               1) 'empty' failed due to the following reason:
365.55/297.10	                  
365.55/297.10	                  Empty strict component of the problem is NOT empty.
365.55/297.10	               
365.55/297.10	               2) 'With Problem ...' failed due to the following reason:
365.55/297.10	                  
365.55/297.10	                  None of the processors succeeded.
365.55/297.10	                  
365.55/297.10	                  Details of failed attempt(s):
365.55/297.10	                  -----------------------------
365.55/297.10	                  1) 'empty' failed due to the following reason:
365.55/297.10	                     
365.55/297.10	                     Empty strict component of the problem is NOT empty.
365.55/297.10	                  
365.55/297.10	                  2) 'With Problem ...' failed due to the following reason:
365.55/297.10	                     
365.55/297.10	                     None of the processors succeeded.
365.55/297.10	                     
365.55/297.10	                     Details of failed attempt(s):
365.55/297.10	                     -----------------------------
365.55/297.10	                     1) 'empty' failed due to the following reason:
365.55/297.10	                        
365.55/297.10	                        Empty strict component of the problem is NOT empty.
365.55/297.10	                     
365.55/297.10	                     2) 'With Problem ...' failed due to the following reason:
365.55/297.10	                        
365.55/297.10	                        Empty strict component of the problem is NOT empty.
365.55/297.10	                     
365.55/297.10	                  
365.55/297.10	               
365.55/297.10	            
365.55/297.10	            2) 'With Problem ...' failed due to the following reason:
365.55/297.10	               
365.55/297.10	               None of the processors succeeded.
365.55/297.10	               
365.55/297.10	               Details of failed attempt(s):
365.55/297.10	               -----------------------------
365.55/297.10	               1) 'empty' failed due to the following reason:
365.55/297.10	                  
365.55/297.10	                  Empty strict component of the problem is NOT empty.
365.55/297.10	               
365.55/297.10	               2) 'With Problem ...' failed due to the following reason:
365.55/297.10	                  
365.55/297.10	                  Empty strict component of the problem is NOT empty.
365.55/297.10	               
365.55/297.10	            
365.55/297.10	         
365.55/297.10	      
365.55/297.10	   
365.55/297.10	   2) 'Best' failed due to the following reason:
365.55/297.10	      
365.55/297.10	      None of the processors succeeded.
365.55/297.10	      
365.55/297.10	      Details of failed attempt(s):
365.55/297.10	      -----------------------------
365.55/297.10	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
365.55/297.10	         following reason:
365.55/297.10	         
365.55/297.10	         The processor is inapplicable, reason:
365.55/297.10	           Processor only applicable for innermost runtime complexity analysis
365.55/297.10	      
365.55/297.10	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
365.55/297.10	         to the following reason:
365.55/297.10	         
365.55/297.10	         The processor is inapplicable, reason:
365.55/297.10	           Processor only applicable for innermost runtime complexity analysis
365.55/297.10	      
365.55/297.10	   
365.55/297.10	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
365.55/297.10	      failed due to the following reason:
365.55/297.10	      
365.55/297.10	      None of the processors succeeded.
365.55/297.10	      
365.55/297.10	      Details of failed attempt(s):
365.55/297.10	      -----------------------------
365.55/297.10	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
365.55/297.10	         failed due to the following reason:
365.55/297.10	         
365.55/297.10	         match-boundness of the problem could not be verified.
365.55/297.10	      
365.55/297.10	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
365.55/297.10	         failed due to the following reason:
365.55/297.10	         
365.55/297.10	         match-boundness of the problem could not be verified.
365.55/297.10	      
365.55/297.10	   
365.55/297.10	
365.55/297.10	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
365.55/297.10	   the following reason:
365.55/297.10	   
365.55/297.10	   We add the following weak dependency pairs:
365.55/297.10	   
365.55/297.10	   Strict DPs:
365.55/297.10	     { r^#(xs, ys, zs, nil()) -> c_1(xs)
365.55/297.10	     , r^#(xs, nil(), zs, cons(w, ws)) ->
365.55/297.10	       c_2(r^#(xs, xs, cons(succ(zero()), zs), ws))
365.55/297.10	     , r^#(xs, cons(y, ys), nil(), cons(w, ws)) ->
365.55/297.10	       c_3(r^#(xs, xs, cons(succ(zero()), nil()), ws))
365.55/297.10	     , r^#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
365.55/297.10	       c_4(r^#(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))) }
365.55/297.10	   
365.55/297.10	   and mark the set of starting terms.
365.55/297.10	   
365.55/297.10	   We are left with following problem, upon which TcT provides the
365.55/297.10	   certificate MAYBE.
365.55/297.10	   
365.55/297.10	   Strict DPs:
365.55/297.10	     { r^#(xs, ys, zs, nil()) -> c_1(xs)
365.55/297.10	     , r^#(xs, nil(), zs, cons(w, ws)) ->
365.55/297.10	       c_2(r^#(xs, xs, cons(succ(zero()), zs), ws))
365.55/297.10	     , r^#(xs, cons(y, ys), nil(), cons(w, ws)) ->
365.55/297.10	       c_3(r^#(xs, xs, cons(succ(zero()), nil()), ws))
365.55/297.10	     , r^#(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
365.55/297.10	       c_4(r^#(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))) }
365.55/297.10	   Strict Trs:
365.55/297.10	     { r(xs, ys, zs, nil()) -> xs
365.55/297.10	     , r(xs, nil(), zs, cons(w, ws)) ->
365.55/297.10	       r(xs, xs, cons(succ(zero()), zs), ws)
365.55/297.10	     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
365.55/297.10	       r(xs, xs, cons(succ(zero()), nil()), ws)
365.55/297.10	     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
365.55/297.10	       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws))) }
365.55/297.10	   Obligation:
365.55/297.10	     runtime complexity
365.55/297.10	   Answer:
365.55/297.10	     MAYBE
365.55/297.10	   
365.55/297.10	   Empty strict component of the problem is NOT empty.
365.55/297.10	
365.55/297.10	
365.55/297.10	Arrrr..
365.55/297.15	EOF