MAYBE
788.75/297.01	MAYBE
788.75/297.01	
788.75/297.01	We are left with following problem, upon which TcT provides the
788.75/297.01	certificate MAYBE.
788.75/297.01	
788.75/297.01	Strict Trs:
788.75/297.01	  { f(a(), g(y)) -> g(g(y))
788.75/297.01	  , f(g(x), a()) -> f(x, g(a()))
788.75/297.01	  , f(g(x), g(y)) -> h(g(y), x, g(y))
788.75/297.01	  , h(a(), y, z) -> z
788.75/297.01	  , h(g(x), y, z) -> f(y, h(x, y, z)) }
788.75/297.01	Obligation:
788.75/297.01	  runtime complexity
788.75/297.01	Answer:
788.75/297.01	  MAYBE
788.75/297.01	
788.75/297.01	None of the processors succeeded.
788.75/297.01	
788.75/297.01	Details of failed attempt(s):
788.75/297.01	-----------------------------
788.75/297.01	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
788.75/297.01	   following reason:
788.75/297.01	   
788.75/297.01	   Computation stopped due to timeout after 297.0 seconds.
788.75/297.01	
788.75/297.01	2) 'Best' failed due to the following reason:
788.75/297.01	   
788.75/297.01	   None of the processors succeeded.
788.75/297.01	   
788.75/297.01	   Details of failed attempt(s):
788.75/297.01	   -----------------------------
788.75/297.01	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
788.75/297.01	      seconds)' failed due to the following reason:
788.75/297.01	      
788.75/297.01	      The weightgap principle applies (using the following nonconstant
788.75/297.01	      growth matrix-interpretation)
788.75/297.01	      
788.75/297.01	      The following argument positions are usable:
788.75/297.01	        Uargs(f) = {2}
788.75/297.01	      
788.75/297.01	      TcT has computed the following matrix interpretation satisfying
788.75/297.01	      not(EDA) and not(IDA(1)).
788.75/297.01	      
788.75/297.01	            [f](x1, x2) = [1] x2 + [0]
788.75/297.01	                                      
788.75/297.01	                    [a] = [5]         
788.75/297.01	                                      
788.75/297.01	                [g](x1) = [0]         
788.75/297.01	                                      
788.75/297.01	        [h](x1, x2, x3) = [1] x3 + [0]
788.75/297.01	      
788.75/297.01	      The order satisfies the following ordering constraints:
788.75/297.01	      
788.75/297.01	         [f(a(), g(y))] =  [0]               
788.75/297.01	                        >= [0]               
788.75/297.01	                        =  [g(g(y))]         
788.75/297.01	                                             
788.75/297.01	         [f(g(x), a())] =  [5]               
788.75/297.01	                        >  [0]               
788.75/297.01	                        =  [f(x, g(a()))]    
788.75/297.01	                                             
788.75/297.01	        [f(g(x), g(y))] =  [0]               
788.75/297.01	                        >= [0]               
788.75/297.01	                        =  [h(g(y), x, g(y))]
788.75/297.01	                                             
788.75/297.01	         [h(a(), y, z)] =  [1] z + [0]       
788.75/297.01	                        >= [1] z + [0]       
788.75/297.01	                        =  [z]               
788.75/297.01	                                             
788.75/297.01	        [h(g(x), y, z)] =  [1] z + [0]       
788.75/297.01	                        >= [1] z + [0]       
788.75/297.01	                        =  [f(y, h(x, y, z))]
788.75/297.01	                                             
788.75/297.01	      
788.75/297.01	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
788.75/297.01	      
788.75/297.01	      We are left with following problem, upon which TcT provides the
788.75/297.01	      certificate MAYBE.
788.75/297.01	      
788.75/297.01	      Strict Trs:
788.75/297.01	        { f(a(), g(y)) -> g(g(y))
788.75/297.01	        , f(g(x), g(y)) -> h(g(y), x, g(y))
788.75/297.01	        , h(a(), y, z) -> z
788.75/297.01	        , h(g(x), y, z) -> f(y, h(x, y, z)) }
788.75/297.01	      Weak Trs: { f(g(x), a()) -> f(x, g(a())) }
788.75/297.01	      Obligation:
788.75/297.01	        runtime complexity
788.75/297.01	      Answer:
788.75/297.01	        MAYBE
788.75/297.01	      
788.75/297.01	      The weightgap principle applies (using the following nonconstant
788.75/297.01	      growth matrix-interpretation)
788.75/297.01	      
788.75/297.01	      The following argument positions are usable:
788.75/297.01	        Uargs(f) = {2}
788.75/297.01	      
788.75/297.01	      TcT has computed the following matrix interpretation satisfying
788.75/297.01	      not(EDA) and not(IDA(1)).
788.75/297.01	      
788.75/297.01	            [f](x1, x2) = [1] x2 + [1]
788.75/297.01	                                      
788.75/297.01	                    [a] = [7]         
788.75/297.01	                                      
788.75/297.01	                [g](x1) = [0]         
788.75/297.01	                                      
788.75/297.01	        [h](x1, x2, x3) = [1] x3 + [0]
788.75/297.01	      
788.75/297.01	      The order satisfies the following ordering constraints:
788.75/297.01	      
788.75/297.01	         [f(a(), g(y))] =  [1]               
788.75/297.01	                        >  [0]               
788.75/297.01	                        =  [g(g(y))]         
788.75/297.01	                                             
788.75/297.01	         [f(g(x), a())] =  [8]               
788.75/297.01	                        >  [1]               
788.75/297.01	                        =  [f(x, g(a()))]    
788.75/297.01	                                             
788.75/297.01	        [f(g(x), g(y))] =  [1]               
788.75/297.01	                        >  [0]               
788.75/297.01	                        =  [h(g(y), x, g(y))]
788.75/297.01	                                             
788.75/297.01	         [h(a(), y, z)] =  [1] z + [0]       
788.75/297.01	                        >= [1] z + [0]       
788.75/297.01	                        =  [z]               
788.75/297.01	                                             
788.75/297.01	        [h(g(x), y, z)] =  [1] z + [0]       
788.75/297.01	                        ?  [1] z + [1]       
788.75/297.01	                        =  [f(y, h(x, y, z))]
788.75/297.01	                                             
788.75/297.01	      
788.75/297.01	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
788.75/297.01	      
788.75/297.01	      We are left with following problem, upon which TcT provides the
788.75/297.01	      certificate MAYBE.
788.75/297.01	      
788.75/297.01	      Strict Trs:
788.75/297.01	        { h(a(), y, z) -> z
788.75/297.01	        , h(g(x), y, z) -> f(y, h(x, y, z)) }
788.75/297.01	      Weak Trs:
788.75/297.01	        { f(a(), g(y)) -> g(g(y))
788.75/297.01	        , f(g(x), a()) -> f(x, g(a()))
788.75/297.01	        , f(g(x), g(y)) -> h(g(y), x, g(y)) }
788.75/297.01	      Obligation:
788.75/297.01	        runtime complexity
788.75/297.01	      Answer:
788.75/297.01	        MAYBE
788.75/297.01	      
788.75/297.01	      The weightgap principle applies (using the following nonconstant
788.75/297.01	      growth matrix-interpretation)
788.75/297.01	      
788.75/297.01	      The following argument positions are usable:
788.75/297.01	        Uargs(f) = {2}
788.75/297.01	      
788.75/297.01	      TcT has computed the following matrix interpretation satisfying
788.75/297.01	      not(EDA) and not(IDA(1)).
788.75/297.01	      
788.75/297.01	            [f](x1, x2) = [1] x2 + [4]
788.75/297.01	                                      
788.75/297.01	                    [a] = [5]         
788.75/297.01	                                      
788.75/297.01	                [g](x1) = [4]         
788.75/297.01	                                      
788.75/297.01	        [h](x1, x2, x3) = [1] x3 + [4]
788.75/297.01	      
788.75/297.01	      The order satisfies the following ordering constraints:
788.75/297.01	      
788.75/297.01	         [f(a(), g(y))] =  [8]               
788.75/297.01	                        >  [4]               
788.75/297.01	                        =  [g(g(y))]         
788.75/297.01	                                             
788.75/297.01	         [f(g(x), a())] =  [9]               
788.75/297.01	                        >  [8]               
788.75/297.01	                        =  [f(x, g(a()))]    
788.75/297.01	                                             
788.75/297.01	        [f(g(x), g(y))] =  [8]               
788.75/297.01	                        >= [8]               
788.75/297.01	                        =  [h(g(y), x, g(y))]
788.75/297.01	                                             
788.75/297.01	         [h(a(), y, z)] =  [1] z + [4]       
788.75/297.01	                        >  [1] z + [0]       
788.75/297.01	                        =  [z]               
788.75/297.01	                                             
788.75/297.01	        [h(g(x), y, z)] =  [1] z + [4]       
788.75/297.01	                        ?  [1] z + [8]       
788.75/297.01	                        =  [f(y, h(x, y, z))]
788.75/297.01	                                             
788.75/297.01	      
788.75/297.01	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
788.75/297.01	      
788.75/297.01	      We are left with following problem, upon which TcT provides the
788.75/297.01	      certificate MAYBE.
788.75/297.01	      
788.75/297.01	      Strict Trs: { h(g(x), y, z) -> f(y, h(x, y, z)) }
788.75/297.01	      Weak Trs:
788.75/297.01	        { f(a(), g(y)) -> g(g(y))
788.75/297.01	        , f(g(x), a()) -> f(x, g(a()))
788.75/297.01	        , f(g(x), g(y)) -> h(g(y), x, g(y))
788.75/297.01	        , h(a(), y, z) -> z }
788.75/297.01	      Obligation:
788.75/297.01	        runtime complexity
788.75/297.01	      Answer:
788.75/297.01	        MAYBE
788.75/297.01	      
788.75/297.01	      None of the processors succeeded.
788.75/297.01	      
788.75/297.01	      Details of failed attempt(s):
788.75/297.01	      -----------------------------
788.75/297.01	      1) 'empty' failed due to the following reason:
788.75/297.01	         
788.75/297.01	         Empty strict component of the problem is NOT empty.
788.75/297.01	      
788.75/297.01	      2) 'With Problem ...' failed due to the following reason:
788.75/297.01	         
788.75/297.01	         None of the processors succeeded.
788.75/297.01	         
788.75/297.01	         Details of failed attempt(s):
788.75/297.01	         -----------------------------
788.75/297.01	         1) 'empty' failed due to the following reason:
788.75/297.01	            
788.75/297.01	            Empty strict component of the problem is NOT empty.
788.75/297.01	         
788.75/297.01	         2) 'Fastest' failed due to the following reason:
788.75/297.01	            
788.75/297.01	            None of the processors succeeded.
788.75/297.01	            
788.75/297.01	            Details of failed attempt(s):
788.75/297.01	            -----------------------------
788.75/297.01	            1) 'With Problem ...' failed due to the following reason:
788.75/297.01	               
788.75/297.01	               None of the processors succeeded.
788.75/297.01	               
788.75/297.01	               Details of failed attempt(s):
788.75/297.02	               -----------------------------
788.75/297.02	               1) 'empty' failed due to the following reason:
788.75/297.02	                  
788.75/297.02	                  Empty strict component of the problem is NOT empty.
788.75/297.02	               
788.75/297.02	               2) 'With Problem ...' failed due to the following reason:
788.75/297.02	                  
788.75/297.02	                  Empty strict component of the problem is NOT empty.
788.75/297.02	               
788.75/297.02	            
788.75/297.02	            2) 'With Problem ...' failed due to the following reason:
788.75/297.02	               
788.75/297.02	               None of the processors succeeded.
788.75/297.02	               
788.75/297.02	               Details of failed attempt(s):
788.75/297.02	               -----------------------------
788.75/297.02	               1) 'empty' failed due to the following reason:
788.75/297.02	                  
788.75/297.02	                  Empty strict component of the problem is NOT empty.
788.75/297.02	               
788.75/297.02	               2) 'With Problem ...' failed due to the following reason:
788.75/297.02	                  
788.75/297.02	                  None of the processors succeeded.
788.75/297.02	                  
788.75/297.02	                  Details of failed attempt(s):
788.75/297.02	                  -----------------------------
788.75/297.02	                  1) 'empty' failed due to the following reason:
788.75/297.02	                     
788.75/297.02	                     Empty strict component of the problem is NOT empty.
788.75/297.02	                  
788.75/297.02	                  2) 'With Problem ...' failed due to the following reason:
788.75/297.02	                     
788.75/297.02	                     None of the processors succeeded.
788.75/297.02	                     
788.75/297.02	                     Details of failed attempt(s):
788.75/297.02	                     -----------------------------
788.75/297.02	                     1) 'empty' failed due to the following reason:
788.75/297.02	                        
788.75/297.02	                        Empty strict component of the problem is NOT empty.
788.75/297.02	                     
788.75/297.02	                     2) 'With Problem ...' failed due to the following reason:
788.75/297.02	                        
788.75/297.02	                        Empty strict component of the problem is NOT empty.
788.75/297.02	                     
788.75/297.02	                  
788.75/297.02	               
788.75/297.02	            
788.75/297.02	         
788.75/297.02	      
788.75/297.02	   
788.75/297.02	   2) 'Best' failed due to the following reason:
788.75/297.02	      
788.75/297.02	      None of the processors succeeded.
788.75/297.02	      
788.75/297.02	      Details of failed attempt(s):
788.75/297.02	      -----------------------------
788.75/297.02	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
788.75/297.02	         following reason:
788.75/297.02	         
788.75/297.02	         The processor is inapplicable, reason:
788.75/297.02	           Processor only applicable for innermost runtime complexity analysis
788.75/297.02	      
788.75/297.02	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
788.75/297.02	         to the following reason:
788.75/297.02	         
788.75/297.02	         The processor is inapplicable, reason:
788.75/297.02	           Processor only applicable for innermost runtime complexity analysis
788.75/297.02	      
788.75/297.02	   
788.75/297.02	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
788.75/297.02	      failed due to the following reason:
788.75/297.02	      
788.75/297.02	      None of the processors succeeded.
788.75/297.02	      
788.75/297.02	      Details of failed attempt(s):
788.75/297.02	      -----------------------------
788.75/297.02	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
788.75/297.02	         failed due to the following reason:
788.75/297.02	         
788.75/297.02	         match-boundness of the problem could not be verified.
788.75/297.02	      
788.75/297.02	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
788.75/297.02	         failed due to the following reason:
788.75/297.02	         
788.75/297.02	         match-boundness of the problem could not be verified.
788.75/297.02	      
788.75/297.02	   
788.75/297.02	
788.75/297.02	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
788.75/297.02	   the following reason:
788.75/297.02	   
788.75/297.02	   We add the following weak dependency pairs:
788.75/297.02	   
788.75/297.02	   Strict DPs:
788.75/297.02	     { f^#(a(), g(y)) -> c_1(y)
788.75/297.02	     , f^#(g(x), a()) -> c_2(f^#(x, g(a())))
788.75/297.02	     , f^#(g(x), g(y)) -> c_3(h^#(g(y), x, g(y)))
788.75/297.02	     , h^#(a(), y, z) -> c_4(z)
788.75/297.02	     , h^#(g(x), y, z) -> c_5(f^#(y, h(x, y, z))) }
788.75/297.02	   
788.75/297.02	   and mark the set of starting terms.
788.75/297.02	   
788.75/297.02	   We are left with following problem, upon which TcT provides the
788.75/297.02	   certificate MAYBE.
788.75/297.02	   
788.75/297.02	   Strict DPs:
788.75/297.02	     { f^#(a(), g(y)) -> c_1(y)
788.75/297.02	     , f^#(g(x), a()) -> c_2(f^#(x, g(a())))
788.75/297.02	     , f^#(g(x), g(y)) -> c_3(h^#(g(y), x, g(y)))
788.75/297.02	     , h^#(a(), y, z) -> c_4(z)
788.75/297.02	     , h^#(g(x), y, z) -> c_5(f^#(y, h(x, y, z))) }
788.75/297.02	   Strict Trs:
788.75/297.02	     { f(a(), g(y)) -> g(g(y))
788.75/297.02	     , f(g(x), a()) -> f(x, g(a()))
788.75/297.02	     , f(g(x), g(y)) -> h(g(y), x, g(y))
788.75/297.02	     , h(a(), y, z) -> z
788.75/297.02	     , h(g(x), y, z) -> f(y, h(x, y, z)) }
788.75/297.02	   Obligation:
788.75/297.02	     runtime complexity
788.75/297.02	   Answer:
788.75/297.02	     MAYBE
788.75/297.02	   
788.75/297.02	   Empty strict component of the problem is NOT empty.
788.75/297.02	
788.75/297.02	
788.75/297.02	Arrrr..
789.27/297.50	EOF