MAYBE
250.70/147.32	MAYBE
250.70/147.32	
250.70/147.32	We are left with following problem, upon which TcT provides the
250.70/147.32	certificate MAYBE.
250.70/147.32	
250.70/147.32	Strict Trs:
250.70/147.32	  { a__f(X1, X2, X3) -> f(X1, X2, X3)
250.70/147.32	  , a__f(b(), X, c()) -> a__f(X, a__c(), X)
250.70/147.32	  , a__c() -> b()
250.70/147.32	  , a__c() -> c()
250.70/147.32	  , mark(b()) -> b()
250.70/147.32	  , mark(c()) -> a__c()
250.70/147.32	  , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
250.70/147.32	Obligation:
250.70/147.32	  runtime complexity
250.70/147.32	Answer:
250.70/147.32	  MAYBE
250.70/147.32	
250.70/147.32	None of the processors succeeded.
250.70/147.32	
250.70/147.32	Details of failed attempt(s):
250.70/147.32	-----------------------------
250.70/147.32	1) 'Best' failed due to the following reason:
250.70/147.32	   
250.70/147.32	   None of the processors succeeded.
250.70/147.32	   
250.70/147.32	   Details of failed attempt(s):
250.70/147.32	   -----------------------------
250.70/147.32	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
250.70/147.32	      seconds)' failed due to the following reason:
250.70/147.32	      
250.70/147.32	      None of the processors succeeded.
250.70/147.32	      
250.70/147.32	      Details of failed attempt(s):
250.70/147.32	      -----------------------------
250.70/147.32	      1) 'empty' failed due to the following reason:
250.70/147.32	         
250.70/147.32	         Empty strict component of the problem is NOT empty.
250.70/147.32	      
250.70/147.32	      2) 'With Problem ...' failed due to the following reason:
250.70/147.32	         
250.70/147.32	         None of the processors succeeded.
250.70/147.32	         
250.70/147.32	         Details of failed attempt(s):
250.70/147.32	         -----------------------------
250.70/147.32	         1) 'empty' failed due to the following reason:
250.70/147.32	            
250.70/147.32	            Empty strict component of the problem is NOT empty.
250.70/147.32	         
250.70/147.32	         2) 'Fastest' failed due to the following reason:
250.70/147.32	            
250.70/147.32	            None of the processors succeeded.
250.70/147.32	            
250.70/147.32	            Details of failed attempt(s):
250.70/147.32	            -----------------------------
250.70/147.32	            1) 'With Problem ...' failed due to the following reason:
250.70/147.32	               
250.70/147.32	               None of the processors succeeded.
250.70/147.32	               
250.70/147.32	               Details of failed attempt(s):
250.70/147.32	               -----------------------------
250.70/147.32	               1) 'empty' failed due to the following reason:
250.70/147.32	                  
250.70/147.32	                  Empty strict component of the problem is NOT empty.
250.70/147.32	               
250.70/147.32	               2) 'With Problem ...' failed due to the following reason:
250.70/147.32	                  
250.70/147.32	                  None of the processors succeeded.
250.70/147.32	                  
250.70/147.32	                  Details of failed attempt(s):
250.70/147.32	                  -----------------------------
250.70/147.32	                  1) 'empty' failed due to the following reason:
250.70/147.32	                     
250.70/147.32	                     Empty strict component of the problem is NOT empty.
250.70/147.32	                  
250.70/147.32	                  2) 'With Problem ...' failed due to the following reason:
250.70/147.32	                     
250.70/147.32	                     None of the processors succeeded.
250.70/147.32	                     
250.70/147.32	                     Details of failed attempt(s):
250.70/147.32	                     -----------------------------
250.70/147.32	                     1) 'empty' failed due to the following reason:
250.70/147.32	                        
250.70/147.32	                        Empty strict component of the problem is NOT empty.
250.70/147.32	                     
250.70/147.32	                     2) 'With Problem ...' failed due to the following reason:
250.70/147.32	                        
250.70/147.32	                        Empty strict component of the problem is NOT empty.
250.70/147.32	                     
250.70/147.32	                  
250.70/147.32	               
250.70/147.32	            
250.70/147.32	            2) 'With Problem ...' failed due to the following reason:
250.70/147.32	               
250.70/147.32	               None of the processors succeeded.
250.70/147.32	               
250.70/147.32	               Details of failed attempt(s):
250.70/147.32	               -----------------------------
250.70/147.32	               1) 'empty' failed due to the following reason:
250.70/147.32	                  
250.70/147.32	                  Empty strict component of the problem is NOT empty.
250.70/147.32	               
250.70/147.32	               2) 'With Problem ...' failed due to the following reason:
250.70/147.32	                  
250.70/147.32	                  Empty strict component of the problem is NOT empty.
250.70/147.32	               
250.70/147.32	            
250.70/147.32	         
250.70/147.32	      
250.70/147.32	   
250.70/147.32	   2) 'Best' failed due to the following reason:
250.70/147.32	      
250.70/147.32	      None of the processors succeeded.
250.70/147.32	      
250.70/147.32	      Details of failed attempt(s):
250.70/147.32	      -----------------------------
250.70/147.32	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
250.70/147.32	         following reason:
250.70/147.32	         
250.70/147.32	         The processor is inapplicable, reason:
250.70/147.32	           Processor only applicable for innermost runtime complexity analysis
250.70/147.32	      
250.70/147.32	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
250.70/147.32	         to the following reason:
250.70/147.32	         
250.70/147.32	         The processor is inapplicable, reason:
250.70/147.32	           Processor only applicable for innermost runtime complexity analysis
250.70/147.32	      
250.70/147.32	   
250.70/147.32	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
250.70/147.32	      failed due to the following reason:
250.70/147.32	      
250.70/147.32	      None of the processors succeeded.
250.70/147.32	      
250.70/147.32	      Details of failed attempt(s):
250.70/147.32	      -----------------------------
250.70/147.32	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
250.70/147.32	         failed due to the following reason:
250.70/147.32	         
250.70/147.32	         match-boundness of the problem could not be verified.
250.70/147.32	      
250.70/147.32	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
250.70/147.32	         failed due to the following reason:
250.70/147.32	         
250.70/147.32	         match-boundness of the problem could not be verified.
250.70/147.32	      
250.70/147.32	   
250.70/147.32	
250.70/147.32	2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
250.70/147.32	   the following reason:
250.70/147.32	   
250.70/147.32	   We add the following weak dependency pairs:
250.70/147.32	   
250.70/147.32	   Strict DPs:
250.70/147.32	     { a__f^#(X1, X2, X3) -> c_1(X1, X2, X3)
250.70/147.32	     , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X))
250.70/147.32	     , a__c^#() -> c_3()
250.70/147.32	     , a__c^#() -> c_4()
250.70/147.32	     , mark^#(b()) -> c_5()
250.70/147.32	     , mark^#(c()) -> c_6(a__c^#())
250.70/147.32	     , mark^#(f(X1, X2, X3)) -> c_7(a__f^#(X1, mark(X2), X3)) }
250.70/147.32	   
250.70/147.32	   and mark the set of starting terms.
250.70/147.32	   
250.70/147.32	   We are left with following problem, upon which TcT provides the
250.70/147.32	   certificate MAYBE.
250.70/147.32	   
250.70/147.32	   Strict DPs:
250.70/147.32	     { a__f^#(X1, X2, X3) -> c_1(X1, X2, X3)
250.70/147.32	     , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X))
250.70/147.32	     , a__c^#() -> c_3()
250.70/147.32	     , a__c^#() -> c_4()
250.70/147.32	     , mark^#(b()) -> c_5()
250.70/147.32	     , mark^#(c()) -> c_6(a__c^#())
250.70/147.32	     , mark^#(f(X1, X2, X3)) -> c_7(a__f^#(X1, mark(X2), X3)) }
250.70/147.32	   Strict Trs:
250.70/147.32	     { a__f(X1, X2, X3) -> f(X1, X2, X3)
250.70/147.32	     , a__f(b(), X, c()) -> a__f(X, a__c(), X)
250.70/147.32	     , a__c() -> b()
250.70/147.32	     , a__c() -> c()
250.70/147.32	     , mark(b()) -> b()
250.70/147.32	     , mark(c()) -> a__c()
250.70/147.32	     , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
250.70/147.32	   Obligation:
250.70/147.32	     runtime complexity
250.70/147.32	   Answer:
250.70/147.32	     MAYBE
250.70/147.32	   
250.70/147.32	   We estimate the number of application of {3,4,5} by applications of
250.70/147.32	   Pre({3,4,5}) = {1,6}. Here rules are labeled as follows:
250.70/147.32	   
250.70/147.32	     DPs:
250.70/147.32	       { 1: a__f^#(X1, X2, X3) -> c_1(X1, X2, X3)
250.70/147.32	       , 2: a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X))
250.70/147.32	       , 3: a__c^#() -> c_3()
250.70/147.32	       , 4: a__c^#() -> c_4()
250.70/147.32	       , 5: mark^#(b()) -> c_5()
250.70/147.32	       , 6: mark^#(c()) -> c_6(a__c^#())
250.70/147.32	       , 7: mark^#(f(X1, X2, X3)) -> c_7(a__f^#(X1, mark(X2), X3)) }
250.70/147.32	   
250.70/147.32	   We are left with following problem, upon which TcT provides the
250.70/147.32	   certificate MAYBE.
250.70/147.32	   
250.70/147.32	   Strict DPs:
250.70/147.32	     { a__f^#(X1, X2, X3) -> c_1(X1, X2, X3)
250.70/147.32	     , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X))
250.70/147.32	     , mark^#(c()) -> c_6(a__c^#())
250.70/147.32	     , mark^#(f(X1, X2, X3)) -> c_7(a__f^#(X1, mark(X2), X3)) }
250.70/147.32	   Strict Trs:
250.70/147.32	     { a__f(X1, X2, X3) -> f(X1, X2, X3)
250.70/147.32	     , a__f(b(), X, c()) -> a__f(X, a__c(), X)
250.70/147.32	     , a__c() -> b()
250.70/147.32	     , a__c() -> c()
250.70/147.32	     , mark(b()) -> b()
250.70/147.32	     , mark(c()) -> a__c()
250.70/147.32	     , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
250.70/147.32	   Weak DPs:
250.70/147.32	     { a__c^#() -> c_3()
250.70/147.32	     , a__c^#() -> c_4()
250.70/147.32	     , mark^#(b()) -> c_5() }
250.70/147.32	   Obligation:
250.70/147.32	     runtime complexity
250.70/147.32	   Answer:
250.70/147.32	     MAYBE
250.70/147.32	   
250.70/147.32	   We estimate the number of application of {3} by applications of
250.70/147.32	   Pre({3}) = {1}. Here rules are labeled as follows:
250.70/147.32	   
250.70/147.32	     DPs:
250.70/147.32	       { 1: a__f^#(X1, X2, X3) -> c_1(X1, X2, X3)
250.70/147.32	       , 2: a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X))
250.70/147.32	       , 3: mark^#(c()) -> c_6(a__c^#())
250.70/147.32	       , 4: mark^#(f(X1, X2, X3)) -> c_7(a__f^#(X1, mark(X2), X3))
250.70/147.32	       , 5: a__c^#() -> c_3()
250.70/147.32	       , 6: a__c^#() -> c_4()
250.70/147.32	       , 7: mark^#(b()) -> c_5() }
250.70/147.32	   
250.70/147.32	   We are left with following problem, upon which TcT provides the
250.70/147.32	   certificate MAYBE.
250.70/147.32	   
250.70/147.32	   Strict DPs:
250.70/147.32	     { a__f^#(X1, X2, X3) -> c_1(X1, X2, X3)
250.70/147.32	     , a__f^#(b(), X, c()) -> c_2(a__f^#(X, a__c(), X))
250.70/147.32	     , mark^#(f(X1, X2, X3)) -> c_7(a__f^#(X1, mark(X2), X3)) }
250.70/147.32	   Strict Trs:
250.70/147.32	     { a__f(X1, X2, X3) -> f(X1, X2, X3)
250.70/147.32	     , a__f(b(), X, c()) -> a__f(X, a__c(), X)
250.70/147.32	     , a__c() -> b()
250.70/147.32	     , a__c() -> c()
250.70/147.32	     , mark(b()) -> b()
250.70/147.32	     , mark(c()) -> a__c()
250.70/147.32	     , mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3) }
250.70/147.32	   Weak DPs:
250.70/147.32	     { a__c^#() -> c_3()
250.70/147.32	     , a__c^#() -> c_4()
250.70/147.32	     , mark^#(b()) -> c_5()
250.70/147.32	     , mark^#(c()) -> c_6(a__c^#()) }
250.70/147.32	   Obligation:
250.70/147.32	     runtime complexity
250.70/147.32	   Answer:
250.70/147.32	     MAYBE
250.70/147.32	   
250.70/147.32	   Empty strict component of the problem is NOT empty.
250.70/147.32	
250.70/147.32	
250.70/147.32	Arrrr..
250.90/147.50	EOF